copilot 0.22 → 0.23

raw patch · 23 files changed

+816/−431 lines, 23 filesdep ~atomsetup-changedPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: atom

API changes (from Hackage documentation)

Files

• Language/Copilot.hs +3/−1
• Language/Copilot/AdHocC.hs +34/−7
• Language/Copilot/Analyser.hs +153/−74
• Language/Copilot/AtomToC.hs +38/−18
• Language/Copilot/Compiler.hs +154/−69
• Language/Copilot/Core.hs +149/−81
• Language/Copilot/Dispatch.hs +71/−48
• Language/Copilot/Examples/Examples.hs +29/−8
• Language/Copilot/Examples/LTLExamples.hs +11/−14
• Language/Copilot/Examples/PTLTLExamples.hs +1/−5
• Language/Copilot/Help.hs +19/−6
• Language/Copilot/Interface.hs +34/−29
• Language/Copilot/Interpreter.hs +16/−19
• Language/Copilot/Language.hs +48/−25
• Language/Copilot/Libs/ErrorChks.hs +1/−1
• Language/Copilot/Libs/Indexes.hs +1/−1
• Language/Copilot/Libs/LTL.hs +1/−2
• Language/Copilot/Libs/PTLTL.hs +3/−4
• Language/Copilot/Tests/Random.hs +20/−10
• README +17/−2
• Setup.hs +0/−2
• Setup.lhs +8/−0
• copilot.cabal +5/−5

@@ -12,6 +12,7 @@   , module Language.Copilot.Libs.Indexes   , module Language.Copilot.Libs.LTL   , module Language.Copilot.Libs.PTLTL+  -- , module Language.Copilot.AdHocC   -- , module Language.Copilot.Examples.Examples   -- , module Language.Copilot.Examples.LTLExamples   -- , module Language.Copilot.Examples.PTLTLExamples@@ -23,7 +24,7 @@ import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler-import Language.Copilot.Language (opsF, opsF2, opsF3)+import Language.Copilot.Language -- (opsF, opsF2, opsF3) import Language.Copilot.PrettyPrinter() import Language.Copilot.Tests.Random import Language.Copilot.Dispatch@@ -31,6 +32,7 @@ import Language.Copilot.Libs.Indexes import Language.Copilot.Libs.LTL import Language.Copilot.Libs.PTLTL+-- import Language.Copilot.AdHocC -- import Language.Copilot.Examples.Examples -- import Language.Copilot.Examples.LTLExamples -- import Language.Copilot.Examples.PTLTLExamples

@@ -1,10 +1,9 @@--- TODO-Robin : Improve a lot that -> new package in Hackage ? -- generate C-Code with combinators, high-level, safe haskell.  -- | Helper functions for writing free-form C code. module Language.Copilot.AdHocC (-        varDecl, includeBracket, includeQuote,-        printf, printfNewline+         varDecl, arrDecl, varInit, arrayInit, funcDecl+       , includeBracket, includeQuote, printf, printfNewline     ) where  import Data.List (intersperse) @@ -14,12 +13,39 @@ -- | Takes a type and a list of variable names and declares them. varDecl :: Type -> [String] -> String varDecl t vars = -    cType' t ++ " " ++ (unwords (intersperse "," vars)) ++ ";"-    where-        cType' Bool = "int"-        cType' typ = cType typ+    cType t ++ " " ++ unwords (intersperse "," vars) ++ ";" +-- | Takes a type and a list of array names and their sizes declares them.+arrDecl :: Type -> [(String,Int)] -> String+arrDecl t arrs = +    cType t ++ " " ++ unwords (intersperse "," mkArrs) ++ ";"+  where mkArrs = map (\(a,size) -> a ++ "[" ++ show size ++ "]") arrs +-- | Takes a type and a variable and initializes it.  It is YOUR responsibility+-- to ensure that @val@ is of type @t@.+varInit :: Show a => Type -> String -> a -> String+varInit t var val = cType t ++ " " ++ var ++ " = " ++ show val ++ ";"++-- Show a list with braces {} rather than brackets [].+bracesListShow :: Show a => [a] -> String+bracesListShow ls =+  "{" ++ (foldl (++) "" $ intersperse "," $ map show ls) ++ "}"++-- | Takes a type and an array and initializes it.  It is YOUR responsibility to+-- ensure that @vals@ is of type @t@.+arrayInit :: Show a => Type -> String -> [a] -> String+arrayInit t var vals = +  cType t ++ " " ++ var ++ " = " ++ bracesListShow vals ++ ";"++-- | Declare function prototypes, given a return type, a function name, and a+-- | list of argument types.  Use 'Nothing' for a return type of @void@.+funcDecl :: Maybe Type -> String -> [Type] -> String+funcDecl t fn argTs = makeRet t ++ " " ++ fn ++ "(" ++ makeArgTs ++ ");"+  where makeRet Nothing = "void"+        makeRet (Just t') = cType t'+        makeArgTs | null argTs = "void"+                  | otherwise  = unwords (intersperse "," $ map cType argTs)+ -- | Add an include of a library includeBracket :: String -> String includeBracket lib = "#include <" ++ lib ++ ">"@@ -43,3 +69,4 @@ printf, printfNewline :: String -> [String] -> String printfNewline text vars = (printfPre text) ++ newline ++ (printfPost vars) printf text vars = (printfPre text) ++ (printfPost vars)+

@@ -1,17 +1,18 @@ {-# OPTIONS_GHC -XRelaxedPolyRec #-} --- | This module provides a way to check that a /Copilot/ specification is compilable+-- | This module provides a way to check that a /Copilot/ specification is+-- compilable module Language.Copilot.Analyser(         -- * Main error checking functions         check, Error(..), SpecSet(..),         -- * Varied other things-        getExternalVars, getAtomType+        getExternalVars, ExtVars(..)         {-         -- * Dependency Graphs (experimental)         Weight, Node(..), DependencyGraph,         mkDepGraph, showDG -}     ) where-    + import Language.Copilot.Core  import qualified Language.Atom as A@@ -21,45 +22,103 @@ type Weight = Int  -- | Used for representing an error in the specification, detected by @'check'@-data Error = +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-    | BadType Var Var -- ^ either a 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 negative weighted closed path in the specification, as described in the original research paper-    | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but would need bigger prophecyArrays-    | DependsOnFuture [Var] Var Weight-- ^ If an output depends of a future of an input it will be hard to compile to say the least+    | 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+                                 -- 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/+    | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile+                                                 -- /Copilot/ specification can+                                                 -- only work if there is no+                                                 -- negative weighted closed+                                                 -- path in the specification,+                                                 -- as described in the original+                                                 -- research paper+    | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but+                                                 -- would need bigger+                                                 -- prophecyArrays+    | DependsOnFuture [Var] Var Weight -- ^ If an output depends of a future of+                                       -- an input it will be hard to compile to+                                       -- say the least  instance Show Error where-    show (BadSyntax s v) = -        "Error syntax : " ++ s ++ "is not allowed in that position in stream " ++ v ++ "\n"-    show (BadDrop i v) = -        "Error : a Drop in stream " ++ v ++ "drops the number " ++ show i ++ -        "of elements. " ++ show i ++ " is negative, and Drop only accepts positive arguments. \n"-    show (BadSamplingPhase v v' ph) = -        "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 (BadSyntax s v) =+       unlines +        ["Error syntax : " ++ s ++ " is not allowed in that position in stream " +         ++ v ++ "."]+    show (BadDrop i v) =+       unlines+        [ "Error : a Drop in stream " ++ v ++ " drops the number " ++ show i +++          "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 (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 "+            ++ "form.\n"+        ]     show (BadType v v') =-        "Error : the monitor variable " ++ v ++ ", called in the stream " ++ v' ++-            " either does not exist, or don't have the right type (there is no implicit conversion)\n"+       unlines+        [ "Error : the monitor variable " ++ 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) =-        "Error : the following path is closed in the dependency graph of this "-            ++ "specification and have weight " ++ show w ++ " which is positive (append decrease the weight, "-            ++ "while drop increase it). This is forbidden to avoid streams which could "-            ++ "take 0 or several different values.  Try adding some initial elements (e.g., [0,0,0] ++ ...) "-            ++ "to the offending streams. \n"-            ++ "Path : " ++ show (reverse vs) ++ "\n"+       unlines +        [ "Error : the following path is closed in the dependency graph of the "+            ++ "specification and has" +        , "weight " ++ show w ++ " which is positive (append decreases the weight, "+          ++ "while drop increases it)."  +        , "This is forbidden to avoid streams which could take 0 or several different"+          ++ " values."+        , "Try adding some initial elements (e.g., [0,0,0] ++ ...) "+            ++ "to the offending streams."+        , "Path : " ++ show (reverse vs) ++ "\n"+        ]     show (DependsOnClosePast vs v w len) =-        "Error : the following path is of weight " ++ show w ++ " ending in "-            ++ "the external variable " ++ 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. \n"-            ++ "Path : " ++ show (reverse vs) ++ "\n" +       unlines+        [ "Error : the following path is of weight " ++ show w ++ " ending in "+          ++ "the external variable " ++ 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."+        , "Path : " ++ show (reverse vs) ++ "\n"+        ]     show (DependsOnFuture vs v w) =-        "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 ++ " which is quoted in the last variable of the path. This is obviously impossible. \n"-            ++ "Path : " ++ show (reverse vs) ++ "\n"+       unlines+        [ "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 +        , "which is quoted in the last variable of the path.  This is "+          ++ "obviously impossible."+        , "Path : " ++ show (reverse vs) ++ "\n"+        ]  (&&>) :: Maybe a -> Maybe a -> Maybe a m &&> m' =@@ -76,15 +135,16 @@ infixr 2 ||> infixr 1 &&> --- | Check a /Copilot/ specification. +-- | Check a /Copilot/ specification. -- If it is not compilable, then returns an error describing the issue. -- Else, returns @Nothing@ check :: StreamableMaps Spec -> Maybe Error-check streams = +check streams =     syntaxCheck streams &&> defCheck streams --- Represents all the kind of specs that are authorized after a given operator-data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet deriving Eq+-- Represents all the kind of specs that are authorized after a given operator.+data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet | PArrSet +             deriving Eq  -- Check that the AST of the copilot specification match the BNF -- Could have been verified by the type checker if the type of Spec had been cut@@ -94,33 +154,35 @@ syntaxCheck streams =     foldStreamableMaps (checkSyntaxSpec AllSpecSet) streams Nothing     where-        checkSyntaxSpec :: Streamable a => SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error+        checkSyntaxSpec :: Streamable a +                        => SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error         checkSyntaxSpec set v s e =             e &&>                 case s of-                    PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph                     Var _ -> Nothing                     Const _ -> Nothing-                    F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v &&>-                        (checkSyntaxSpec FunSpecSet v s0 Nothing)-                    F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v &&>-                        (checkSyntaxSpec FunSpecSet v s0 Nothing) &&>-                        checkSyntaxSpec FunSpecSet v s1 Nothing-                    F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v &&>-                        (checkSyntaxSpec FunSpecSet v s0 Nothing) &&> -                        (checkSyntaxSpec FunSpecSet v s1 Nothing) &&>-                        checkSyntaxSpec FunSpecSet v s2 Nothing -                    Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v &&> -                        checkSyntaxSpec AllSpecSet v s0 Nothing-                    Drop i s0 -> (0 <= i) ||> BadDrop i v &&> -                                 (checkSyntaxSpec DropSpecSet v s0 Nothing)+                    PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph+                    PArr _ (arr,s0) ph -> 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+                    F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v +                      &&> checkSyntaxSpec FunSpecSet v s0 Nothing+                      &&> checkSyntaxSpec FunSpecSet v s1 Nothing+                    F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v +                      &&> checkSyntaxSpec FunSpecSet v s0 Nothing+                      &&> checkSyntaxSpec FunSpecSet v s1 Nothing+                      &&> checkSyntaxSpec FunSpecSet v s2 Nothing+                    Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v +                      &&> checkSyntaxSpec AllSpecSet v s0 Nothing+                    Drop i s0 -> (0 <= i) ||> BadDrop i v +                      &&> checkSyntaxSpec DropSpecSet v s0 Nothing+        checkIndex _ _ (Var _)      = Nothing+        checkIndex _ _ (Const _)    = Nothing+        checkIndex v arr idx = Just $ BadPArrSpec v arr (show idx) --- checks that streams are well defined (ie can be compiled)--- Currently very inefficient (for simplicity's sake), --- could probably be optimized if need be--- by keeping weights of paths in a matrix and doing some linear algebra--- (fast exponentiation could give some nice results)--- could also reuse the dependency graph (see below)+-- | Checks that streams are well defined (i.e., can be compiled). defCheck :: StreamableMaps Spec -> Maybe Error defCheck streams =     let checkPathsFromSpec :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error@@ -136,9 +198,22 @@                     case s 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)+                                   | n > negate (prophecyArrayLength s0) -> +                                           Just $ DependsOnClosePast vs v n +                                                    (prophecyArrayLength s0)+                                   | t /= getAtomType s -> Just $ BadType v (head vs)                                 _ -> Nothing+                        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)+                                   | otherwise -> +                                       case idx of+                                         Const _ -> checkPath n vs idx+                                         Var _   -> checkPath n vs idx+                                         _       -> Just $ BadPArrSpec v0 arr (show idx)                         Var v ->                              if elem v vs                                 then if n >= 0@@ -152,37 +227,41 @@                         Const _ -> Nothing                         F _ _ s1 -> checkPath n vs s1                         F2 _ _ s1 s2 -> checkPath n vs s1 &&> checkPath n vs s2-                        F3 _ _ s1 s2 s3 -> checkPath n vs s1 &&> checkPath n vs s2 &&> checkPath n vs s3+                        F3 _ _ s1 s2 s3 -> checkPath n vs s1 &&> checkPath n vs s2 +                                             &&> checkPath n vs s3                         Append l s' -> checkPath (n - length l) vs s'                         Drop i s' -> checkPath (n + i) vs s'-    in-    foldStreamableMaps checkPathsFromSpec streams Nothing+    in foldStreamableMaps checkPathsFromSpec streams Nothing -getAtomType :: Streamable a => Spec a -> A.Type-getAtomType s =-  let unitElem = unit-      _ = (Const unitElem) `asTypeOf` s -- to help the typechecker-  in atomType unitElem+type Exs = (A.Type, Var, ExtVars) -getExternalVars :: StreamableMaps Spec -> [(A.Type, Var, Phase)]+data ExtVars = ExtV Phase +             | ExtA Phase String+  deriving Eq++getExternalVars :: StreamableMaps Spec -> [Exs] getExternalVars streams =     nub $ foldStreamableMaps decl streams []     where-        decl :: Streamable a => Var -> Spec a -> [(A.Type, Var, Phase)] -> [(A.Type, Var, Phase)]+        decl :: Streamable a +             => Var -> Spec a -> [Exs] -> [Exs]         decl _ s ls =             case s of-                PVar t v ph -> (t, v, ph) : ls+                PVar t v ph -> (t, v, ExtV ph) : ls+                PArr t (arr, s0) ph -> (t, arr, ExtA ph (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 $ decl undefined s2 ls+                F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 +                                     $ decl undefined s2 ls                 Drop _ s' -> decl undefined s' ls                 Append _ s' -> decl undefined s' ls                 _ -> ls + ---- Dependency graphs (for next version of nNWCP, and for scheduling) {- type Weight = Int-data Node = +data Node =     InternalVar Var [(Weight, Node)]     | ExternalVar Var Phase     deriving Show -- for debug

@@ -3,8 +3,10 @@ -- | 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.AdHocC import Language.Copilot.Core+import Language.Copilot.Analyser (ExtVars(..))  import qualified Language.Atom as A @@ -13,15 +15,26 @@ -- 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, Phase)] -> Vars -> Period -> (String, String)-getPrePostCode cName streams allExts inputExts p =-    (preCode $ extDecls allExts, postCode cName streams allExts inputExts p)+getPrePostCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] +               -> [(String,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, Phase)] -> [String]-extDecls allExtVars =-    let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars in-    map (\ (t, v, _) -> varDecl t [v]) uniqueExtVars+extDecls :: [(A.Type, Var, ExtVars)] -> [(String,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 _ _) = +          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)] +        getIdx arr = lookup arr arrDecs+    in +    map getDec uniqueExtVars  preCode :: [String] -> String preCode extDeclarations = unlines $@@ -37,7 +50,7 @@ vPre :: Name -> String vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." -postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> String+postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] -> Vars -> Period -> String postCode cName streams allExts inputExts p =    unlines $   (if isEmptySM inputExts@@ -102,22 +115,29 @@         decl v l ls =             let string = "string_" ++ v in             (indent ++ "char " ++ string ++ " [50] = \"\";") :-            (indent ++ "fgets (" ++ string ++ ", sizeof(" ++ string ++ "), stdin);") :-            (indent ++ "sscanf (" ++ string ++ ", \"" ++ typeId (head l) ++ "\", &" ++ v ++ ");") :+            (indent ++ "fgets (" ++ string ++ ", sizeof(" ++ string +                    ++ "), stdin);") :+            (indent ++ "sscanf (" ++ string ++ ", \"" +                    ++ typeId (head l) ++ "\", &" ++ v ++ ");") :             (indent ++ "clean (" ++ string ++ ", stdin);") : ls -sampleExtVars :: [(A.Type, Var, Phase)] -> Name -> [String]+sampleExtVars :: [(A.Type, Var, ExtVars)] -> Name -> [String] sampleExtVars allExts cName =-    map sample allExts-    where-        sample :: (A.Type, Var, Phase) -> String-        sample (_, v, ph) =-            "  " ++ vPre cName ++ "tmpSampleVal__" ++ v ++ "_" ++ show ph ++ " = " ++ v ++ ";"+    map (\ext -> let (v,e) = sample ext in+           "  " ++ vPre cName ++ tmpSampleStr ++ 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)  outputVars :: Name -> StreamableMaps Spec -> [String] outputVars cName streams =     foldStreamableMaps decl streams []     where-        decl :: forall a. Streamable a => Var -> Spec a -> [String] -> [String]+        decl :: forall a. Streamable a +             => Var -> Spec a -> [String] -> [String]         decl v _ ls =-            ("    " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ "   ") [vPre cName ++ "outputVal__" ++ v]) : ls+            ("    " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ "   ") +            [vPre cName ++ "outputVal__" ++ v]) : ls

@@ -3,36 +3,34 @@ -- Note : for now, the initial state is computed during the first tick  -- | Transform the copilot specification in an atom one, and then compile that one.-module Language.Copilot.Compiler(copilotToAtom) where+module Language.Copilot.Compiler(copilotToAtom, tmpSampleStr) where  import Language.Copilot.Core -import Data.Word import Data.Maybe import Data.Map as M import Data.List-import Control.Monad (when) +import Control.Monad (when)  import qualified Language.Atom as A-import Language.Copilot.Analyser (getAtomType) -getValue :: PhasedValue a -> A.V a-getValue (Ph _ val) = val- -- | 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 :: StreamableMaps Spec -> Sends -> Maybe Period -> Maybe [(Var, String)] -> (Period, A.Atom ())+copilotToAtom :: StreamableMaps Spec -> Sends -> Maybe Period +              -> [(Var, String)] -> (Period, A.Atom ()) copilotToAtom streams sends p triggers =    (p', A.period p' $ do-    -- Three streamableMaps : -    -- prophecy arrays (Int, A.A a), outputs (A.V a), temporary samples (Phase, A.V a)+     prophArrs <- mapStreamableMapsM initProphArr streams     outputs <- mapStreamableMapsM initOutput streams-    tmpSamples <- foldStreamableMaps initTmpSamples streams (return emptySM)+     updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty)     outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty) +    tmpSamples <- foldStreamableMaps (\_ -> initExtSamples streams prophArrs outputIndexes) +                    streams +                    (return emptyTmpSamples)+     -- One atom rule for each stream     foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples                             updateIndexes outputIndexes) @@ -44,8 +42,10 @@      foldSendableMaps (makeSend outputs) sends (return ()) -    -- Sampling of the external variables-    sampleVars tmpSamples)+    -- Sampling of the external variables.  Remove redundancies.+    sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ +      foldStreamableMaps (\_ -> sampleExts tmpSamples) streams []+    )   where     optP = getOptimalPeriod streams     p' = @@ -75,35 +75,74 @@                 _ -> []  initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a)-initOutput v s = streamToUnitValue ("outputVal__" ++ normalizeVar v) s+initOutput v _ = do+  atomConstructor ("outputVal__" ++ normalizeVar v) (unit::a) -initTmpSamples :: forall a. Streamable a => Var -> Spec a -> A.Atom TmpSamples -> A.Atom TmpSamples-initTmpSamples _ s tmpSamples =+tmpSampleStr :: String+tmpSampleStr = "tmpSampleVal__"++initExtSamples :: forall a. Streamable a +               => StreamableMaps Spec -> ProphArrs -> Indexes -> Spec a +                  -> A.Atom TmpSamples -> A.Atom TmpSamples+initExtSamples streams prophArrs outputIndexes s tmpSamples = do     case s of         Const _ -> tmpSamples-        Var _ -> tmpSamples-        Drop _ s' -> initTmpSamples undefined s' tmpSamples-        Append _ s' -> initTmpSamples undefined s' tmpSamples-        F _ _ s0 -> initTmpSamples undefined s0 tmpSamples-        F2 _ _ s0 s1 -> initTmpSamples undefined s0 $-            initTmpSamples undefined s1 tmpSamples-        F3 _ _ s0 s1 s2 -> initTmpSamples undefined s0 $-            initTmpSamples undefined s1 $-            initTmpSamples undefined s2 tmpSamples+        Var _ ->   tmpSamples+        Drop _ s0 -> initExtSamples' s0 tmpSamples+        Append _ s0 -> initExtSamples' s0 tmpSamples+        F _ _ s0 -> initExtSamples' s0 tmpSamples+        F2 _ _ s0 s1 -> initExtSamples' s0 $+                           initExtSamples' s1 tmpSamples+        F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $+                             initExtSamples' s2 tmpSamples         PVar _ v ph -> -            do+            do  checkVar v                  ts <- tmpSamples-                let v' = normalizeVar v ++ "_" ++ show ph-                    maybeElem = (getMaybeElem v' ts)::(Maybe (PhasedValue a))-                    name = "tmpSampleVal__" ++ normalizeVar v'+                let v' = tmpVarName v ph+                    vts = tmpVars ts+                    maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a)+                    name = tmpSampleStr ++ normalizeVar v'                 case maybeElem of                     Nothing -> -                        do-                            val <- streamToUnitValue name s-                            let m' = M.insert v' (Ph ph val) (getSubMap ts)-                            return $ updateSubMap (\_ -> m') ts-                    Just _ -> return ts -- to avoid duplicates. -                        -- Beware : crashes if "tmpSamples" instead of "return ts" +                        do  val <- atomConstructor name (unit::a)+                            let m' = M.insert v' (PhV ph 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)+                    arrts = tmpArrs ts+                    idxts = tmpIdxs ts+                    maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a)+                    name = tmpSampleStr ++ normalizeVar arr'+                case maybeElem of +                  Nothing -> -- if the array isn't in the map, neither is the index+                      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+                                   _    -> error "Unexpected Spec in initExtSamples."+                         let m' = M.insert arr' (PhA ph 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+                          => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples+          initExtSamples' = initExtSamples streams prophArrs outputIndexes  makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes makeUpdateIndex v (B n arr) indexes =@@ -130,7 +169,7 @@     Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom () makeRule streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do     r -    let B n maybeArr = (getElem v prophArrs)::(BoundedArray a)+    let B n maybeArr = getElem v prophArrs::BoundedArray a     case maybeArr of         Nothing ->             -- Fusing together the update and the output if the prophecy array doesn't exist @@ -149,47 +188,92 @@                 ((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)             -            A.phase 1 $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do+            -- Spread these out evenly accross the remaining phases, staring no+            -- earlier than phase 1.+            A.phase ((maxSampleDep v streams) + 1)+              $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do                 updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1) ---            A.phase 2 $ A.atom ("incrOutputIndex__" ++ normalizeVar v) $ do--        where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0+             +-- | Find the maximum phase as which an array sampling depends on this stream.+-- | 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 =-    r >>-    do+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 -sampleVars :: TmpSamples -> A.Atom ()-sampleVars tmpSamples = -    sequence_ $ foldStreamableMaps sample tmpSamples []-    where-        sample :: Streamable a => Var -> PhasedValue a -> [A.Atom ()] -> [A.Atom ()]-        sample v' (Ph ph val) xs = -            (A.exactPhase ph $ -                A.atom ("sample__" ++ normalizeVar v') $ -                val A.<== (A.value $ externalAtomConstructor v)-                ) : xs-            where-                -- TODO : fix this mess-                v0 = reverse (tail (dropWhile (\c -> c /= '_') (reverse v')))-                (v1, n_final) = foldl (\ (s, n) c -> -                        if c == '_' -                            then (s, n + 1) -                            else (s ++ underscoreNumber2Symbol n ++ [c],0)-                        ) ("", 0) v0-                v = v1 ++ underscoreNumber2Symbol n_final-                underscoreNumber2Symbol 0 = ""-                underscoreNumber2Symbol 1 = "_"-                underscoreNumber2Symbol 2 = "."-                underscoreNumber2Symbol 3 = "["-                underscoreNumber2Symbol 4 = "]"-                underscoreNumber2Symbol _ = undefined+-- 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+-- samples, the type of the index may differ from the type of the array, and+-- 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+  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)+     ) : a +    PArr _ (arr, idx) ph -> +         let arr' = tmpArrName arr ph (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++-- 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+getIdx arr s ts = +  case s of+    Var _   -> case getMaybeElem arr ts of+                 Nothing -> error "Error in function getIdx."+                 Just x  -> x+    Const e -> PhIdx $ A.Const e+    _       -> error $ "Expecing either a variable or constant for the index "+                 ++ "in the external array access for array " ++ arr ++ "."+ getOptimalPeriod :: StreamableMaps Spec -> Period getOptimalPeriod streams =   foldStreamableMaps getMaximumSamplingPhase streams 2@@ -198,6 +282,7 @@     getMaximumSamplingPhase _ spec n =       case spec of         PVar _ _ p -> max (p + 1) n+        PArr _ _ p -> max (p + 1) n         F _ _ s -> getMaximumSamplingPhase "" s n         F2 _ _ s0 s1 -> maximum [n,                 (getMaximumSamplingPhase "" s0 n),

@@ -13,20 +13,19 @@         Spec(..), Streams, Stream, Sends, Send(..), DistributedStreams, 	-- * General functions on 'Streams' and 'StreamableMaps' 	Streamable(..), Sendable(..), StreamableMaps(..), emptySM,-        isEmptySM, getMaybeElem, getElem, streamToUnitValue,+        isEmptySM, getMaybeElem, getElem,          foldStreamableMaps, foldSendableMaps, mapStreamableMaps, mapStreamableMapsM,-        filterStreamableMaps, normalizeVar, getVars,-        Vars-        -- Compiler-        , nextSt, BoundedArray(..), Outputs, TmpSamples-        , PhasedValue(..), ProphArrs, Indexes+        filterStreamableMaps, normalizeVar, getVars, Vars,+        -- compiler+        BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, +        ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..),+        tmpVarName, tmpArrName, getAtomType     ) where  import qualified Language.Atom as A import Data.Int import Data.Word-import Data.Maybe-import Data.List+import Data.List hiding (union) import qualified Data.Map as M import Text.Printf import Control.Monad.Writer @@ -47,18 +46,39 @@ -- | Specification of a stream, parameterized by the type of the values of the stream. -- The only requirement on @a@ is that it should be 'Streamable'. data Spec a where-    PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a     Var :: Streamable a => Var -> Spec a     Const :: Streamable a => a -> Spec a++    PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a+    PArr :: (Streamable a, Streamable b, A.IntegralE b) +         => A.Type -> (Var, Spec b) -> Phase -> Spec a+     F :: (Streamable a, Streamable b) =>  	    (b -> a) -> (A.E b -> A.E a) -> Spec b -> Spec a     F2 :: (Streamable a, Streamable b, Streamable c) =>          (b -> c -> a) -> (A.E b -> A.E c -> A.E a) -> Spec b -> Spec c -> Spec a     F3 :: (Streamable a, Streamable b, Streamable c, Streamable d) => -        (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a) -> Spec b -> Spec c -> Spec d -> Spec a+        (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a) +                           -> Spec b -> Spec c -> Spec d -> Spec a+     Append :: Streamable a => [a] -> Spec a -> Spec a     Drop :: Streamable a => Int -> Spec a -> Spec a +-- 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+    (*) = F2 (*) (*)+    (-) = F2 (-) (-)+    negate = F negate negate+    abs = F abs abs+    signum = F signum signum+    fromInteger i = Const (fromInteger i)++instance (Streamable a, A.NumE a, Fractional a) => Fractional (Spec a) where+    (/) = F2 (/) (/)+    recip = F recip recip+    fromRational r = Const (fromRational r)+ {-# RULES "Copilot.Core appendAppend" forall ls1 ls2 s. Append ls1 (Append ls2 s) = Append (ls1 ++ ls2) s "Copilot.Core dropDrop" forall i1 i2 s. Drop i1 (Drop i2 s) = Drop (i1 + i2) s@@ -70,6 +90,8 @@  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'     (==) (Var v) (Var v') = v == v'     (==) (Const x) (Const x') = x == x'     (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s'@@ -81,7 +103,6 @@  -- | Container for mutually recursive streams, whose specifications may be -- parameterized by different types---type Streams = StreamableMaps Spec type Streams = Writer (StreamableMaps Spec) () -- | A named stream type Stream a = Streamable a => (Var, Spec a)@@ -135,13 +156,13 @@     -- for example the booleans are first converted to 0 or 1, and floats and doubles     -- have the good precision.     showAsC :: a -> String--    -- | To make customer C triggers.  Only for Spec Bool (others through an error).-    makeTrigger :: Maybe [(Var, String)] -> StreamableMaps Spec + +    -- | To make customer C triggers.  Only for Spec Bool (others throw an error).+    -- XXX make them throw errors!+    makeTrigger :: [(Var, String)] -> StreamableMaps Spec                  -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a                  -> A.Atom () -> A.Atom () - class Streamable a => Sendable a where     send :: A.E a -> Port -> A.Atom () @@ -160,10 +181,8 @@                 A.cond (nextSt streams prophArrs tmpSamples outputIndexes s 0)                 A.call trig)         else return ()-      where trigs = case triggers of-                      Nothing -> []-                      Just t -> t-            trig = case M.lookup v (M.fromList trigs) of+      where +            trig = case M.lookup v (M.fromList triggers) of                      Nothing -> ""                      Just fn -> fn @@ -176,7 +195,7 @@     typeId _ = "%d"     atomType _ = A.Int8     showAsC x = printf "%d" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int16 where     getSubMap = i16Map     updateSubMap f sm = sm {i16Map = f $ i16Map sm}@@ -186,7 +205,7 @@     typeId _ = "%d"     atomType _ = A.Int16     showAsC x = printf "%d" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int32 where     getSubMap = i32Map     updateSubMap f sm = sm {i32Map = f $ i32Map sm}@@ -196,7 +215,7 @@     typeId _ = "%d"     atomType _ = A.Int32     showAsC x = printf "%d" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int64 where     getSubMap = i64Map     updateSubMap f sm = sm {i64Map = f $ i64Map sm}@@ -206,7 +225,7 @@     typeId _ = "%lld"     atomType _ = A.Int64     showAsC x = printf "%d" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word8 where     getSubMap = w8Map     updateSubMap f sm = sm {w8Map = f $ w8Map sm}@@ -216,7 +235,7 @@     typeId _ = "%u"     atomType _ = A.Word8     showAsC x = printf "%u" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word16 where     getSubMap = w16Map     updateSubMap f sm = sm {w16Map = f $ w16Map sm}@@ -226,7 +245,7 @@     typeId _ = "%u"     atomType _ = A.Word16     showAsC x = printf "%u" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word32 where     getSubMap = w32Map     updateSubMap f sm = sm {w32Map = f $ w32Map sm}@@ -236,7 +255,7 @@     typeId _ = "%u"     atomType _ = A.Word32     showAsC x = printf "%u" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word64 where     getSubMap = w64Map     updateSubMap f sm = sm {w64Map = f $ w64Map sm}@@ -246,7 +265,7 @@     typeId _ = "%llu"     atomType _ = A.Word64     showAsC x = printf "%u" (toInteger x)-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Float where     getSubMap = fMap     updateSubMap f sm = sm {fMap = f $ fMap sm}@@ -257,7 +276,7 @@     typeIdPrec _ = "%.5f"     atomType _ = A.Float     showAsC x = printf "%.5f" x-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Double where     getSubMap = dMap     updateSubMap f sm = sm {dMap = f $ dMap sm}@@ -268,7 +287,7 @@     typeIdPrec _ = "%.10lf"     atomType _ = A.Double     showAsC x = printf "%.10f" x-    makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+    makeTrigger _ _ _ _ _ _ _ r = r >> return ()  instance Sendable Word8 where     send e port =@@ -284,41 +303,45 @@ -- Launch an exception if the index is not in it {-# INLINE getElem #-} getElem :: Streamable a => Var -> StreamableMaps b -> b a-getElem v sm = fromJust $ getMaybeElem v sm+getElem v sm = case getMaybeElem v sm of+                 Nothing -> error "Error in application of getElem from Core.hs."+                 Just x -> x --- | Just produce an @Atom@ value named after its first argument,--- with an unspecified value. The second argument only coerces the type, it is discarded-{-# INLINE streamToUnitValue #-}-streamToUnitValue :: Streamable a => Var -> Spec a -> A.Atom (A.V a)-streamToUnitValue v _ = atomConstructor v unit+getAtomType :: Streamable a => Spec a -> A.Type+getAtomType s =+  let unitElem = unit+      _ = (Const unitElem) `asTypeOf` s -- to help the typechecker+  in atomType unitElem  -- | This function is used to iterate on all the values in all the maps stored -- by a @'StreamableMaps'@, accumulating a value over time {-# INLINE foldStreamableMaps #-} foldStreamableMaps :: forall b c. -    (forall a. Streamable a => Var -> c a -> b -> b) -> +    (Streamable a => Var -> c a -> b -> b) ->      StreamableMaps c -> b -> b foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =-    let acc0 = M.foldWithKey f acc bm-        acc1 = M.foldWithKey f acc0 i8m        -        acc2 = M.foldWithKey f acc1 i16m-        acc3 = M.foldWithKey f acc2 i32m-        acc4 = M.foldWithKey f acc3 i64m-        acc5 = M.foldWithKey f acc4 w8m-        acc6 = M.foldWithKey f acc5 w16m-        acc7 = M.foldWithKey f acc6 w32m-        acc8 = M.foldWithKey f acc7 w64m-        acc9 = M.foldWithKey f acc8 fm      -        acc10 = M.foldWithKey f acc9 dm+    let acc0  = M.foldrWithKey f acc  bm+        acc1  = M.foldrWithKey f acc0 i8m        +        acc2  = M.foldrWithKey f acc1 i16m+        acc3  = M.foldrWithKey f acc2 i32m+        acc4  = M.foldrWithKey f acc3 i64m+        acc5  = M.foldrWithKey f acc4 w8m+        acc6  = M.foldrWithKey f acc5 w16m+        acc7  = M.foldrWithKey f acc6 w32m+        acc8  = M.foldrWithKey f acc7 w64m+        acc9  = M.foldrWithKey f acc8 fm      +        acc10 = M.foldrWithKey f acc9 dm     in acc10 +-- XXX only sends Word8s right now -- | This function is used to iterate on all the values in all the maps stored -- by a @'StreamableMaps'@, accumulating a value over time {-# INLINE foldSendableMaps #-} foldSendableMaps :: forall b c.      (forall a. Sendable a => Var -> c a -> b -> b) ->      StreamableMaps c -> b -> b-foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =+--foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =+foldSendableMaps f (SM _ _ _ _ _ w8m _ _ _ _ _) acc =     let acc1 = M.foldWithKey f acc w8m     in acc1 @@ -343,7 +366,7 @@  {-# INLINE mapStreamableMapsM #-} mapStreamableMapsM :: forall s s' m. Monad m => -    (forall a. Streamable a => Var -> s a -> m (s' a)) -> +    (Streamable a => Var -> s a -> m (s' a)) ->      StreamableMaps s -> m (StreamableMaps s') mapStreamableMapsM f sm =     foldStreamableMaps (@@ -353,12 +376,11 @@                     return $ updateSubMap (\ m -> M.insert v s' m) sm'         ) sm (return emptySM) --- | Only keeps in @sm@ the values whose key+type are in @l@.--- Also returns a bool saying whether all the elements in sm--- were in l.--- Works even if some elements in @l@ are not in @sm@.--- Not optimised at all-filterStreamableMaps :: forall c. StreamableMaps c -> [(A.Type, Var, Phase)] -> (StreamableMaps c, Bool)+-- | Only keeps in @sm@ the values whose key+type are in @l@.  Also returns a+-- bool saying whether all the elements in sm were in l.  Works even if some+-- elements in @l@ are not in @sm@.  Not optimised at all.+filterStreamableMaps :: +  forall c b. StreamableMaps c -> [(A.Type, Var, b)] -> (StreamableMaps c, Bool) filterStreamableMaps sm l =     let (sm2, l2) = foldStreamableMaps filterElem sm (emptySM, []) in     (sm2, (l' \\ nub l2) == [])@@ -443,10 +465,16 @@         M.null fm &&         M.null dm  --- | Replace all accepted special characters by sequences of underscores+-- | Replace all accepted special characters by sequences of underscores.   normalizeVar :: Var -> Var normalizeVar v =-    foldl (\ acc c -> acc ++ case c of '.' -> "__" ; '[' -> "___" ; ']' -> "____" ; _ -> [c]) "" v+    foldl (\ acc c -> acc ++ case c of +                               '.' -> "_" +                               '[' -> "_"  +                               ']' -> "_"  +                               ' ' -> "_"+                               _ -> [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, @@ -465,6 +493,8 @@  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 (Var v) _ = "Var " ++ v showRaw (Const e) _ = "Const " ++ show e showRaw (F _ _ s0) n = @@ -492,28 +522,57 @@         (concat $ replicate n "  ") ++ ")"  --- Compiler: the code below really belongs in Core.hs, but its called by++-- Compiler: the code below really belongs in Compiler.hs, but its called by -- makeTrigger, which is a method of the class Streamable. +-- For the prophecy arrays type ArrIndex = Word64- type ProphArrs = StreamableMaps BoundedArray type Outputs = StreamableMaps A.V-type TmpSamples = StreamableMaps PhasedValue type Indexes = M.Map Var (A.V ArrIndex)-data PhasedValue a = Ph Phase (A.V a)--- important invariant : the maybe is Nothing iff the int is 0-data BoundedArray a = B ArrIndex (Maybe (A.A a)) -getValue :: PhasedValue a -> A.V a-getValue (Ph _ val) = val+-- 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 =+nextSt streams prophArrs tmpSamples outputIndexes s index =      case s of-        PVar _ v ph -> A.value . getValue -                  $ getElem (normalizeVar v ++ "_" ++ show ph) tmpSamples+        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@@ -521,22 +580,31 @@             -- so it increases the size of code (sadly),             -- but is the only thing preventing race conditions from occuring             if index < initLen-                -- if maybeArr == Nothing, then initLen == 0 and is <= index-                then-                    let outputIndex = fromJust $ M.lookup v outputIndexes in-                    (fromJust maybeArr) A.!. -                        ((A.Const index + A.VRef outputIndex) `A.mod_`  -                        (A.Const (initLen + 1)))-                else next (getElem v streams) (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)+            f (next s0 index) +              (next s1 index)         F3 _ f s0 s1 s2 ->-            f (next s0 index) (next s1 index) (next s2 index)-        Append _ s' -> next s' index-        Drop i s' -> next s' (fromInteger (toInteger i) + index)+            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-+        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)))

@@ -8,7 +8,8 @@ -- used to check automatically the equivalence between the interpreter and the -- compiler.  The Dispatch module only parses the command-line arguments before -- calling that module.-module Language.Copilot.Dispatch (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where+module Language.Copilot.Dispatch +  (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where  import Language.Copilot.Core import Language.Copilot.Analyser@@ -34,13 +35,16 @@     , 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 :: Maybe [(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)@.+    , 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)@.+    , 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+                                 -- containing the name of the array and it's+                                 -- size allows them to be declared."      } @@ -69,19 +73,19 @@ dispatch streams sends inputExts backEnd iterations verbose =     do         hSetBuffering stdout LineBuffering-        when isVerbose $ mapM_ putStrLn preludeText +        mapM_ putStrLn preludeText          isValid <-             case check streams of                 Just x -> putStrLn (show x) >> return False                 Nothing -> return True         when isValid $             -- because haskell is lazy, will only get computed if later used-            let interpretedLines = showVars (interpretStreams streams trueInputExts) iterations +            let interpretedLines = showVars (interpretStreams streams trueInputExts) +                                     iterations              in case backEnd of                 Interpreter ->                      do-                        when (not allInputsPresents) $ error -                            "the interpreter don't have the values for some of the external variables"+                        when (not allInputsPresents) $ error errMsg                         mapM_ putStrLn interpretedLines                 Opts opts ->                     let isInterpreted =@@ -90,30 +94,35 @@                                 NotInterpreted -> False                         dirName = outputDir opts                     in do-                        putStrLn $ "Trying to create (if missing) " ++ dirName ++ "  ..."+                        putStrLn $ "Trying to create the directory " ++ dirName +                                     ++  "(if missing)  ..."                         createDirectoryIfMissing False dirName                         checkTriggerVars streams (triggers opts) -                        copilotToC streams sends allExts trueInputExts -                                   (cName opts) (getPeriod opts) (prePostCode opts) -                                   (triggers opts) isVerbose-                        let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext)+                        -- copilotToC streams sends allExts trueInputExts +                        --            (cName opts) (getPeriod opts) (prePostCode opts) +                        --            (triggers opts) isVerbose+                        copilotToC streams sends allExts trueInputExts opts isVerbose+                        let copy ext = copyFile (cName opts ++ ext) +                                        (dirName ++ cName opts ++ ext)                         let delete ext = do                                f0 <- canonicalizePath (cName opts ++ ext)                                f1 <- canonicalizePath (dirName ++ cName opts ++ ext)                               if f0 == f1 then return ()                                 else removeFile (cName opts ++ ext)-                        putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts ++ ".h to " -                                  ++ dirName ++ "  ..."+                        putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts +                                        ++ ".h to " ++ dirName ++ "  ..."                         copy ".c"                         copy ".h"                         delete ".c"                         delete ".h"                         when (prePostCode opts == Nothing) $ gccCall (Opts opts)-                        when ((isInterpreted || isExecuted) && not allInputsPresents) $ error -                            "The interpreter doesn't have the values for some of the external variables."-                        when isExecuted $ execute streams (dirName ++ cName opts) trueInputExts isInterpreted +                        when ((isInterpreted || isExecuted) && not allInputsPresents) $ +                            error errMsg+                        when isExecuted $ execute streams (dirName ++ cName opts) +                                             trueInputExts isInterpreted                              interpretedLines iterations isSilent     where+        errMsg = "The interpreter does not have values for some of the external variables."         isVerbose = verbose == Verbose         isSilent = verbose == OnlyErrors         isExecuted = iterations /= 0@@ -121,8 +130,8 @@         (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts  -- Check that each trigger references an actual Copilot variable of type Bool.-checkTriggerVars :: StreamableMaps Spec -> Maybe [(Var, String)] -> IO ()-checkTriggerVars streams triggers = +checkTriggerVars :: StreamableMaps Spec -> [(Var, String)] -> IO ()+checkTriggerVars streams trigs =    if null badDefs     then if null badTypes            then return ()@@ -132,24 +141,22 @@     else error $ "Copilot error in defining triggers: the variables " ++ show badDefs                  ++ " are given triggers but "                 ++ "don't define streams in-scope."-  where badDefs = map fst bareTriggers \\ getVars streams+  where badDefs = map fst trigs \\ getVars streams         listAtomTypes :: Streamable a => Var -> Spec a -> [(Var, A.Type)] -> [(Var, A.Type)]         listAtomTypes v s ls =            let t = getAtomType s -          in  if t /= A.Bool && v `elem` (map fst bareTriggers) then (v, t):ls else ls+          in  if t /= A.Bool && v `elem` (map fst trigs) then (v, t):ls else ls         badTypes = foldStreamableMaps listAtomTypes streams []-        bareTriggers = -          case triggers of-            Nothing -> []-            Just t -> t -copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, Phase)] -> Vars -           -> Name -> Maybe Period -> Maybe (String, String) -> Maybe [(Var, String)] -> Bool -> IO ()-copilotToC streams sends allExts trueInputExts cFileName p prePostC triggers isVerbose =-    let (p', program) = copilotToAtom streams sends p triggers+copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, ExtVars)] -> Vars +           -> AtomToC -> Bool -> IO ()+copilotToC streams sends allExts trueInputExts opts isVerbose =+    let (p', program) = copilotToAtom streams sends (getPeriod opts) (triggers opts)+        cFileName = cName opts         (preCode, postCode) = -            case prePostC of-                Nothing ->  getPrePostCode cFileName streams allExts trueInputExts p'+            case (prePostCode opts) of+                Nothing ->  +                  getPrePostCode cFileName streams allExts (arrDecs opts) trueInputExts p'                 Just (pre, post) -> (pre, post)         atomConfig = A.defaults              {A.cCode = \_ _ _ -> (preCode, postCode),@@ -159,10 +166,28 @@     in do         putStrLn $ "Compiling Copilot specs to C  ..."         (sched, _, _, _, _) <- A.compile cFileName atomConfig program-        if isVerbose +        if isVerbose             then putStrLn $ A.reportSchedule sched             else return ()         putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"+-- copilotToC streams sends allExts trueInputExts cFileName p prePostC trigs isVerbose =+--     let (p', program) = copilotToAtom streams sends p trigs+--         (preCode, postCode) = +--             case prePostC of+--                 Nothing ->  getPrePostCode cFileName streams allExts trueInputExts p'+--                 Just (pre, post) -> (pre, post)+--         atomConfig = A.defaults +--             {A.cCode = \_ _ _ -> (preCode, postCode),+--             A.cRuleCoverage = False,+--             A.cAssert = False,+--             A.cStateName = "copilotState" ++ cFileName}+--     in do+--         putStrLn $ "Compiling Copilot specs to C  ..."+--         (sched, _, _, _, _) <- A.compile cFileName atomConfig program+--         if isVerbose +--             then putStrLn $ A.reportSchedule sched+--             else return ()+--         putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"  gccCall :: BackEnd -> IO () gccCall backend = @@ -245,18 +270,16 @@             (s', vs')                  preludeText :: [String]--- XXX TODO : fill the blanks in the text below preludeText = -    [ "================================================================="-    , " CoPilot, a stream language for generating "-    , " hard real-time C monitors."-    , "================================================================="-    , "Built on the Atom, for generating deterministic time and space"-    , "embedded C programs."+    [ ""+    , "========================================================================="+    , "  CoPilot, a stream language for generating hard real-time C monitors.  "+    , "========================================================================="+    , "Copyright, Galois, Inc. 2010"     , "BSD3 License" -    , "<Some copyright text.>"-    , "<Website.>"-    , "Lee Pike, Robin Morisset, and Sebastian Niller"-    , "Usage: <help>"+    , "Website: http://leepike.github.com/Copilot/"+    , "Maintainer: Lee Pike <leepike--at--gmail.com> (remove dashes)."+    , "Usage: > help"+    , "========================================================================="     , ""     ]

@@ -4,8 +4,8 @@  import Data.Word import Prelude (($))-import qualified Prelude as P import qualified Prelude as Prelude+import qualified Prelude as P  -- for specifying options import Data.Map (fromList) @@ -13,14 +13,9 @@ import System.Random import Data.Int -import Language.Copilot.Core-import Language.Copilot.Language-import Language.Copilot.Interface+import Language.Copilot  import Language.Copilot.Variables-import Language.Copilot.PrettyPrinter -import Language.Copilot.Libs.LTL- fib :: Streams fib = do   "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")@@ -43,7 +38,7 @@ t3 :: Streams t3 = do      a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1-     b .= [True, False] ++ 2 + var a < 5 + extW32 "ext" 1+     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1  t4 :: Streams t4 = do@@ -186,3 +181,29 @@ --     "loop1" .= [0] ++ varI32 "loop2" + 2  --     "loop2" .= [1] ++ varI32 "loop1" - 1  --     "other" .= drop 3 (varI32 "loop1") ++-- testing external array references+testArr :: Streams+testArr = do +  -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1 +  --       && extArrB ("ff", varW16 b) 2+  -- b .= [7] ++ varW16 b + const 3 + extArrW16 ("gg", varW16 f) 2 +  -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4 +  -- c .= [True] ++ var c+  -- d .= varB c +  e .= varW16 g -- + extArrW16 ("gg", varW16 b) 2+--  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 +  g .= extArrW16 ("gg", varW16 e) 2 +  -- h .= [0] ++ drop 1 (varW16 g)+++-- t3 :: use an external variable called ext, typed Word32+t99 :: Streams+t99 = do+     a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1+     b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1++-- test external idx before after and in the stream it references+-- test multiple defs+-- test defs in functions+-- test arrays at different indexes

@@ -4,42 +4,39 @@  import Prelude (replicate, Int) -import Language.Copilot.Core-import Language.Copilot.Language +import Language.Copilot import Language.Copilot.Variables-import Language.Copilot.Libs.LTL-import Language.Copilot.Libs.Indexes  ---------------- -- LTL tests --- ---------------- -test, output :: Var-test = "test"+testing, output :: Var+testing = "test" output = "output"   -- Can be tested with various values of n.  Use  the interpreter to see the outputs.  tSoonest :: Int -> Streams-tSoonest n = do test .= (replicate (n+2) False) ++ const True-                output .= soonest n (var test)+tSoonest n = do testing .= (replicate (n+2) False) ++ const True+                output .= soonest n (var testing)              tLatest :: Int -> Streams-tLatest n = do test .= (replicate (n-2) False) ++ const True-               output .= latest n (var test)+tLatest n = do testing .= (replicate (n-2) False) ++ const True+               output .= latest n (var testing)             tAlways :: Int -> Streams-tAlways n = do test .= (replicate (n+3) True) ++ const False-               output .= always n (varB test)+tAlways n = do testing .= (replicate (n+3) True) ++ const False+               output .= always n (varB testing)             tFuture :: Int -> Streams-tFuture n = do test .= (replicate (n+3) False) ++ varB a+tFuture n = do testing .= (replicate (n+3) False) ++ varB a                a .= [False] ++ not (var a)-               output .= eventually n (varB test)+               output .= eventually n (varB testing)             tUntil :: Int -> Streams

@@ -4,12 +4,8 @@  import Prelude () -import Language.Copilot.Core-import Language.Copilot.Language-import Language.Copilot.Interface +import Language.Copilot import Language.Copilot.Variables-import Language.Copilot.PrettyPrinter-import Language.Copilot.Libs.PTLTL  -- Next examples are for testing of the ptLTL library 

@@ -11,12 +11,14 @@   , "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"   , "   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"   , "   Compiles the Copilot specification STREAMS to constant-time & constant-"   , "   constant-space C program named FILENAME.c with header FILENAME.h"@@ -28,13 +30,15 @@   , "   the interpreter over RNDS rounds.  RNDS must be greater than 0.  This"   , "   command is equivalent to executing the interpret command and the"   , "   compile command for a randomly-generated stream and comparing the"-  , "   results by-hand.  Throws an error if the outputs differ."+  , "   results by-hand.  Throws an error if the outputs differ.  Testing"+  , "   external arrays is currently not supported."   , ""   , " > Prelude.putStr $ Prelude.show STREAMS     -- or simply"   , " > STREAMS                                   -- in ghci"   , "   Pretty-prints the parsed Copilot specification of type 'Streams'."   , ""-  , " > verify PATH/FILE.c"+  , " verify :: FilePath -> Int -> IO () (FilePath is a synonym for String)"+  , " > verify PATH/FILE.c n"   , "   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"@@ -43,9 +47,12 @@   , "   checks that there are no buffer overflows (both lower and upper), that"   , "   there are no pointer deferences of NULL, that there is no division by"   , "   zero, that floating point computations do not result in not-a-number"-  , "   (NaN), and that no uninitialized local variables are used.  For more"  -  , "   information on the properties checked, see"-  , "   <http://www.cprover.org/cprover-manual/properties.shtml>."+  , "   (NaN), and that no uninitialized local variables are used.  The entry"+  , "   point of main() is assumed, and it is also assumed that main() can be"+  , "   unrolled at least n times, where n is an Int.  This command is thus"+  , "   best used when generating a simulation program (i.e., the setPP flag"+  , "   is not used when compiling).  For more information on the properties"  +  , "   checked, see <http://www.cprover.org/cprover-manual/properties.shtml>."   , ""   , " > help "   , "   Displays this help message."@@ -127,6 +134,12 @@   , "    setTriggers MUST be used in conjunction with the setPP option, as the"   , "    simulator does not know about custom trigger functions."   , ""+  , "  setArrs :: [(String,Int)] -> Options -> Options                       (c)"+  , "    default: Nothing" +  , "    When generating C programs to test, we don't know how large external"+  , "    arrays are, so we cannot declare them.  Passing in pairs containing the"+  , "    name of the array and it's size allows them to be declared."  +  , ""   , "  setO :: Name -> Options -> Options                                    (t)"   , "    default: \"copilotProgram\""   , "    Sets the name of the executable (e.g., -o) generated by the C"@@ -141,7 +154,7 @@   , "   Interprets t0 for 50 iterations."   , ""   , " > interpret t3 40"-  , "     $ setE setE (emptySM {w32Map = fromList "+  , "     $ setE (emptySM {w32Map = fromList "   , "                     [ (\"ext0\", [0,1..])"   , "                     , (\"ext1\", [3,3..])]})"   , "       $ setV Verbose baseOpts"

@@ -2,7 +2,7 @@ module Language.Copilot.Interface (           Options(), baseOpts, test, interpret, compile, verify, interface         , help , setS, setE, setC, setO, setP, setI, setPP, setN, setV, setR-        , setDir, setGCC, setTriggers,+        , setDir, setGCC, setTriggers, setArrs,         module Language.Copilot.Dispatch     ) where @@ -16,7 +16,6 @@ import Data.List ((\\)) import System.Random import System.Exit-import System.FilePath (takeBaseName) import System.Cmd import Data.Maybe import Control.Monad@@ -36,17 +35,21 @@         optCompiler :: String, -- ^ The C compiler to use, as a path to the executable.         optOutputDir :: String, -- ^ Where to place the output C files (.c, .h, and binary).         optPrePostCode :: Maybe (String, String), -- ^ Code to append above and below the C file.-        optTriggers :: Maybe [(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)@.  There-                                             -- should be no more than one-                                             -- function per trigger variable.-                                             -- Triggers fire in the same phase (1)-                                             -- that output vars are assigned.+        optTriggers :: [(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)@.  There+                                        -- should be no more than one function+                                        -- per trigger variable.  Triggers fire+                                        -- in the same phase (1) that output+                                        -- vars are assigned.+        optArrs :: [(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 containing the name of the array and+                                   -- it's size allows them to be declared."     }  baseOpts :: Options@@ -64,7 +67,8 @@         optCompiler = "gcc",         optOutputDir = "./",         optPrePostCode = Nothing,-        optTriggers = Nothing+        optTriggers = [],+        optArrs = []     }  -- Functions for making it easier for configuring copilot in the frequent use cases@@ -80,8 +84,8 @@ compile streams fileName opts =    interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams} -verify :: FilePath -> IO ()-verify file = do+verify :: FilePath -> Int -> IO ()+verify file n = 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"@@ -90,7 +94,7 @@   putStrLn "  --overflow-check     enable arithmetic over- and underflow checks"   putStrLn "  --nan-check          check floating-point for NaN"   putStrLn ""-  putStrLn $ "  assuming " ++ theMain ++ " as the entry point:"+  putStrLn $ "  assuming main() as the entry point:"   putStrLn cmd   code <- system cmd   case code of@@ -99,24 +103,21 @@                       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, or the dispatch function in" ++ file-                      putStrLn $ "is not called " ++ theMain ++ "."  -                      putStrLn "See <http://www.cprover.org/cbmc/>"+                      putStrLn "does not exist.  See <http://www.cprover.org/cbmc/>"                       putStrLn "for more information on cbmc."-    where theMain = takeBaseName file-          cmd = unwords ("cbmc" : args)+    where cmd = unwords ("cbmc" : args)           args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"                  , "--nan-check", "--pointer-check"-                 , "--function " ++ theMain, file] +                 , "--unwind " ++ show n, file]                      - -- Small functions for easy modification of the Options record  setS :: DistributedStreams -> Options -> Options setS (streams, sends)  opts = opts {optStreams = Just streams, optSends = sends} --- | Sets the environment for simulation by giving a mapping of external variables to lists of values. E.g., +-- | Sets the environment for simulation by giving a mapping of external+-- variables to lists of values. E.g., --  -- @ setE (emptySM {w32Map = fromList [(\"ext\", [0,1..])]}) ... @ -- @@ -124,6 +125,9 @@ setE :: Vars -> Options -> Options setE vs opts = opts {optExts = Just vs} +setArrs :: [(String,Int)] -> Options -> Options+setArrs ls opts = opts {optArrs = ls}+ -- | Sets the options for the compiler, e.g., -- -- @ setC \"-O2\" ... @@@ -177,12 +181,12 @@ -- | Give C function triggers for Copilot Boolean streams.  The tiggers fire if -- the stream becoms true. setTriggers :: [(Var, String)] -> Options -> Options-setTriggers triggers opts = +setTriggers trigs opts =    if null repeats -    then opts {optTriggers = Just triggers}+    then opts {optTriggers = trigs}     else error $ "Error: only one trigger per Copilot variable.  Variables "                  ++ show (Set.fromList repeats) ++ " are given multiple triggers."-  where vars = map fst triggers+  where vars = map fst trigs         repeats = vars \\ Set.toList (Set.fromList vars)  -- | The "main" function@@ -236,7 +240,8 @@                 outputDir = optOutputDir opts,                 compiler  = optCompiler opts,                 prePostCode = optPrePostCode opts,-                triggers = optTriggers opts+                triggers = optTriggers opts,+                arrDecs = optArrs opts                     }  help :: IO ()

@@ -1,12 +1,8 @@--- | This interpreter is mostly used for checking the /Copilot/ implementation.--- But it can also be used for quick testing of a /Copilot/ design+-- | The Copilot interpreter. module Language.Copilot.Interpreter(interpretStreams) where  import Language.Copilot.Core -import Data.List -import Prelude- -- | The main function of this module. -- It takes a /Copilot/ specification, the values of the monitored values, -- and returns the values of the streams.@@ -18,17 +14,18 @@  interpret :: 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-            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')-            F2 f _ s0 s1 -> zipWith f -                (interpret inVs moVs s0)-                (interpret inVs moVs s1)-            F3 f _ s0 s1 s2 -> zipWith3 f -                (interpret inVs moVs s0) -                (interpret inVs moVs s1)-                (interpret inVs moVs s2)+  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')+    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')+    F2 f _ s0 s1 -> zipWith f (interpret inVs moVs s0)+                              (interpret inVs moVs s1)+    F3 f _ s0 s1 s2 -> zipWith3 f +                       (interpret inVs moVs s0) +                       (interpret inVs moVs s1)+                       (interpret inVs moVs s2)

@@ -23,6 +23,9 @@         -- * 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,         -- * Constructs of the copilot language@@ -42,12 +45,10 @@ import qualified Language.Atom as A import Data.Int import Data.Word-import Data.Monoid-import Data.List(elem) import System.Random import qualified Data.Map as M-import Prelude ( Fractional((/)), Bool(..), Num(..), Float, Double-               , Fractional(..), fromInteger, fail, zip, (>>=), Show(..), error, ($))+import Prelude ( Bool(..), Num(..), Float, Double+               , Fractional(..), fromInteger, zip, Show(..), Integer) import qualified Prelude as P import Control.Monad.Writer @@ -60,30 +61,20 @@ not :: Spec Bool -> Spec Bool not = F P.not A.not_ -instance (Streamable a, A.NumE a) => P.Num (Spec a) where-    (+) = F2 (P.+) (P.+) -- A.NumE a => E a is an instance of Num-    (*) = F2 (P.*) (P.*)-    (-) = F2 (P.-) (P.-)-    negate = F P.negate P.negate-    abs = F P.abs P.abs-    signum = F P.signum P.signum-    fromInteger i = Const (P.fromInteger i) -instance (Streamable a, A.NumE a, P.Fractional a) => P.Fractional (Spec a) where-    (/) = F2 (P./) (P./)-    recip = F P.recip P.recip-    fromRational r = Const (P.fromRational r)- -- | Beware : crash without any possible recovery if a division by 0 happens. -- Same risk with mod. Use div0 and mod0 if unsure. mod, div :: (Streamable a, A.IntegralE a) => Spec a -> Spec a -> Spec a mod = F2 P.mod A.mod_ div = F2 P.mod A.div_ --- | As mod and div, except that if the division would be by 0, it is instead by the first argument.+-- | As mod and div, except that if the division would be by 0, the first+-- argument is used as a default. mod0, div0 :: (Streamable a, A.IntegralE a) => a -> Spec a -> Spec a -> Spec a-mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d else x0 `P.div` x1) (\ e0 e1 -> A.mod0_ e0 e1 d)-div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d)+mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d +                          else x0 `P.div` x1) (\ e0 e1 -> A.mod0_ e0 e1 d)+div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d +                          else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d)  (<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool (<) = F2 (P.<) (A.<.)@@ -114,22 +105,27 @@             A.Retype P.. A.ue P.. (`A.mod_` (65536::(A.E Word64))) P.. A.Retype P.. A.ue) instance CastIntTo Word32 where     cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ 32)::(A.E Word64))) P.. A.Retype P.. A.ue)+            A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ (32::Integer))::(A.E Word64))) P.. A.Retype P.. A.ue) instance CastIntTo Word64 where     cast = F (P.fromInteger P.. P.toInteger) (A.Retype P.. A.ue)  instance CastIntTo Int8 where     cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) +                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) instance CastIntTo Int16 where     cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^15)::(A.E Word64))) `A.mod_` (2 P.^ 16)) P.- (2 P.^ 15)) P.. A.Retype P.. A.ue)+            A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^ (15::Integer))::(A.E Word64))) +                                          `A.mod_` (2 P.^ (16::Integer))) P.- (2 P.^ (15::Integer))) +                                      P.. A.Retype P.. A.ue) instance CastIntTo Int32 where     cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) +                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) instance CastIntTo Int64 where     cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) +                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)   -- | Beware : both sides are executed, even if the result of one is later discarded@@ -164,6 +160,8 @@ double = P.id  -- Used for easily producing, and coercing PVars++-- for variables extB :: Var -> Phase -> Spec Bool extB = PVar A.Bool extI8 :: Var -> Phase -> Spec Int8@@ -186,6 +184,31 @@ 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 ------------------------------------- 

@@ -2,7 +2,7 @@  module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where -import Prelude (Num, Integral, Int, String, error, ($), show, maxBound, toInteger)+import Prelude (Integral, Int, String, error, ($), show, maxBound, toInteger) import qualified Prelude as P  import Data.Int (Int16) 

@@ -5,7 +5,7 @@  module Language.Copilot.Libs.Indexes(soonest, soonestFail, latest, latestFail) where -import Prelude (Integral, Bool(..), id, Int, String, error, fromIntegral, ($), show)+import Prelude (id, Int, String, fromIntegral, ($)) import qualified Prelude as P  import Data.Int (Int16) 

@@ -3,8 +3,7 @@ module Language.Copilot.Libs.LTL(always, next, eventually, until, release) where  import Prelude (Int, ($))-import qualified Prelude as P -import Data.List(foldl1)+import Data.List (foldl1)  import Language.Copilot.Core import Language.Copilot.Language

@@ -1,7 +1,6 @@--- | Provides past-time linear-temporal logic (ptLTL operators).---- XXX won't make unique tmp stream names if you use the same operator twice in--- one stream definition.+-- | Provides past-time linear-temporal logic (ptLTL operators).  Currently+-- won't make unique tmp stream names if you use the same operator twice in one+-- stream definition.  module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where 

@@ -1,9 +1,11 @@ {-# LANGUAGE ScopedTypeVariables, FlexibleInstances, GADTs, RankNTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} +-- | Generate random specs for testing.  We do not generate external array indexes.+ module Language.Copilot.Tests.Random (randomStreams, Operator(..), Operators, fromOp) where -import Language.Copilot.Core+import Language.Copilot.Core  import Language.Copilot.Analyser  import qualified Language.Atom as A@@ -53,13 +55,17 @@ ---- Tools ---------------------------------------------------------------------  data Operator a = -    Operator (forall g . RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> -    g -> (Spec a, g))+    Operator (forall g . RandomGen g => +       (forall a' g'. (Streamable a', Random a', RandomGen g') => +         g' -> SpecSet -> (Spec a', g')) -> +             g -> (Spec a, g)) type Operators = StreamableMaps Operator  fromOp :: Operator a -> -    (forall g. RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> -    g -> (Spec a, g))+    (forall g. RandomGen g => +       (forall a' g'. (Streamable a', Random a', RandomGen g') => +          g' -> SpecSet -> (Spec a', g')) -> +             g -> (Spec a, g)) fromOp op =     case op of         Operator x -> x@@ -184,7 +190,8 @@  ---- Generation of random streams ---------------------------------------------- -randomStreams :: RandomGen g => Operators -> Operators -> Operators -> g -> (StreamableMaps Spec, Vars)+randomStreams :: RandomGen g => Operators -> Operators -> +     Operators -> g -> (StreamableMaps Spec, Vars) randomStreams opsF opsF2 opsF3 g =     let (vs, g0) = addRandomVNames weightsContinueVar weightsVarTypes g emptySM         (exts, g1) = addRandomVNames weightsContinuePVar weightsPVarTypes g0 emptySM@@ -194,7 +201,8 @@         then (streams, vars)         else randomStreams opsF opsF2 opsF3 g3         -addRandomVNames :: RandomGen g => [(Bool, Int)] -> [(A.Type, Int)] -> g -> Variables -> (Variables, g)+addRandomVNames :: RandomGen g => [(Bool, Int)] -> +      [(A.Type, Int)] -> g -> Variables -> (Variables, g) addRandomVNames wContinue wTypes g vs =     let (b, g0) = randomWeighted g wContinue         (t, g1) = randomWeighted g0 wTypes@@ -229,9 +237,10 @@     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-            FunSpecSet -> weightsFunSpecSet+            AllSpecSet  -> weightsAllSpecSet+            FunSpecSet  -> weightsFunSpecSet             DropSpecSet -> weightsDropSpecSet+            _           -> weightsAllSpecSet         (n::Int, g0) = randomWeighted g weights in     case n of             0 -> -- PVar@@ -263,7 +272,8 @@                 (Drop i s', g2)             _ -> error "Impossible"     where -        randomSpec' :: forall a' g'. (Streamable a', RandomGen g', Random a') => g' -> SpecSet -> (Spec a', g')+        randomSpec' :: forall a' g'. (Streamable a', RandomGen g', Random a') +                    => g' -> SpecSet -> (Spec a', g')         randomSpec' = randomSpec vs exts opsF opsF2 opsF3         getOpStream :: Operators -> g -> (Spec a, g)         getOpStream ops g0 =

@@ -20,7 +20,7 @@ code.  -********+******************************************************************************* Please visit <http://leepike.github.com/Copilot/> for more information about installing and using Copilot. @@ -30,4 +30,19 @@   > git checkout gh-pages   and you should see index.html.-********+++*******************************************************************************+Release notes++* Copilot-0.23++  * All -Wall warnings removed (from importing Copilot.hs).+  * Added support for sampling external array values.  (See Examples.hs).+  * Fixed a bug in calling CBMC to ensure it unrolls it's loop.  Updated+    documentation in Help.hs.+  * Other minor stylistic changes and fixes.++* Copilot-0.22: initial release++

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain

@@ -1,12 +1,12 @@ name:                copilot-version:             0.22+version:             0.23 cabal-version:       >= 1.2 license:             BSD3 license-file:        LICENSE-author:              Lee Pike <leepike@gmail.com>, Robin Morisset, Alwyn Goodloe, Sebastian Niller-synopsis:            A stream DSL for writing embedded C.+author:              Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller+synopsis:            A stream DSL for writing embedded C monitors. build-type:          Simple-maintainer:          Lee Pike <leepike@gmail.com>+maintainer:          Lee Pike <leepike@galois.com> category:            Language homepage:            http://leepike.github.com/Copilot/ description:         Can you write a list in Haskell? Then you can write embedded C code using@@ -32,7 +32,7 @@ library     ghc-options:     -Wall     build-depends:     base > 4 && < 5-                     , atom >= 1.0.5+                     , atom >= 1.0.7                      , containers >= 0.2.0.1                      , process >= 1.0.0.0                      , random >= 1.0.0.0