Skip to content

Commit 79cd7d4

Browse files
Merge branch 'develop-spec-arg'. Close #446.
**Description** The type `Copilot.Language.Stream.Arg` is defined in the same module as a `Stream`, but nothing in that module uses an `Arg`. Architecturally, that type doesn't belong in that module, but, rather, should be listed in `Copilot.Language.Spec`, where it is used in the definition of `Trigger`. Consequently, `Copilot.Language.Stream.Arg` should be moved to `Copilot.Language.Spec`. As per our internal policy of waiting 3 versions from deprecation until a public interface declaration can be hidden, this definition should be deprecated in `Copilot.Language.Stream.Arg` and re-published from `Copilot.Language.Spec`. However, Haskell offers no mechanism to do that. If we deprecate it in `Copilot.Language.Stream.Arg`, we cannot make that warning disappear when imported from `Copilot.Language.Spec`, even with `{-# OPTIONS_GHC -fno-warn-deprecations #-}`. **Type** - Bug: low cohesion in `Copilot.Language.Stream`. **Additional context** None. **Requester** - Ivan Perez **Method to check presence of bug** This is a bug in architecture and design. There is no way to check for this bug automatically. There are signs of this bug. For example, running a search on the codebase indicates that nothing inside `Stream` uses `Arg`, but that is not totally uncommon in modules that define datatypes. In this case, it is important to understand that, conceptually, an `Arg` only makes sense in the context of a `Trigger`, so they belong together. Because `Trigger` is defined in `Copilot.Language.Spec`, then so should `Arg`. We can, however, check that it is defined in `Spec`, as follows: ```Dockerfile FROM ubuntu:trusty RUN apt-get update RUN apt-get install --yes software-properties-common RUN add-apt-repository ppa:hvr/ghc RUN apt-get update RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4 RUN apt-get install --yes libz-dev ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH RUN cabal update RUN cabal v1-sandbox init RUN cabal v1-install alex happy RUN apt-get install --yes git SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-install copilot/copilot-**/ \ && ! cabal v1-exec -- runhaskell <<< "import Copilot.Language.Stream (Arg); main :: IO (); main = return ()" \ && cabal v1-exec -- runhaskell <<< "import Copilot.Language.Spec (Arg(Arg)); main :: IO (); main = return ()" \ && echo "Success" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-446 ``` **Expected result** Running the script above prints Success, indicating that `Arg` is defined in and exported from `Copilot.Language.Spec`, and not `Copilot.Language.Stream`. **Solution implemented** Move `Arg` from `Copilot.Language.Stream` to `Copilot.Language.Spec`. Adjust imports accordingly. **Further notes** We provide the function `arg` precisely so that people do not use the constructor `Arg` directly.
2 parents 050d67c + a77a080 commit 79cd7d4

5 files changed

Lines changed: 10 additions & 7 deletions

File tree

copilot-language/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2023-07-07
2+
* Move Copilot.Language.Stream.Arg to Copilot.Language.Spec. (#446)
3+
14
2023-05-07
25
* Version bump (3.15). (#438)
36
* Remove outdated comment about pretty-printer. (#428)

copilot-language/src/Copilot/Language/Analyze.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Copilot.Language.Analyze
1414

1515
import Copilot.Core (DropIdx)
1616
import qualified Copilot.Core as C
17-
import Copilot.Language.Stream (Stream (..), Arg (..))
17+
import Copilot.Language.Stream (Stream (..))
1818
import Copilot.Language.Spec
1919
import Copilot.Language.Error (badUsage)
2020

copilot-language/src/Copilot/Language/Reify.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ import Copilot.Core (Typed, Id, typeOf)
1717
import Copilot.Language.Analyze (analyze)
1818
import Copilot.Language.Error (impossible)
1919
import Copilot.Language.Spec
20-
import Copilot.Language.Stream (Stream (..), Arg (..))
20+
import Copilot.Language.Stream (Stream (..))
2121

2222
import Copilot.Theorem.Prove
2323

copilot-language/src/Copilot/Language/Spec.hs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ module Copilot.Language.Spec
2222
, Trigger (..)
2323
, trigger, triggers
2424
, arg
25+
, Arg(..)
2526
, Property (..)
2627
, Prop (..)
2728
, prop, properties
@@ -198,3 +199,7 @@ theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]
198199
-- the current samples of the given streams.
199200
arg :: Typed a => Stream a -> Arg
200201
arg = Arg
202+
203+
-- | Wrapper to use 'Stream's as arguments to triggers.
204+
data Arg where
205+
Arg :: Typed a => Stream a -> Arg

copilot-language/src/Copilot/Language/Stream.hs

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99

1010
module Copilot.Language.Stream
1111
( Stream (..)
12-
, Arg (..)
1312
, Copilot.Language.Stream.ceiling
1413
, Copilot.Language.Stream.floor
1514
, Copilot.Language.Stream.atan2
@@ -48,10 +47,6 @@ data Stream :: * -> * where
4847
=> Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d
4948
Label :: Typed a => String -> Stream a -> Stream a
5049

51-
-- | Wrapper to use 'Stream's as arguments to triggers.
52-
data Arg where
53-
Arg :: Typed a => Stream a -> Arg
54-
5550
-- | Dummy instance in order to make 'Stream' an instance of 'Num'.
5651
instance Show (Stream a) where
5752
show _ = "Stream"

0 commit comments

Comments
 (0)