copilot 0.28 → 1.0

raw patch · 21 files changed

+1110/−967 lines, 21 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/Copilot.hs +10/−4
• Language/Copilot/Analyser.hs +48/−43
• Language/Copilot/AtomToC.hs +27/−26
• Language/Copilot/Compiler.hs +215/−146
• Language/Copilot/Core.hs +118/−208
• Language/Copilot/Dispatch.hs +10/−12
• Language/Copilot/Examples/Examples.hs +61/−51
• Language/Copilot/Examples/LTLExamples.hs +5/−5
• Language/Copilot/Examples/PTLTLExamples.hs +22/−22
• Language/Copilot/Examples/StatExamples.hs +4/−4
• Language/Copilot/Help.hs +16/−16
• Language/Copilot/Interface.hs +15/−24
• Language/Copilot/Interpreter.hs +18/−5
• Language/Copilot/Language.hs +64/−392
• Language/Copilot/Language/Casting.hs +99/−0
• Language/Copilot/Language/FunctionCalls.hs +47/−0
• Language/Copilot/Language/RandomOps.hs +206/−0
• Language/Copilot/Language/Sampling.hs +99/−0
• Language/Copilot/Tests/Random.hs +9/−7
• README +11/−0
• copilot.cabal +6/−2

@@ -1,37 +1,43 @@ module Language.Copilot-  ( module Language.Copilot.Core+  ( module Language.Copilot.Core    , module Language.Copilot.Analyser   , module Language.Copilot.Interpreter   , module Language.Copilot.Help   , module Language.Copilot.AtomToC   , module Language.Copilot.Compiler   , module Language.Copilot.Language+  -- , module Language.Copilot.Sampling+  -- , module Language.Copilot.Casting   -- , module Language.Copilot.Dispatch   , module Language.Copilot.Interface   , module Language.Copilot.Tests.Random   -- , module Language.Copilot.Libs.Indexes   -- , module Language.Copilot.Libs.LTL   -- , module Language.Copilot.Libs.PTLTL+  -- , module Language.Copilot.Libs.Clocks   -- , module Language.Copilot.AdHocC   -- , module Language.Copilot.Examples.Examples   -- , module Language.Copilot.Examples.LTLExamples   -- , module Language.Copilot.Examples.PTLTLExamples   ) where -import Language.Copilot.Core+import Language.Copilot.Core (Streams, Spec, emptySM, StreamableMaps(..)) -- XXX for libs, probably need to export all the maps.  Maybe put in a different file? import Language.Copilot.Analyser import Language.Copilot.Interpreter import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler-import Language.Copilot.Language -- (opsF, opsF2, opsF3)-import Language.Copilot.PrettyPrinter() import Language.Copilot.Tests.Random+import Language.Copilot.Language+-- import Language.Copilot.Language.Sampling+-- import Language.Copilot.Language.Casting+-- import Language.Copilot.PrettyPrinter() -- import Language.Copilot.Dispatch import Language.Copilot.Interface -- import Language.Copilot.Libs.Indexes -- import Language.Copilot.Libs.LTL -- import Language.Copilot.Libs.PTLTL+-- import Language.Copilot.Libs.Clocks -- import Language.Copilot.AdHocC -- import Language.Copilot.Examples.Examples -- import Language.Copilot.Examples.LTLExamples

@@ -6,7 +6,7 @@         -- * Main error checking functions         check, Error(..), SpecSet(..),         -- * Varied other things-        getExternalVars, ExtVars(..)+        getExternalVars         {-         -- * Dependency Graphs (experimental)         Weight, Node(..), DependencyGraph,@@ -15,8 +15,6 @@  import Language.Copilot.Core -import qualified Language.Atom as A- import Data.List  type Weight = Int@@ -25,17 +23,20 @@ data Error =       BadSyntax String Var -- ^ the BNF is not respected     | BadDrop Int Var -- ^ A drop expression of less than 0 is used-    | BadSamplingPhase Var Var Phase -- ^ if an external variable is sampled at-                                     -- phase 0 then there is no time for the-                                     -- stream to be updated-    | BadSamplingArrPhase Var Var Phase -- ^ if an external variable is sampled at-                                        -- phase 0 then there is no time for the-                                        -- stream to be updated-    | BadPArrSpec Var Var String -- ^ External array indexes can only take+    -- | BadSamplingPhase Var Ext -- ^ if an external variable is sampled at phase+    --                            -- 0 then there is no time for the stream to be+    --                            -- updated+    -- | BadSamplingArrPhase Var Ext -- ^ if an external variable is sampled at+    --                               -- phase 0 then there is no time for the+    --                               -- stream to be updated+    | BadPArrSpec Var Ext String -- ^ External array indexes can only take                                  -- variables or constants as indexes.     | BadType Var Var -- ^ either a variable is not defined, or not with the                       -- good type ; there is no implicit conversion of types in                       -- /Copilot/+    | BadTypeExt Ext Var -- ^ either an external variable is not defined, or not+                         -- with the good type; there is no implicit conversion+                         -- of types in /Copilot/     | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile                                                  -- /Copilot/ specification can                                                  -- only work if there is no@@ -43,10 +44,10 @@                                                  -- path in the specification,                                                  -- as described in the original                                                  -- research paper-    | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but+    | DependsOnClosePast [Var] Ext Weight Weight -- ^ Could be compiled, but                                                  -- would need bigger                                                  -- prophecyArrays-    | DependsOnFuture [Var] Var Weight -- ^ If an output depends of a future of+    | DependsOnFuture [Var] Ext Weight -- ^ If an output depends of a future of                                        -- an input it will be hard to compile to                                        -- say the least @@ -61,24 +62,24 @@           "of elements.\n"          , show i ++ " is negative, and Drop only accepts positive arguments.\n"         ]-    show (BadSamplingPhase v v' ph) =-       unlines-        [ "Error : the external variable " ++ v' ++ " is sampled at phase " ++ -          show ph ++ " in the stream " ++ v ++ "." -        , "Sampling can only occur from phase 1 onwards.\n"-        ]-    show (BadSamplingArrPhase v arr ph) =-       unlines-        [ "Error : the external array " ++ arr ++ " is sampled at phase " ++ -          show ph ++ " in the stream " ++ v ++ "."-        , " Sampling can only occur from phase 1 onwards.\n"-        ]+    -- show (BadSamplingPhase v v' ph) =+    --    unlines+    --     [ "Error : the external variable " ++ show v' ++ " is sampled at phase " ++ +    --       show ph ++ " in the stream " ++ v ++ "." +    --     , "Sampling can only occur from phase 1 onwards.\n"+    --     ]+    -- show (BadSamplingArrPhase v arr ph) =+    --    unlines+    --     [ "Error : the external array " ++ show arr ++ " is sampled at phase " ++ +    --       show ph ++ " in the stream " ++ v ++ "."+    --     , " Sampling can only occur from phase 1 onwards.\n"+    --     ]     show (BadPArrSpec v arr idx) =         unlines         [ "Error : the index into an external array can only take a "             ++ "variable or a constant.  The index\n"           ,   idx ++ "\n\n in external array "-            ++ arr ++ "in the definition of stream " ++ v ++ " is not of that "+            ++ show arr ++ "in the definition of stream " ++ v ++ " is not of that "             ++ "form.\n"         ]     show (BadType v v') =@@ -88,6 +89,13 @@         , "does not exist, or don't have the right type (there is no implicit "            ++ "conversion).\n"         ]+    show (BadTypeExt v v') =+       unlines+        [ "Error : the external call " ++ show v ++ ", called in the stream " +          ++ v' ++ ", either"+        , "does not exist, or don't have the right type (there is no implicit " +          ++ "conversion).\n"+        ]     show (NonNegativeWeightedClosedPath vs w) =        unlines          [ "Error : the following path is closed in the dependency graph of the "@@ -103,7 +111,7 @@     show (DependsOnClosePast vs v w len) =        unlines         [ "Error : the following path is of weight " ++ show w ++ " ending in "-          ++ "the external variable " ++ v +          ++ "the external variable " ++ show v          , "while the first variable of that path has a prophecy array of length "            ++ show len ++ ","          , "which is strictly greater than the weight. This is forbidden."@@ -114,7 +122,7 @@         [ "Error : the following path is of weight " ++ show w            ++ " which is strictly positive."         , "This means that the first variable depends on the future of the "-          ++ "external variable " ++ v +          ++ "external variable " ++ show v          , "which is quoted in the last variable of the path.  This is "           ++ "obviously impossible."         , "Path : " ++ show (reverse vs) ++ "\n"@@ -161,9 +169,9 @@                 case s of                     Var _ -> Nothing                     Const _ -> Nothing-                    PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph-                    PArr _ (arr,s0) ph -> checkIndex v arr s0 -                      &&> ph > 0 ||> BadSamplingArrPhase v arr ph +                    PVar _ _ -> Nothing -- ph > 0 ||> BadSamplingPhase v v' ph+                    PArr _ (arr,s0) -> checkIndex v arr s0 +--                      &&> ph > 0 ||> BadSamplingArrPhase v arr ph                        &&> checkSyntaxSpec PArrSet v s0 Nothing                     F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v                        &&> checkSyntaxSpec FunSpecSet v s0 Nothing@@ -196,24 +204,27 @@                 checkPath :: Streamable a => Int -> [Var] -> Spec a -> Maybe Error                 checkPath n vs s =                     case s of-                        PVar t v _ -> case () of+                        PVar t v -> case () of                                 () | n > 0 -> Just $ DependsOnFuture vs v n                                    | n > negate (prophecyArrayLength s0) ->                                             Just $ DependsOnClosePast vs v n                                                      (prophecyArrayLength s0)-                                   | t /= getAtomType s -> Just $ BadType v (head vs)+                                   | t /= getAtomType s -> +                                            Just $ BadTypeExt v (head vs)                                 _ -> Nothing-                        PArr t (arr, idx) _ +                        PArr t (arr, idx)                                     | n > 0 -> Just $ DependsOnFuture vs arr n                                    | n > negate (prophecyArrayLength idx) ->                                             Just $ DependsOnClosePast vs arr n                                                      (prophecyArrayLength idx)-                                   | t /= getAtomType s -> Just $ BadType arr (head vs)+                                   | t /= getAtomType s -> +                                       Just $ BadTypeExt arr (head vs)                                    | otherwise ->                                         case idx of                                          Const _ -> checkPath n vs idx                                          Var _   -> checkPath n vs idx-                                         _       -> Just $ BadPArrSpec v0 arr (show idx)+                                         _       -> +                                           Just $ BadPArrSpec v0 arr (show idx)                         Var v ->                              if elem v vs                                 then if n >= 0@@ -233,12 +244,6 @@                         Drop i s' -> checkPath (n + i) vs s'     in foldStreamableMaps checkPathsFromSpec streams Nothing -type Exs = (A.Type, Var, ExtVars)--data ExtVars = ExtV Phase -             | ExtA Phase String-  deriving Eq- getExternalVars :: StreamableMaps Spec -> [Exs] getExternalVars streams =     nub $ foldStreamableMaps decl streams []@@ -247,8 +252,8 @@              => Var -> Spec a -> [Exs] -> [Exs]         decl _ s ls =             case s of-                PVar t v ph -> (t, v, ExtV ph) : ls-                PArr t (arr, s0) ph -> (t, arr, ExtA ph (show s0)) : ls+                PVar t v -> (t, v, ExtRetV) : ls+                PArr t (arr, s0) -> (t, arr, ExtRetA (show s0)) : ls                 F _ _ s0 -> decl undefined s0 ls                 F2 _ _ s0 s1 -> decl undefined s0 $ decl undefined s1 ls                 F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 

@@ -3,35 +3,37 @@ -- | Defines a main() and print statements to easily execute generated Copilot specs. module Language.Copilot.AtomToC(getPrePostCode) where -import Language.Copilot.Compiler (tmpSampleStr)+import Language.Copilot.Compiler (tmpSampleStr, tmpArrName, tmpVarName) import Language.Copilot.AdHocC-import Language.Copilot.Core-import Language.Copilot.Analyser (ExtVars(..)) -import qualified Language.Atom as A+import Language.Copilot.Core  import Data.List --- allExts represents all the variables to monitor (used for declaring them)--- inputExts represents the monitored variables which are to be feed to the standard input of the C program.--- only used for the testing with random streams and values.-getPrePostCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] -               -> [(String,Int)] -> Vars -> Period -> (String, String)+-- allExts represents all the variabbles to monitor (used for declaring them)+-- inputExts represents the monitored variables which are to be fed to the+-- standard input of the C program.  only used for the testing with random+-- streams and values.+getPrePostCode :: Name -> StreamableMaps Spec -> [Exs] +               -> [(Ext,Int)] -> Vars -> Period -> (String, String) getPrePostCode cName streams allExts arrDecs inputExts p =     (preCode $ extDecls allExts arrDecs, postCode cName streams allExts inputExts p)  -- Make the declarations for external vars-extDecls :: [(A.Type, Var, ExtVars)] -> [(String,Int)] -> [String]+extDecls :: [Exs] -> [(Ext,Int)] -> [String] extDecls allExtVars arrDecs =-    let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars -        getDec (t, v, ExtV _) = varDecl t [v]-        getDec (t, arr, ExtA _ _) = +    let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') +                              allExtVars +        getDec :: Exs -> String+        getDec (t, (ExtV v), ExtRetV) = varDecl t [v]+        getDec (_, (Fun _ _), ExtRetV) = ""+        getDec (t, arr, ExtRetA _) =            case getIdx arr of              Nothing -> error $ "Please use the setArrs option to provide a list of " ++                           "pairs (a,idx) where a is the name of an external array and idx " ++                           "is its static size to declare.  There is no size for array " ++-                          arr ++ "."-            Just idx  -> arrDecl t [(arr, idx)] +                          show arr ++ "."+            Just idx  -> arrDecl t [(show arr, idx)]          getIdx arr = lookup arr arrDecs     in      map getDec uniqueExtVars@@ -47,18 +49,14 @@   ]   ++ extDeclarations   -vPre :: Name -> String-vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "."--postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] -> Vars -> Period -> String+postCode :: Name -> StreamableMaps Spec -> [Exs] -> Vars -> Period -> String postCode cName streams allExts inputExts p =    unlines $   (if isEmptySM inputExts     then []     else cleanString)   ++-  [ "// #pragma GCC diagnostic ignored \"-Wformat\""-  , "int main(int argc, char *argv[]) {"+  [ "int main(int argc, char *argv[]) {"   , "  if (argc != 2) {"   , "    " ++ printfNewline           "Please pass a single argument to the simulator containing the number of rounds to execute it." @@ -121,16 +119,19 @@                     ++ typeId (head l) ++ "\", &" ++ v ++ ");") :             (indent ++ "clean (" ++ string ++ ", stdin);") : ls -sampleExtVars :: [(A.Type, Var, ExtVars)] -> Name -> [String]+sampleExtVars :: [Exs] -> Name -> [String] sampleExtVars allExts cName =     map (\ext -> let (v,e) = sample ext in-           "  " ++ vPre cName ++ tmpSampleStr ++ e+           "  " ++ vPre cName ++ tmpSampleStr ++ (normalizeVar e)            ++ " = " ++ v ++ ";")          allExts     where -        sample :: (A.Type, Var, ExtVars) -> (Var, String)-        sample (_, v, ExtV ph) = (v, tmpVarName v ph)-        sample (_, v, ExtA ph idx) = (v ++ "[0]", tmpArrName v ph idx)+        sample :: Exs -> (Var, String)+        sample (_, v, ExtRetV) = ( case v of +                                     ExtV var -> var+                                     Fun fname args -> funcShow cName fname args+                                  , tmpVarName v)+        sample (_, v, ExtRetA idx) = (show v ++ "[0]", tmpArrName v idx)  outputVars :: Name -> StreamableMaps Spec -> [String] outputVars cName streams =

@@ -1,62 +1,130 @@ {-# LANGUAGE ScopedTypeVariables, Rank2Types #-} --- Note : for now, the initial state is computed during the first tick+-- XXX Clean this up!  -- | Transform the copilot specification in an atom one, and then compile that one.-module Language.Copilot.Compiler(copilotToAtom, tmpSampleStr) where+module Language.Copilot.Compiler+  (copilotToAtom, tmpSampleStr, tmpArrName, tmpVarName+  ) where  import Language.Copilot.Core  import Data.Maybe-import Data.Map as M+import qualified Data.Map as M import Data.List+import Data.Word (Word64)  import qualified Language.Atom as A  -- | Compiles an /Copilot/ specification to an /Atom/ one. -- The period is given as a Maybe : if it is Nothing, an optimal period will be chosen.-copilotToAtom :: LangElems -> Maybe Period -> (Period, A.Atom ())-copilotToAtom (LangElems streams sends triggers) p = +copilotToAtom :: LangElems -> Maybe Period -> Name -> (Period, A.Atom ()) +copilotToAtom (LangElems streams sends triggers) p cFileName =    (p', A.period p' $ do-     prophArrs <- mapStreamableMapsM initProphArr streams     outputs <- mapStreamableMapsM initOutput streams-     updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty)     outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty)--    tmpSamples <- foldStreamableMaps (\_ -> initExtSamples streams prophArrs outputIndexes) +    tmpSamples <- foldStreamableMaps +                    (\_ -> initExtSamples streams outputs prophArrs outputIndexes)                      streams                      (return emptyTmpSamples)-     -- One atom rule for each stream-    foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples +    foldStreamableMaps (makeRule p' streams outputs prophArrs tmpSamples                             updateIndexes outputIndexes)        streams (return ()) -    -- foldStreamableMaps (makeTrigger streams prophArrs tmpSamples-    --                        outputIndexes)-    --  triggers (return ())--    M.fold (makeTrigger streams prophArrs tmpSamples outputIndexes) -           (return ()) triggers-+    M.fold (makeTrigger outputs cFileName) (return ()) triggers+                foldStreamableMaps (makeSend outputs) sends (return ())      -- Sampling of the external variables.  Remove redundancies.     sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ -      foldStreamableMaps (\_ -> sampleExts tmpSamples) streams []+      foldStreamableMaps (\_ -> sampleExts outputs tmpSamples cFileName) streams []     )-  where-    optP = getOptimalPeriod streams sends-    p' = -      case p of-        Nothing -> optP-        Just i -> if i >= optP -            then i -            else error $ "Copilot error: the period is too short, " -                     ++ "it should be at least " ++ show optP ++ " ticks."+  where p' = period p+--  where+--    optP = getOptimalPeriod streams sends +-- | For period of length n:+-- Phase 0: state update.+-- Phase 1: Compute output variables.+-- Phase 2 - n-2: send values (if any).+-- Phase 2 - n-2: Sample external vars (if any).+-- Phase n-1: update indexes.+period :: Maybe Int -> Int+period p = +  case p of+    Nothing -> minPeriod+    Just i -> if i >= minPeriod+                then i +                else error $ "Copilot error: the period is too short, " +                       ++ "it should be at least " ++ show minPeriod ++ " ticks."+  where minPeriod :: Int+        minPeriod = 4++-- For the prophecy arrays+type ArrIndex = Word64+type ProphArrs = StreamableMaps BoundedArray+type Outputs = StreamableMaps A.V+type Indexes = M.Map Var (A.V ArrIndex)++-- External variables+data PhasedValueVar a = PhV (A.V a)++data BoundedArray a = B ArrIndex (Maybe (A.A a))++nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes +       -> Spec a -> ArrIndex -> A.E a+nextSt streams prophArrs tmpSamples outputIndexes s index = +    case s of+        PVar _ v  -> +          let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in+          A.value var+        PArr _ (v, idx) -> +          let PhA var = e tmp (tmpArrs tmpSamples) +              tmp = tmpArrName v (show idx) +              e a b = case getMaybeElem a b of+                        Nothing -> +                          error "Error in application of getElem in nextSt."+                        Just x  -> x +          in A.value var+        Var v -> let B initLen maybeArr = getElem v prophArrs in+            -- This check is extremely important+            -- It means that if x at time n depends on y at time n+            -- then x is obtained not by y, but by inlining the definition of y+            -- so it increases the size of code (sadly),+            -- but is the only thing preventing race conditions from occuring+            if index < initLen+                then getVar v initLen maybeArr +                else let s0 = getElem v streams in +                     next s0 (index - initLen)+        Const e -> A.Const e+        F _ f s0 -> f $ next s0 index+        F2 _ f s0 s1 ->+            f (next s0 index) +              (next s1 index)+        F3 _ f s0 s1 s2 ->+            f (next s0 index) +              (next s1 index) +              (next s2 index)+        Append _ s0 -> next s0 index+        Drop i s0 -> next s0 (fromInteger (toInteger i) + index)+    where+        next :: Streamable b => Spec b -> ArrIndex -> A.E b+        next = nextSt streams prophArrs tmpSamples outputIndexes +        getVar :: Streamable a +               => Var -> ArrIndex -> Maybe (A.A a) -> A.E a+        getVar v initLen maybeArr =+           let outputIndex = case M.lookup v outputIndexes of+                               Nothing -> error "Error in function getVar."+                               Just x -> x+               arr = case maybeArr of+                       Nothing -> error "Error in function getVar (maybeArr)."+                       Just x -> x in +           arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_`  +                       (A.Const (initLen + 1)))+ initProphArr :: forall a. Streamable a => Var -> Spec a -> A.Atom (BoundedArray a) initProphArr v s =     let states = initState s@@ -75,6 +143,26 @@                 Append ls s'' -> ls ++ initState s''                 _ -> [] ++-- External arrays+data PhasedValueArr a = PhA (A.V a) -- Array name.+data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. ++data TmpSamples = +  TmpSamples { tmpVars :: StreamableMaps PhasedValueVar+             , tmpArrs :: StreamableMaps PhasedValueArr+             , tmpIdxs :: StreamableMaps PhasedValueIdx+             }++emptyTmpSamples :: TmpSamples+emptyTmpSamples = TmpSamples emptySM emptySM emptySM++tmpVarName :: Ext -> Var+tmpVarName v = show v++tmpArrName :: Ext -> String -> Var+tmpArrName v idx = (tmpVarName v) ++ "_" ++ normalizeVar idx+ initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) initOutput v _ = do   atomConstructor (normalizeVar v) (unit::a)@@ -83,9 +171,9 @@ tmpSampleStr = "tmpSampleVal__"  initExtSamples :: forall a. Streamable a -               => StreamableMaps Spec -> ProphArrs -> Indexes -> Spec a +               => StreamableMaps Spec -> Outputs -> ProphArrs -> Indexes -> Spec a                    -> A.Atom TmpSamples -> A.Atom TmpSamples-initExtSamples streams prophArrs outputIndexes s tmpSamples = do+initExtSamples streams outputs prophArrs outputIndexes s tmpSamples = do     case s of         Const _ -> tmpSamples         Var _ ->   tmpSamples@@ -96,23 +184,21 @@                            initExtSamples' s1 tmpSamples         F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $                              initExtSamples' s2 tmpSamples-        PVar _ v ph -> -            do  -- checkVar v -                ts <- tmpSamples-                let v' = tmpVarName v ph+        PVar _ v -> +            do  ts <- tmpSamples+                let v' = tmpVarName v                      vts = tmpVars ts                     maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a)                     name = tmpSampleStr ++ normalizeVar v'                 case maybeElem of                     Nothing ->                          do  val <- atomConstructor name (unit::a)-                            let m' = M.insert v' (PhV ph val) (getSubMap vts)+                            let m' = M.insert v' (PhV val) (getSubMap vts)                             return $ ts {tmpVars = updateSubMap (\_ -> m') vts}                     Just _ -> return ts-        PArr _ (arr, idx) ph -> -            do  --checkVar arr-                ts <- tmpSamples-                let arr' = tmpArrName arr ph (show idx)+        PArr _ (arr, idx) -> +            do  ts <- tmpSamples+                let arr' = tmpArrName arr (show idx)                     arrts = tmpArrs ts                     idxts = tmpIdxs ts                     maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a)@@ -122,29 +208,17 @@                       do val <- atomConstructor name (unit::a)                          let i = case idx of                                    Const e -> PhIdx $ A.Const e-                                   Var _ -> ---                                     let B initLen maybeArr = getElem v prophArrs ---                                     let B initLen maybeArr = ---                                           case getMaybeElem v prophArrs of---                                             Nothing -> ---                                               error "Error in function initExtSamples."---                                             Just x -> x-                                     PhIdx $ nextSt streams prophArrs -                                                undefined outputIndexes idx 0+                                   Var v   -> PhIdx $ A.value (getElem v outputs)                                    _    -> error "Unexpected Spec in initExtSamples."-                         let m' = M.insert arr' (PhA ph val) (getSubMap arrts)+                         let m' = M.insert arr' (PhA val) (getSubMap arrts)                          let m'' = M.insert arr' i (getSubMap idxts)                          return $ ts { tmpArrs = updateSubMap (\_ -> m') arrts                                      , tmpIdxs = updateSubMap (\_ -> m'') idxts                                      }                   Just _ -> return ts-    where -    --      checkVar v = when (normalizeVar v /= v)-    --                    (error $ "Copilot: external variable " ++ v ++ " is not "-    --                            ++ "a valid C99 variable.")-          initExtSamples' :: Streamable b+    where initExtSamples' :: Streamable b                           => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples-          initExtSamples' = initExtSamples streams prophArrs outputIndexes+          initExtSamples' = initExtSamples streams outputs prophArrs outputIndexes  makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes makeUpdateIndex v (B n arr) indexes =@@ -167,9 +241,9 @@                 return $ M.insert v index mindexes  makeRule :: forall a. Streamable a => -    StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples -> +    Period -> StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples ->      Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()-makeRule streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do+makeRule p streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do     r      let B n maybeArr = getElem v prophArrs::BoundedArray a     case maybeArr of@@ -188,51 +262,37 @@                          A.exactPhase 1 $ A.atom ("output__" ++ normalizeVar v) $ do                 ((getElem v outputs)::(A.V a)) A.<== arr A.!. (A.VRef outputIndex)-                outputIndex A.<== (A.VRef outputIndex + A.Const 1) `A.mod_` A.Const (n + 1)+                outputIndex A.<==          (A.VRef outputIndex + A.Const 1) +                                  `A.mod_` A.Const (n + 1)             -            -- Spread these out evenly accross the remaining phases, staring no-            -- earlier than phase 1.-            A.phase ((maxSampleDep v streams) + 1)+            -- XXX For now, we put these all in the last phase.  We want better+            -- distribution though at some point.+            A.phase (p - 1)               $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do-                updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1)+                updateIndex A.<==          (A.VRef updateIndex + A.Const 1) +                                  `A.mod_` A.Const (n + 1)         where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0              --- | Find the maximum phase as which an array sampling depends on this stream by--- computing it's index in terms of it. Returns zero by default.-maxSampleDep :: Var -> StreamableMaps Spec -> Int-maxSampleDep v streams =-  foldStreamableMaps (\_ -> streamDep) streams 0-  where -    streamDep :: Streamable b => Spec b -> Int -> Int-    streamDep s i = -      case s of-        Var _ -> i-        Const _  -> i-        PVar _ _ _ -> i-        PArr _ (_, Var v') ph | v == v'   -> max ph i-                              | otherwise -> i-        PArr _ _ _ -> i-        F _ _ s0 -> streamDep s0 i-        F2 _ _ s0 s1 -> streamDep s0 $ streamDep s1 i-        F3 _ _ s0 s1 s2 -> streamDep s0 $ streamDep s1 $ streamDep s2 i-        Append _ s0 -> streamDep s0 i-        Drop _ s0 -> streamDep s0 i---- makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom ()--- makeSend outputs name (Send (v, ph, port)) r = do---         r ---         A.exactPhase ph $ A.atom ("__send_" ++ name) $---             send ((A.value (getElem v outputs))::(A.E a)) port+-- Do sends in phase 2. makeSend :: forall a. Streamable a           => Outputs -> String -> Send a -> A.Atom () -> A.Atom ()-makeSend outputs name (Send v ph port portName) r = do+makeSend outputs name (Send v port portName) r = do         r -        A.exactPhase ph $ A.atom ("__send_" ++ name) $-            mkSend (A.value (notVarErr v (\var -> getElem var outputs)) :: A.E a) +        A.exactPhase 2 $ A.atom ("__send_" ++ name) $+            mkSend (A.value $ getElem (getMaybeVar v) outputs :: A.E a)                     port                     portName +-- | Sending data over ports.+mkSend :: (Streamable a) => A.E a -> Port -> String -> A.Atom ()+mkSend e (Port port) portName =+  A.action (\ueStr -> portName ++ "(" ++ head ueStr ++ "," ++ show port ++ ")") +           [A.ue e]++sampleStr :: String+sampleStr = "sample__"+ -- What we really should be doing is just folding over the TmpSamples, since -- that data should contain all the info we need to construct external variable -- and external array samples.  However, there is the issue that for array@@ -240,38 +300,51 @@ -- having the spec available provides typing coercion.  We could fold over the -- TmpSamples, passing streams in, and extract the appropriate Spec a. sampleExts :: forall a. Streamable a -           => TmpSamples -> Spec a -> [(Var, A.Atom ())] -> [(Var, A.Atom ())]-sampleExts ts s a = do+           => Outputs -> TmpSamples -> Name -> Spec a +              -> [(Var, A.Atom ())] -> [(Var, A.Atom ())]+sampleExts outputs ts cFileName s a = do   case s of     Var _ -> a     Const _ -> a-    PVar _ v ph -> -     let v' = tmpVarName v ph -         PhV _ var = getElem v' (tmpVars ts)::PhasedValueVar a in-     (v', A.exactPhase ph $ -            A.atom ("sample__" ++ v') $ -              var A.<== (A.value $ externalAtomConstructor v)+    PVar _ v -> +     let v' = tmpVarName v+--         PhV var = getElem v' (tmpVars ts) :: PhasedValueVar a in+         PhV var = case getMaybeElem v' (tmpVars ts) :: Maybe (PhasedValueVar a) of +                     Nothing ->  error $ "Copilot error: variable " ++ v' +                                   ++ " was not defined!."+                     Just (PhV var') -> PhV var' in+     (v', A.exactPhase minSampPh $ +            A.atom (sampleStr ++ normalizeVar v') $ +               var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v)      ) : a--    PArr _ (arr, idx) ph -> -         let arr' = tmpArrName arr ph (show idx)+    PArr _ (arr, idx) -> +         let arr' = tmpArrName arr (show idx)              PhIdx i = getIdx arr' idx (tmpIdxs ts)---             PhA _ arrV = getElem arr' (tmpArrs ts)::PhasedValueArr a in-             PhA _ arrV = case getMaybeElem arr' (tmpArrs ts)::Maybe (PhasedValueArr a) of-                            Nothing -> error "Error in fucntion sampleExts."-                            Just x -> x-         in -     (arr', A.exactPhase ph $ -              A.atom ("sample__" ++ arr') $ -                arrV A.<== A.array' arr (atomType (unit::a)) A.!. i-     ) : a-    F _ _ s0 -> sampleExts ts s0 a-    F2 _ _ s0 s1 -> sampleExts ts s0 $ sampleExts ts s1 a-    F3 _ _ s0 s1 s2 -> sampleExts ts s0 $ sampleExts ts s1 $-                         sampleExts ts s2 a-    Append _ s0 -> sampleExts ts s0 a-    Drop _ s0 -> sampleExts ts s0 a+             PhA arrV = +               case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of+                 Nothing -> error "Error in fucntion sampleExts."+                 Just x -> x in+         (arr', A.exactPhase minSampPh $ +            A.atom (sampleStr ++ normalizeVar arr') $ +               arrV A.<== A.array' (getSampleFuncVar arr)+                                   (atomType (unit::a)) A.!. i+            ) : a+    F _ _ s0 -> sampleExts' s0 a+    F2 _ _ s0 s1 -> sampleExts' s0 $ sampleExts' s1 a+    F3 _ _ s0 s1 s2 -> sampleExts' s0 $ sampleExts' s1 $+                         sampleExts' s2 a+    Append _ s0 -> sampleExts' s0 a+    Drop _ s0 -> sampleExts' s0 a+  where minSampPh :: Int+        minSampPh = 2+        sampleExts' s' a' = sampleExts outputs ts cFileName s' a'+        getSampleFuncVar v = case v of+                               ExtV extV -> extV+                               -- XXX A bit of a hack.  Atom should be changed to allow+                               -- "out-of-Atom" assignments.  But this works for now.+                               Fun nm args -> funcShow cFileName nm args + -- lookup the idx for external array accesses in the map. getIdx :: forall a. (Streamable a, A.IntegralE a)         => Var -> Spec a -> StreamableMaps PhasedValueIdx -> PhasedValueIdx a@@ -284,33 +357,29 @@     _       -> error $ "Expecing either a variable or constant for the index "                  ++ "in the external array access for array " ++ arr ++ "." --- XXX bound min, max send phases-getOptimalPeriod :: StreamableMaps Spec -> StreamableMaps Send -> Period-getOptimalPeriod streams sends =-  max (foldStreamableMaps getMaximumSamplingPhase streams 2)-      (foldStreamableMaps getMaxSendPhase sends 0)-  where-    getMaximumSamplingPhase :: Var -> Spec a -> Period -> Period -    getMaximumSamplingPhase _ spec n =-      case spec of-        PVar _ _ ph -> max (ph + 1) n -        PArr _ (_, Var _) ph -> max (ph + 2) n -- because this may depend on a-                                               -- variable, and if that variable-                                               -- has a prophecy array, it needs-                                               -- an extra phase to update after-                                               -- the index is taken.-        PArr _ _ ph -> max (ph + 1) n-        F _ _ s -> getMaximumSamplingPhase "" s n-        F2 _ _ s0 s1 -> maximum [n,-                (getMaximumSamplingPhase "" s0 n),-                (getMaximumSamplingPhase "" s1 n)]-        F3 _ _ s0 s1 s2 -> maximum [n,-                (getMaximumSamplingPhase "" s0 n), -                (getMaximumSamplingPhase "" s1 n), -                (getMaximumSamplingPhase "" s2 n)]-        Drop _ s -> getMaximumSamplingPhase "" s n-        Append _ s -> getMaximumSamplingPhase "" s n-        _ -> n+-- TRIGGERS ----------------------------- -    getMaxSendPhase :: Var -> Send a -> Period -> Period-    getMaxSendPhase _ (Send _ ph _ _) n = max (ph+1) n+-- | To make customer C triggers.  Only for Spec Bool (others throw an+-- error).  +makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom ()+makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = +  do r +     (A.exactPhase 2 $ A.atom (show trigger) $ +        do A.cond (getOutput outputs s)+           fnCall cFileName fnName args)++-- | Building an external function call in Atom.+fnCall :: Name -> String -> Args -> A.Atom ()+fnCall cFileName fnName args = +  A.action (\_ -> funcShow cFileName fnName args) []++getOutput :: Streamable a => Outputs -> Spec a -> A.E a+getOutput outputs s = +  case s of+    (Var v) -> A.value +      (case getMaybeElem v outputs of+         Nothing -> error $ "Copilot error in trigger specification: variable " +                      ++ v ++ " was not defined!."+         Just v' -> v')+    (Const c) -> A.Const c+    _ -> error "Impossible error in getOutput in Compiler.hs."

@@ -1,5 +1,5 @@ {-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, -    FlexibleInstances #-}+    FlexibleInstances, TypeSynonymInstances #-}  -- | Provides basic types and functions for other parts of /Copilot/. --@@ -8,22 +8,17 @@ -- to add an ext[Type], a [type] and a var[Type] -- functions in Language.hs to make it easier to use.  module Language.Copilot.Core (-        -- * Type hierarchy for the copilot language-        Var, Name, Period, Phase, Port(..),-        Spec(..), Streams, Stream, Send(..), --DistributedStreams,-        Trigger(..), Triggers, notVarErr, LangElems(..),-	-- * General functions on 'Streams' and 'StreamableMaps'-	Streamable(..), mkSend, -- Sendable(..)-        StreamableMaps(..), emptySM,+        Period, Var, Name, Port(..), Ext(..),+        Exs, ExtRet(..), Args, ArgConstVar(..),+        Spec(..), Streams, Stream, Send(..), +        Trigger(..), Triggers, LangElems(..),+	Streamable(..), StreamableMaps(..), emptySM,         isEmptySM, getMaybeElem, getElem, -        foldStreamableMaps, --foldSendableMaps, +        foldStreamableMaps,          mapStreamableMaps, mapStreamableMapsM,         filterStreamableMaps, normalizeVar, getVars, Vars,-        -- compiler-        BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, -        ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..),-        tmpVarName, tmpArrName, getAtomType,-        getSpecs, getSends, getTriggers, makeTrigger -- XXX compiler+        getAtomType, getSpecs, getSends, getTriggers, vPre, funcShow,+        getMaybeVar, notConstVarErr     ) where  import qualified Language.Atom as A@@ -41,10 +36,10 @@ type Var = String -- | C file name type Name = String--- | Atom period+-- | Atom period -- used as an option to control the duration of a Copilot "tick". type Period = Int--- | Phase of an Atom phase-type Phase = Int+-- -- | Phase of an Atom phase+-- type Phase = Int -- | Port over which to broadcast information data Port = Port Int @@ -54,9 +49,9 @@     Var :: Streamable a => Var -> Spec a     Const :: Streamable a => a -> Spec a -    PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a+    PVar :: Streamable a => A.Type -> Ext  -> Spec a     PArr :: (Streamable a, Streamable b, A.IntegralE b) -         => A.Type -> (Var, Spec b) -> Phase -> Spec a+         => A.Type -> (Ext, Spec b) -> Spec a      F :: (Streamable a, Streamable b) =>  	    (b -> a) -> (A.E b -> A.E a) -> Spec b -> Spec a@@ -69,6 +64,68 @@     Append :: Streamable a => [a] -> Spec a -> Spec a     Drop :: Streamable a => Int -> Spec a -> Spec a +-- | Arguments to be passed to a C function.  Either a Copilot variable or a+-- constant.  A little hacky that I store constants as strings so we don't have+-- to pass around types.  However, these data are just used to make external C+-- calls, for which we have no type info anyway, so it's a bit of a moot point.+data ArgConstVar = V Var+                 | C String+  deriving Eq++instance Show ArgConstVar where +  show args = case args of+                V v -> normalizeVar v+                C c -> "_const_" ++ c ++ "_"++type Args = [ArgConstVar]++data Trigger =+  Trigger { trigVar  :: Spec Bool+          , trigName :: String+          -- We carry around both the value and the vars of the arguments to be+          -- passed to the trigger.  The vars are used to put the arguments in+          -- the correct order, since the values are stored in a map, destroying+          -- their order.+          , trigArgs :: Args} ++type Triggers = M.Map String Trigger++instance Show Trigger where +  show (Trigger s fnName args) =+    "trigger_" ++ getMaybeVar s ++ "_" ++ fnName ++ "_" ++ normalizeVar (show args)++-- XXX change the constructors to SimpleVar and Function (or something like that)+-- XXX in Ext, we throw away the type info for Args.  This is because we're just+-- making external calls, and we don't know anything about the types anyway (we+-- just make strings).  Remove from the datatype.+-- | Holds external variables or external functions to call.+data Ext = ExtV Var+         | Fun String Args++type Exs = (A.Type, Ext, ExtRet)++data ExtRet = ExtRetV +            | ExtRetA String+  deriving Eq++instance Show Ext where+  show (ExtV v) = v+  show (Fun f args) = normalizeVar f ++ show args++-- | For calling a function with Atom variables.+funcShow :: Name -> String -> Args -> String+funcShow cName fname args = +  fname ++ "(" ++ (unwords $ intersperse "," +    (map (\arg -> case arg of+                    v@(V _) -> vPre cName ++ show v+                    C c -> c+         ) args)) ++ ")"++instance Eq Ext where+  (==) (ExtV v0) (ExtV v1) = v0 == v1+  (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1  +  (==) _ _ = False+ -- These belong in Language.hs, but we don't want orphan instances. instance (Streamable a, A.NumE a) => Num (Spec a) where     (+) = F2 (+) (+) -- A.NumE a => E a is an instance of Num@@ -94,9 +151,9 @@     #-}  instance Eq a => Eq (Spec a) where-    (==) (PVar t v ph) (PVar t' v' ph') = t == t' && v == v' && ph == ph'-    (==) (PArr t (v, idx) ph) (PArr t' (v', idx') ph') = -           t == t' && v == v' && show idx == show idx' && ph == ph'+    (==) (PVar t v) (PVar t' v') = t == t' && v == v' -- && ph == ph'+    (==) (PArr t (v, idx)) (PArr t' (v', idx')) = +           t == t' && v == v' && show idx == show idx' -- && ph == ph'     (==) (Var v) (Var v') = v == v'     (==) (Const x) (Const x') = x == x'     (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s'@@ -106,35 +163,26 @@     (==) (Drop i s) (Drop i' s') = i == i' && s == s'     (==) _ _ = False --- | An instruction to send data on a port at a given phase.  Uses a phantom type.+-- | Get a variable name from a spec; throw an error otherwise.+getMaybeVar :: Streamable a => Spec a -> Var+getMaybeVar (Var v) = v+getMaybeVar s = error $ "Expected a Copilot variable but provided " ++ show s ++ " instead."++-- | Copilot variable reference, taking the name of the generated C file.+vPre :: Name -> String+vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "."++-- | An instruction to send data on a port at a given phase.   -- data Send a = Sendable a => Send (Var, Phase, Port) data Send a =     Send { sendVar  :: Spec a -       , sendPh   :: Phase        , sendPort :: Port        , sendName :: String}  instance Streamable a => Show (Send a) where -  show (Send s ph (Port port) portName) = -    notVarErr s (\var -> (portName ++ "_port_" ++ show port ++ "_var_" -                            ++ var ++ "_ph_" ++ show ph))-data Trigger =-  Trigger { trigVar  :: Spec Bool-          , trigName :: String-          -- We carry around both the value and the vars of the arguments to be-          -- passed to the trigger.  The vars are used to put the arguments in-          -- the correct order, since the values are stored in a map, destroying-          -- their order.-          , trigArgs :: ([Var], StreamableMaps Spec)} --type Triggers = M.Map String Trigger--instance Show Trigger where -  show (Trigger s fnName _) =-    notVarErr s (\var -> ("trigger_" ++ var ++ "_" ++ fnName ++ "_")) -- XXX add args---                            ++ map (\x -> if x == ' ' then '_' else x) ---                                   (concatMap show args)))-+  show (Send s (Port port) portName) = +    portName ++ "_port_" ++ show port ++ "_var_" ++ getMaybeVar s+                             -- | Holds all the different kinds of language elements that are pushed into the -- Writer monad.  This currently includes the actual specs, "send" directives, -- and trigger directives. (Use the functions in Language.hs to make sends and@@ -150,13 +198,13 @@  getSpecs :: Streams -> StreamableMaps Spec getSpecs streams = -  let (LangElems strms _ _) = execWriter streams-  in  strms+  let (LangElems ss _ _) = execWriter streams+  in  ss  getSends :: Streams -> StreamableMaps Send getSends streams = -  let (LangElems _ snds _) = execWriter streams-  in  snds+  let (LangElems _ sendMap _) = execWriter streams+  in  sendMap  getTriggers :: Streams -> Triggers getTriggers streams = @@ -166,7 +214,17 @@ -- | A named stream type Stream a = Streamable a => (Var, Spec a) +-- | If the 'Spec' isn't a 'Var' or 'Const', then throw an error; otherwise,+-- apply the function.+notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b+notConstVarErr s f =+  case s of+    Var v -> f (V v)+    Const c -> f (C (showAsC c))+    _     -> error $ "You provided specification \n" ++ "  " ++ show s +                        ++ "\n where you needed to give a Copilot variable or constant." + -- | Holds the complete specification of a distributed monitor -- type DistributedStreams = (Streams, Sends) @@ -215,21 +273,6 @@     -- doubles have the good precision.     showAsC :: a -> String  --- | If the 'Spec' isn't a 'Var', then throw an error; otherwise, apply the--- function.-notVarErr :: Streamable a => Spec a -> (Var -> b) -> b-notVarErr s f =-  case s of-    Var v -> f v-    _     -> error $ "You provided specification \n" ++ show s -                      ++ "\n where you needed to give a variable."---- | Sending data over ports.-mkSend :: (Streamable a) => A.E a -> Port -> String -> A.Atom ()-mkSend e (Port port) portName =-  A.action (\[ueStr] -> portName ++ "(" ++ ueStr ++ "," ++ show port ++ ")") -           [A.ue e]- instance Streamable Bool where     getSubMap = bMap     updateSubMap f sm = sm {bMap = f $ bMap sm}@@ -341,9 +384,11 @@ -- Launch an exception if the index is not in it {-# INLINE getElem #-} getElem :: Streamable a => Var -> StreamableMaps b -> b a-getElem v sm = case getMaybeElem v sm of-                 Nothing -> error "Error in application of getElem from Core.hs."-                 Just x -> x+getElem v sm = +  case getMaybeElem v sm of+    Nothing -> error $ "Error in application of getElem from Core.hs for variable "+                 ++ v ++ "."+    Just x -> x  getAtomType :: Streamable a => Spec a -> A.Type getAtomType s =@@ -499,14 +544,9 @@  -- | Replace all accepted special characters by sequences of underscores.   normalizeVar :: Var -> Var-normalizeVar v =-    foldl (\ acc c -> acc ++ case c of -                               '.' -> "_" -                               '[' -> "_"  -                               ']' -> "_"  -                               ' ' -> "_"-                               _ -> [c]) -          "" v+normalizeVar v = +  map (\c -> if (c `elem` ".[]()") then '_' else c)+      (filter (\c -> c /= ',' && c /= ' ') v)   -- | For each typed variable, this type holds all its successive values in an infinite list -- Beware : each element of one of those lists corresponds to a full @Atom@ period, @@ -524,11 +564,11 @@     tabs ++ showRaw s n  showRaw :: Spec a -> Int -> String-showRaw (PVar t v ph) _ = "PVar " ++ show t ++ " " ++ v ++ " " ++ show ph-showRaw (PArr t (v, idx) ph) _ = -  "PArr " ++ show t ++ " (" ++ v ++ " ! (" ++ show idx ++ ")) " ++ show ph+showRaw (PVar t v) _ = "PVar " ++ show t ++ " " ++ show v -- ++ " " ++ show ph+showRaw (PArr t (v, idx)) _ = +  "PArr " ++ show t ++ " (" ++ show v ++ " ! (" ++ show idx ++ "))" -- ++ show ph showRaw (Var v) _ = "Var " ++ v-showRaw (Const e) _ = "Const " ++ show e+showRaw (Const e) _ = show e showRaw (F _ _ s0) n =      "F op? (\n" ++          showIndented s0 (n + 1) ++ "\n" ++ @@ -555,133 +595,3 @@   --- XXX--- Compiler: the code below really belongs in Compiler.hs, but its called by--- makeTrigger, which is a method of the class Streamable.---- XXX--- Check that a trigger references a Copilot variable of type 'Spec' 'Bool'.--- checkTrigger :: forall a m. (Monad m, Streamable a) ---              => Trigger a -> StreamableMaps Spec -> m ()--- checkTrigger (Trigger var _ args) streams =---   if null badDefs---     then if getAtomType var == A.Bool---            then return ()---            else error $ "Copilot error in defining triggers: the variable " ---                           ++ show var ++ " are of a type other than Bool."---     else error $ "Copilot error in defining triggers: the variables " ++ show badDefs ---                    ++ "don't define streams in-scope."---   where varChk v = case getMaybeElem v streams :: Maybe (Spec a) of---                      Nothing -> [v]---                      Just _  -> []---         badDefs = notVarErr var varChk ++ concatMap varChk args----- | To make customer C triggers.  Only for Spec Bool (others throw an--- error).  XXX make them throw errors!-makeTrigger :: StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -            -> Trigger -> A.Atom () -> A.Atom ()--makeTrigger streams prophArrs tmpSamples outputIndexes -            trigger@(Trigger s fnName (vars,args)) r = -  do r -     A.liftIO $ putStrLn ("len" ++ (show $ length vars)) ---         checkTrigger trigger streams-     (A.exactPhase 0 $ A.atom (show trigger) $ -        do A.cond (nextSt streams prophArrs tmpSamples outputIndexes s 0)-           A.action (\ues -> fnName ++ "(" ++ unwords (intersperse "," ues) ++ ")")-              (reorder vars []-                (foldStreamableMaps -                  (\v argSpec ls -> (v,next argSpec):ls) args [])))-     where next :: Streamable a => Spec a -> A.UE -           next a = A.ue $ nextSt streams prophArrs -                             tmpSamples outputIndexes a 0-           reorder [] acc _ = reverse $ snd (unzip acc)-           reorder (v:vs) acc ls = -               case lookup v ls of-                 Nothing -> error "Error in makeTrigger in Core.hs."-                 Just x  -> let n = (v,x)-                            in reorder vs (n:acc) ls---- For the prophecy arrays-type ArrIndex = Word64-type ProphArrs = StreamableMaps BoundedArray-type Outputs = StreamableMaps A.V-type Indexes = M.Map Var (A.V ArrIndex)---- External variables-data PhasedValueVar a = PhV Phase (A.V a)---type TmpVarSamples = StreamableMaps PhasedValueVar--tmpVarName :: Var -> Phase -> Var-tmpVarName v ph = normalizeVar v ++ "_" ++ show ph----- External arrays-data PhasedValueArr a = PhA Phase (A.V a) -- Array name.-data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. --data TmpSamples = -  TmpSamples { tmpVars :: StreamableMaps PhasedValueVar-             , tmpArrs :: StreamableMaps PhasedValueArr-             , tmpIdxs :: StreamableMaps PhasedValueIdx-             }--emptyTmpSamples :: TmpSamples-emptyTmpSamples = TmpSamples emptySM emptySM emptySM--tmpArrName :: Var -> Phase -> String -> Var-tmpArrName v ph idx = (tmpVarName v ph) ++ "_" ++ normalizeVar idx--data BoundedArray a = B ArrIndex (Maybe (A.A a))--nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -       -> Spec a -> ArrIndex -> A.E a-nextSt streams prophArrs tmpSamples outputIndexes s index = -    case s of-        PVar _ v ph  -> -          let PhV _ var = getElem (tmpVarName v ph) (tmpVars tmpSamples) in-          A.value var-        PArr _ (v, idx) ph -> -          let PhA _ var = e tmp (tmpArrs tmpSamples) -              tmp = tmpArrName v ph (show idx) -              e a b = case getMaybeElem a b of-                        Nothing -> -                          error "Error in application of getElem in nextSt."-                        Just x  -> x -          in A.value var-        Var v -> let B initLen maybeArr = getElem v prophArrs in-            -- This check is extremely important-            -- It means that if x at time n depends on y at time n-            -- then x is obtained not by y, but by inlining the definition of y-            -- so it increases the size of code (sadly),-            -- but is the only thing preventing race conditions from occuring-            if index < initLen-                then getVar v initLen maybeArr -                else let s0 = getElem v streams in -                     next s0 (index - initLen)-        Const e -> A.Const e-        F _ f s0 -> f $ next s0 index-        F2 _ f s0 s1 ->-            f (next s0 index) -              (next s1 index)-        F3 _ f s0 s1 s2 ->-            f (next s0 index) -              (next s1 index) -              (next s2 index)-        Append _ s0 -> next s0 index-        Drop i s0 -> next s0 (fromInteger (toInteger i) + index)-    where-        next :: Streamable b => Spec b -> ArrIndex -> A.E b-        next = nextSt streams prophArrs tmpSamples outputIndexes -        getVar :: Streamable a -               => Var -> ArrIndex -> Maybe (A.A a) -> A.E a-        getVar v initLen maybeArr =-           let outputIndex = case M.lookup v outputIndexes of-                               Nothing -> error "Error in function getVar."-                               Just x -> x-               arr = case maybeArr of-                       Nothing -> error "Error in function getVar (maybeArr)."-                       Just x -> x in -           arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_`  -                       (A.Const (initLen + 1)))

@@ -12,7 +12,7 @@   (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where  import Language.Copilot.Core-import Language.Copilot.Analyser+import Language.Copilot.Analyser (check, getExternalVars) import Language.Copilot.Interpreter import Language.Copilot.AtomToC import Language.Copilot.Compiler@@ -33,12 +33,8 @@     , interpreted :: Interpreted -- ^ Interpret the program or not     , outputDir :: String -- ^ Where to put the executable     , compiler :: String -- ^ Which compiler to use-    , prePostCode :: Maybe (String, String) -- ^ Code to replace the default initialization and main-    -- , triggers :: [(Var, String)] -- ^ A list of Copilot variable C function-    --                               -- name pairs.  The C funciton is called if-    --                               -- the Copilot stream becomes True.  The-    --                               -- Stream must be of Booleans and the C-    --                               -- function must be of type void @foo(void)@.+    , prePostCode :: Maybe (String, String) -- ^ Code to replace the default+                                            -- initialization and main     , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we                                  -- don't know how large external arrays are, so                                  -- we cannot declare them.  Passing in pairs@@ -123,17 +119,19 @@         isSilent = verbose == OnlyErrors         isExecuted = iterations /= 0         allExts = getExternalVars (strms elems)-        (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts+        (trueInputExts :: StreamableMaps [] , allInputsPresents :: Bool) = +          filterStreamableMaps inputExts (map (\(a,v,r) -> (a, show v, r)) allExts) -copilotToC :: LangElems -> [(A.Type, Var, ExtVars)] -> Vars -> AtomToC -> Bool -> IO ()+copilotToC :: LangElems -> [Exs] -> Vars -> AtomToC -> Bool -> IO () copilotToC elems allExts trueInputExts opts isVerbose =-    let (p', program) = copilotToAtom elems (getPeriod opts)-        cFileName = cName opts+    let cFileName = cName opts+        (p', program) = copilotToAtom elems (getPeriod opts) cFileName         (preCode, postCode) =              case (prePostCode opts) of                 Nothing ->                     getPrePostCode cFileName (strms elems) allExts -                                 (arrDecs opts) trueInputExts p'+                                 (map (\(x,y) -> (ExtV x,y)) (arrDecs opts))+                                 trueInputExts p'                 Just (pre, post) -> (pre, post)         atomConfig = A.defaults              { A.cCode = \_ _ _ -> (preCode, postCode)

@@ -10,7 +10,7 @@ -- for specifying options import Data.Map (fromList)  import Data.Maybe (Maybe (..))-import System.Random+--import System.Random  import Language.Copilot  -- import Language.Copilot.Variables@@ -18,7 +18,7 @@ fib :: Streams fib = do   let f = varW64 "f"-  let t   = varB "t"+      t   = varB "t"   f .= [0,1] ++ f + (drop 1 f)   t .= even f     where even :: Spec Word64 -> Spec Bool@@ -27,9 +27,9 @@ t1 :: Streams t1 = do   let x = varI32 "x"-  let y = varB "y"-  let z = varB "z"-  let w = varB "w"+      y = varB "y"+      z = varB "z"+      w = varB "w"   x .= [0, 1, 2] ++ x - (drop 1 x)   y .= [True, False] ++ y ^ z   z .= x <= drop 1 x@@ -44,35 +44,31 @@ t3 :: Streams t3 = do   let a    = varW32 "a"-  let b    = varB "b"-  let ext8 = extW32 "ext" 8-  let ext1 = extW32 "ext" 1+      b    = varB "b"+      ext8 = extW32 "ext"+      ext1 = extW32 "ext"   a .= [0,1] ++ a + ext8 + ext8 + ext1   b .= [True, False] ++ 2 + a < 5 + ext1  t4 :: Streams t4 = do   let a = varB "a"-  let b = varB "b"+      b = varB "b"   a .= [True,False] ++ not a   b .= drop 1 a  t5 :: Streams t5 = do   let x = varW16 "x"-  let t = varF "t"-  let y = varB "y"-  let w = varB "w"-  let z = varB "z"-  x .= cast (drop 3 y)-  t .= [0] ++ t-  y .= [True, True] ++ not z-  z .= [False] ++ false-  w .= z || y+      y = varB "y"+      z = varB "z"+  x .= [0] ++ x + 1+  y .= [True, True] ++ y+  z .= [False] ++ not z   -- triggers-  trigger y "w_trigger" (w <> x <> x <>> t) -- XXX wrong arg seem generated for x-  trigger z "y_trigger" void-  trigger w "z_trigger" (x <> y <> z <>> x)+  trigger y "y_trigger" void+  trigger z "z0_trigger" x+  trigger z "z1_trigger" (y <> constW16 3 <> x)    yy :: Streams yy = @@ -82,7 +78,7 @@ zz :: Streams zz = do   let a = varW32 "a"-  let b = varW32 "b"+      b = varW32 "b"   --a .= [0..4] ++ drop 4 (varW32 a) + 1   a .= a + 1   b .= drop 3 a@@ -90,47 +86,57 @@ xx :: Streams xx = do   let a = varW32 "a"-  let b = varW32 "b"-  let c = varW32 "c"-  let ext = extW32 "ext" 1-  a .= ext+      b = varW32 "b"+      c = varW32 "c"+      e = extW32 "ext"+      d = varB "d"+      f = extW32 (fun "fun1" void) +      h = extArrW16 (fun "g" b) a +      g = extW16 (fun "fun2" (true <> b <> constW16 3))+      w = varB "w"+  a .= e + f   b .= [3] ++ a   c .= [0, 1, 3, 4] ++ drop 1 b+  d .= h < g+  -- triggers+  trigger d "y_trigger" void+  trigger w "z0_trigger" (a <> b <> true)+  trigger w "z1_trigger" (d <> constW16 3 <> w)  -- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the -- engine is immediately shut off.  From the paper. engine :: Streams engine = do   -- external vars-  let temp     = extF "temp" 1      -  let shutoff  = extB "shutoff" 2+  let temp     = extF "temp"+      shutoff  = extB "shutoff"   -- Copilot vars-  let temps    = varF "temps"-  let overTemp = varB "overTemp"-  let trigger  = varB "trigger"+      temps    = varF "temps"+      overTemp = varB "overTemp"+      err  = varB "trigger"    temps    .= [0, 0, 0] ++ temp   overTemp .= drop 2 temps > 2.3 + temps-  trigger  .= overTemp ==> shutoff+  err  .= overTemp ==> shutoff  -- | Sending over ports. distrib :: Streams distrib = do   -- vars   let a = varW8 "a"-  let b = varB "b"+      b = varB "b"   -- spec   a .= [0,1] ++ a + 1   b .= mod a 2 == 0    -- sends-  send "portA" (port 2) a 1-  send "portB" (port 1) b 2+  send "portA" (port 2) a +  send "portB" (port 1) b   -- greatest common divisor. gcd :: Word16 -> Word16 -> Streams gcd n0 n1 = do   let a = varW16 "a"-  let b = varW16 "b"+      b = varW16 "b"   a .= alg n0 a b   b .= alg n1 b a @@ -148,18 +154,18 @@ -- sample the external variables. gcd' :: Streams gcd' = do -  let n = extW16 "n" 1-  let m = extW16 "m" 1--  let a = varW16 "a"-  let b = varW16 "b"-  let init = varB "init"+  -- externals+  let n = extW16 "n"+      m = extW16 "m"+  -- copilot vars+      a = varW16 "a"+      b = varW16 "b"+      init = varB "init"+      ans  = varB "ans"+     a .= alg n (sub a b) init   b .= alg m (sub b a) init--  let ans = varB "ans"   ans .= a == b && not init-   init .= [True] ++ false    where sub hi lo = mux (hi > lo) (hi - lo) hi@@ -189,8 +195,7 @@   y .= cast x + cast x  i8 :: Streams-i8 = -  let v = varI8 "v" in v .= [0, 1] ++ v + 1 +i8 = let v = varI8 "v" in v .= [0, 1] ++ v + 1       trap :: Streams trap = do@@ -262,7 +267,7 @@ --  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2    let g = varB "g"   let gg = extArrW16 "gg" e -  g .= gg 1 == gg 2+  g .= gg < 13   -- h .= [0] ++ drop 1 (varW16 g)  @@ -270,11 +275,16 @@ t99 :: Streams t99 = do   let ext = extW32 "ext"-  let a = varW32 "a"-  a .= [0,1] ++ a + ext 8 + ext 8 + ext 1+      a = varW32 "a"+  a .= [0,1] ++ a + ext + ext + ext     let b = varB "b"-  b .= [True, False] ++ 2 + a < 5 + ext 1+  b .= [True, False] ++ 2 + a < 5 + ext ++t11 :: Streams+t11 = do+  let v = varB "v"+  v .= [False, True, False] ++ v  -- test external idx before after and in the stream it references -- test multiple defs

@@ -72,12 +72,12 @@ testRules :: Streams testRules = do   let v1 = varB "v1"-  let v2 = varB "v2"-  let v3 = varI16 "v3"-  let v4 = varB "v4"-  let ext = extI8 "ext" 5 +      v2 = varB "v2"+      v3 = varI16 "v3"+      v4 = varB "v4"+      ex = extI8 "ex"    v1 .=    (not true) || v2-  v2 .=    [True, False] ++ [True] ++ v3 < cast ext+  v2 .=    [True, False] ++ [True] ++ v3 < cast ex   v3 .=    0 + drop 3 6   v4 `ltl` always 5 v1 

@@ -20,7 +20,7 @@ tprv :: Streams tprv = do   let c = varB "c"-  let a = varB "a"+      a = varB "a"   tstdatprv    c `ptltl` previous a @@ -33,7 +33,7 @@ tAB :: Streams tAB = do    let f = varB "f"-   let d = varB "d"+       d = varB "d"    tstdatAB     f `ptltl` alwaysBeen d @@ -46,7 +46,7 @@ tEP :: Streams tEP = do     let h = varB "h"-    let g = varB "g"+        g = varB "g"     tstdatEP      h `ptltl` eventuallyPrev g @@ -61,7 +61,6 @@  tstdat2Sin :: Streams tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2-                    tSince :: Streams  tSince = do@@ -73,19 +72,19 @@ -- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 tSinExt :: Streams  tSinExt = do-  let e1 = extB "e1" 2-  let e2 = extB "e2" 3+  let e1 = extB "e1"+      e2 = extB "e2"   z `ptltl` (e1 `since` e2)  tSinExt2 :: Streams  tSinExt2 = do-  let e1 = extB "e1" 2-  let e2 = extB "e2" 2-  let a = varB "a"-  let s = varB "s"-  let d = varB "d"-  let t = varB "t"-  let e = varB "e"+  let e1 = extB "e1"+      e2 = extB "e2"+      a = varB "a"+      s = varB "s"+      d = varB "d"+      t = varB "t"+      e = varB "e"    a .= not e1   s `ptltl` (e2 `since` d)@@ -98,15 +97,15 @@ engine :: Streams engine = do   -- external vars-  let engineTemp = extW8 "engineTemp" 1-  let engineOff  = extB "engineOff" 1-  let coolerOn   = extB "coolerOn" 1+  let engineTemp = extW8 "engineTemp"+      engineOff  = extB "engineOff"+      coolerOn   = extB "coolerOn"   -- Copilot vars-  let cnt        = varW8 "cnt"-  let temp       = varB "temp"-  let cooler     = varB "cooler"-  let off        = varB "off"-  let monitor    = varB "monitor"+      cnt        = varW8 "cnt"+      temp       = varB "temp"+      cooler     = varB "cooler"+      off        = varB "off"+      monitor    = varB "monitor"    temp    `ptltl` (alwaysBeen (engineTemp > 250))   cnt     .=      [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt@@ -122,5 +121,6 @@                             , ("coolerOn", replicate 9 False P.++ repeat True)                             ]                   , w8Map = fromList [("engineTemp", [99,100..])]-                  }) baseOpts+                  }) +    baseOpts 

@@ -10,9 +10,9 @@ t0 :: Streams t0 = do   let minV = varW16 "min"-  let maxV = varW16 "max"-  let sumV = varW16 "sum"-  let a = varW16 "a"+      maxV = varW16 "max"+      sumV = varW16 "sum"+      a = varW16 "a"    a .= [0..5] ++ a + 6   minV .= min 3 a@@ -22,7 +22,7 @@ tMean :: Streams tMean = do   let a = varD "a"-  let out = varD "out"+      out = varD "out"    a .= [0..5] ++ a + 6   out .= mean 4 a

@@ -11,20 +11,20 @@   , "There are 4 essential Copilot commands.  Each command may take a variety"   , "of options. We describe the commands then list the possible options."   , ""-  , " interpret :: Streams -> Int -> Options -> IO ()"-  , " > interpret STREAMS RNDS [$ OPTS] baseOpts"+  , " interpret :: Streams -> Int -> (Options -> Options) -> IO ()"+  , " > interpret STREAMS RNDS (noOpts | [$ OPTS])"   , "   Executes the interpreter for the Copilot specification STREAMS of type"   , "   'Streams', where the specification is interpreted as a set of mutually-"   , "   recursive Haskell infinite lists.  The output from the lists is given"   , "   for RNDS indexes.  RNDS must be greater than 0."   , ""-  , " compile :: Streams -> String -> Options -> IO ()"-  , " > compile STREAMS FILENAME [$ OPTS] baseOpts"+  , " compile :: Streams -> String -> (Options -> Options) -> IO ()"+  , " > compile STREAMS FILENAME (noOpts | [$ OPTS])"   , "   Compiles the Copilot specification STREAMS to constant-time & constant-"   , "   constant-space C program named FILENAME.c with header FILENAME.h"   , "   and executable FILENAME."   , ""-  , " > test RNDS [$ OPTS] baseOpts"+  , " > test RNDS (noOpts | [$ OPTS])"   , "   Generates a random set of streams & inputs for external variables, and"   , "   tests the equivalence between the output of the compiled C program and"   , "   the interpreter over RNDS rounds.  RNDS must be greater than 0.  This"@@ -37,8 +37,8 @@   , " > STREAMS                                   -- in ghci"   , "   Pretty-prints the parsed Copilot specification of type 'Streams'."   , ""-  , " verify :: FilePath -> Int -> IO () (FilePath is a synonym for String)"-  , " > verify PATH/FILE.c n"+  , " verify :: FilePath -> Int -> String -> IO () (FilePath is a synonym for String)"+  , " > verify PATH/FILE.c n opts (opts are additional options for cbmc.)"   , "   Calls cbmc, developed by Daniel Kroening \& Edmund Clarke"   , "   <http://www.cprover.org/cbmc/> on a C file generated by Copilot."   , "   cbmc is a bounded model-checker that verifies C programs.  While there"@@ -64,8 +64,7 @@   , "relevant to; e.g., (i, t) means that an option is relevant to the"   , "interpreter and test functions."   , ""-  , "For each option, there is a default, that is included in baseOpts.  For"-  , "each option, we describe the default."+  , "For each option, there is a default described below."   , ""   , "  setE :: Vars -> Options -> Options                                    (i)"   , "    default: Nothing (no assignments)" @@ -139,7 +138,7 @@   , "The following examples reference Copilot specs defined in"   , "Language.Copilot.Examples.Examples."   , ""-  , " > interpret t0 50 baseOpts"+  , " > interpret t0 50 noOpts"   , "   Interprets t0 for 50 iterations."   , ""   , " > interpret t3 40"@@ -150,23 +149,24 @@   , "   Interpret t3 for 40 iterations, seeding the external variable \"ext\""   , "   to [0,1,..], with 'Verbose' verbosity."   , ""-  , " > compile t1 \"t1\" baseOpts"+  , " > compile t1 \"t1\" noOpts"   , "   Compile Copilot spec t1 to t1.c, t1.h, and executable t1 in the default"   , "   directory, /tmp/copilot/ .  This is compiled with a simulation main()"   , ""-  , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100 baseOpts"+  , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100"   , "   Compile Copilot spec t2 to t2.c, t2.h, and executable t2 in the default"   , "   directory, /tmp/copilot/ , with optimization level -02 and period 100."   , "   This is compiled with a simulation main()."   , ""-  , " > test 1000 baseOpts"+  , " > test 1000"   , "   Compare the compiler and interpreter for a randomly-generated Copilot"   , "   spec for 1000 iterations."   , ""-  , " > Prelude.sequence_ [test 100 $ setR x baseOpts | x <- [0..100]]"+  , " > Prelude.sequence_ [test 100 $ setR x | x <- [0..100]]"   , "   Compare the compiler and interpreter on 100 randomly-generated Copilot"   , "   specs, for 100 iterations each."   , ""-  , " > verify \"foo.c\""-  , "   Calls cbmc on foo.c (where foo.c is in the current directory)."+  , " > verify \"foo.c\" n"+  , "   Calls cbmc on foo.c (where foo.c is in the current directory) and"+  , "   unrolls the program n times."   ]

@@ -1,13 +1,16 @@+{-# LANGUAGE FlexibleInstances #-}+ -- | Used by the end-user to easily give its arguments to dispatch. module Language.Copilot.Interface (           Options(), baseOpts, test, interpret, compile, verify, interface         , help , setE, setC, setO, setP, setI, setPP, setN, setV, setR-        , setDir, setGCC, setArrs, setClock,+        , setDir, setGCC, setArrs, setClock, noOpts,         module Language.Copilot.Dispatch     ) where  import Language.Copilot.Core-import Language.Copilot.Language (opsF, opsF2, opsF3)+--import Language.Copilot.Language (opsF, opsF2, opsF3)+import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3) import Language.Copilot.Tests.Random import Language.Copilot.Dispatch import Language.Copilot.Help@@ -76,6 +79,9 @@  -- Functions for making it easier for configuring copilot in the frequent use cases +noOpts :: Options -> Options+noOpts = id+ test :: Int -> Options -> IO () test n opts =    interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts @@ -90,8 +96,8 @@     $ setTriggers (getTriggers streams)        $ opts {optStreams = Just (getSpecs streams)} -verify :: FilePath -> Int -> IO ()-verify file n = do+verify :: FilePath -> Int -> String -> IO ()+verify file n opts = do   putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke."   putStrLn "<http://www.cprover.org/cbmc/>, with the following checks:"   putStrLn "  --bounds-check       enable array bounds checks"@@ -100,21 +106,17 @@   putStrLn "  --overflow-check     enable arithmetic over- and underflow checks"   putStrLn "  --nan-check          check floating-point for NaN"   putStrLn ""-  putStrLn $ "  assuming main() as the entry point:"+  putStrLn "Assuming main() as the entry point unless specified otherwise (--function f)"   putStrLn cmd   code <- system cmd   case code of     ExitSuccess -> return ()-    _           -> do putStrLn $ "cbmc could not be called on file " ++ file ++ "."-                      putStrLn "Perhaps cbmc is not installed on your system, is"-                      putStrLn "not in your path, cbmc cannot be called from the"-                      putStrLn $ "command line on your system, or " ++ file -                      putStrLn "does not exist.  See <http://www.cprover.org/cbmc/>"-                      putStrLn "for more information on cbmc."+    _           -> do putStrLn ""+                      putStrLn $ "An error was returned by cbmc.  This may have be due to cbmc not finding the file " ++ file ++ ".  Perhaps cbmc is not installed on your system, is not in your path, cbmc cannot be called from the command line on your system, or " ++ file ++ " does not exist.  See <http://www.cprover.org/cbmc/>  for more information on cbmc."     where cmd = unwords ("cbmc" : args)           args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"                  , "--nan-check", "--pointer-check"-                 , "--unwind " ++ show n, file] +                 , "--unwind " ++ show n, opts, file]                       -- Small functions for easy modification of the Options record@@ -123,7 +125,7 @@ setS :: StreamableMaps Send -> Options -> Options setS sends opts = opts {optSends = sends} --- | Set the directives for sending stream values on ports.+-- -- | Set the directives for sending stream values on ports. setTriggers :: Triggers -> Options -> Options setTriggers triggers opts = opts {optTriggers = triggers} @@ -194,17 +196,6 @@ -- If nothing, then code appropriate for communication with the interpreter is generated setPP :: (String, String) -> Options -> Options setPP pp opts = opts {optPrePostCode = Just pp}---- -- | Give C function triggers for Copilot Boolean streams.  The tiggers fire if--- -- the stream becoms true.--- setTriggers :: [(Var, String)] -> Options -> Options--- setTriggers trigs opts = opts {optTriggers = trigs}---   -- if null repeats ---   --   then ---   --   else error $ "Error: only one trigger per Copilot variable.  Variables "---   --                ++ show (Set.fromList repeats) ++ " are given multiple triggers."---   -- where vars = map fst trigs---   --       repeats = vars \\ Set.toList (Set.fromList vars)  -- | The "main" function that dispatches. interface :: Options -> IO ()

@@ -1,5 +1,8 @@+{-# LANGUAGE Rank2Types #-}+ -- | The Copilot interpreter.-module Language.Copilot.Interpreter(interpretStreams) where+module Language.Copilot.Interpreter+    (interpretStreams) where  import Language.Copilot.Core @@ -12,14 +15,15 @@     where          inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams -interpret :: Streamable a => Vars -> Vars -> Spec a -> [a]+interpret :: forall a. Streamable a => Vars -> Vars -> Spec a -> [a] interpret inVs moVs s =   case s of     Const c -> repeat c     Var v -> getElem v inVs-    PVar _ v _ -> getElem v moVs-    PArr _ (v,s') _ -> map (\i -> getElem v moVs !! fromIntegral i) -                           (interpret inVs moVs s')+    PVar _ v -> checkV v (\v' -> (getElem v' moVs))+    PArr _ (v,s') -> checkV v (\v' -> map (\i ->    getElem v' moVs +                                                   !! fromIntegral i)+                                            (interpret inVs moVs s'))     Append ls s' -> ls ++ interpret inVs moVs s'     Drop i s' -> drop i $ interpret inVs moVs s'     F f _ s' -> map f (interpret inVs moVs s')@@ -29,3 +33,12 @@                        (interpret inVs moVs s0)                         (interpret inVs moVs s1)                        (interpret inVs moVs s2)+  where +    checkV :: Ext -> (Var -> [a]) -> [a]+    checkV v f = +          case v of+            ExtV v' -> f v'+            -- XXX support this?  +            Fun _ _ -> error $ "Sampling functions is not currently supported"+                               ++ " in the Copilot interpreter."+                          

@@ -1,9 +1,11 @@-{-# LANGUAGE NoImplicitPrelude, Rank2Types, ScopedTypeVariables, FlexibleContexts #-}+{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}  -- | Describes the language /Copilot/. ----- If you wish to add a new operator, the only modification needed is adding it in this module.--- But if you want it to be used in the random generated streams, add it to either @'opsF'@, @'opsF2'@ or @'opsF3'@+-- If you wish to add a new operator, the only modification needed is adding it+-- in this module.  But if you want it to be used in the random generated+-- streams, add it to either @'opsF'@, @'opsF2'@ or @'opsF3'@ module Language.Copilot.Language (         -- * Operators and functions         mod, div, mod0, div0,@@ -19,41 +21,41 @@         -- * Copilot variable declarations.         var, varB, varI8, varI16, varI32, varI64,         varW8, varW16, varW32, varW64, varF, varD,-        -- * The next functions provide easier access to typed external variables.-        extB, extI8, extI16, extI32, extI64,-        extW8, extW16, extW32, extW64, extF, extD,-        -- * The next functions provide easier access to typed external arrays.-        extArrB, extArrI8, extArrI16, extArrI32, extArrI64,-        extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD,-        -- * Set of operators from which to choose during the generation of random streams-        opsF, opsF2, opsF3,+        -- * Copilot constant declarations.  For the most part, these are+        -- unnecessary, as constants are automatically lifted in into the *+        -- Copilot types.  They are useful though for specifying triggers and *+        -- function samplings.+        const, constI8, constI16, constI32, constI64,+        constW8, constW16, constW32, constW64, constF, constD,+        -- * Boolean stream constants+        true, false,+        module Language.Copilot.Language.Sampling,         -- * Constructs of the copilot language         drop, (++), (.=), -- (..|),          -- * The next functions help typing the send operations-        -- Warning: there is no typechecking of that yet-        -- sendB, sendI8, sendI16, sendI32, sendI64,-        send, port, -- , sendW16, sendW32, sendW64, sendF, sendD+        send, port,          -- * Triggers-        trigger, void, (<>), (<>>),+        module Language.Copilot.Language.FunctionCalls,+--        trigger, (<>), void,         -- * Safe casting-        cast,-        -- * Boolean stream constants-        const, true, false+        module Language.Copilot.Language.Casting,+        notConstVarErr     ) where  import qualified Language.Atom as A import Data.Int import Data.Word-import System.Random-import qualified Data.Map as M-import Prelude ( Bool(..), Num(..), Float, Double, (.), String, error, ($)-               , Fractional(..), fromInteger, zip, Show(..))+import Prelude ( Bool(..), Num(..), Float, Double, String, ($), error+               , Fractional(..), fromInteger, Show(..)) import qualified Prelude as P import Control.Monad.Writer (tell)+import qualified Data.Map as M  import Language.Copilot.Core-import Language.Copilot.Analyser-import Language.Copilot.Tests.Random+import Language.Copilot.Language.Sampling+import Language.Copilot.Language.Casting+import Language.Copilot.Language.FunctionCalls+--import Language.Copilot.Language.RandomOps  ---- Operators and functions --------------------------------------------------- @@ -99,95 +101,6 @@     (\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x)) (==>) = F2 (\ x y -> y P.|| P.not x) A.imply --- | Cast 'a' into 'b'.  We only allow "safe casts" to larger types.-class Streamable a => Castable a where-  castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b-  cast :: (Castable b, Streamable b) => Spec b -> Spec a--castErr :: String -> A.Type -> String-castErr toT fromT = "Error: cannot cast type " P.++ show fromT -                    P.++ " into " P.++ toT P.++ ".  Only casts guarnateed \n" -                    P.++ "not to change sign and to larger types are allowed."--instance Castable Bool where-  castFrom = F (\b -> if b then 1 else 0)-               (\b -> A.mux b 1 0)-  cast x =  error $ castErr "Bool" (getAtomType x)--instance Castable Word8 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    t        -> error $ castErr "Word8" t--instance Castable Word16 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    A.Word8  -> castFrom x-    t        -> error $ castErr "Word16" t--instance Castable Word32 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    A.Word8  -> castFrom x-    A.Word16 -> castFrom x-    t        -> error $ castErr "Word32" t--instance Castable Word64 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =   case getAtomType x of-    A.Bool   -> castFrom x-    A.Word8  -> castFrom x-    A.Word16 -> castFrom x-    A.Word32 -> castFrom x-    t        -> error $ castErr "Word64" t--instance Castable Int8 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    t        -> error $ castErr "Int8" t--instance Castable Int16 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x = case getAtomType x of-    A.Bool   -> castFrom x-    A.Int8   -> castFrom x-    A.Word8  -> castFrom x-    t        -> error $ castErr "Int16" t--instance Castable Int32 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    A.Int8  -> castFrom x-    A.Int16 -> castFrom x-    A.Word8  -> castFrom x-    A.Word16  -> castFrom x-    t        -> error $ castErr "Int32" t--instance Castable Int64 where-  castFrom = F (P.fromInteger . P.toInteger) -               (A.Retype . A.ue)-  cast x =  case getAtomType x of-    A.Bool   -> castFrom x-    A.Int8  -> castFrom x-    A.Int16 -> castFrom x-    A.Int32 -> castFrom x-    A.Word8  -> castFrom x-    A.Word16  -> castFrom x-    A.Word32  -> castFrom x-    t        -> error $ castErr "Int64" t- -- | Beware : both sides are executed, even if the result of one is later discarded mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a mux = F3 (\ b x y -> if b then x else y) A.mux@@ -196,244 +109,6 @@ infixr 4 ||, &&, ^, ==>  --- Used for easily producing, and coercing PVars---- for variables-extB :: Var -> Phase -> Spec Bool-extB = PVar A.Bool-extI8 :: Var -> Phase -> Spec Int8-extI8 = PVar A.Int8-extI16 :: Var -> Phase -> Spec Int16-extI16 = PVar A.Int16-extI32 :: Var -> Phase -> Spec Int32-extI32 = PVar A.Int32-extI64 :: Var -> Phase -> Spec Int64-extI64 = PVar A.Int64-extW8 :: Var -> Phase -> Spec Word8-extW8 = PVar A.Word8-extW16 :: Var -> Phase -> Spec Word16-extW16 = PVar A.Word16-extW32 :: Var -> Phase -> Spec Word32-extW32 = PVar A.Word32-extW64 :: Var -> Phase -> Spec Word64-extW64 = PVar A.Word64-extF :: Var -> Phase -> Spec Float-extF = PVar A.Float-extD :: Var -> Phase -> Spec Double-extD = PVar A.Double---- for arrays -extArrB ::  (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Bool-extArrB = \v idx ph -> PArr A.Bool (v, idx) ph-extArrI8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int8-extArrI8 = \v idx ph -> PArr A.Int8 (v, idx) ph-extArrI16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int16-extArrI16 = \v idx ph -> PArr A.Int16 (v, idx) ph-extArrI32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int32-extArrI32 = \v idx ph -> PArr A.Int32 (v, idx) ph-extArrI64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int64-extArrI64 = \v idx ph -> PArr A.Int64 (v, idx) ph-extArrW8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word8-extArrW8 = \v idx ph -> PArr A.Word8 (v, idx) ph-extArrW16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word16-extArrW16 = \v idx ph -> PArr A.Word16 (v, idx) ph-extArrW32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word32-extArrW32 = \v idx ph -> PArr A.Word32 (v, idx) ph-extArrW64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word64-extArrW64 = \v idx ph -> PArr A.Word64 (v, idx) ph-extArrF :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Float-extArrF = \v idx ph -> PArr A.Float (v, idx) ph-extArrD :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Double-extArrD = \v idx ph -> PArr A.Double (v, idx) ph------- Sets of operators for Tests.Random.hs ------------------------------------------- Helper functions--mkOp :: (Random arg1, Streamable arg1) =>-    (Spec arg1 -> Spec r) -> Operator r-mkOp op =-    Operator (\ rand g ->-            let (s0, g0) = rand g FunSpecSet in-            (op s0, g0)-        )--mkOp2 :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>-    (Spec arg1 -> Spec arg2 -> Spec r) -> Operator r-mkOp2 op =-    Operator (\ rand g ->-            let (s0, g0) = rand g FunSpecSet -                (s1, g1) = rand g0 FunSpecSet in-            (op s0 s1, g1)-        )-        -mkOp3 :: (Random arg1, Random arg2, Random arg3, -    Streamable arg1, Streamable arg2, Streamable arg3) =>-    (Spec arg1 -> Spec arg2 -> Spec arg3 -> Spec r) -> Operator r-mkOp3 op =-    Operator (\ rand g ->-            let (s0, g0) = rand g FunSpecSet-                (s1, g1) = rand g0 FunSpecSet-                (s2, g2) = rand g1 FunSpecSet in-            (op s0 s1 s2, g2)-        )--mkOp2Coerce :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>-    (Spec arg1 -> Spec arg2 -> Spec r) -> arg1 -> arg2 -> Operator r-mkOp2Coerce op c0 c1 =-    Operator (\ rand g ->-            let (s0, g0) = rand g FunSpecSet-                (s1, g1) = rand g0 FunSpecSet in-            (op (s0 `P.asTypeOf` (Const c0)) (s1 `P.asTypeOf` (Const c1)), g1)-        )--mkOp2Ord :: forall r. (forall arg. -    (Random arg, A.OrdE arg, Streamable arg) =>-    (Spec arg -> Spec arg -> Spec r)) -    -> Operator r-mkOp2Ord op =-    let opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: -            RandomGen g => -            (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)-        opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8)-        opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16)-        opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32)-        opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64)-        opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8)-        opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16)-        opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32)-        opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64)-        opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float)-        opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in-    Operator (\ rand g ->-            let (t, g0) = randomR (A.Int8, A.Double) g in-            case t of-                A.Int8 -> opI8 rand g0-                A.Int16 -> opI16 rand g0-                A.Int32 -> opI32 rand g0-                A.Int64 -> opI64 rand g0-                A.Word8 -> opW8 rand g0-                A.Word16 -> opW16 rand g0-                A.Word32 -> opW32 rand g0-                A.Word64 -> opW64 rand g0-                A.Float -> opF rand g0-                A.Double -> opD rand g0-                _ -> P.error "Impossible"-        )--mkOp2Eq :: forall r. (forall arg. -    (Random arg, A.EqE arg, Streamable arg) =>-    (Spec arg -> Spec arg -> Spec r)) -    -> Operator r-mkOp2Eq op =-    let opB, opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: -            RandomGen g => -            (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)-        opB = fromOp P.$ mkOp2Coerce op (unit::Bool) (unit::Bool)-        opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8)-        opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16)-        opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32)-        opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64)-        opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8)-        opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16)-        opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32)-        opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64)-        opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float)-        opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in-    Operator (\ rand g ->-            let (t, g0) = random g in-            case t of-                A.Bool -> opB rand g0-                A.Int8 -> opI8 rand g0-                A.Int16 -> opI16 rand g0-                A.Int32 -> opI32 rand g0-                A.Int64 -> opI64 rand g0-                A.Word8 -> opW8 rand g0-                A.Word16 -> opW16 rand g0-                A.Word32 -> opW32 rand g0-                A.Word64 -> opW64 rand g0-                A.Float -> opF rand g0-                A.Double -> opD rand g0-        )------ Definition of each operator--not_ :: Operator Bool-not_ = mkOp not    -    -(+$), (-$), (*$) :: (Streamable a, A.NumE a, Random a) => Operator a-(+$) = mkOp2 (P.+)-(-$) = mkOp2 (P.-)-(*$) = mkOp2 (P.*)--(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a-(/$) = mkOp2 (P./)--(<$), (<=$), (>=$), (>$) :: Operator Bool-(<$) = mkOp2Ord (<)-(<=$) = mkOp2Ord (<=)-(>=$) = mkOp2Ord (>=)-(>$) = mkOp2Ord (>)--(==$), (/=$) :: Operator Bool-(==$) = mkOp2Eq (==)-(/=$) = mkOp2Eq (/=)--(||$), (&&$), (^$), (==>$) :: Operator Bool-(||$) = mkOp2 (||)-(&&$) = mkOp2 (&&)-(^$) = mkOp2 (^)-(==>$) = mkOp2 (==>)--mux_ :: (Streamable a, Random a) => Operator a-mux_ = mkOp3 mux---- Packing of the operators in StreamableMaps--createMapFromElems :: [val] -> M.Map Var val-createMapFromElems vals =-    let ks = [[x] | x <- ['a'..]]-        l = zip ks vals in-    M.fromAscList l---- | opsF, opsF2 and opsF3 are feeded to Tests.Random.randomStreams.--- They allows the random generated streams to include lots of operators.--- If you add a new operator to Copilot, it would be nice to add it to one of those,--- that way it could be used in the random streams used for testing.--- opsF holds all the operators of arity 1, opsF2 of arity 2 and opsF3 of arity3--- They are StreamableMaps, because operators are sorted based on their return type.-opsF, opsF2, opsF3 :: Operators-opsF = emptySM {bMap = createMapFromElems [not_]}--opsF2 = emptySM {-        bMap = createMapFromElems [(<$), (<=$), (>=$), (>$), (==$), (/=$), (||$), (&&$), (^$), (==>$)],-        i8Map = createMapFromElems [(+$), (-$), (*$)],-        i16Map = createMapFromElems [(+$), (-$), (*$)],-        i32Map = createMapFromElems [(+$), (-$), (*$)],-        i64Map = createMapFromElems [(+$), (-$), (*$)],-        w8Map = createMapFromElems [(+$), (-$), (*$)],-        w16Map = createMapFromElems [(+$), (-$), (*$)],-        w32Map = createMapFromElems [(+$), (-$), (*$)],-        w64Map = createMapFromElems [(+$), (-$), (*$)],-        fMap = createMapFromElems [(+$), (-$), (*$), (/$)],-        dMap = createMapFromElems [(+$), (-$), (*$), (/$)]-    }--opsF3 = emptySM {-        bMap = createMapFromElems [mux_],-        i8Map = createMapFromElems [mux_],-        i16Map = createMapFromElems [mux_],-        i32Map = createMapFromElems [mux_],-        i64Map = createMapFromElems [mux_],-        w8Map = createMapFromElems [mux_],-        w16Map = createMapFromElems [mux_],-        w32Map = createMapFromElems [mux_],-        w64Map = createMapFromElems [mux_],-        fMap = createMapFromElems [mux_],-        dMap = createMapFromElems [mux_]-    }- ---- Constructs of the language ------------------------------------------------  @@ -470,57 +145,56 @@ -- | Define a stream variable. (.=) :: Streamable a => Spec a -> Spec a -> Streams v .= s = -  notVarErr v (\var -> tell $ LangElems -                               (updateSubMap (M.insert var s) emptySM) -                               emptySM -                               M.empty)+  case v of+    (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM) +                                    emptySM +                                    M.empty+    _ -> error $ "Given spec " P.++ show v +                   P.++ " but expected a variable in a Copilot definition (.=)."  port :: Int -> Port port = Port --- | Takes a function @name@, a port @number@, a Copilot variable @v@, and a--- phase @ph@, and constructs a call to the C function @name(x,y)@ where @x@ is--- the value of the Copilot stream @v@ and @y@ is the port number.  The sending--- of the value on the port occurs at phase @ph@.-send :: Streamable a => String -> Port -> Spec a -> Phase -> Streams-send portName port s ph = +-- | Takes a function @name@, a port @number@, and a Copilot variable @v@ and+-- constructs a call to the C function @name(x,y)@ where @x@ is the value of the+-- Copilot stream @v@ and @y@ is the port number.+send :: Streamable a => String -> Port -> Spec a -> Streams+send portName thePort s =    tell $ LangElems             emptySM             (updateSubMap (M.insert (show sending) sending) emptySM)             M.empty-  where sending = Send s ph port portName--type TriggerLst = ([Var], StreamableMaps Spec)---- | No C arguments -void :: TriggerLst-void = ([],emptySM)---- | Turn a @Spec Var@ into an arguement for a C function.-(<>) :: Streamable a => Spec a -> TriggerLst -> TriggerLst-s <> (vars,sm) = notVarErr s (\v -> (v:vars, updateSubMap (\m -> M.insert v s m) sm))---- | Turn a @Spec Var@ into an arguement for a C function.-(<>>) :: (Streamable a, Streamable b) => Spec a -> Spec b -      -> TriggerLst-s <>> s' = (update s (update s' void))-  where update x (vars,sm) = -          notVarErr x (\v -> (v:vars,updateSubMap (\m -> M.insert v x m) sm))---- | Takes a Boolean stream, -trigger :: Spec Bool -> String -> TriggerLst -> Streams-trigger var fnName args =-  tell $ LangElems -           emptySM -           emptySM ---           (updateSubMap (M.insert (show trigger) trigger) emptySM) -           (M.insert (show trigger) trigger M.empty)-  where trigger = Trigger var fnName args+  where sending = case s of +                    v@(Var _) -> Send v thePort portName+                    _ -> error $ "Expected a Copilot variable but given " +                           P.++ show s P.++ " instead."  -- | Coerces a type that is 'Streamable' into a Copilot constant. const :: Streamable a => a -> Spec a const = Const +constI8 :: Int8 -> Spec Int8+constI8 = Const+constI16 :: Int16 -> Spec Int16+constI16 = Const+constI32 :: Int32 -> Spec Int32+constI32 = Const+constI64 :: Int64 -> Spec Int64+constI64 = Const+constW8 :: Word8 -> Spec Word8+constW8 = Const +constW16 :: Word16 -> Spec Word16+constW16 = Const+constW32 :: Word32 -> Spec Word32+constW32 = Const+constW64 :: Word64 -> Spec Word64+constW64 = Const+constF :: Float -> Spec Float+constF = Const+constD :: Double -> Spec Double+constD = Const++ true, false :: Spec Bool true = Const True false = Const False@@ -536,7 +210,6 @@  infixr 3 ++ infixr 2 .=-infixr 1 <>  ---- Optimisation rules -------------------------------------------------------- @@ -568,5 +241,4 @@ "Copilot.Language ImpliesDef" forall s0 s1. (||) s1 (not s0) = s0 ==> s1       #-} --- "Copilot.Language CastLift" forall s i. drop i (cast s) = cast (drop i s)-+-- "Copilot.Core CastLift" forall s i. drop i (cast s) = cast (drop i s)

@@ -0,0 +1,99 @@+-- | Safe casting of values.++module Language.Copilot.Language.Casting ( cast ) where++import qualified Language.Atom as A++import Data.Int+import Data.Word++import Language.Copilot.Core++-- | Cast 'a' into 'b'.  We only allow "safe casts" to larger types.+class Streamable a => Castable a where+  castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b+  cast :: (Castable b, Streamable b) => Spec b -> Spec a++castErr :: String -> A.Type -> String+castErr toT fromT = "Error: cannot cast type " ++ show fromT +                    ++ " into " ++ toT ++ ".  Only casts guarnateed \n" +                    ++ "not to change sign and to larger types are allowed."++instance Castable Bool where+  castFrom = F (\b -> if b then 1 else 0)+               (\b -> A.mux b 1 0)+  cast x =  error $ castErr "Bool" (getAtomType x)++instance Castable Word8 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    t        -> error $ castErr "Word8" t++instance Castable Word16 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    t        -> error $ castErr "Word16" t++instance Castable Word32 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    A.Word16 -> castFrom x+    t        -> error $ castErr "Word32" t++instance Castable Word64 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =   case getAtomType x of+    A.Bool   -> castFrom x+    A.Word8  -> castFrom x+    A.Word16 -> castFrom x+    A.Word32 -> castFrom x+    t        -> error $ castErr "Word64" t++instance Castable Int8 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    t        -> error $ castErr "Int8" t++instance Castable Int16 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x = case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8   -> castFrom x+    A.Word8  -> castFrom x+    t        -> error $ castErr "Int16" t++instance Castable Int32 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8  -> castFrom x+    A.Int16 -> castFrom x+    A.Word8  -> castFrom x+    A.Word16  -> castFrom x+    t        -> error $ castErr "Int32" t++instance Castable Int64 where+  castFrom = F (fromInteger . toInteger) +               (A.Retype . A.ue)+  cast x =  case getAtomType x of+    A.Bool   -> castFrom x+    A.Int8  -> castFrom x+    A.Int16 -> castFrom x+    A.Int32 -> castFrom x+    A.Word8  -> castFrom x+    A.Word16  -> castFrom x+    A.Word32  -> castFrom x+    t        -> error $ castErr "Int64" t

@@ -0,0 +1,47 @@+{-# LANGUAGE TypeSynonymInstances #-}++module Language.Copilot.Language.FunctionCalls +  ((<>), trigger, void, fun) where++import Language.Copilot.Core++import Control.Monad.Writer (tell)+import qualified Data.Map as M++-- | No C arguments +void :: Args+void = []++class ArgCl a where +  (<>) :: Streamable b => Spec b -> a -> Args+  trigger :: Spec Bool -> String -> a -> Streams+  fun :: String -> a -> Ext++instance ArgCl Args where +  s <> args = argUpdate s args+  trigger v fnName args = trigger' v fnName args+  fun = Fun++instance Streamable b => ArgCl (Spec b) where +  s <> s' = (argUpdate s (argUpdate s' []))+  trigger v fnName arg = +    let arg' = argUpdate arg [] in+    trigger' v fnName arg'+  fun f arg = +    let arg' = argUpdate arg [] in+    Fun f arg'++infixr 1 <>++-- | XXX document+trigger' :: Spec Bool -> String -> Args -> Streams+trigger' v fnName args =+  tell $ LangElems +           emptySM +           emptySM +           (M.insert (show trig) trig M.empty)+  where trig = Trigger v fnName args++argUpdate :: Streamable a => Spec a -> Args -> Args+argUpdate s args = notConstVarErr s (\v -> v:args)+

@@ -0,0 +1,206 @@+{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}++-- | Sets of operators for Tests.Random.hs++module Language.Copilot.Language.RandomOps (+--  mkOp, mkOp2, mkOp3, mkOp2Coerce, mkOp2Ord, mkOp2Eq,+  opsF, opsF2, opsF3,+  module Language.Copilot.Tests.Random+                                           ) where  ++import qualified Language.Atom as A++import Prelude (($), Float, Double, error, zip, asTypeOf)+import Data.Int+import Data.Word+import System.Random+import Data.Map as M++import Language.Copilot.Core+import Language.Copilot.Language+import Language.Copilot.Analyser+import Language.Copilot.Tests.Random++mkOp :: (Random arg1, Streamable arg1) =>+    (Spec arg1 -> Spec r) -> Operator r+mkOp op =+    Operator (\ rand g ->+            let (s0, g0) = rand g FunSpecSet in+            (op s0, g0)+        )++mkOp2 :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>+    (Spec arg1 -> Spec arg2 -> Spec r) -> Operator r+mkOp2 op =+    Operator (\ rand g ->+            let (s0, g0) = rand g FunSpecSet +                (s1, g1) = rand g0 FunSpecSet in+            (op s0 s1, g1)+        )+        +mkOp3 :: (Random arg1, Random arg2, Random arg3, +    Streamable arg1, Streamable arg2, Streamable arg3) =>+    (Spec arg1 -> Spec arg2 -> Spec arg3 -> Spec r) -> Operator r+mkOp3 op =+    Operator (\ rand g ->+            let (s0, g0) = rand g FunSpecSet+                (s1, g1) = rand g0 FunSpecSet+                (s2, g2) = rand g1 FunSpecSet in+            (op s0 s1 s2, g2)+        )++mkOp2Coerce :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>+    (Spec arg1 -> Spec arg2 -> Spec r) -> arg1 -> arg2 -> Operator r+mkOp2Coerce op c0 c1 =+    Operator (\ rand g ->+            let (s0, g0) = rand g FunSpecSet+                (s1, g1) = rand g0 FunSpecSet in+            (op (s0 `asTypeOf` (Const c0)) (s1 `asTypeOf` (Const c1)), g1)+        )++mkOp2Ord :: forall r. +              (forall arg. (Random arg, A.OrdE arg, Streamable arg) +              => (Spec arg -> Spec arg -> Spec r)) -> Operator r+mkOp2Ord op =+    let opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: +            RandomGen g +            => (forall a' g'. (Streamable a', Random a', RandomGen g') +               => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)+        opI8 = fromOp $ mkOp2Coerce op (unit::Int8) (unit::Int8)+        opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16)+        opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32)+        opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64)+        opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8)+        opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16)+        opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32)+        opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64)+        opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float)+        opD = fromOp $ mkOp2Coerce op (unit::Double) (unit::Double) in+    Operator (\ rand g ->+            let (t, g0) = randomR (A.Int8, A.Double) g in+            case t of+                A.Int8 -> opI8 rand g0+                A.Int16 -> opI16 rand g0+                A.Int32 -> opI32 rand g0+                A.Int64 -> opI64 rand g0+                A.Word8 -> opW8 rand g0+                A.Word16 -> opW16 rand g0+                A.Word32 -> opW32 rand g0+                A.Word64 -> opW64 rand g0+                A.Float -> opF rand g0+                A.Double -> opD rand g0+                _ -> error "Impossible"+        )++mkOp2Eq :: forall r. (forall arg. +    (Random arg, A.EqE arg, Streamable arg) =>+    (Spec arg -> Spec arg -> Spec r)) +    -> Operator r+mkOp2Eq op =+    let opB, opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: +            RandomGen g => +              (forall a' g'. (Streamable a', Random a', RandomGen g') => +                g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)+        opB = fromOp $ mkOp2Coerce op (unit::Bool) (unit::Bool)+        opI8 = fromOp $ mkOp2Coerce op (unit::Int8) (unit::Int8)+        opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16)+        opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32)+        opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64)+        opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8)+        opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16)+        opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32)+        opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64)+        opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float)+        opD = fromOp $ mkOp2Coerce op (unit::Double) (unit::Double) in+    Operator (\ rand g ->+            let (t, g0) = random g in+            case t of+                A.Bool -> opB rand g0+                A.Int8 -> opI8 rand g0+                A.Int16 -> opI16 rand g0+                A.Int32 -> opI32 rand g0+                A.Int64 -> opI64 rand g0+                A.Word8 -> opW8 rand g0+                A.Word16 -> opW16 rand g0+                A.Word32 -> opW32 rand g0+                A.Word64 -> opW64 rand g0+                A.Float -> opF rand g0+                A.Double -> opD rand g0+        )++---- Definition of each operator++not_ :: Operator Bool+not_ = mkOp not    +    +(+$), (-$), (*$) :: (Streamable a, A.NumE a, Random a) => Operator a+(+$) = mkOp2 (+)+(-$) = mkOp2 (-)+(*$) = mkOp2 (*)++(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a+(/$) = mkOp2 (/)++(<$), (<=$), (>=$), (>$) :: Operator Bool+(<$) = mkOp2Ord (<)+(<=$) = mkOp2Ord (<=)+(>=$) = mkOp2Ord (>=)+(>$) = mkOp2Ord (>)++(==$), (/=$) :: Operator Bool+(==$) = mkOp2Eq (==)+(/=$) = mkOp2Eq (/=)++(||$), (&&$), (^$), (==>$) :: Operator Bool+(||$) = mkOp2 (||)+(&&$) = mkOp2 (&&)+(^$) = mkOp2 (^)+(==>$) = mkOp2 (==>)++mux_ :: (Streamable a, Random a) => Operator a+mux_ = mkOp3 mux++-- Packing of the operators in StreamableMaps++createMapFromElems :: [val] -> M.Map Var val+createMapFromElems vals =+    let ks = [[x] | x <- ['a'..]]+        l = zip ks vals in+    M.fromAscList l++-- | opsF, opsF2 and opsF3 are fed to Tests.Random.randomStreams.  They allows+-- the random generated streams to include lots of operators.  If you add a new+-- operator to Copilot, it would be nice to add it to one of those, that way it+-- could be used in the random streams used for testing.  opsF holds all the+-- operators of arity 1, opsF2 of arity 2 and opsF3 of arity3 They are+-- StreamableMaps, because operators are sorted based on their return type.+opsF, opsF2, opsF3 :: Operators+opsF = emptySM {bMap = createMapFromElems [not_]}++opsF2 = emptySM {+        bMap = createMapFromElems [(<$), (<=$), (>=$), (>$), (==$), (/=$), (||$), (&&$), (^$), (==>$)],+        i8Map = createMapFromElems [(+$), (-$), (*$)],+        i16Map = createMapFromElems [(+$), (-$), (*$)],+        i32Map = createMapFromElems [(+$), (-$), (*$)],+        i64Map = createMapFromElems [(+$), (-$), (*$)],+        w8Map = createMapFromElems [(+$), (-$), (*$)],+        w16Map = createMapFromElems [(+$), (-$), (*$)],+        w32Map = createMapFromElems [(+$), (-$), (*$)],+        w64Map = createMapFromElems [(+$), (-$), (*$)],+        fMap = createMapFromElems [(+$), (-$), (*$), (/$)],+        dMap = createMapFromElems [(+$), (-$), (*$), (/$)]+    }++opsF3 = emptySM {+        bMap = createMapFromElems [mux_],+        i8Map = createMapFromElems [mux_],+        i16Map = createMapFromElems [mux_],+        i32Map = createMapFromElems [mux_],+        i64Map = createMapFromElems [mux_],+        w8Map = createMapFromElems [mux_],+        w16Map = createMapFromElems [mux_],+        w32Map = createMapFromElems [mux_],+        w64Map = createMapFromElems [mux_],+        fMap = createMapFromElems [mux_],+        dMap = createMapFromElems [mux_]+    }

@@ -0,0 +1,99 @@+{-# LANGUAGE TypeSynonymInstances #-}++-- | Functions for sampling external variables.++module Language.Copilot.Language.Sampling (+        -- * The next functions provide easier access to typed external variables.+        extB, extI8, extI16, extI32, extI64,+        extW8, extW16, extW32, extW64, extF, extD,+        -- * The next functions provide easier access to typed external arrays.+        extArrB, extArrI8, extArrI16, extArrI32, extArrI64,+        extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD,+                                          ) where+++import qualified Language.Atom as A+import Data.Int+import Data.Word++import Language.Copilot.Core++class ExtCl a where +  extB :: a -> Spec Bool+  extI8 :: a -> Spec Int8+  extI16 :: a -> Spec Int16+  extI32 :: a -> Spec Int32+  extI64 :: a -> Spec Int64+  extW8 :: a -> Spec Word8+  extW16 :: a -> Spec Word16+  extW32 :: a -> Spec Word32+  extW64 :: a -> Spec Word64+  extF :: a -> Spec Float+  extD :: a -> Spec Double++  -- for arrays +  extArrB ::  (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Bool+  extArrI8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int8+  extArrI16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int16+  extArrI32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int32+  extArrI64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int64+  extArrW8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word8+  extArrW16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word16+  extArrW32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word32+  extArrW64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word64+  extArrF :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Float+  extArrD :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Double++-- | For global variables.+instance ExtCl String where+  extB var = PVar A.Bool (ExtV var)+  extI8 var = PVar A.Int8 (ExtV var)+  extI16 var = PVar A.Int16 (ExtV var)+  extI32 var = PVar A.Int32 (ExtV var)+  extI64 var = PVar A.Int64 (ExtV var)+  extW8 var = PVar A.Word8 (ExtV var)+  extW16 var = PVar A.Word16 (ExtV var)+  extW32 var = PVar A.Word32 (ExtV var)+  extW64 var = PVar A.Word64 (ExtV var)+  extF var = PVar A.Float (ExtV var)+  extD var = PVar A.Double (ExtV var)++  -- for arrays +  extArrB = \v idx -> PArr A.Bool (ExtV v, idx)+  extArrI8 = \v idx -> PArr A.Int8 (ExtV v, idx)+  extArrI16 = \v idx -> PArr A.Int16 (ExtV v, idx)+  extArrI32 = \v idx -> PArr A.Int32 (ExtV v, idx)+  extArrI64 = \v idx -> PArr A.Int64 (ExtV v, idx)+  extArrW8 = \v idx -> PArr A.Word8 (ExtV v, idx)+  extArrW16 = \v idx -> PArr A.Word16 (ExtV v, idx)+  extArrW32 = \v idx -> PArr A.Word32 (ExtV v, idx)+  extArrW64 = \v idx -> PArr A.Word64 (ExtV v, idx)+  extArrF = \v idx -> PArr A.Float (ExtV v, idx)+  extArrD = \v idx -> PArr A.Double (ExtV v, idx)++-- | For functions.+instance ExtCl Ext where+  extB = PVar A.Bool +  extI8 = PVar A.Int8 +  extI16 = PVar A.Int16 +  extI32 = PVar A.Int32 +  extI64 = PVar A.Int64 +  extW8 = PVar A.Word8 +  extW16 = PVar A.Word16+  extW32 = PVar A.Word32+  extW64 = PVar A.Word64+  extF = PVar A.Float+  extD = PVar A.Double+  -- for arrays +  extArrB = \fn idx -> PArr A.Bool (fn, idx)+  extArrI8 = \fn idx -> PArr A.Int8 (fn, idx)+  extArrI16 = \fn idx -> PArr A.Int16 (fn, idx)+  extArrI32 = \fn idx -> PArr A.Int32 (fn, idx)+  extArrI64 = \fn idx -> PArr A.Int64 (fn, idx)+  extArrW8 = \fn idx -> PArr A.Word8 (fn, idx)+  extArrW16 = \fn idx -> PArr A.Word16 (fn, idx)+  extArrW32 = \fn idx -> PArr A.Word32 (fn, idx)+  extArrW64 = \fn idx -> PArr A.Word64 (fn, idx)+  extArrF = \fn idx -> PArr A.Float (fn, idx)+  extArrD = \fn idx -> PArr A.Double (fn, idx)+

@@ -3,7 +3,8 @@  -- | Generate random specs for testing.  We do not generate external array indexes. -module Language.Copilot.Tests.Random (randomStreams, Operator(..), Operators, fromOp) where+module Language.Copilot.Tests.Random +  (randomStreams, Operator(..), Operators, fromOp) where  import Language.Copilot.Core  import Language.Copilot.Analyser@@ -19,9 +20,9 @@  ---- Parameters of the random generation --------------------------------------- -maxDrop, maxSamplePhase :: Int+maxDrop :: Int maxDrop = 4 -- The maximum value for i in Drop i _-maxSamplePhase = 8 -- The maximum value for ph in PVar _ _ ph+-- maxSamplePhase = 8 -- The maximum value for ph in PVar _ _ ph  -- These determines the number of streams and of monitored variables. -- Bools are drawn each time with the following weights, until a False is drawn@@ -233,8 +234,9 @@     let (spec::(Spec a), g') = randomSpec vs exts opsF opsF2 opsF3 g AllSpecSet in     (updateSubMap (\m -> M.insert v spec m) streams, g') -randomSpec :: forall a g. (Streamable a, RandomGen g, Random a) => -    Variables -> Variables -> Operators -> Operators -> Operators -> g -> SpecSet -> (Spec a, g)+randomSpec :: forall a g. (Streamable a, RandomGen g, Random a) +           => Variables -> Variables -> Operators -> Operators +              -> Operators -> g -> SpecSet -> (Spec a, g) randomSpec vs exts opsF opsF2 opsF3 g set =     let weights = case set of             AllSpecSet  -> weightsAllSpecSet@@ -246,8 +248,8 @@             0 -> -- PVar                 case getVar g0 exts of                     (Just v, g1) -> -                        let (ph, g2) = randomR (1, maxSamplePhase)  g1 in-                        (PVar (atomType (unit::a)) v ph, g2)+--                        let (ph, g2) = randomR (1, maxSamplePhase)  g1 in+                        (PVar (atomType (unit::a)) (ExtV v), g1)                     (Nothing, g1) -> randomSpec' g1 set             1 -> -- Var                 case getVar g0 vs of

@@ -43,6 +43,17 @@ ******************************************************************************* Release notes *******************************************************************************++* Copilot-1.0+  * Language frozen. +  * Added sampling functions and returning arrays.++* Copilot-0.29++  * Refactor Language.hs into submodules.+  * Removed the notion of phases from sampling.  That is a compiler-level+    concern.+   * Copilot-0.28      * Make triggers part of the Copilot language (see example t5 in Examples.hs).

@@ -1,5 +1,5 @@ name:                copilot-version:             0.28+version:             1.0 cabal-version:       >= 1.2 license:             BSD3 license-file:        LICENSE@@ -32,7 +32,7 @@ extra-source-files:  README  library-    ghc-options:     -Wall+    ghc-options:     -Wall      -- These build depends represent my current system.  This will probably     -- build on packages outside these constaints.     build-depends:     @@ -50,6 +50,10 @@                      Language.Copilot.AdHocC                      Language.Copilot.Core                      Language.Copilot.Language+                     Language.Copilot.Language.Sampling+                     Language.Copilot.Language.FunctionCalls+                     Language.Copilot.Language.RandomOps+                     Language.Copilot.Language.Casting                      Language.Copilot.AtomToC                      Language.Copilot.Compiler                      Language.Copilot.Interpreter