copilot 1.0.2 → 2.0

raw patch · 34 files changed

+299/−4717 lines, 34 filesdep +copilot-c99dep +copilot-cbmcdep +copilot-coredep −atomdep −containersdep −filepathdep ~basedep ~directorysetup-changednew-component:exe:copilot-regressionPVP ok

version bump matches the API change (PVP)

Dependencies added: copilot-c99, copilot-cbmc, copilot-core, copilot-language, copilot-libraries

Dependencies removed: atom, containers, filepath, mtl, process, random

Dependency ranges changed: base, directory

API changes (from Hackage documentation)

Files

• Language/Copilot.hs +0/−44
• Language/Copilot/AdHocC.hs +0/−73
• Language/Copilot/Analyser.hs +0/−403
• Language/Copilot/AtomToC.hs +0/−140
• Language/Copilot/Compiler.hs +0/−407
• Language/Copilot/Core.hs +0/−591
• Language/Copilot/Dispatch.hs +0/−246
• Language/Copilot/Examples/Examples.hs +0/−372
• Language/Copilot/Examples/LTLExamples.hs +0/−83
• Language/Copilot/Examples/PTLTLExamples.hs +0/−132
• Language/Copilot/Examples/StatExamples.hs +0/−26
• Language/Copilot/Help.hs +0/−172
• Language/Copilot/Interface.hs +0/−263
• Language/Copilot/Interpreter.hs +0/−42
• Language/Copilot/Language.hs +0/−222
• Language/Copilot/Language/Casting.hs +0/−99
• Language/Copilot/Language/FunctionCalls.hs +0/−46
• Language/Copilot/Language/RandomOps.hs +0/−206
• Language/Copilot/Language/Sampling.hs +0/−99
• Language/Copilot/Libs/ErrorChks.hs +0/−28
• Language/Copilot/Libs/Indexes.hs +0/−48
• Language/Copilot/Libs/LTL.hs +0/−125
• Language/Copilot/Libs/PTLTL.hs +0/−65
• Language/Copilot/Libs/Statistics.hs +0/−50
• Language/Copilot/Libs/Vote.hs +0/−76
• Language/Copilot/PrettyPrinter.hs +0/−37
• Language/Copilot/Tests/Random.hs +0/−315
• README +0/−235
• README.md +88/−0
• Setup.hs +11/−0
• Setup.lhs +0/−8
• Tests/Test.hs +127/−0
• copilot.cabal +34/−64
• src/Language/Copilot.hs +39/−0

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

@@ -1,73 +0,0 @@--- generate C-Code with combinators, high-level, safe haskell.---- | Helper functions for writing free-form C code.-module Language.Copilot.AdHocC (-         varDecl, arrDecl, varInit, arrayInit, funcDecl-       , includeBracket, includeQuote, printf, printfNewline-    ) where--import Data.List (intersperse) -import Language.Atom (Type(..))-import Language.Atom.Code (cType) -- C99---- | Takes a type and a list of variable names and declares them.-varDecl :: Type -> [String] -> String-varDecl t vars = -    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 ++ ";"---- | 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 ++ "[" ++ show (length vals)-        ++ "] = " ++ bracesListShow ++ ";"-  where -  -- Show a list with braces {} rather than brackets [].-  bracesListShow :: String-  bracesListShow =-    "{" ++ (foldl (++) "" $ intersperse "," $ map show 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 ++ ">"---- | Add an include of a header file-includeQuote :: String -> String-includeQuote lib = "#include \"" ++ lib ++ "\""--printfPre :: String -> String-printfPre = ("printf(\"" ++)--printfPost :: [String] -> String-printfPost vars = -  let sep = if null vars then " " else ", " -  in "\"" ++ sep ++ unwords (intersperse "," vars) ++ ");"--newline :: String-newline = "\\n"---- | printf, with and without a newline (nl) character.-printf, printfNewline :: String -> [String] -> String-printfNewline text vars = (printfPre text) ++ newline ++ (printfPost vars)-printf text vars = (printfPre text) ++ (printfPost vars)-

@@ -1,403 +0,0 @@-{-# LANGUAGE RelaxedPolyRec #-}---- | 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-        {--        -- * Dependency Graphs (experimental)-        Weight, Node(..), DependencyGraph,-        mkDepGraph, showDG -}-    ) where--import Language.Copilot.Core--import Data.List-import Data.Maybe(mapMaybe)--type Weight = Int---- | Used for representing an error in the specification, detected by @'check'@-data Error =-      BadSyntax String Var -- ^ the BNF is not respected-    | BadDrop Int Var -- ^ A drop expression of less than 0 is used-    | BadPArrSpec Var Ext String -- ^ External array indexes can only take-                                 -- variables or constants as indexes.-    | BadType Var String -- ^ either a variable is not defined, or not with the-                         -- good type ; there is no implicit conversion of types-                         -- in /Copilot/.-    | BadTypeExt Ext Var -- ^ either an external variable is not defined, or not-                         -- with the good type; there is no implicit conversion-                         -- of types in /Copilot/-    | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile-                                                 -- /Copilot/ specification can-                                                 -- only work if there is no-                                                 -- negative weighted closed-                                                 -- path in the specification,-                                                 -- as described in the original-                                                 -- research paper-    | DependsOnClosePast [Var] Ext Weight Weight -- ^ Could be compiled, but-                                                 -- would need bigger-                                                 -- prophecyArrays-    | DependsOnFuture [Var] Ext Weight -- ^ If an output depends of a future of-                                       -- an input it will be hard to compile to-                                       -- say the least-    | NoInit Var -- ^ If we are sampling a function and it has an-                 -- argument that is a Copilot stream, the weight of-                 -- that stream must have at least one initial element.--instance Show Error where-    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 (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 "-            ++ show arr ++ "in the definition of stream " ++ v ++ " is not of that "-            ++ "form.\n"-        ]-    show (BadType v v') =-       unlines-        [ "Error : the monitor variable " ++ v ++ ", called from " -          ++ v' ++ ", either"-        , "does not exist, or don't have the right type (there is no implicit " -          ++ "conversion).\n"-        ]-    show (BadTypeExt v v') =-       unlines-        [ "Error : the external call " ++ show v ++ ", called in the stream " -          ++ v' ++ ", either"-        , "does not exist, or don't have the right type (there is no implicit " -          ++ "conversion).\n"-        ]-    show (NonNegativeWeightedClosedPath vs w) =-       unlines -        [ "Error : the following path is closed in the dependency graph of the "-            ++ "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) =-       unlines-        [ "Error : the following path is of weight " ++ show w ++ " ending in "-          ++ "the external variable " ++ show v -        , "while the first variable of that path has a prophecy array of length " -          ++ show len ++ "," -        , "which is strictly greater than the weight. This is forbidden."-        , "Path : " ++ show (reverse vs) ++ "\n"-        ]-    show (DependsOnFuture vs v w) =-       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 " ++ show v -        , "which is quoted in the last variable of the path.  This is "-          ++ "obviously impossible."-        , "Path : " ++ show (reverse vs) ++ "\n"-        ]-    show (NoInit v) = -          "Error : the Copilot variable " ++ v ++ " appears either as an argument in an "-          ++ "external function that is sampled or an index in an external array being sampled. "-          ++ "In either case, the stream must have an initial value (that is not drawn from an "-          ++ "external variable)."--(&&>) :: Maybe a -> Maybe a -> Maybe a-m &&> m' =-    case m of-        Just _ -> m-        Nothing -> m'--(||>) :: Bool -> a -> Maybe a-b ||> x =-    if b-        then Nothing-        else Just x--infixr 2 ||>-infixr 1 &&>---- | 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 =-  syntaxCheck streams &&> defCheck streams &&> checkInitsArgs streams---- Represents all the kind of specs that are authorized after a given operator.-data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet -  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 But then there--- would have been quite a lot construction/deconstruction to do everywhere.--- Hence the compact type for Spec and this extra check.-syntaxCheck :: StreamableMaps Spec -> Maybe Error-syntaxCheck streams =-    foldStreamableMaps (checkSyntaxSpec AllSpecSet) streams Nothing-    where-        checkSyntaxSpec :: Streamable a -                        => SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error-        checkSyntaxSpec set v s e =-            e &&>-                case s of-                    Var _ -> Nothing-                    Const _ -> Nothing-                    PVar _ _ -> Nothing -- checkSampling s0-                    PArr _ (arr,s0) -> checkIndex v arr s0 --- case chkInitElem streams (getElem v streams `asTypeOf` s0) of---                                       Left ()  -> Just $ NoInit (show arr) v---                                       Right () -> Nothing---                          _       -> Just $ BadArrIdx (show arr) (show s0)---                      ) &&> checkSampling arr---                        &&> checkSyntaxSpec PArrSet v s0 Nothing                      -                    -- PVar _ _ -> Nothing -                    -- PArr _ (arr,s0) -> -                    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)-        -- checkSampling s = -        --   case s of-        --     ExtV _   -> Nothing-        --     fun@(Fun f args) ->  -        --       foldl (\n arg -> case arg of-        --                          C _ -> n &&> Nothing-        --                                 -- already check elems defined in defCheck-        --                          V v -> n &&> (case chkInitElem streams (getElem v streams) of -        --                                          Left ()  -> Just $ NoInit (show fun) v-        --                                          Right () -> Nothing-        --                                       )-        --             ) Nothing args----- | 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-        checkPathsFromSpec v0 s0 e =-            e &&> checkPath 0 [v0] s0-            where-                prophecyArrayLength s =-                    case s of-                        Append ls s' -> length ls + prophecyArrayLength s'-                        _ -> 0-                checkPath :: Streamable a => Int -> [Var] -> Spec a -> Maybe Error-                checkPath n vs s =-                    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 $ BadTypeExt 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 $ BadTypeExt 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-                                    then Just $ NonNegativeWeightedClosedPath vs n-                                    else Nothing-                                else-                                    let spec = getMaybeElem v streams in-                                    case spec of-                                        Nothing -> Just $ BadType v (head vs)-                                        Just s' -> checkPath n (v:vs) (s' `asTypeOf` s)-                        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-                        Append l s' -> checkPath (n - length l) vs s'-                        Drop i s' -> checkPath (n + i) vs s'-    in foldStreamableMaps checkPathsFromSpec streams Nothing--getExternalVars :: StreamableMaps Spec -> [Exs]-getExternalVars streams =-    nub $ foldStreamableMaps decl streams []-    where-        decl :: Streamable a => Var -> Spec a -> [Exs] -> [Exs]-        decl _ s ls =-            case s of-                PVar t v -> (t, v, ExtRetV) : ls-                PArr t (arr, s0) -> (t, arr-                                    , ExtRetA (case s0 of-                                                 Var v -> V v-                                                 Const c -> C (show c)-                                                 _ -> error "Error in getExternalVars.")-                                    ) : 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-                Drop _ s' -> decl undefined s' ls-                Append _ s' -> decl undefined s' ls-                _ -> ls---- | Is there an initial element (for sampling functions)?-checkInitsArgs :: StreamableMaps Spec -> Maybe Error-checkInitsArgs streams =-  let checkInits :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error-      checkInits v s err =-        err &&> if checkPath 0 [v] s >= 0 then Just (NoInit v)-                  else Nothing-        where checkPath :: Streamable a => Int -> [Var] -> Spec a -> Int-              checkPath n vs s0 = -                if (v `elem` samplingFuncs) || (v `elem` arrIndices)-                  then case s0 of-                         Var v0    -> if elem v0 vs then n-                                       else checkPath n (v0:vs) -                                              (getElem v0 streams `asTypeOf` s0)-                         Append ls s1 -> checkPath (n - length ls) vs s1-                         Drop m s1    -> checkPath (m + n) vs s1-                         _ -> n-                         -- Const _  -> n-                         -- PVar _ _ -> n-                         -- PArr _ _ -> n-                         -- F _ _ _      -> n-                         -- F2 _ _ _ _   -> n-                         -- F3 _ _ _ _ _ -> n-                  else (-1)-              samplingFuncs = -                concatMap (\x -> case x of -                                   (_, Fun _ args, _) -> -                                     mapMaybe (\arg -> -                                       case arg of-                                         C _ -> Nothing-                                         V v0 -> Just v0-                                              ) args-                                   (_, ExtV _, _) -> [])-                (getExternalVars streams)-              arrIndices = mapMaybe (\x -> case x of-                                             (_,_,ExtRetV) -> Nothing -                                             (_,_,ExtRetA idx) -> -                                               case idx of-                                                 V v' -> Just v'-                                                 C _ -> Nothing)-                           (getExternalVars streams)-  in foldStreamableMaps checkInits streams Nothing---- chkInitElem :: Streamable a => StreamableMaps Spec -> Spec a -> Either () ()--- chkInitElem streams spec = ---   initElem spec 0 []---   where ---     -- getSpec :: Streamable a => Var -> Spec a---     -- getSpec v = let s = getMaybeElem v streams in---     --                case s of---     --                  Nothing -> error $ "Error: No Copilot stream "---     --                             ++ v ++ " exists."---     --                  Just s0 -> s0 `asTypeOf` s---     initElem :: Streamable a => Spec a -> Int -> [Var] -> Either () ()---     initElem s cnt vs =---       case s of---         Var v    -> if elem v vs then initChk ---                       else initElem (getElem v streams) cnt (v:vs)---         Const _  -> initChk---         PVar t v -> initChk---         PArr t (arr, s0) -> initChk---         F _ _ _      -> initChk---         F2 _ _ _ _   -> initChk---         F3 _ _ _ _ _ -> initChk---         Append ls s0 -> initElem s0 (cnt - length ls) vs---         Drop n s0    -> initElem s0 (cnt + n) vs---       where initChk = if cnt < 0 then Right () else Left ()------ Dependency graphs (for next version of nNWCP, and for scheduling)-{--type Weight = Int-data Node =-    InternalVar Var [(Weight, Node)]-    | ExternalVar Var Phase-    deriving Show -- for debug--instance Eq Node where-    InternalVar v _ == InternalVar v' _ = v == v'-    ExternalVar v ph == ExternalVar v' ph' = v == v' && ph == ph'-    _ == _ = False--type DependencyGraph = [Node]--showDG :: DependencyGraph -> [String]-showDG dG = map show dG--mkDepGraph :: StreamableMaps Spec -> DependencyGraph-mkDepGraph streams =-    dGFixpoint-    where-        dGFixpoint :: DependencyGraph-        dGFixpoint = foldStreamableMaps mkNode streams []-        mkNode :: Streamable a => Var -> Spec a -> DependencyGraph -> DependencyGraph-        mkNode v s dG =-            let edges = mkEdges 0 s-                externalNodes = mkExternalNodes s in-            (InternalVar v edges) : (nub $ externalNodes ++ dG)-        -- TODO : the following functions can probably be fused together-        mkExternalNodes :: Spec a -> [Node]-        mkExternalNodes s =-            case s of-                PVar _ v ph -> [ExternalVar v ph]-                Var _ -> []-                Const _ -> []-                F _ _ s0 -> mkExternalNodes s0-                F2 _ _ s0 s1 -> mkExternalNodes s0 ++ mkExternalNodes s1-                F3 _ _ s0 s1 s2 -> mkExternalNodes s0 ++ mkExternalNodes s1 ++ mkExternalNodes s2-                Append _ s0 -> mkExternalNodes s0-                Drop _ s0 -> mkExternalNodes s0-        mkEdges :: Weight -> Spec a -> [(Weight, Node)]-        mkEdges w s =-            case s of-                PVar _ v ph -> [(w, getNode v $ Just ph)]-                Var v -> [(w, getNode v Nothing)]-                Const _ -> []-                F _ _ s0 -> mkEdges w s0-                F2 _ _ s0 s1 -> mkEdges w s0 ++ mkEdges w s1-                F3 _ _ s0 s1 s2 -> mkEdges w s0 ++ mkEdges w s1 ++ mkEdges w s2-                Append ls s0 -> mkEdges (w - length ls) s0-                Drop i s0 -> mkEdges (w + i) s0-        getNode :: Var -> Maybe Phase -> Node-        getNode v mp =-             case mp of-                Nothing -> fromJust $ find ((==) (InternalVar v [])) dGFixpoint-                Just ph -> fromJust $ find ((==) (ExternalVar v ph)) dGFixpoint -}

@@ -1,140 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}---- | Defines a main() and print statements to easily execute generated Copilot specs.-module Language.Copilot.AtomToC(getPrePostCode) where--import Language.Copilot.AdHocC--import Language.Copilot.Core--import Data.Maybe (fromMaybe)-import Data.List---- allExts represents all the variabbles to monitor (used for declaring them)--- inputExts represents the monitored variables which are to be fed to the--- standard input of the C program.  only used for the testing with random--- streams and values.-getPrePostCode :: Bool -> (Maybe String, Maybe String) -> Name -               -> StreamableMaps Spec -> [Exs] -> [(Ext,Int)] -> Vars -               -> Period -> (String, String)-getPrePostCode simulatation (pre, post) cName streams allExts -               arrDecs inputExts p =-    ( (if simulatation then preCode (extDecls allExts arrDecs)-         else "") ++ fromMaybe "" pre-    , fromMaybe "" post ++ periodLoop cName p -      ++ if simulatation then (postCode cName streams inputExts)-           else ""-    )---- Make the declarations for external vars-extDecls :: [Exs] -> [(Ext,Int)] -> [String]-extDecls allExtVars arrDecs =-    let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') -                              allExtVars -        getDec :: Exs -> String-        getDec (t, (ExtV v), ExtRetV) = varDecl t [v]-        getDec (_, (Fun _ _), ExtRetV) = ""-        getDec (t, arr, ExtRetA _) = -          case getIdx arr of -            Nothing -> error $ "Please use the setArrs option to provide a list of " ++-                          "pairs (a,idx) where a is the name of an external array and idx " ++-                          "is its static size to declare.  There is no size for array " ++-                          show arr ++ "."-            Just idx  -> arrDecl t [(show arr, idx)] -        getIdx arr = lookup arr arrDecs-    in -    map getDec uniqueExtVars--preCode :: [String] -> String-preCode extDeclarations = unlines $-  [ includeBracket "stdio.h"-  , includeBracket "stdlib.h"-  , includeBracket "string.h"---  , includeBracket "inttypes.h"-  , ""-  , "unsigned long long rnd;"-  ]-  ++ extDeclarations---- | Generate a temporary C file name. -tmpCFileName :: String -> String-tmpCFileName name = "__" ++ name--periodLoop :: Name -> Period -> String-periodLoop cName p = unlines-  [ "\n"-  , "void " ++ tmpCFileName cName ++ "(void) {"-  , "  int i;"-  , "  for(i = 0; i < " ++ show p ++ "; i++) {"-  , "    "  ++ cName ++ "();"-  , "  }"-  , "}"-  ]--postCode :: Name -> StreamableMaps Spec -> Vars -> String-postCode cName streams inputExts = -  unlines $-  [""] ++-  (if isEmptySM inputExts-     then []-     else cleanString)-  ++ -- make a loop to complete a period of computation.-  [ "int main(int argc, char *argv[]) {"-  , "  if (argc != 2) {"-  , "    " ++ printfNewline -         "Please pass a single argument to the simulator containing the number of rounds to execute it." -         []-  , "    return 1;"-  , "  }"-  , "  rnd = atoi(argv[1]);"-  , "  int i;"-  , "  for(i = 0; i < rnd ; i++) {"-  , "    " ++ printf "period: %i   " ["i"]-  ]-  ++ inputExtVars inputExts "    "-  ++ ["    " ++ tmpCFileName cName ++ "();"]-  ++ outputVars cName streams -  ++ -  [ "    " ++ printfNewline "" []-  , "    fflush(stdout);"-  , "  }"-  , "  return EXIT_SUCCESS;"-  , "}"-  ]-  where-    cleanString =-        [ "void clean(const char *buffer, FILE *fp) {"-        , "  char *p = strchr(buffer,'\\n');"-        , "  if (p != NULL)"-        , "    *p = 0;"-        , "  else {"-        , "    int c;"-        , "    while ((c = fgetc(fp)) != '\\n' && c != EOF);"-        , "  }"-        , "}"-        , ""-        ]--inputExtVars :: Vars -> String -> [String]-inputExtVars exts indent =-    foldStreamableMaps decl exts []-    where-        decl :: Streamable a => Var -> [a] -> [String] -> [String]-        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 ++ "clean (" ++ string ++ ", stdin);") : ls--outputVars :: Name -> StreamableMaps Spec -> [String]-outputVars cName streams =-    foldStreamableMaps decl streams []-    where-        decl :: forall a. Streamable a -             => Var -> Spec a -> [String] -> [String]-        decl v _ ls =-            ("    " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ "   ") -            [vPre cName ++ v]) : ls

@@ -1,407 +0,0 @@-{-# LANGUAGE ScopedTypeVariables, Rank2Types, GADTs #-}---- XXX Clean this up!---- | Transform the copilot specification in an atom one, and then compile that one.-module Language.Copilot.Compiler-  (copilotToAtom, tmpSampleStr, tmpArrName, tmpVarName-  ) where--import Language.Copilot.Core--import Data.Maybe-import qualified Data.Map as M-import Data.List-import Data.Word (Word32)--import qualified Language.Atom as A---- | Compiles an /Copilot/ specification to an /Atom/ one.--- The period is given as a Maybe : if it is Nothing, an optimal period will be chosen.-copilotToAtom :: LangElems -> Maybe Period -> Name -> (Period, A.Atom ()) -copilotToAtom (LangElems streams triggers) p cFileName = -  (p', A.period p' $ do-    prophArrs <- mapStreamableMapsM initProphArr streams-    outputs <- mapStreamableMapsM initOutput streams-    updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty)-    outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty)-    tmpSamples <- foldStreamableMaps -                    (\_ -> initExtSamples streams outputs prophArrs outputIndexes) -                    streams -                    (return emptyTmpSamples)--    let nextStates = makeStates $ -          mapStreamableMaps -            (nextSt streams prophArrs tmpSamples outputIndexes 0) -            streams--    -- One atom rule for each stream-    foldStreamableMaps (makeRule nextStates outputs prophArrs-                           updateIndexes outputIndexes) -      streams (return ())--    M.fold (makeTrigger outputs cFileName) (return ()) triggers-           -    -- Sampling of the external variables.  Remove redundancies.-    sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ -      foldStreamableMaps (\_ -> sampleExts outputs tmpSamples cFileName) streams []-    )-  where p' = period p---- | For period n >= 5:--- Phase 0: Sample external vars (if any).--- Phase 1: state update.--- Phase 2: Compute output variables.--- Phase 3: Fire triggers (if any).--- Phase 4 up to n: update indexes.-period :: Maybe Int -> Int-period p = -  case p of-    Nothing -> minPeriod-    Just i -> if i >= minPeriod-                then i -                else error $ "Copilot error: the period is too short, " -                       ++ "it should be at least " ++ show minPeriod ++ " ticks."-  where minPeriod :: Int-        minPeriod = 5---- For the prophecy arrays-type ArrIndex = Word32-type ProphArrs = StreamableMaps BoundedArray-type Outputs = StreamableMaps A.V-type Indexes = M.Map Var (A.V ArrIndex)---- External variables-data PhasedValueVar a = PhV (A.V a)--data BoundedArray a = B ArrIndex (Maybe (A.A a))---- | Takes the NextSts and walks over the tree building the Atom expression.  -makeStates :: StreamableMaps NextSt -> StreamableMaps A.E-makeStates trees = -  mapStreamableMaps (\_ -> makeState) trees-  where -    makeState :: (Streamable a) => NextSt a -> A.E a-    makeState tree = -      case tree of -        ExpLeaf s -> s-        F1Node f s0 -> f (makeState s0) -        F2Node f s0 s1 -> f (makeState s0) (makeState s1)-        F3Node f s0 s1 s2 -> f (makeState s0) (makeState s1) (makeState s2)-        VarRefLeaf v -> makeState (getElem v trees)---- | A tree datatype that holds Atom expressions from the 'nextSt' function--- | until we've got all variable references collected up.  In particular, we--- | have told function applications.-data NextSt a where-    -- Leaves-    ExpLeaf :: A.E a -> NextSt a-    VarRefLeaf :: Var -> NextSt a-    -- Parent nodes-    F1Node :: (Streamable a, Streamable b) -           => (A.E b -> A.E a) -> NextSt b -> NextSt a-    F2Node :: (Streamable a, Streamable b, Streamable c) -           => (A.E b -> A.E c -> A.E a) -> NextSt b -> NextSt c -> NextSt a -    F3Node :: (Streamable a, Streamable b, Streamable c, Streamable d) -           => (A.E b -> A.E c -> A.E d -> A.E a) -              -> NextSt b -> NextSt c -> NextSt d -> NextSt a---- | Compute the next state value.-nextSt :: Streamable a -       => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -> ArrIndex -       -> Var -> Spec a -> NextSt a-nextSt streams prophArrs tmpSamples outputIndexes index _ s = -    case s of-        PVar _ v  -> ExpLeaf $ -          let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in-          A.value var-        PArr _ (v, idx) -> ExpLeaf $-          let PhA var = e tmp (tmpArrs tmpSamples) -              tmp = tmpArrName v (show idx) -              e a b = case getMaybeElem a b of-                        Nothing -> -                          error "Error in application of getElem in nextSt."-                        Just x  -> x -          in A.value var-        Var v -> nextStVar v streams prophArrs tmpSamples outputIndexes index-        Const e -> ExpLeaf $ A.Const e-        F _ f s0 -> F1Node f (next s0 index)-        F2 _ f s0 s1 -> F2Node f (next s0 index) (next s1 index)-        F3 _ f s0 s1 s2 -> F3Node 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 -> NextSt b-          next s' ind = -            nextSt streams prophArrs tmpSamples outputIndexes ind undefined s'---- | Get the next state when one stream references another Copilot stream variable.-nextStVar :: Streamable a => Var -> StreamableMaps Spec -> ProphArrs -          -> TmpSamples -> Indexes -> ArrIndex -> NextSt a-nextStVar v streams prophArrs tmpSamples outputIndexes index = -  let B initLen maybeArr = getElem v prophArrs in-  -- This check is extremely important. It means that if x at time n depends on y-  -- at time n then x is obtained not by y, but by inlining the definition of y-  -- so it increases the size of code (sadly), but is the only thing preventing-  -- race conditions from occuring.-  if index < initLen-    then getVar v initLen maybeArr -    else let s0 = getElem v streams in -         -- XXX This should be generalized to handle arbitrary index values.-         -- For now, as a test, we'll just use the cahced nextState value if-         -- it's like computing that stream's nextState from scratch.-         let newIndex = index - initLen in-         if newIndex == 0 then VarRefLeaf v-           else nextSt streams prophArrs tmpSamples outputIndexes -                  newIndex undefined s0-  where getVar :: Streamable a => Var -> ArrIndex -> Maybe (A.A a) -> NextSt a-        getVar v' initLen maybeArr = ExpLeaf $-           let outputIndex = case M.lookup v' outputIndexes of-                               Nothing -> error "Error in function getVar."-                               Just x -> x-               arr = case maybeArr of-                       Nothing -> error "Error in function getVar (maybeArr)."-                       Just x -> x in -           arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_`  -                       (A.Const (initLen + 1)))--initProphArr :: forall a. Streamable a -             => Var -> Spec a -> A.Atom (BoundedArray a)-initProphArr v s =-    let states = initState s-        name = "prophVal__" ++ normalizeVar v-        n = genericLength states in-    if n > 0-        then-            do-                array <- A.array name (states ++ [unit])-                -- unit is replaced by the good value during the first tick-                return $ B n $ Just array-    else return $ B n Nothing-    where-        initState s' =-            case s' of-                Append ls s'' -> ls ++ initState s''-                _ -> []----- External arrays-data PhasedValueArr a = PhA (A.V a) -- Array name.-data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. --data TmpSamples = -  TmpSamples { tmpVars :: StreamableMaps PhasedValueVar-             , tmpArrs :: StreamableMaps PhasedValueArr-             , tmpIdxs :: StreamableMaps PhasedValueIdx-             }--emptyTmpSamples :: TmpSamples-emptyTmpSamples = TmpSamples emptySM emptySM emptySM--tmpVarName :: Ext -> Var-tmpVarName v = show v--tmpArrName :: Ext -> String -> Var-tmpArrName v idx = (tmpVarName v) ++ "_" ++ normalizeVar idx--initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a)-initOutput v _ = do-  atomConstructor (normalizeVar v) (unit::a)--tmpSampleStr :: String-tmpSampleStr = "tmpSampleVal__"--initExtSamples :: forall a. Streamable a -               => StreamableMaps Spec -> Outputs -> ProphArrs -> Indexes -> Spec a -                  -> A.Atom TmpSamples -> A.Atom TmpSamples-initExtSamples streams outputs prophArrs outputIndexes s tmpSamples = do-    case s of-        Const _ -> 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 -> -            do  ts <- tmpSamples-                let v' = tmpVarName v -                    vts = tmpVars ts-                    maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a)-                    name = tmpSampleStr ++ normalizeVar v'-                case maybeElem of-                    Nothing -> -                        do  val <- atomConstructor name (unit::a)-                            let m' = M.insert v' (PhV val) (getSubMap vts)-                            return $ ts {tmpVars = updateSubMap (\_ -> m') vts}-                    Just _ -> return ts-        PArr _ (arr, idx) -> -            do  ts <- tmpSamples-                let arr' = tmpArrName arr (show idx)-                    arrts = tmpArrs ts-                    idxts = tmpIdxs ts-                    maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a)-                    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 v   -> PhIdx $ A.value (getElem v outputs)-                                   _    -> error "Unexpected Spec in initExtSamples."-                         let m' = M.insert arr' (PhA val) (getSubMap arrts)-                         let m'' = M.insert arr' i (getSubMap idxts)-                         return $ ts { tmpArrs = updateSubMap (\_ -> m') arrts-                                     , tmpIdxs = updateSubMap (\_ -> m'') idxts-                                     }-                  Just _ -> return ts-    where initExtSamples' :: Streamable b-                          => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples-          initExtSamples' = initExtSamples streams outputs prophArrs outputIndexes---- | For each stream, make an index into its array of values telling you where--- the next value in the array to update is.-makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes-makeUpdateIndex v (B n arr) indexes =-    case arr of-        Nothing -> indexes-        Just _ ->  -            do  mindexes <- indexes-                index <- atomConstructor ("updateIndex__" ++ normalizeVar v) n-                return $ M.insert v index mindexes---- | For each stream, make an index into its array of values telling you where--- its current output value is.-makeOutputIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes-makeOutputIndex v (B _ arr) indexes =-    case arr of-        Nothing -> indexes-        Just _ ->  -            do  mindexes <- indexes-                index <- atomConstructor ("outputIndex__" ++ normalizeVar v) 0-                return $ M.insert v index mindexes--makeRule :: forall a. Streamable a => -    StreamableMaps A.E -> Outputs -> ProphArrs-    -> Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()-makeRule exps outputs prophArrs updateIndexes outputIndexes v _ r = do-    r -    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 -            -- (ie if it would only have hold the output value)-            A.exactPhase 1 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do-                ((getElem v outputs)::(A.V a)) A.<== getElem v exps--        Just arr -> do-            let updateIndex = fromJust $ M.lookup v updateIndexes-                outputIndex = fromJust $ M.lookup v outputIndexes--            A.exactPhase 1 $ A.atom ("update__" ++ normalizeVar v) $ do-                arr A.! (A.VRef updateIndex) A.<== getElem v exps-            -            A.exactPhase 2 $ A.atom ("output__" ++ normalizeVar v) $ do-                ((getElem v outputs)::(A.V a)) A.<== arr A.!. (A.VRef outputIndex)-                outputIndex A.<==          (A.VRef outputIndex + A.Const 1) -                                  `A.mod_` A.Const (n + 1)-            -            A.phase 4-              $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do-                updateIndex A.<==          (A.VRef updateIndex + A.Const 1) -                                  `A.mod_` A.Const (n + 1)--sampleStr :: String-sampleStr = "sample__"---- What we really should be doing is just folding over the TmpSamples, since--- that data should contain all the info we need to construct external variable--- and external array samples.  However, there is the issue that for array--- 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 -           => Outputs -> TmpSamples -> Name -> Spec a -              -> [(Var, A.Atom ())] -> [(Var, A.Atom ())]-sampleExts outputs ts cFileName s a = do-  case s of-    Var _ -> a-    Const _ -> a-    PVar _ v -> -     let v' = tmpVarName v-         PhV var = case getMaybeElem v' (tmpVars ts) :: Maybe (PhasedValueVar a) of -                     Nothing ->  error $ "Copilot error: variable " ++ v' -                                   ++ " was not defined!."-                     Just (PhV var') -> PhV var' in-     (v', A.exactPhase 0 $ -            A.atom (sampleStr ++ normalizeVar v') $ -               var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v)-     ) : a-    PArr _ (arr, idx) -> -         let arr' = tmpArrName arr (show idx)-             PhIdx i = getIdx arr' idx (tmpIdxs ts)-             PhA arrV = -               case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of-                 Nothing -> error "Error in fucntion sampleExts."-                 Just x -> x in-         (arr', A.exactPhase 0 $ -            A.atom (sampleStr ++ normalizeVar arr') $ -               arrV A.<== A.array' (getSampleFuncVar arr)-                                   (atomType (unit::a)) A.!. i-            ) : a-    F _ _ s0 -> sampleExts' s0 a-    F2 _ _ s0 s1 -> sampleExts' s0 $ sampleExts' s1 a-    F3 _ _ s0 s1 s2 -> sampleExts' s0 $ sampleExts' s1 $-                         sampleExts' s2 a-    Append _ s0 -> sampleExts' s0 a-    Drop _ s0 -> sampleExts' s0 a-  where -    sampleExts' :: Streamable b => Spec b -> [(Var, A.Atom ())] -> [(Var, A.Atom ())]-    sampleExts' s' a' = sampleExts outputs ts cFileName s' a'-    getSampleFuncVar v = -      case v of-        ExtV extV -> extV-        -- XXX A bit of a hack.  Atom should be changed to allow "out-of-Atom"-        -- assignments.  But this works for now.-        Fun nm args -> funcShow cFileName nm args----- lookup the idx for external array accesses in the map.-getIdx :: forall a. (Streamable a, A.IntegralE a) -       => Var -> Spec a -> StreamableMaps PhasedValueIdx -> PhasedValueIdx a-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 ++ "."---- TRIGGERS --------------------------------- | To make customer C triggers.  Only for Spec Bool (others throw an--- error).  -makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom ()-makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = -  do r -     (A.exactPhase 3 $ A.atom (show trigger) $ -        do A.cond (getOutput outputs s)-           fnCall cFileName fnName args)---- | Building an external function call in Atom.-fnCall :: Name -> String -> Args -> A.Atom ()-fnCall cFileName fnName args = -  A.action (\_ -> funcShow cFileName fnName args) []--getOutput :: Streamable a => Outputs -> Spec a -> A.E a-getOutput outputs s = -  case s of-    (Var v) -> A.value -      (case getMaybeElem v outputs of-         Nothing -> error $ "Copilot error in trigger specification: variable " -                      ++ v ++ " was not defined!."-         Just v' -> v')-    (Const c) -> A.Const c-    _ -> error "Impossible error in getOutput in Compiler.hs."

@@ -1,591 +0,0 @@-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, -    FlexibleInstances, TypeSynonymInstances #-}---- | Provides basic types and functions for other parts of /Copilot/.------ If you wish to add a new type, you need to make it an instance of @'Streamable'@,--- to add it to @'foldStreamableMaps'@, @'mapStreamableMaps'@, and optionnaly --- to add an ext[Type], a [type] and a var[Type]--- functions in Language.hs to make it easier to use. -module Language.Copilot.Core (-        Period, Var, Name, Port(..), Ext(..),-        Exs, ExtRet(..), Args, ArgConstVar(..),-        Spec(..), Streams, Stream, -        Trigger(..), Triggers, LangElems(..),-	Streamable(..), StreamableMaps(..), emptySM,-        isEmptySM, getMaybeElem, getElem, -        foldStreamableMaps, -        mapStreamableMaps, mapStreamableMapsM,-        filterStreamableMaps, normalizeVar, getVars, Vars,-        getAtomType, getSpecs, getTriggers, vPre, funcShow,-        notConstVarErr-    ) where--import qualified Language.Atom as A--import Data.Int-import Data.Word-import Data.List hiding (union)-import qualified Data.Map as M-import Text.Printf-import Control.Monad.Writer (Writer, Monoid(..), execWriter)------ Type hierarchy for the copilot language --------------------------------------- | Names of the streams or external variables-type Var = String--- | C file name-type Name = String--- | Atom period -- used as an option to control the duration of a Copilot "tick".-type Period = Int--- -- | Phase of an Atom phase--- type Phase = Int--- | Port over which to broadcast information-data Port = Port Int---- | 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-    Var :: Streamable a => Var -> Spec a-    Const :: Streamable a => a -> Spec a--    PVar :: Streamable a => A.Type -> Ext -> Spec a-    PArr :: (Streamable a, Streamable b, A.IntegralE b) -         => A.Type -> (Ext, Spec b) -> 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--    Append :: Streamable a => [a] -> Spec a -> Spec a-    Drop :: Streamable a => Int -> Spec a -> Spec a---- | Arguments to be passed to a C function.  Either a Copilot variable or a--- constant.  A little hacky that I store constants as strings so we don't have--- to pass around types.  However, these data are just used to make external C--- calls, for which we have no type info anyway, so it's a bit of a moot point.-data ArgConstVar = V Var-                 | C String-  deriving Eq--instance Show ArgConstVar where -  show args = case args of-                V v -> normalizeVar v-                C c -> "_const_" ++ c ++ "_"--type Args = [ArgConstVar]--data Trigger =-  Trigger { trigVar  :: Spec Bool-          , trigName :: String-          -- We carry around both the value and the vars of the arguments to be-          -- passed to the trigger.  The vars are used to put the arguments in-          -- the correct order, since the values are stored in a map, destroying-          -- their order.-          , trigArgs :: Args} --type Triggers = M.Map String Trigger--instance Show Trigger where -  show (Trigger s fnName args) =-    "trigger_" ++ notConstVarErr s show ++ "_" ++ fnName ++ "_" ++ normalizeVar (show args)--  -- getMaybeVar :: Streamable a => Spec a -> Var-  -- getMaybeVar (Var v) = v-  -- getMaybeVar s = -  --   error $ "Expected a Copilot variable but provided " ++ show s ++ " instead."---- XXX change the constructors to SimpleVar and Function (or something like that)--- XXX in Ext, we throw away the type info for Args.  This is because we're just--- making external calls, and we don't know anything about the types anyway (we--- just make strings).  Remove from the datatype.---- | Holds external variables or external functions to call.-data Ext = ExtV Var-         | Fun String Args--instance Show Ext where-  show (ExtV v) = v-  show (Fun f args) = normalizeVar f ++ show args--type Exs = (A.Type, Ext, ExtRet)--data ExtRet = ExtRetV -            | ExtRetA ArgConstVar-  deriving Eq---- | For calling a function with Atom variables.-funcShow :: Name -> String -> Args -> String-funcShow cName fname args = -  fname ++ "(" ++ (unwords $ intersperse "," -    (map (\arg -> case arg of-                    v@(V _) -> vPre cName ++ show v-                    C c -> c-         ) args)) ++ ")"--instance Eq Ext where-  (==) (ExtV v0) (ExtV v1) = v0 == v1-  (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1  -  (==) _ _ = False---- These belong in Language.hs, but we don't want orphan instances.-instance (Streamable a, A.NumE a) => Num (Spec a) where-    (+) = F2 (+) (+) -- A.NumE a => E a is an instance of Num-    (*) = 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-"Copilot.Core dropConst" forall i x. Drop i (Const x) = Const x-"Copilot.Core FConst" forall fI fC x0. F fI fC (Const x0) = Const (fI x0)-"Copilot.Core F2Const" forall fI fC x0 x1. F2 fI fC (Const x0) (Const x1) = Const (fI x0 x1)-"Copilot.Core F3Const" forall fI fC x0 x1 x2. F3 fI fC (Const x0) (Const x1) (Const x2) = Const (fI x0 x1 x2)-    #-}--instance Eq a => Eq (Spec a) where-    (==) (PVar t v) (PVar t' v') = t == t' && v == v' -- && ph == ph'-    (==) (PArr t (v, idx)) (PArr t' (v', idx')) = -           t == t' && v == v' && show idx == show idx' -- && ph == ph'-    (==) (Var v) (Var v') = v == v'-    (==) (Const x) (Const x') = x == x'-    (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s'-    (==) s@(F2 _ _ _ _) s'@(F2 _ _ _ _) = show s == show s'-    (==) s@(F3 _ _ _ _ _) s'@(F3 _ _ _ _ _) = show s == show s'-    (==) (Append ls s) (Append ls' s') = ls == ls' && s == s'-    (==) (Drop i s) (Drop i' s') = i == i' && s == s'-    (==) _ _ = False---- | Copilot variable reference, taking the name of the generated C file.-vPre :: Name -> String-vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "."---- -- | An instruction to send data on a port at a given phase.  --- -- data Send a = Sendable a => Send (Var, Phase, Port)--- data Send a =  ---   Send { sendVar  :: Spec a ---        , sendPort :: Port---        , sendName :: String}---- instance Streamable a => Show (Send a) where ---   show (Send s (Port port) portName) = ---     portName ++ "_port_" ++ show port ++ "_var_" ++ getMaybeVar s-                            --- | Holds all the different kinds of language elements that are pushed into the--- Writer monad.  This currently includes the actual specs and trigger--- directives. (Use the functions in Language.hs to make sends and triggers.)-data LangElems = LangElems -       { strms :: StreamableMaps Spec-       , trigs :: Triggers}---- | Container for mutually recursive streams, whose specifications may be--- parameterized by different types-type Streams = Writer LangElems ()--getSpecs :: Streams -> StreamableMaps Spec-getSpecs streams = -  let (LangElems ss _) = execWriter streams-  in  ss--getTriggers :: Streams -> Triggers-getTriggers streams = -  let (LangElems _ triggers) = execWriter streams-  in  triggers---- | A named stream-type Stream a = Streamable a => (Var, Spec a)---- | If the 'Spec' isn't a 'Var' or 'Const', then throw an error; otherwise,--- apply the function.-notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b-notConstVarErr s f = f $-  case s of-    Var v -> V v-    Const c -> C (showAsC c)-    _     -> error $ "You provided specification \n" ++ "  " ++ show s -                        ++ "\n where you needed to give a Copilot variable or constant."----- | Holds the complete specification of a distributed monitor--- type DistributedStreams = (Streams, Sends)------ General functions on streams -------------------------------------------------- | A type is streamable iff a stream may emit values of that type--- --- There are very strong links between @'Streamable'@ and @'StreamableMaps'@ :--- the types aggregated in @'StreamableMaps'@ are exactly the @'Streamable'@--- types and that invariant should be kept (see methods)-class (A.Expr a, A.Assign a, Show a) => Streamable a where-    -- | Provides access to the Map in a StreamableMaps which store values-    -- of the good type-    getSubMap :: StreamableMaps b -> M.Map Var (b a)--    -- | Provides a way to modify (mostly used for insertions) the Map in a-    -- StreamableMaps which store values of the good type-    updateSubMap :: (M.Map Var (b a) -> M.Map Var (b a)) -                 -> StreamableMaps b -> StreamableMaps b--    -- | A default value for the type @a@. Its value is not important.-    unit :: a-    -    -- | A constructor to produce an @Atom@ value-    atomConstructor :: Var -> a -> A.Atom (A.V a)--    -- | A constructor to get an @Atom@ value from an external variable-    externalAtomConstructor :: Var -> A.V a--    -- | The argument only coerces the type, it is discarded.  Returns the-    -- format for outputting a value of this type with printf in C-    ---    -- For example "%f" for a float-    typeId :: a -> String-    -    -- | The same, only adds the wanted precision for floating points.-    typeIdPrec :: a -> String-    typeIdPrec x = typeId x-    -    -- | The argument only coerces the type, it is discarded.-    -- Returns the corresponding /Atom/ type.-    atomType :: a -> A.Type-    -    -- | Like Show, except that the formatting is exactly the same as the one of-    -- C for example the booleans are first converted to 0 or 1, and floats and-    -- doubles have the good precision.-    showAsC :: a -> String- -instance Streamable Bool where-    getSubMap = bMap-    updateSubMap f sm = sm {bMap = f $ bMap sm}-    unit = False-    atomConstructor = A.bool-    externalAtomConstructor = A.bool'-    typeId _ = "%i"-    atomType _ = A.Bool-    showAsC x = printf "%u" (if x then 1::Int else 0)-instance Streamable Int8 where-    getSubMap = i8Map-    updateSubMap f sm = sm {i8Map = f $ i8Map sm}-    unit = 0-    atomConstructor = A.int8-    externalAtomConstructor = A.int8'-    typeId _ = "%d"-    atomType _ = A.Int8-    showAsC x = printf "%d" (toInteger x)-instance Streamable Int16 where-    getSubMap = i16Map-    updateSubMap f sm = sm {i16Map = f $ i16Map sm}-    unit = 0-    atomConstructor = A.int16-    externalAtomConstructor = A.int16'-    typeId _ = "%d"-    atomType _ = A.Int16-    showAsC x = printf "%d" (toInteger x)-instance Streamable Int32 where-    getSubMap = i32Map-    updateSubMap f sm = sm {i32Map = f $ i32Map sm}-    unit = 0-    atomConstructor = A.int32-    externalAtomConstructor = A.int32'-    typeId _ = "%d"-    atomType _ = A.Int32-    showAsC x = printf "%d" (toInteger x)-instance Streamable Int64 where-    getSubMap = i64Map-    updateSubMap f sm = sm {i64Map = f $ i64Map sm}-    unit = 0-    atomConstructor = A.int64-    externalAtomConstructor = A.int64'-    typeId _ = "%lld"-    atomType _ = A.Int64-    showAsC x = printf "%d" (toInteger x)-instance Streamable Word8 where-    getSubMap = w8Map-    updateSubMap f sm = sm {w8Map = f $ w8Map sm}-    unit = 0-    atomConstructor = A.word8-    externalAtomConstructor = A.word8'-    typeId _ = "%u"-    atomType _ = A.Word8-    showAsC x = printf "%u" (toInteger x)-instance Streamable Word16 where-    getSubMap = w16Map-    updateSubMap f sm = sm {w16Map = f $ w16Map sm}-    unit = 0-    atomConstructor = A.word16-    externalAtomConstructor = A.word16'-    typeId _ = "%u"-    atomType _ = A.Word16-    showAsC x = printf "%u" (toInteger x)-instance Streamable Word32 where-    getSubMap = w32Map-    updateSubMap f sm = sm {w32Map = f $ w32Map sm}-    unit = 0-    atomConstructor = A.word32-    externalAtomConstructor = A.word32'-    typeId _ = "%u"-    atomType _ = A.Word32-    showAsC x = printf "%u" (toInteger x)-instance Streamable Word64 where-    getSubMap = w64Map-    updateSubMap f sm = sm {w64Map = f $ w64Map sm}-    unit = 0-    atomConstructor = A.word64-    externalAtomConstructor = A.word64'-    typeId _ = "%llu"-    atomType _ = A.Word64-    showAsC x = printf "%u" (toInteger x)-instance Streamable Float where-    getSubMap = fMap-    updateSubMap f sm = sm {fMap = f $ fMap sm}-    unit = 0-    atomConstructor = A.float-    externalAtomConstructor = A.float'-    typeId _ = "%f"-    typeIdPrec _ = "%.5f"-    atomType _ = A.Float-    showAsC x = printf "%.5f" x-instance Streamable Double where-    getSubMap = dMap-    updateSubMap f sm = sm {dMap = f $ dMap sm}-    unit = 0-    atomConstructor = A.double-    externalAtomConstructor = A.double'-    typeId _ = "%lf"-    typeIdPrec _ = "%.10lf"-    atomType _ = A.Double-    showAsC x = printf "%.10f" x---- | Lookup into the map of the right type in @'StreamableMaps'@-{-# INLINE getMaybeElem #-}-getMaybeElem :: Streamable a => Var -> StreamableMaps b -> Maybe (b a)-getMaybeElem v sm = M.lookup v $ getSubMap sm---- | Lookup into the map of the right type in @'StreamableMaps'@--- Launch an exception if the index is not in it-{-# INLINE getElem #-}-getElem :: Streamable a => Var -> StreamableMaps b -> b a-getElem v sm = -  case getMaybeElem v sm of-    Nothing -> error $ "Error in application of getElem from Core.hs for variable "-                 ++ v ++ "."-    Just x -> x--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. -    (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.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--{-# INLINE mapStreamableMaps #-}-mapStreamableMaps :: forall s s'. -    (forall a. Streamable a => Var -> s a -> s' a) -> -    StreamableMaps s -> StreamableMaps s'-mapStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =-    SM {-            bMap = M.mapWithKey f bm,-            i8Map = M.mapWithKey f i8m,-            i16Map = M.mapWithKey f i16m,-            i32Map = M.mapWithKey f i32m,-            i64Map = M.mapWithKey f i64m,-            w8Map = M.mapWithKey f w8m,-            w16Map = M.mapWithKey f w16m,-            w32Map = M.mapWithKey f w32m,-            w64Map = M.mapWithKey f w64m,-            fMap = M.mapWithKey f fm,-            dMap = M.mapWithKey f dm-        }--{-# INLINE mapStreamableMapsM #-}-mapStreamableMapsM :: forall s s' m. Monad m => -    (Streamable a => Var -> s a -> m (s' a)) -> -    StreamableMaps s -> m (StreamableMaps s')-mapStreamableMapsM f sm =-    foldStreamableMaps (-            \ v s sm'M ->  do-                    sm' <- sm'M-                    s' <- f v s-                    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 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) == [])-    where-        filterElem :: forall a. Streamable a => Var -> c a -> -            (StreamableMaps c, [(A.Type, Var)]) -> -            (StreamableMaps c, [(A.Type, Var)])-        filterElem v s (sm', l2) =-            let x = (atomType (unit::a), v) in-            if x `elem` l'-                then (updateSubMap (\m -> M.insert v s m) sm', x:l2)-                else (sm', l2)-        l' = nub $ map (\(x,y,_) -> (x,y)) l---- | This is a generalization of @'Streams'@--- which is used for storing Maps over values parameterized by different types.------ It is extensively used in the internals of Copilot, in conjunction with--- @'foldStreamableMaps'@ and @'mapStreamableMaps'@-data StreamableMaps a =-    SM {-            bMap   :: M.Map Var (a Bool),-            i8Map  :: M.Map Var (a Int8),-            i16Map :: M.Map Var (a Int16),-            i32Map :: M.Map Var (a Int32),-            i64Map :: M.Map Var (a Int64),-            w8Map  :: M.Map Var (a Word8),-            w16Map :: M.Map Var (a Word16),-            w32Map :: M.Map Var (a Word32),-            w64Map :: M.Map Var (a Word64),-            fMap   :: M.Map Var (a Float),-            dMap   :: M.Map Var (a Double)-        }--instance Monoid (StreamableMaps Spec) where-  mempty = emptySM-  mappend x y = overlap x y--instance Monoid LangElems where-  mempty = LangElems emptySM M.empty-  mappend (LangElems x z) (LangElems x' z') = -    LangElems (overlap x x') (M.union z z') -overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s -overlap x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) -        y@(SM bm' i8m' i16m' i32m' i64m' w8m' w16m' w32m' w64m' fm' dm') =-  let multDefs = (getVars x `intersect` getVars y)-  in  if null multDefs then union-        else error $    "Copilot error: The variables " -                     ++ show multDefs ++ " have multiple definitions."-  where union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m') -                   (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m') -                   (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m') -                   (M.union fm fm') (M.union dm dm')---- | Get the Copilot variables.-getVars :: StreamableMaps s -> [Var]-getVars streams = foldStreamableMaps (\k _ ks -> k:ks) streams []                         ---- | An empty streamableMaps. -emptySM :: StreamableMaps a-emptySM = SM-    {-        bMap = M.empty, -        i8Map = M.empty,-        i16Map = M.empty,-        i32Map = M.empty,-        i64Map = M.empty,-        w8Map = M.empty,-        w16Map = M.empty,-        w32Map = M.empty,-        w64Map = M.empty,-        fMap = M.empty,-        dMap = M.empty -    }---- | Verifies if its argument is equal to emptySM-isEmptySM :: StreamableMaps a -> Bool-isEmptySM (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) = -    M.null bm &&-        M.null i8m &&-        M.null i16m &&-        M.null i32m &&-        M.null i64m &&-        M.null w8m &&-        M.null w16m &&-        M.null w32m &&-        M.null w64m &&-        M.null fm &&-        M.null dm ---- | Replace all accepted special characters by sequences of underscores.  -normalizeVar :: Var -> Var-normalizeVar v = -  map (\c -> if (c `elem` ".[]()") then '_' else c)-      (filter (\c -> c /= ',' && c /= ' ') v) ---- | For each typed variable, this type holds all its successive values in an infinite list--- Beware : each element of one of those lists corresponds to a full @Atom@ period, --- not to a single clock tick.-type Vars = StreamableMaps []---- Pretty printer: can't put in PrettyPrinter since that causes circular deps.--instance Show a => Show (Spec a) where-    show s = showIndented s 0--showIndented :: Spec a -> Int -> String-showIndented s n =-    let tabs = concat $ replicate n "  " in-    tabs ++ showRaw s n--showRaw :: Spec a -> Int -> String-showRaw (PVar t v) _ = "PVar " ++ show t ++ " " ++ show v -- ++ " " ++ show ph-showRaw (PArr t (v, idx)) _ = -  "PArr " ++ show t ++ " (" ++ show v ++ " ! (" ++ show idx ++ "))" -- ++ show ph-showRaw (Var v) _ = "Var " ++ v-showRaw (Const e) _ = show e-showRaw (F _ _ s0) n = -    "F op? (\n" ++ -        showIndented s0 (n + 1) ++ "\n" ++ -        (concat $ replicate n "  ") ++ ")"-showRaw (F2 _ _ s0 s1) n = -    "F2 op? (\n" ++-        showIndented s0 (n + 1) ++ "\n" ++ -        showIndented s1 (n + 1) ++ "\n" ++ -        (concat $ replicate n "  ") ++ ")"-showRaw (F3 _ _ s0 s1 s2) n = -    "F3 op? (\n" ++ -        showIndented s0 (n + 1) ++ "\n" ++ -        showIndented s1 (n + 1) ++ "\n" ++ -        showIndented s2 (n + 1) ++ "\n" ++ -        (concat $ replicate n "  ") ++ ")"-showRaw (Append ls s0) n = -    "Append " ++ show ls ++ " (\n" ++-        showIndented s0 (n + 1) ++ "\n" ++ -        (concat $ replicate n "  ") ++ ")"-showRaw (Drop i s0) n = -    "Drop " ++ show i ++ " (\n" ++-        showIndented s0 (n + 1) ++ "\n" ++ -        (concat $ replicate n "  ") ++ ")"---

@@ -1,246 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}---- | The Dispatch module : does all the IO, and offers an unified interface to both--- the interpreter and the compiler.------ Also communicates with GCC in order to compile the C code, and then transmits--- the results of the execution of that C code.  This functionnality is mostly--- 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--import Language.Copilot.Core-import Language.Copilot.Analyser (check, getExternalVars)-import Language.Copilot.Interpreter-import Language.Copilot.AtomToC-import Language.Copilot.Compiler-import Language.Copilot.PrettyPrinter ()--import qualified Language.Atom as A-import qualified Data.Map as M--import System.Directory -import System.Process-import System.IO-import Control.Monad--data AtomToC = AtomToC -    { cName :: Name -- ^ Name of the C file to generate-    , gccOpts :: String -- ^ Options to pass to the compiler-    , getPeriod :: Maybe Period -- ^ The optional period-    , interpreted :: Interpreted -- ^ Interpret the program or not-    , outputDir :: String -- ^ Where to put the executable-    , compiler :: String -- ^ Which compiler to use-    , sim :: Bool -- ^ Are we running a C simulator?-    , prePostCode :: (Maybe String, Maybe String) -- ^ Code to replace the default-                                                  -- initialization and main-    , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we-                                 -- don't know how large external arrays are, so-                                 -- we cannot declare them.  Passing in pairs-                                 -- containing the name of the array and it's-                                 -- size allows them to be declared.-    , clock :: Maybe A.Clock     -- Use the hardware clock to drive the timing-                                 -- of the program.-    }--data BackEnd = Opts AtomToC -             | Interpreter--data Interpreted = Interpreted | NotInterpreted-type Iterations = Int-data Verbose = OnlyErrors | DefaultVerbose | Verbose deriving Eq---- | This function is the core of /Copilot/ :--- it glues together analyser, interpreter and compiler, and does all the IO.--- It can be called either from interface (which justs decodes the command-line argument)--- or directly from the interactive prompt in ghci.--- @streams@ is a specification, --- @inputExts@ allows the user to give at runtime values for---      the monitored variables. Useful for testing on randomly generated values and specifications,---      or for the interpreted version.--- @be@ chooses between compilation or interpretation,---      and if compilation is chosen (AtomToC) holds a few additionnal informations.---      see description of @'BackEnd'@--- @iterations@ just gives the number of periods the specification must be executed.---      If you would rather execute it by hand, then just choose AtomToC for backEnd and 0 for iterations--- @verbose@ determines what is output.-dispatch :: LangElems -> Vars -> BackEnd -> Iterations -> Verbose -> IO ()-dispatch elems inputExts backEnd iterations verbose =-    do-        hSetBuffering stdout LineBuffering-        mapM_ putStrLn preludeText -        isValid <--            case check (strms elems) of-                Just x -> print x >> return False-                Nothing -> return True-        when isValid $-            -- because haskell is lazy, will only get computed if later used-            let interpretedLines = showVars (interpretStreams (strms elems) trueInputExts) -                                     iterations -            in case backEnd of-                Interpreter -> -                    do-                        unless allInputsPresents $ error errMsg-                        mapM_ putStrLn interpretedLines-                Opts opts ->-                    let isInterpreted =-                            case (interpreted opts) of-                                Interpreted -> True-                                NotInterpreted -> False-                        dirName = outputDir opts-                    in do-                        putStrLn $ "Trying to create the directory " ++ dirName -                                     ++  " (if missing)  ..."-                        createDirectoryIfMissing False dirName-                        copilotToC elems 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)-                              unless (f0 == f1) $ removeFile (cName opts ++ ext)-                        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 (sim opts) (gccCall (Opts opts))-                        when ((isInterpreted || isExecuted) && not allInputsPresents) $ -                            error errMsg-                        when isExecuted $ execute (strms elems) (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-        allExts = getExternalVars (strms elems)-        (trueInputExts :: StreamableMaps [] , allInputsPresents :: Bool) = -          filterStreamableMaps inputExts (map (\(a,v,r) -> (a, show v, r)) allExts)--copilotToC :: LangElems -> [Exs] -> Vars -> AtomToC -> Bool -> IO ()-copilotToC elems allExts trueInputExts opts isVerbose =-    let cFileName = cName opts-        (p', program) = copilotToAtom elems (getPeriod opts) cFileName-        (preCode, postCode) = -            getPrePostCode (sim opts) (prePostCode opts) cFileName -                           (strms elems) allExts (map (\(x,y) -> (ExtV x,y)) -                           (arrDecs opts)) trueInputExts p'-            -- case (prePostCode opts) of-            --     Nothing ->  -            --       getPrePostCode cFileName (strms elems) allExts -            --                      (map (\(x,y) -> (ExtV x,y)) (arrDecs opts))-            --                      trueInputExts p'-            --     Just (pre, post) -> (pre, post)-        atomConfig = A.defaults -            { A.cCode = \_ _ _ -> (preCode, postCode)-            , A.cRuleCoverage = False-            , A.cAssert = False-            , A.hardwareClock = clock opts-            , A.cStateName = "copilotState" ++ cFileName-            }-    in do-        putStrLn $ "Compiling Copilot specs to C  ..."-        (sched, _, _, _, _) <- A.compile cFileName atomConfig program-        when isVerbose (putStrLn $ A.reportSchedule sched)-        putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"---- | Call Gcc to compile the code.-gccCall :: BackEnd -> IO ()-gccCall backend = -  case backend of-    Interpreter -> error "Impossible: gccCall called with Interpreter."-    Opts opts   -> -      let dirName = outputDir opts-          programName = cName opts-      in-        do-          let command = compiler opts ++ " " ++ dirName ++ cName opts -                        ++ ".c" ++ " -o " ++ dirName ++ programName -                        ++ " " ++ gccOpts opts-          putStrLn "Calling the C compiler  ..."-          putStrLn command-          _ <- system command-          return ()--execute :: StreamableMaps Spec -> String -> Vars -> Bool -> [String] -> Iterations -> Bool -> IO ()-execute streams programName trueInputExts isInterpreted interpretedLines iterations isSilent =-    do  (Just hin, Just hout, _, _) <- createProcess processConfig-        hSetBuffering hout LineBuffering-        hSetBuffering hin LineBuffering--        when isInterpreted -                 (do putStrLn "\n *** Checking the randomly-generated Copilot specification: ***\n"-                     print streams)-        let inputVar v (val:vals) ioVars =-                do  hPutStr hin (showAsC val ++ " \n")-                    hFlush hin-                    vars <- ioVars-                    return $ updateSubMap (\m -> M.insert v vals m) vars-            inputVar _ [] _ = error "Impossible : empty inputVar"-            executePeriod _ [] 0 = putStrLn "Execution complete." -            executePeriod _ [] _ = error "Impossible : empty ExecutePeriod"-            executePeriod inputExts (inLine:inLines) n =-                when (n > 0) $ -                    do  nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM)-                        line <- hGetLine hout-                        let nextPeriod = -                                (unless isSilent $ putStrLn line) >> -                                    executePeriod nextInputExts inLines (n - 1)-                        -- Checking the compiler and interpreter.-                        if isInterpreted-                            then if inLine == line-                                       then nextPeriod-                                       else error $ unlines -                                              [ "Failure: interpreter /= compiler"-                                              , "  program name: " ++ programName-                                              , "  interpreter: " ++ inLine-                                              , "  compiler: "    ++ line-                                              ]-                            else nextPeriod-                            -        -- useful for initializing the sampling temporary variables-        firstInputExts <- foldStreamableMaps inputVar trueInputExts (return emptySM)-        executePeriod firstInputExts interpretedLines iterations-    where-        processConfig = -            (shell $ programName ++ " " ++ show iterations)-            {std_in = CreatePipe, std_out = CreatePipe, std_err = UseHandle stdout}--showVars :: Vars -> Int-> [String]-showVars interpretedVars n =-    showVarsLine interpretedVars 0-    where-        showVarsLine inVs i =-            if i == n -                then []-                else -                    let (string, inVs') = foldStreamableMaps prettyShow inVs ("", emptySM) -                        endString = showVarsLine inVs' (i + 1) -                        beginString = "period: " ++ show i ++ "   " ++ string -                    in-                    beginString:endString-        prettyShow v l (s, vs) =-            let s' = v ++ ": " ++ showAsC (head l) ++ "   " ++ s-                vs' = updateSubMap (\ m -> M.insert v (tail l) m) vs in-            (s', vs')-                -preludeText :: [String]-preludeText = -    [ ""-    , "========================================================================="-    , "  CoPilot, a stream language for generating hard real-time C monitors.  "-    , "========================================================================="-    , "Copyright, Galois, Inc. 2010"-    , "BSD3 License" -    , "Website: http://leepike.github.com/Copilot/"-    , "Maintainer: Lee Pike <leepike--at--gmail.com> (remove dashes)."-    , "Usage: > help"-    , "========================================================================="-    , ""-    ]

@@ -1,372 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}--module Language.Copilot.Examples.Examples where--import Data.Word-import Prelude (($))-import qualified Prelude as Prelude-import qualified Prelude as P---- for specifying options-import Data.Map (fromList) ---import Data.Maybe (Maybe (..))---import System.Random--import Language.Copilot --- import Language.Copilot.Variables--fib :: Streams-fib = do-  let f = varW64 "f"-      t   = varB "t"-  f .= [0,1] ++ f + (drop 1 f)-  t .= even f-    where even :: Spec Word64 -> Spec Bool-          even w' = w' `mod` 2 == 0--t1 :: Streams-t1 = do-  let x = varI32 "x"-      y = varB "y"-      z = varB "z"-      w = varB "w"-  x .= [0, 1, 2] ++ x - (drop 1 x)-  y .= [True, False] ++ y ^ z-  z .= x <= drop 1 x-  w .= 3 == x---- t2 :: Streams--- t2 = do---      a .= [True] ++ not (var a) ---      b .= mux (var a) 2 (int8 3) ---- t3 :: use an external variable called ext, typed Word32-t3 :: Streams-t3 = do-  let a    = varW32 "a"-      b    = varB "b"-      ext8 = extW32 "ext"-      ext1 = extW32 "ext"-  a .= [0,1] ++ a + ext8 + ext8 + ext1-  b .= [True, False] ++ 2 + a < 5 + ext1--t4 :: Streams-t4 = do-  let a = varB "a"-      b = varB "b"-  a .= [True,False] ++ not a-  b .= drop 1 a--t5 :: Streams-t5 = do-  let x = varW16 "x"-      y = varB "y"-      z = varB "z"-  x .= [0] ++ x + 1-  y .= [True, True] ++ y-  z .= [False] ++ not z-  -- triggers-  trigger y "y_trigger" void-  trigger z "z0_trigger" x-  trigger z "z1_trigger" (y <> constW16 3 <> x)-  -yy :: Streams-yy = do-  let a = varW32 "a"---      ans2 = varW32 "ans2"-  a .= [3,5] ++ a + 1---  ans2 .= a--maj1 :: Streams-maj1 = do-  let v0  = varW32 "v0"-      ans2 = varW32 "ans2"-  v0  .= [3,7] ++ v0 + 1-  ans2 .= v0---zz :: Streams-zz = do-  let a = varW32 "a"-      b = varW32 "b"-  --a .= [0..4] ++ drop 4 (varW32 a) + 1-  a .= a + 1-  b .= drop 3 a--xx :: Streams-xx = do-  let a = varW32 "a"-      b = varW32 "b"-      c = varW32 "c"-      e = extW32 "ext"-      d = varB "d"-      f = extW32 (fun "fun1" void) -      h = extArrW16 (fun "g" b) a -      g = extW16 (fun "fun2" (true <> b <> constW16 3))-      w = varB "w"-  a .= e + f-  b .= [3] ++ a-  c .= [0, 1, 3, 4] ++ drop 1 b-  d .= h < g-  -- triggers-  trigger d "y_trigger" void-  trigger w "z0_trigger" (a <> b <> true)-  trigger w "z1_trigger" (d <> constW16 3 <> w)----- | Sending over ports.-distrib :: Streams-distrib = do-  -- vars-  let a = varW8 "a"-      b = varB "b"-  -- spec-  a .= [0,1] ++ a + 1-  b .= mod a 2 == 0 -  -- sends-  trigger true "portA" a -  trigger true "portB" b--monitor :: Streams-monitor = do-  -- external variables-  let word     = extW32 "rx"-      arbiter  = extB "arbiter"-  -- Copilot variables-      words    = varW32 "words"-      arbiters = varB "arbiters"-  words   .=      [0] ++ mux arbiter word words-  arbiters .= [False] ++ mux arbiter false arbiter---- greatest common divisor.-gcd :: Word16 -> Word16 -> Streams-gcd n0 n1 = do-  let a = varW16 "a"-      b = varW16 "b"-  a .= alg n0 a b-  b .= alg n1 b a--  let ans = varB "ans"-  ans .= a == b-    where alg x0 x1 x2 = [x0] ++ mux (x1 > x2) (x1 - x2) x1---- greatest common divisor of two external vars.  Compare to--- Language.Atom.Example Try ------ interpret gcd' 40 $ setE (emptySM {w16Map = ---      fromList [("n", [9,9..]), ("m", [7,7..])]}) baseOpts ------ Note we have to start streams a and b with a dummy value 0 before they can--- sample the external variables.-gcd' :: Streams-gcd' = do -  -- externals-  let n = extW16 "n"-      m = extW16 "m"-  -- copilot vars-      a = varW16 "a"-      b = varW16 "b"-      init = varB "init"-      ans  = varB "ans"-  -  a .= alg n (sub a b) init-  b .= alg m (sub b a) init-  ans .= a == b && not init-  init .= [True] ++ false--  where sub hi lo = mux (hi > lo) (hi - lo) hi-        alg ext ex init = [0] ++ mux init ext ex--testCoercions :: Streams-testCoercions = do-  let word = varW8 "word"-      int = varI16 "int"-  word .= [1] ++ word * (-2)-  int  .= 1 + cast word--testCoercions2 :: Streams-testCoercions2 = do-  let b = varB "b"-      i = varI16 "i"-      j = varI16 "j"-  b .= [True] ++ not b-  i .= cast j-  j .= 3--testCoercions3 :: Streams-testCoercions3 = do-  let x = varB "x"-      y = varI32 "y"-      z = varI32 "z"-  x .= [True, True] ++ not x-  y .= cast x + cast x---  z .= drop 1 (cast x)-  z .= cast (not true)--i8 :: Streams-i8 = let v = varI8 "v" in v .= [0, 1] ++ v + 1 -    -trap :: Streams-trap = do-  let target = varW32 "target"-  target .= [0] ++ target + 1 --  let x = varW32 "x"-  let y = varW32 "y"-  x .= [0,0] ++ y + target-  y .= [0,0] ++ x + target---- vicious :: Streams--- vicious = do ---     "varExt" .= extW32 "ext" 5 ---     "vicious" .= [0,1,2,3] ++ drop 4 (varW32 "varExt") + drop 1 (var "varExt") + var "varExt" ---- testVicious :: Streams--- testVicious = do---     "counter" .= [0] ++ varW32 "counter" + 1 ---     "testVicious" .= [0,0,0,0,0,0,0,0,0,0] ++ drop 8 (varW32 "counter") ---- -- The issue is when a variable v with a prophecy array of length n deps on--- -- an external variable pv with a weight w, and that w > - n + 1 Here, w = 0 and--- -- n = 2, so 0 > -1 holds.  That means that it is impossible to fill the last--- -- case of the prophecy array, because it is not yet known what the external--- -- variable will be worth.  It could be easily forbidden in the analyser.--- -- However theoretically, nothing seems to prevent us form compiling it, we--- -- would only need a way to say that in these case the middle of the prophecy--- -- array should be updated and not the . (it would be safe because if another--- -- variable was to dep on the  of it it would dep on the external--- -- variable with a weight > 0, which is always forbidden).  It is probably--- -- easier for now to just forbid it. But it could become an issue.--- isBugged :: Streams--- isBugged = do---     "v" .= extW16 "ext" 5 ---     "v2" .= [0,1,3] ++ drop 1 (varW16 "v") -    ---- -- The next two examples are currently refused, because they include a--- -- non-negative weighted closed path. But they could be compiled.  More--- -- generally I think that this restriction could be partially lifted to--- -- forbiding non-negative circuits.  However, this would demand longer--- -- prophecyArrays than we have for now.  (and probably a slightly different--- -- algorithm) So even if we partially lift this restriction, a warning should--- -- stay, because it breaks the current easy-to-evaluate bound on the memory--- -- requirement of a Copilot monitor.--- shouldBeRight :: Streams--- shouldBeRight = do---     "v1" .= [0] ++ varI32 "v1" + 1 ---     "v2" .= drop 2 (varI32 "v1") ---- shouldBeRight2 :: Streams--- shouldBeRight2 = do---     "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 + 3 + extArrW16 ("gg", varW16 f) 2 -  -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4 -  -- c .= [True] ++ var c-  -- d .= varB c -  let e = varW16 "e"-  e .= [6,7,8] ++ 3 -- + extArrW16 ("gg", varW16 b) 2---  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 -  let g = varB "g"-  let gg = extArrW16 "gg" e -  g .= gg < 13-  -- h .= [0] ++ drop 1 (varW16 g)----- t3 :: use an external variable called ext, typed Word32-t99 :: Streams-t99 = do-  let ext = extW32 "ext"-      a = varW32 "a"-  a .= [0,1] ++ a + ext + ext + ext --  let b = varB "b"-  b .= [True, False] ++ 2 + a < 5 + ext --t11 :: Streams-t11 = do-  let v = varB "v"-  v .= [False, True, False] ++ v--tdiv :: Streams-tdiv = do-  let a = varW16 "a"-      b = varW16 "b"-  a .= [3] ++ a `div` 5-  b .= [3] ++ a `mod` 5--extT :: Streams-extT = do-  let x = extW16 "x"-  let y = varW16 "y"-  y .= x ---- Examples:-interpretExtT :: Prelude.IO ()-interpretExtT =-  interpret extT 10 $ -    setE (emptySM {w16Map = fromList [("x", [8,9..])]})-      baseOpts-compileExtT :: P.IO ()-compileExtT =-  compile extT "extT" $ setCode (P.Just "#include \"mylib.h\"", P.Nothing) baseOpts---- Testing error checking for badly-formed external sampling.---- Should fail.-extT2 :: Streams-extT2 = do-  let y = varW16 "y"-      x = extW16 (fun "f" y)-  y .= x ---- Should pass.-extT3 :: Streams-extT3 = do-  let y = varW16 "y"-      x = extW16 (fun "f" y)-  y .= [3] ++ x ---- Should fail.-extT4 :: Streams-extT4 = do-  let y = varW16 "y"-      x = extArrW16 "arr" y-      z = extW16 "z"-      w = varW16 "w"-  y .= z-  w .= x---- Should fail.-extT5 :: Streams-extT5 = do-  let y = varW16 "y"-      x = extW16 (fun "f" y)-      z = extW16 "z"-      w = varW16 "w"-  y .= z-  w .= x---- Should work.-extT6 :: Streams-extT6 = do-  let y = varW16 "y"-      x = extArrW16 "arr" y-      z = extW16 "z"-      w = varW16 "w"-  y .= [7] ++ z-  w .= x------ test external idx before after and in the stream it references--- test multiple defs--- test defs in functions--- test arrays at different indexes

@@ -1,83 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}--module Language.Copilot.Examples.LTLExamples where--import Prelude (replicate, Int, replicate)-import qualified Prelude as P--import Language.Copilot-import Language.Copilot.Libs.Indexes-import Language.Copilot.Libs.LTL--------------------- LTL tests ------------------------ Can be tested with various values of val.  Use the interpreter to see the--- outputs.--testing, output :: Spec Bool-testing = varB "testing"-output = varB "output"--tSoonest :: Int -> Streams-tSoonest val = do -  testing .= replicate (val+2) False ++ true-  let out = varI16 "out"-  out     .= soonest val testing--tLatest :: Int -> Streams-tLatest val = do -  testing .= replicate (val-2) False ++ true-  let out = varI16 "out"-  out     .= latest val testing--tAlways :: Int -> Int -> Streams-tAlways i1 i2 = do -  testing .=    (replicate i1 True P.++ [False]) ++ true-  output  `ltl` always i2 testing--tNext :: Int -> Streams-tNext i1 = do -  testing .=    (replicate i1 False P.++ [True]) ++ false-  output  `ltl` next testing--tFuture :: Int -> Int -> Streams-tFuture i1 i2 = do -  testing .=    (replicate i1 False P.++ [True]) ++ testing-  output  `ltl` eventually i2 testing---c, t0, t1 :: Spec Bool-t0 = varB "t0"-t1 = varB "t1"-c = varB "c"--tUntil :: Int -> Int -> Int -> Streams-tUntil i1 i2 i3 = do -  t1   .=    replicate i1 False ++ true-  t0   .=    replicate i2 True ++ false-  output `ltl` until i3 t0 t1--tRelease0 :: Int -> Streams-tRelease0 val = output `ltl` release val false true--tRelease1 :: Int -> Int -> Streams-tRelease1 i1 i2 = do -  t1   .=    replicate i1 True ++ c-  c    .=    [False] ++ not c-  t0   .=    true-  output `ltl` release i2 t0 t1-          -testRules :: Streams-testRules = do-  let v1 = varB "v1"-      v2 = varB "v2"-      v3 = varI16 "v3"-      v4 = varB "v4"-      ex = extI8 "ex" -  v1 .=    (not true) || v2-  v2 .=    [True, False] ++ [True] ++ v3 < cast ex-  v3 .=    0 + drop 3 6-  v4 `ltl` always 5 v1-

@@ -1,132 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}--module Language.Copilot.Examples.PTLTLExamples where--import Prelude (($), repeat, replicate, IO())-import qualified Prelude as P-import Data.Map (fromList)--import Language.Copilot hiding (check)-import Language.Copilot.Libs.PTLTL-import Language.Copilot.Libs.Vote---- Next examples are for testing of the ptLTL library---- test of previous-tstdatprv :: Streams-tstdatprv = do-  let a = varB "a"-  a .= [True, False] ++ a -               -tprv :: Streams-tprv = do-  let c = varB "c"-      a = varB "a"-  tstdatprv -  c `ptltl` previous a---- test of alwaysBeen-tstdatAB ::  Streams-tstdatAB = do-  let d = varB "d"-  d .= [True, True, True, True, True, True, True, False] ++ d--tAB :: Streams-tAB = do-   let f = varB "f"-       d = varB "d"-   tstdatAB -   f `ptltl` alwaysBeen d---- test of eventuallyPrev-tstdatEP ::  Streams-tstdatEP = do-  let g = varB "g"-  g .= [False, False, False, False, False, True, False] ++ g --tEP :: Streams-tEP = do-    let h = varB "h"-        g = varB "g"-    tstdatEP -    h `ptltl` eventuallyPrev g--q1, q2, z :: Spec Bool-q1 = varB "q1"-q2 = varB "q2"-z = varB "z"---- test of since-tstdat1Sin :: Streams-tstdat1Sin = q1 .= [False, False, False, False, True] ++ true --varB "q1"--tstdat2Sin :: Streams-tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2-                  -tSince :: Streams -tSince = do-    tstdat1Sin -    tstdat2Sin -    z `ptltl` (q1 `since` q2)---- with external variables--- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20-tSinExt :: Streams -tSinExt = do-  let e1 = extB "e1"-      e2 = extB "e2"-  z `ptltl` (e1 `since` e2)--tSinExt2 :: Streams -tSinExt2 = do-  let e1 = extB "e1"-      e2 = extB "e2"-      a = varB "a"-      s = varB "s"-      d = varB "d"-      t = varB "t"-      e = varB "e"--  a .= not e1-  s `ptltl` (e2 `since` d)-  t `ptltl` (alwaysBeen $ not a)-  e .= e1 ==> d---- "If the majority of the engine temperature probes exeeds 250 degrees, then--- the cooler is engaged and remains engaged until the majority of the engine--- temperature drops to 250 or below.  Otherwise, trigger an immediate shutdown--- of the engine."-engine :: Streams-engine = do-  -- external vars-  let t0       = extW8 "temp_probe_0"-      t1       = extW8 "temp_probe_1"-      t2       = extW8 "temp_probe_2"-      cooler   = extB  "fan_status"-  -- Copilot vars-      maj      = varW8 "maj"-      check    = varB  "maj_check"-      overHeat = varB  "over_heat"-      monitor  = varB  "monitor"-  -- local vars-      temps    = [t0, t1, t2]-  maj      .= majority temps-  check    .= aMajority temps maj-  overHeat `ptltl` (        (cooler || (maj <= 250 && check)) -                    `since` (maj > 250))-  monitor .= not overHeat-  trigger monitor "shutoff_engine" void---engineRun :: Bool -> IO ()-engineRun b = if b then -  interpret engine 40 $ -    setE (emptySM { bMap  = fromList [("fan_status", replicate 3 False P.++ repeat False)]-                  , w8Map = fromList [ ("temp_probe_0", [240,240..])-                                     , ("temp_probe_1", [240,241..])-                                     , ("temp_probe_2", [240,241..])-                                     ]-                  }) -    baseOpts-  else compile engine "engine" $ setSim baseOpts-

@@ -1,26 +0,0 @@-module Language.Copilot.Examples.StatExamples where--import Prelude ()-import Language.Copilot.Core-import Language.Copilot.Language-import Language.Copilot.Libs.Statistics--t0 :: Streams-t0 = do-  let minV = varW16 "min"-      maxV = varW16 "max"-      sumV = varW16 "sum"-      a = varW16 "a"--  a .= [0..5] ++ a + 6-  minV .= min 3 a-  maxV .= max 3 a-  sumV .= sum 3 a--tMean :: Streams-tMean = do-  let a = varD "a"-      out = varD "out"--  a .= [0..5] ++ a + 6-  out .= mean 4 a

@@ -1,172 +0,0 @@--- | Help to display.-module Language.Copilot.Help (helpStr)--where--helpStr :: String-helpStr =-  unlines-  [ ""-  , "USAGE:"-  , "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 -> Options) -> IO ()"-  , " > interpret STREAMS RNDS (noOpts | [$ OPTS])"-  , "   Executes the interpreter for the Copilot specification STREAMS of type"-  , "   'Streams', where the specification is interpreted as a set of mutually-"-  , "   recursive Haskell infinite lists.  The output from the lists is given"-  , "   for RNDS indexes.  RNDS must be greater than 0."-  , ""-  , " compile :: Streams -> String -> (Options -> Options) -> IO ()"-  , " > compile STREAMS FILENAME (noOpts | [$ OPTS])"-  , "   Compiles the Copilot specification STREAMS to constant-time & constant-"-  , "   constant-space C program named FILENAME.c with header FILENAME.h"-  , "   and executable FILENAME."-  , ""-  , " > test RNDS (noOpts | [$ OPTS])"-  , "   Generates a random set of streams & inputs for external variables, and"-  , "   tests the equivalence between the output of the compiled C program and"-  , "   the interpreter over RNDS rounds.  RNDS must be greater than 0.  This"-  , "   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.  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 :: FilePath -> Int -> String -> IO () (FilePath is a synonym for String)"-  , " > verify PATH/FILE.c n opts (opts are additional options for cbmc.)"-  , "   Calls cbmc, developed by Daniel Kroening \& Edmund Clarke"-  , "   <http://www.cprover.org/cbmc/> on a C file generated by Copilot."-  , "   cbmc is a bounded model-checker that verifies C programs.  While there"-  , "   should be no incorrect C programs generated by the Copilot compiler,"-  , "   cbmc provides independent evidence of this claim.  Specifically, it"-  , "   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.  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 (see the setSim option)."  -  , "   For more information on the properties checked, see"-  , "   <http://www.cprover.org/cprover-manual/properties.shtml>."-  , ""-  , " > help "-  , "   Displays this help message."-  , ""-  , ""-  , "OPTIONS:"-  , "In the following, we designate the interpreter by (i), the compiler by (c),"-  , "and the test function by (t).  Options are marked by which tool they are"-  , "relevant to; e.g., (i, t) means that an option is relevant to the"-  , "interpreter and test functions."-  , ""-  , "For each option, there is a default described below."-  , ""-  , "  setE :: Vars -> Options -> Options                                    (i)"-  , "    default: Nothing (no assignments)" -  , "    Set the environment for program variables.  E.g., for the spec"-  , ""-  , "    t :: Streams"-  , "    t =  \"a\" .= [0,1] ++ extW32 \"ext0\" 7 + extW32 \"ext1\" 8 "-  , "      .| end"-  , ""-  , "    setE (emptySM {w32Map = fromList "-  , "                     [ (\"ext0\", [0,1..])"-  , "                     , (\"ext1\", [3,3..])]})"-  , "    assigns external variable \"ext0\" the values 0,1,2... and "-  , "    external variable \"ext1\" the values 3,3,3... over Word32 in the"-  , "    sequential rounds.  "-  , ""-  , "  setV :: Verbose -> Options -> Options                           (i, c, t)"-  , "    default: DefaultVerbose"-  , "    Set the verbosity level.  One of OnlyErrors | DefaultVerbose | Verbose."-  , ""-  , "  setGCC :: String -> Options -> Options                             (c, t)"-  , "    default: \"gcc\""-  , "    Sets the compiler to use, given as a path (String) to the executable."-  , ""-  , "  setDir :: String -> Options -> Options                             (c, t)"-  , "    default: \"./\""-  , "    The location for the generated .c, .h, and binary files.  The"-  , "    path can be either absolute or relative, but MUST containing the"-  , "    trailing '/'."-  , ""-  , "  setC :: String -> Options -> Options                               (c, t)"-  , "    default: Nothing"-  , "    Set the additional options to pass to the compiler.  E.g.,"-  , "    setC \"-O2\"."-  , ""-  , "  setP :: Period -> Options -> Options                               (c, t)"-  , "    default: automatically computed minimal period."-  , "    Manually set the number of ticks per period for execution.  An error"-  , "    is returned if the number is too small.  For any program, the number"-  , "    of ticks must be at least 2."-  , ""-  , "  setR :: Int -> Options -> Options                                     (t)"-  , "    default: 0"-  , "    Sets the seed for generating random Copilot specification during"-  , "    testing."-  , ""-  , "  setCode :: (Maybe String, Maybe String) -> Options -> Options         (c)"-  , "    default: (Nothing, Nothing)."-  , "    To place arbitrary C code in the generated file.  The first element of"-  , "    the pair is code to place above the generated code, and the second"-  , "    element is code to place below.  For writing ad-hoc C, please see"-  , "    Language.Copilot.AdHocC (and please add to it and send patches!)."-  , "    For exmple, pre-code might include 'includes'.  Post-code might include"-  , "    a custom main() function."  -  , "" -  , "  setSim :: Options -> Options                                          (c)"-  , "    default: False"-  , "    When used, generates a main() function in the generated C file that"-  , "    includes a driver to call the scheduler to simulate the function and"-  , "    print the reults to standard out.  Additionally, we attempt to compile"-  , "    the code when setSim is used."-  , ""-  , "  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."  -  , ""-  , ""-  , "EXAMPLES:"-  , "The following examples reference Copilot specs defined in"-  , "Language.Copilot.Examples.Examples."-  , ""-  , " > interpret t0 50 baseOpts"-  , "   Interprets t0 for 50 iterations."-  , ""-  , " > interpret t3 40"-  , "     $ setE (emptySM {w32Map = fromList "-  , "                     [ (\"ext0\", [0,1..])"-  , "                     , (\"ext1\", [3,3..])]})"-  , "       $ setV Verbose baseOpts"-  , "   Interpret t3 for 40 iterations, seeding the external variable \"ext\""-  , "   to [0,1,..], with 'Verbose' verbosity."-  , ""-  , " > compile t1 \"t1\" baseOpts"-  , "   Compile Copilot spec t1 to t1.c, t1.h, and executable t1 in the default"-  , "   directory, /tmp/copilot/ .  This is compiled with a simulation main()"-  , ""-  , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100 baseOpts"-  , "   Compile Copilot spec t2 to t2.c, t2.h, and executable t2 in the default"-  , "   directory, /tmp/copilot/ , with optimization level -02 and period 100."-  , "   This is compiled with a simulation main()."-  , ""-  , " > test 1000 baseOpts"-  , "   Compare the compiler and interpreter for a randomly-generated Copilot"-  , "   spec for 1000 iterations."-  , ""-  , " > Prelude.sequence_ [test 10 $ setR x baseOpts | x <- [0..100]]"-  , "   Compare the compiler and interpreter on 100 random seeds generating"-  , "   Copilot specs, for 10 iterations each."-  , ""-  , " > verify \"foo.c\" n baseOpts"-  , "   Calls cbmc on foo.c (where foo.c is in the current directory) and"-  , "   unrolls the program n times."-  ]

@@ -1,263 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}---- | Used by the end-user to easily give its arguments to dispatch.-module Language.Copilot.Interface (-          Options(), baseOpts, test, interpret, compile, verify, interface-        , help , setE, setC, setO, setP, setI, setCode, setN, setV, setR-        , setDir, setGCC, setArrs, setClock, setSim,-        module Language.Copilot.Dispatch-    ) where--import Language.Copilot.Core---import Language.Copilot.Language (opsF, opsF2, opsF3)-import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3)-import Language.Copilot.Tests.Random-import Language.Copilot.Dispatch-import Language.Copilot.Help-import qualified Language.Atom as A (Clock)--import System.Random-import System.Exit-import System.Cmd-import Data.Maybe-import qualified Data.Map as M (empty)-import Control.Monad (when)--data Options = Options {-        optStreams :: Maybe (StreamableMaps Spec), -- ^ If there's no Streams,-                                                   -- then generate random-                                                   -- streams.---        optSends :: StreamableMaps Send, -- ^ For distributed monitors.-        optExts :: Maybe Vars, -- ^ Assign values to external variables.-        optCompile :: Maybe String, -- ^ Set gcc options.-        optPeriod :: Maybe Period, -- ^ Set the period.  If none is given, then-                                   -- the smallest feasible period is computed.-        optInterpret :: Bool, -- ^ Interpreting?-        optIterations :: Int, -- ^ How many iterations are we simulating for?-        optVerbose :: Verbose, -- ^ Verbosity level: OnlyErrors | DefaultVerbose | Verbose.-        optRandomSeed :: Maybe Int, -- ^ Random seed for generating Copilot specs.-        optCName :: Name, -- ^ Name of the C file generated.-        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, Maybe String), -- ^ Code to append above and below the C file.-        optSimulate :: Bool, -- ^ Do we want a simulation driver?-        optTriggers :: Triggers, -- ^ 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.-        optClock :: Maybe A.Clock  -- ^ Use the hardware clock to drive the timing of the program?-    }--baseOpts :: Options-baseOpts = Options {-        optStreams = Nothing,---        optSends = emptySM,-        optExts = Nothing,-        optCompile = Nothing,-        optPeriod = Nothing,-        optInterpret = False,-        optIterations = 0,-        optVerbose = DefaultVerbose,-        optRandomSeed = Nothing,-        optCName = "copilotProgram",-        optCompiler = "gcc",-        optOutputDir = "./",-        optPrePostCode = (Nothing, Nothing),-        optSimulate = False,-        optTriggers = M.empty,-        optArrs = [],-        optClock = Nothing-    }---- Functions for making it easier for configuring copilot in the frequent use cases--test :: Int -> Options -> IO ()-test n opts = -  interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ setSim opts --interpret :: Streams -> Int -> Options -> IO ()-interpret streams n opts = -  interface $ setI $ setN n $ opts {optStreams = Just (getSpecs streams)}--compile :: Streams -> Name -> Options -> IO ()-compile streams fileName opts = -  interface $ setC "-Wall" $ setO fileName -    $ setTriggers (getTriggers streams) -      $ opts {optStreams = Just (getSpecs streams)}--verify :: FilePath -> Int -> String -> IO ()-verify file n opts = do-  putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke."-  putStrLn "<http://www.cprover.org/cbmc/>, with the following checks:"-  putStrLn "  --bounds-check       enable array bounds checks"-  putStrLn "  --div-by-zero-check  enable division by zero checks"-  putStrLn "  --pointer-check      enable pointer checks"-  putStrLn "  --overflow-check     enable arithmetic over- and underflow checks"-  putStrLn "  --nan-check          check floating-point for NaN"-  putStrLn ""-  putStrLn "Assuming main() as the entry point unless specified otherwise (--function f)"-  putStrLn cmd-  code <- system cmd-  case code of-    ExitSuccess -> return ()-    _           -> do putStrLn ""-                      putStrLn $ "An error was returned by cbmc.  This may have be due to cbmc not finding the file " ++ file ++ ".  Perhaps cbmc is not installed on your system, is not in your path, cbmc cannot be called from the command line on your system, or " ++ file ++ " does not exist.  See <http://www.cprover.org/cbmc/>  for more information on cbmc."-    where cmd = unwords ("cbmc" : args)-          args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"-                 , "--nan-check", "--pointer-check"-                 , "--unwind " ++ show n, opts, file] -                   ---- Small functions for easy modification of the Options record---- -- | Set the directives for sending stream values on ports.--- setS :: StreamableMaps Send -> Options -> Options--- setS sends opts = opts {optSends = sends}---- -- | Set the directives for sending stream values on ports.-setTriggers :: Triggers -> Options -> Options-setTriggers triggers opts = opts {optTriggers = triggers}---- | 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..])]}) ... @--- --- sets the external variable names "ext" to take the natural numbers, up to the limit of Word32.-setE :: Vars -> Options -> Options-setE vs opts = opts {optExts = Just vs}---- | Set the external arrays.-setArrs :: [(String,Int)] -> Options -> Options-setArrs ls opts = opts {optArrs = ls}---- | Sets the hardware clock.  See--- http://github.com/tomahawkins/atom/blob/master/Language/Atom/Code.hs.-setClock :: A.Clock -> Options -> Options-setClock clk opts = opts {optClock = Just clk}---- | Sets the options for the compiler, e.g.,------ @ setC \"-O2\" ... @------ Sets gcc options.-setC :: String -> Options -> Options-setC gccOptions opts = opts {optCompile = Just gccOptions}---- | Manually set the period for the program.  Otherwise, the minimum required period is computed automatically.  E.g.,------ @ setP 100 ... @--- sets the period to be 100.  The period must be at least 1.-setP :: Period -> Options -> Options-setP p opts = opts {optPeriod = Just p}--setI :: Options -> Options-setI opts = opts {optInterpret = True}---- | Sets the number of iterations of the program to simulation:------ @ setN 50 @--- simulations the program for 50 steps.-setN :: Int -> Options -> Options-setN n opts = opts {optIterations = n}---- | Set the verbosity level.  -setV :: Verbose -> Options -> Options-setV v opts = opts {optVerbose = v}---- | Set the random seed for generating random `Copilot` specs.-setR :: Int -> Options -> Options-setR seed opts = opts {optRandomSeed = Just seed}--setO :: Name -> Options -> Options-setO fileName opts = opts {optCName = fileName}---- | Sets the compiler to use, given as a path to the executable.  The default--- is \"gcc\".-setGCC :: String -> Options -> Options-setGCC compilerStr opts = opts {optCompiler = compilerStr}---- | Sets the directory into which the output of compiled programs should be--- placed.  If the directory does not exist, it will be created.-setDir :: String -> Options -> Options-setDir dir opts = opts {optOutputDir = dir}---- | Sets the code to precede and follow the copilot specification--- If nothing, then code appropriate for communication with the interpreter is generated-setCode :: (Maybe String, Maybe String) -> Options -> Options-setCode pp opts = opts {optPrePostCode = pp}---- | Include simulation driver code (in a main() loop)?-setSim :: Options -> Options-setSim opts = opts {optSimulate = True}---- | The "main" function that dispatches.-interface :: Options -> IO ()-interface opts =-    do-        seed <- createSeed opts -        let (streams, vars) = getStreamsVars opts seed---            sends = optSends opts-            triggers = optTriggers opts-            backEnd = getBackend opts seed-            iterations = optIterations opts-            verbose = optVerbose opts-        when (verbose == Verbose) $-            putStrLn $ "Random seed :" ++ show seed-        -- dispatch is doing all the heavy plumbing between -        -- analyser, compiler, interpreter, gcc and the generated program-        dispatch (LangElems streams triggers) vars backEnd iterations verbose --createSeed :: Options -> IO Int-createSeed opts =-    case optRandomSeed opts of-        Nothing -> -            do-                g <- newStdGen -                return . fst . random $ g-        Just i -> return i---- | Were streams given?  If not, just make random streams.-getStreamsVars :: Options -> Int -> (StreamableMaps Spec, Vars)-getStreamsVars opts seed = -    case optStreams opts of-        Nothing -> randomStreams opsF opsF2 opsF3 (mkStdGen seed)-        Just s ->-            case optExts opts of-                Nothing -> (s, emptySM)-                Just vs -> (s, vs)-        -getBackend :: Options -> Int -> BackEnd-getBackend opts seed =-    case optCompile opts of-        Nothing -> -            if not $ optInterpret opts-                then error "neither interpreted nor compiled: nothing to be done"-                else Interpreter-        Just gccOptions ->-            Opts $ AtomToC {-                cName     = optCName opts ++ if isJust $ optRandomSeed opts then show seed else "",-                gccOpts   = gccOptions,-                getPeriod = optPeriod opts,-                interpreted = if optInterpret opts then Interpreted else NotInterpreted,-                outputDir = optOutputDir opts,-                compiler  = optCompiler opts,-                prePostCode = optPrePostCode opts,-                sim = optSimulate opts,---                triggers = optTriggers opts,-                arrDecs = optArrs opts,-                clock = optClock opts-                    }--help :: IO ()-help = putStrLn helpStr

@@ -1,42 +0,0 @@-{-# LANGUAGE Rank2Types #-}---- | The Copilot interpreter.-module Language.Copilot.Interpreter-    (interpretStreams) where--import Language.Copilot.Core---- | The main function of this module.--- It takes a /Copilot/ specification, the values of the monitored values,--- and returns the values of the streams.-interpretStreams :: StreamableMaps Spec -> Vars -> Vars-interpretStreams streams moVs = inVs-  where inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams--interpret :: forall a. Streamable a => Vars -> Vars -> Spec a -> [a]-interpret inVs moVs s =-  case s of-    Const c -> repeat c-    Var v -> getElem v inVs-    PVar _ v -> checkV v (\v' -> (getElem v' moVs))-    PArr _ (v,s') -> checkV v (\v' -> map (\i ->    getElem v' moVs -                                                   !! fromIntegral i)-                                            (interpret inVs moVs s'))-    Append ls s' -> ls ++ interpret inVs moVs s'-    Drop i s' -> drop i $ interpret inVs moVs s'-    F f _ s' -> map f (interpret inVs moVs s')-    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)-  where -    checkV :: Ext -> (Var -> [a]) -> [a]-    checkV v f = -          case v of-            ExtV v' -> f v'-            -- XXX support this?  -            Fun _ _ -> error $ "Sampling functions is not currently supported"-                               ++ " in the Copilot interpreter."-                          

@@ -1,222 +0,0 @@-{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}---- | Describes the language /Copilot/.------ If you wish to add a new operator, the only modification needed is adding it--- in this module.  But if you want it to be used in the random generated--- streams, add it to either @'opsF'@, @'opsF2'@ or @'opsF3'@-module Language.Copilot.Language (-        -- * Operators and functions-        mod, div, mod0, div0,-        (<), (<=), (==), (/=), (>=), (>),-        not, (||), (&&), (^), (==>),-        -- * Boolean constants-        Bool(..),-        -- * Arithmetic operators (derived)-        Num(..),-        -- * Division-        Fractional((/)),-        mux, -        -- * Copilot variable declarations.-        var, varB, varI8, varI16, varI32, varI64,-        varW8, varW16, varW32, varW64, varF, varD,-        -- * Copilot constant declarations.  For the most part, these are-        -- unnecessary, as constants are automatically lifted in into the *-        -- Copilot types.  They are useful though for specifying triggers and *-        -- function samplings.-        const, constI8, constI16, constI32, constI64,-        constW8, constW16, constW32, constW64, constF, constD,-        -- * Boolean stream constants-        true, false,-        module Language.Copilot.Language.Sampling,-        -- * Constructs of the copilot language-        drop, (++), (.=), -- (..|), -        -- * Triggers-        module Language.Copilot.Language.FunctionCalls,-        -- * Safe casting-        module Language.Copilot.Language.Casting,-        notConstVarErr-    ) where--import qualified Language.Atom as A-import Data.Int-import Data.Word-import Prelude ( Bool(..), Num(..), Float, Double, ($), error-               , Fractional(..), fromInteger, Show(..))-import qualified Prelude as P-import Control.Monad.Writer (tell)-import qualified Data.Map as M--import Language.Copilot.Core-import Language.Copilot.Language.Sampling-import Language.Copilot.Language.Casting-import Language.Copilot.Language.FunctionCalls---import Language.Copilot.Language.RandomOps------ Operators and functions -----------------------------------------------------not :: Spec Bool -> Spec Bool-not = F P.not A.not_----- | 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.div A.div_---- | 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)--  --- class (Streamable a, A.OrdE a) => SpecOrd a where---   (<)--(<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool-(<) = F2 (P.<) (A.<.)-(<=) = F2 (P.<=) (A.<=.)-(>=) = F2 (P.>=) (A.>=.)-(>) = F2 (P.>) (A.>.)--(==), (/=) :: (Streamable a, A.EqE a) => Spec a -> Spec a -> Spec Bool-(==) = F2 (P.==) (A.==.)-(/=) = F2 (P./=) (A./=.)--(||), (&&), (^), (==>) :: Spec Bool -> Spec Bool -> Spec Bool-(||) = F2 (P.||) (A.||.)-(&&) = F2 (P.&&) (A.&&.)-(^) = F2 -    (\ x y -> (x P.&& P.not y) P.|| (y P.&& P.not x)) -    (\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x))-(==>) = F2 (\ x y -> y P.|| P.not x) A.imply---- | Beware : both sides are executed, even if the result of one is later discarded-mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a-mux = F3 (\ b x y -> if b then x else y) A.mux--infix 5 ==, /=, <, <=, >=, >-infixr 4 ||, &&, ^, ==>------- Constructs of the language ----------------------------------------------------- If a generic 'var' declaration is insufficient for the type-checker to--- determine the type, a monomorphic var operator can be used.---- | Useful for writing libraries.-var :: Streamable a => Var -> Spec a-var = Var--varB :: Var -> Spec Bool-varB = Var-varI8 :: Var -> Spec Int8-varI8 = Var-varI16 :: Var -> Spec Int16-varI16 = Var-varI32 :: Var -> Spec Int32-varI32 = Var-varI64 :: Var -> Spec Int64-varI64 = Var-varW8 :: Var -> Spec Word8-varW8 = Var -varW16 :: Var -> Spec Word16-varW16 = Var-varW32 :: Var -> Spec Word32-varW32 = Var-varW64 :: Var -> Spec Word64-varW64 = Var-varF :: Var -> Spec Float-varF = Var-varD :: Var -> Spec Double-varD = Var---- | Define a stream variable.-(.=) :: Streamable a => Spec a -> Spec a -> Streams-v .= s = -  case v of-    (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM) -                                 M.empty-    _ -> error $ "Given spec " P.++ show v -                   P.++ " but expected a variable in a Copilot definition (.=)."---- | Coerces a type that is 'Streamable' into a Copilot constant.-const :: Streamable a => a -> Spec a-const = Const--constI8 :: Int8 -> Spec Int8-constI8 = Const-constI16 :: Int16 -> Spec Int16-constI16 = Const-constI32 :: Int32 -> Spec Int32-constI32 = Const-constI64 :: Int64 -> Spec Int64-constI64 = Const-constW8 :: Word8 -> Spec Word8-constW8 = Const -constW16 :: Word16 -> Spec Word16-constW16 = Const-constW32 :: Word32 -> Spec Word32-constW32 = Const-constW64 :: Word64 -> Spec Word64-constW64 = Const-constF :: Float -> Spec Float-constF = Const-constD :: Double -> Spec Double-constD = Const--true, false :: Spec Bool-true = Const True-false = Const False---- | Drop @i@ elements from a stream.-drop :: Streamable a => Int -> Spec a -> Spec a-drop i s = Drop i s---- | Just a trivial wrapper over the @'Append'@ constructor-(++) :: Streamable a => [a] -> Spec a -> Spec a-ls ++ s = Append ls s---infixr 3 ++-infixr 2 .=------ Optimisation rules ----------------------------------------------------------{-# RULES-"Copilot.Language Plus0R" forall s. (P.+) s (Const 0) = s-"Copilot.Language Plus0L" forall s. (P.+) (Const 0) s = s-"Copilot.Language Minus0R" forall s. (P.-) s (Const 0) = s-"Copilot.Language Minus0L" forall s. (P.-) (Const 0) s = s-"Copilot.Language Times1R" forall s. (P.*) s (Const 1) = s-"Copilot.Language Times1L" forall s. (P.*) (Const 1) s = s-"Copilot.Language Times0R" forall s. (P.*) s (Const 0) = Const 0-"Copilot.Language Times0L" forall s. (P.*) (Const 0) s = Const 0-"Copilot.Language FracBy0" forall s. (P./) s (Const 0.0) = P.error "division by zero !" -"Copilot.Language FracBy1" forall s. (P./) s (Const 1.0) = s -"Copilot.Language Frac0" forall s. (P./) (Const 0.0) s = (Const 0.0)-"Copilot.Language OrFR" forall s. (||) s (Const False) = s-"Copilot.Language OrFL" forall s. (||) (Const False) s = s-"Copilot.Language OrTR" forall s. (||) s (Const True) = Const True-"Copilot.Language OrTL" forall s. (||) (Const True) s = Const True-"Copilot.Language AndFR" forall s. (&&) s (Const False) = Const False-"Copilot.Language AndFL" forall s. (&&) (Const False) s = Const False-"Copilot.Language AndTR" forall s. (&&) s (Const True) = s-"Copilot.Language AndTL" forall s. (&&) (Const True) s = s-"Copilot.Language ImpliesFL" forall s. (==>) (Const False) s = Const True-"Copilot.Language NotF" not (Const False) = Const True-"Copilot.Language NotT" not (Const True) = Const False-"Copilot.Language MuxF" forall s0 s1. mux (Const False) s0 s1 = s1-"Copilot.Language MuxT" forall s0 s1. mux (Const True) s0 s1 = s0-"Copilot.Language ImpliesDef" forall s0 s1. (||) s1 (not s0) = s0 ==> s1-      #-}---- "Copilot.Core CastLift" forall s i. drop i (cast s) = cast (drop i s)

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

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

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

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

@@ -1,28 +0,0 @@--- | Basic error checking for other libraries.--module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where--import Data.Int (Int16)--import Language.Copilot.Core--chk :: String -> Int -> Spec a -> Int -> Spec a-chk name n s m = -  if n < m -    then error $ "Value " ++ show n ++ " in operator " ++ name -         ++ " must be greater than or equal to " ++ show m ++ "."-    else s--nPosChk :: String -> Int -> Spec a -> Spec a-nPosChk name n s = chk name n s 0--nOneChk :: String -> Int -> Spec a -> Spec a-nOneChk name n s = chk name n s 1--int16Chk :: String -> Int -> Spec a -> Spec a-int16Chk name n s = -  if (toInteger n) > maxVal-    then error $ "Offset " ++ show n ++ " in operator " ++ name -         ++ " is larger than the Int16 maxBound, " ++ show maxVal ++ "."-    else s-  where maxVal = toInteger (maxBound::Int16)

@@ -1,48 +0,0 @@--- | Queries into how long until properties hold or fail.  We use Int16 to--- return the value, so your queries must not require looking more than 32,767--- periods :) .  Thus, in the following, the parameter @n@ must be @0 <= n <=--- 32,767@.  -1 indicates the test failed.--module Language.Copilot.Libs.Indexes(soonest, soonestFail, latest, latestFail) where--import Prelude (id, Int, String, fromIntegral, ($))-import qualified Prelude as P -import Data.Int (Int16)--import Language.Copilot.Libs.ErrorChks-import Language.Copilot.Core-import Language.Copilot.Language--soonestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16-soonestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr 0)-  where buildStr m = -          if m P.> n then (-1)-             else mux (f $ drop m s) (fI m) (buildStr (m P.+ 1))-        fI = fromIntegral--latestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16-latestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr n)-  where buildStr m = -          if m P.< 0 then (-1)-             else mux (f $ drop m s) (fI m) (buildStr (m P.- 1))-        fI = fromIntegral---- | Returns the smallest @m <= n@ such that @drop m s@ is true, and @-1@ if no--- such @m@ exists. -soonest :: Int -> Spec Bool -> Spec Int16-soonest = soonestHlp "soonest" id---- | Returns the smallest @m <= n@ such that @drop m s@ is false, and @-1@ if no--- such @m@ exists.  -soonestFail :: Int -> Spec Bool -> Spec Int16-soonestFail = soonestHlp "soonestFail" not---- | Returns the largest @m <= n@ such that @drop m s@ is true, and @-1@ if no--- such @m@ exists.  -latest :: Int -> Spec Bool -> Spec Int16-latest = latestHlp "latest" id---- | Returns the largest @m <= n@ such that @drop m s@ is false, and @-1@ if no--- such @m@ exists.  -latestFail :: Int -> Spec Bool -> Spec Int16-latestFail = latestHlp "latest" not

@@ -1,125 +0,0 @@--- XXX test until, release--- XXX move the engineLTL example--- XXX fix engine example in ppt slides---- | Bounded Linear Temporal Logic (LTL) operators.  For a bound @n@, a property--- @p@ holds if it holds on the next @n@ transitions (between periods).  If @n--- == 0@, then the trace includes only the current period.  For example,--- @--- always 3 p--- @--- holds if @p@ holds at least once every four periods (3 transitions).  --- --- Interface: see Examples/LTLExamples.hs You can embed a LTL specification--- within a Copilot specification using the form:--- @---   var `ltl` (operator spec)--- @--- where 'var' is the variable you want to assign to the LTL specification--- you're writing.------ For some properties, stream dependencies may not allow their specification.--- In particular, you cannot determine the "future" value of an external--- variable.  In general, the ptLTL library is probaby more useful.--module Language.Copilot.Libs.LTL-  ( ltl, eventually, next, always, until, release -  ) -  where--import Prelude (Int, ($), String, error)-import qualified Prelude as P-import Data.List (foldl1)--import Language.Copilot.Core-import Language.Copilot.Language-import Language.Copilot.Libs.Indexes-import Language.Copilot.Libs.ErrorChks--ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams-ltl v f = f v--tmpName :: Spec Bool -> String -> Spec Bool-tmpName v name = -  case v of -    Var v' -> varB (v' P.++ "_" P.++ name)-    _      -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs."---- | Property @s@ holds for the next @n@ periods.  We require @n >= 0@. If @n ==--- 0@, then @s@ holds in the current period.  E.g., if @p = always 2 s@, then we--- have the following relationship between the streams generated:--- @---      0 1 2 3 4 5 6 7--- s => T T T F T T T T ...--- p => T F F F T T ...--- @-always :: Int -> Spec Bool -> Spec Bool -> Streams-always n s v = do-  v .= (nPosChk "always" n $ foldl1 (&&) [drop x s' | x <- [0..n]])-  s' .= s-  where s' = tmpName v "always"---- | Property @s@ holds at the next period.  For example:--- @---           0 1 2 3 4 5 6 7--- s      => F F F T F F T F ...--- next s => F F T F F T F ...--- @--- Note: s must have sufficient history to drop a value from it.-next :: Spec Bool -> Spec Bool -> Streams-next s v = do -  v  .= drop 1 s'-  s' .= s-  where s' = tmpName v "next"---- | Property @s@ holds at some period in the next @n@ periods.  If @n == 0@,--- then @s@ holds in the current period.  We require @n >= 0@.  E.g., if @p =--- eventually 2 s@, then we have the following relationship between the streams--- generated:--- @--- s => F F F T F F F T ...--- p => F T T T F T T T ...--- @-eventually :: Int -> Spec Bool -> Spec Bool -> Streams-eventually n s v = do-  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x s' | x <- [0..n]])-  s' .= s-  where s' = tmpName v "eventually"---- | @until n s0 s1@ means that @eventually n s1@, and up until at least the--- period before @s1@ holds, @s0@ continuously holds.-until :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams-until n s0 s1 v = do-  v'  .= (nPosChk "until" n $ -            (   (whenS0 < 0) -- s0 didn't fail within n periods.-             || (soonest n s1' <= whenS0))) -- s0 failed at some point before n.-  v'' `ltl` eventually n s1' -- guarantees that soonest n s1 >= 0-  v   .= v' && v''-  s0' .= s0-  s1' .= s1-  where -    s0' = tmpName v "until_0"-    s1' = tmpName v "until_1"-    v''  = tmpName v "until_2"-    v' = tmpName v "until3"-    whenS0 = soonestFail n s0'---- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and--- including the period at which @s0@ becomes true.-release :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams-release n s0 s1 v = do-  v' .= (nPosChk "release" n $ (   (whenS0 >= 0) -- s0 becomes true at some point-                                && (whenS0 < whenS1))) -- and when s0 becomes true,-                                                       -- is strictly sooner than-                                                       -- when s1 fails.-  v'' `ltl` always n s1' -- s1 never fails-  v   .= v' || v''-  s0' .= s0-  s1' .= s1-  where -    s0' = tmpName v "release0"-    s1' = tmpName v "release1"-    v''  = tmpName v "release2"-    v' = tmpName v "release3"-    whenS1 = soonestFail n s1'-    whenS0 = soonest n s0'

@@ -1,65 +0,0 @@--- | Provides past-time linear-temporal logic (ptLTL operators).--- --- Interface: see Examples/PTLTLExamples.hs, particularly function tSinExt2 in--- that file.  You can embed a ptLTL specification within a Copilot--- specification using the form:--- @---   var `ptltl` (operator spec)--- @--- where 'var' is the variable you want to assign to the ptLTL specification--- you're writing.--module Language.Copilot.Libs.PTLTL -  ( ptltl, since, alwaysBeen, eventuallyPrev, previous ) -  where--import Prelude (String, ($), error)-import qualified Prelude as P--import Language.Copilot.Core-import Language.Copilot.Language--tmpName :: Spec Bool -> String -> Spec Bool-tmpName v name = -  case v of-    Var v' -> varB (v' P.++ "_" P.++ name)-    _     -> error "Copilot error in tmpName in PTLTL.hs."--ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams-ptltl v f = f v---- | Did @s@ hold in the previous period?-previous :: Spec Bool -> Spec Bool -> Streams-previous s v = v .= [False] ++ s  ---- | Has @s@ always held (up to and including the current state)?-alwaysBeen :: Spec Bool -> Spec Bool -> Streams-alwaysBeen s v = do-     tmp .= [True] ++ v-     v   .= tmp && s'-     s'  .= s-  where -    tmp = tmpName v "ab_tmp"-    s'  = tmpName v "ab"-    --- | Did @s@ hold at some time in the past (including the current state)?-eventuallyPrev :: Spec Bool -> Spec Bool -> Streams-eventuallyPrev s v = do-     tmp .= [False] ++ tmp || s'-     v   .= s' || tmp-     s'  .= s-  where -    tmp = tmpName v "ep_tmp"-    s'  = tmpName v "ep"---- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? -since ::  Spec Bool -> Spec Bool -> Spec Bool -> Streams-since s1 s2 v = do-    tmp `ptltl` (eventuallyPrev $ [False] ++ s2) -- has s2 been true at some point?-    v   `ptltl` (alwaysBeen $ tmp ==> s1')-    s1' .= s1-    s2' .= s2-  where -    tmp  = tmpName v "since_tmp"-    s1'  = tmpName v "since1"-    s2'  = tmpName v "since2"

@@ -1,50 +0,0 @@--- | Basic bounded statistics.  In the following, a bound @n@ is given stating--- the number of periods over which to compute the statistic (@n == 1@ computes--- it only over the current period). --module Language.Copilot.Libs.Statistics-    (max, min, sum, mean, meanNow) where--import Prelude (Int, ($), foldl1, fromIntegral, foldl, error, length)---import qualified Prelude as P --import qualified Language.Atom as A--import Language.Copilot.Libs.ErrorChks (nOneChk)-import Language.Copilot.Core-import Language.Copilot.Language--foldDrops :: (Streamable a) => Int -> (Spec a -> Spec a -> Spec a) -> Spec a -> Spec a-foldDrops n f s = foldl1 f [drop x s | x <- [0..(n-1)]]---- | Summation.-sum :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a-sum n s = -  nOneChk "sum" n $ foldDrops n (+) s ---- | Maximum value.-max :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a-max n s = -  nOneChk "max" n $ foldDrops n largest s -  where largest = \ x y -> mux (x <= y) y x---- | Minimum value.-min :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a-min n s = -  nOneChk "max" n $ foldDrops n smallest s-  where smallest = \ x y -> mux (x <= y) x y---- | Mean value.  @n@ must not overflow--- for word size @a@ for streams over which computation is peformed.-mean :: (Streamable a, Fractional a, A.NumE a) => Int -> Spec a -> Spec a-mean n s = -  nOneChk "mean" n $ (sum n s) / (fromIntegral n)---- | Mean value over the current set of specs passed in.-meanNow :: (Streamable a, A.IntegralE a) => [Spec a] -> Spec a-meanNow [] = error -    "Error in majority: list of arguments must be nonempty."-meanNow ls = -  (foldl (+) 0 ls) `div` (fromIntegral $ length ls)--

@@ -1,76 +0,0 @@--- | Voting algorithms over streams of data.--module Language.Copilot.Libs.Vote -    (majority, aMajority, ftAvg) where--import Prelude -  ( ($), fromIntegral, error, length, otherwise-  , Bounded(..), maxBound, minBound, Int)-import Data.List (replicate, foldl')-import qualified Prelude as P -import Data.Word--import Language.Copilot.Language-import Language.Copilot.Core-import qualified Language.Atom as A---- | Boyer-Moore linear majority algorithm.  Warning!  Returns an arbitary--- element if no majority is returned.  See 'aMajority' below.-majority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a-majority [] = -  error "Error in majority: list of arguments must be nonempty."-majority ls = majority' ls (const unit) 0--majority' :: (Streamable a, A.EqE a) -          => [Spec a] -> Spec a -> Spec Word32 -> Spec a-majority' [] candidate _ = candidate-majority' (x:xs) candidate cnt = -  majority' xs (mux (cnt == 0) x candidate)-               (mux (cnt == 0 || x == candidate) (cnt + 1) (cnt - 1))--aMajority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a -> Spec Bool-aMajority [] _ = -  error "Error in aMajority: list of arguments must be nonempty."-aMajority ls candidate = -    (foldl' (\cnt x -> mux (x == candidate)-                           (cnt + 1)-                           cnt :: Spec Word32-            ) 0 ls-    ) * 2-  > (fromIntegral $ length ls)---- | Fault-tolerant average.  Throw away the bottom and top @n@ elements and--- take the average of the rest.  Return an error if there are less than @2 * n--- + 1@ elements in the list.-ftAvg :: (Streamable a, A.IntegralE a, Bounded a) => [Spec a] -> Int -> Spec a-ftAvg ls n | length ls P.<= 2 P.* n = -  error $      "Error in ftAvg: list of arguments must be at least " -          P.++ P.show (2 * n + 1) P.++ "."-           | otherwise =       (ftAvg' ls (replicate n low) (replicate n high) 0)-                         `div` (fromIntegral $ length ls P.- (2 P.* n))-  where low = const maxBound-        high = const minBound---- | Return the total sum of values, minus the high and low values.-ftAvg' :: (Streamable a, A.IntegralE a, Bounded a) -       => [Spec a] -> [Spec a] -> [Spec a] -> Spec a -> Spec a-ftAvg' [] lows highs sum = foldl' (-) sum (lows P.++ highs)-ftAvg' (x:xs) lows highs sum = -  ftAvg' xs (insert (<) lows x) (insert (>) highs x) (sum + x)---- | Insert an element into an ordered list.--- insert :: (Streamable a, A.OrdE a) ---        => (Spec a -> Spec a -> Spec Bool) ---        -> [Spec a] -> Spec a -> Int -> [Spec a]--- insert _ xs _ idx   | idx P.== length xs = []--- insert ord xs x idx | otherwise =---   let n = xs !! idx---       choice = mux (x `ord` n) x n in---   choice : insert ord xs choice (idx + 1)-insert :: (Streamable a, A.OrdE a) -       => (Spec a -> Spec a -> Spec Bool) -       -> [Spec a] -> Spec a -> [Spec a]-insert _ [] _ = []-insert ord (n:ns) x = -  let pred = x `ord` n in-  mux pred x n : insert ord ns (mux pred n x) 

@@ -1,37 +0,0 @@-{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances, TypeSynonymInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}---- | Only exports instances for Show which allows the printing of streams-module Language.Copilot.PrettyPrinter () where--import Data.Int-import Data.Word-import Data.Map as M--import Language.Copilot.Core--instance (Show (a Bool), Show (a Int8), Show (a Int16), Show (a Int32), Show (a Int64),-    Show (a Word8), Show (a Word16), Show (a Word32), Show (a Word64), -    Show (a Float), Show (a Double)) => Show (StreamableMaps a) where-        show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =-            let acc0 = M.foldrWithKey showVal "" bm-                acc1 = M.foldrWithKey showVal acc0 i8m        -                acc2 = M.foldrWithKey showVal acc1 i16m-                acc3 = M.foldrWithKey showVal acc2 i32m-                acc4 = M.foldrWithKey showVal acc3 i64m-                acc5 = M.foldrWithKey showVal acc4 w8m-                acc6 = M.foldrWithKey showVal acc5 w16m-                acc7 = M.foldrWithKey showVal acc6 w32m-                acc8 = M.foldrWithKey showVal acc7 w64m-                acc9 = M.foldrWithKey showVal acc8 fm      -                acc10 = M.foldrWithKey showVal acc9 dm-            in acc10-            where-                showVal :: (Streamable a, Show (b a)) => Var -> b a -> String -> String-                showVal v val string = v ++ " .= " ++ show val ++ "\n" ++ string--instance Show Streams where-  show s = show (getSpecs s)---

@@ -1,315 +0,0 @@-{-# 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.Analyser--import qualified Language.Atom as A--import qualified Data.Map as M-import Prelude -import System.Random-import Data.Int-import Data.Word-import Data.Maybe------ Parameters of the random generation -----------------------------------------maxDrop :: Int-maxDrop = 4 -- The maximum value for i in Drop i _--- maxSamplePhase = 8 -- The maximum value for ph in PVar _ _ ph---- These determines the number of streams and of monitored variables.--- Bools are drawn each time with the following weights, until a False is drawn-weightsContinueVar, weightsContinuePVar :: [(Bool, Int)]-weightsContinueVar = [(True, 3), (False, 1)]-weightsContinuePVar = [(True, 1), (False, 1)]---- These determines the frequency of each atom type for the streams and the monitored variables-weightsVarTypes, weightsPVarTypes :: [(A.Type, Int)]-weightsVarTypes = -    [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4),-            (A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)]-weightsPVarTypes = -    [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4),-            (A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)]-            --- These determines the frequency of each constructor in the random streams--- 0 -> PVar--- 1 -> Var--- 2 -> Const--- 3 -> F--- 4 -> F2--- 5 -> F3--- 6 -> Append--- 7 -> Drop-weightsAllSpecSet, weightsFunSpecSet, weightsDropSpecSet :: [(Int, Int)]-weightsAllSpecSet = [(0, 2),(1,2),(2,6),(3,1),(4,3),(5,1),(6,4),(7,1)]-weightsFunSpecSet = [(0, 2),(1,2),(2,6),(3,1),(4,3),(5,1),(7,1)]-weightsDropSpecSet = [(1,2),(2,6),(7,1)]------ 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))-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))-fromOp op =-    case op of-        Operator x -> x--foldRandomableMaps :: forall b c. -    (forall a. (Streamable a, Random a) => Var -> c a -> b -> b) -> -    StreamableMaps c -> b -> b-foldRandomableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =-    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--randomWeighted :: (RandomGen g, Random a) => g -> [(a, Int)] -> (a, g)-randomWeighted g l =-    let l' = concatMap (\ (x, n) -> replicate n x) l-        len = length l'-        (i, g') = randomR (0, len - 1) g in-    (l' !! i, g')--data VName a = VName a-type Variables = StreamableMaps VName------ Instances of Random ---------------------------------------------------------instance Random Int8 where-    random g = -        let ((i::Int), g') = random g in-        (fromInteger $ toInteger i, g')-    randomR (lo, hi) g =-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random Int16 where-    random g = -        let ((i::Int), g') = random g in-        (fromInteger $ toInteger i, g')-    randomR (lo, hi) g =-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random Int32 where-    random g = -        let ((i::Int), g') = random g in-        (fromInteger $ toInteger i, g')-    randomR (lo, hi) g = -        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random Int64 where-    random g = -        let ((i0::Int32), g0) = random g-            ((i1::Int32), g1) = random g0 in-        (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (32::Int), g1)-    randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random Word8 where-    random g = -        let ((i::Int), g') = random g in-        (fromInteger $ toInteger i, g')-    randomR (lo, hi) g =-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random Word16 where-    random g = -        let ((i::Int), g') = random g in-        (fromInteger $ toInteger i, g')-    randomR (lo, hi) g =-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')---instance Random Word32 where-    random g = -        let ((i0::Word16), g0) = random g-            ((i1::Word16), g1) = random g0 in-        (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (16::Int), g1)-    randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')---instance Random Word64 where-    random g = -        let ((i0::Word32), g0) = random g-            ((i1::Word32), g1) = random g0 in-        (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (32::Int), g1)-    randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it-        let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in-        (fromInteger $ toInteger i, g')--instance Random a => Random [a] where-    random g =-        let (x, g0) = random g-            (b, g1) = random g0-            (l, g2) = -                if b -                    then random g1-                    else ([], g1) in-        (x:l, g2)-    -- Totally useless as lists are not ordered (could be, however)-    randomR (_, _) g = random g--instance Random A.Type where-    random g =-        let (n, g') = randomR (0::Int, 10) g in-        (toEnum n, g')-    randomR (t, t') g =-        let (n, g') = randomR (fromEnum t, fromEnum t') g in-        (toEnum n, g')------ Generation of random streams ------------------------------------------------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-        (streams, g2) = foldRandomableMaps (addRandomSpec opsF opsF2 opsF3 vs exts) vs (emptySM, g1)-        (vars, g3) = foldRandomableMaps addRandomExternal exts (emptySM, g2) in-    if isNothing $ check streams-        then (streams, vars)-        else randomStreams opsF opsF2 opsF3 g3-        -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-        (v_int::Word64, g2) = random g1-        v = "v" ++ show v_int-        vs' = -            case t of-                A.Bool -> updateSubMap (\ m -> M.insert v (VName (unit::Bool)) m) vs-                A.Int8 -> updateSubMap (\ m -> M.insert v (VName (unit::Int8)) m) vs-                A.Int16 -> updateSubMap (\ m -> M.insert v (VName (unit::Int16)) m) vs-                A.Int32 -> updateSubMap (\ m -> M.insert v (VName (unit::Int32)) m) vs-                A.Int64 -> updateSubMap (\ m -> M.insert v (VName (unit::Int64)) m) vs-                A.Word8 -> updateSubMap (\ m -> M.insert v (VName (unit::Word8)) m) vs-                A.Word16 -> updateSubMap (\ m -> M.insert v (VName (unit::Word16)) m) vs-                A.Word32 -> updateSubMap (\ m -> M.insert v (VName (unit::Word32)) m) vs-                A.Word64 -> updateSubMap (\ m -> M.insert v (VName (unit::Word64)) m) vs -                A.Float -> updateSubMap (\ m -> M.insert v (VName (unit::Float)) m) vs-                A.Double -> updateSubMap (\ m -> M.insert v (VName (unit::Double)) m) vs             -    in-    if b -        then addRandomVNames wContinue wTypes g2 vs'-        else (vs', g2)--addRandomSpec :: forall a g. (Streamable a, Random a, RandomGen g) => -    Operators -> Operators -> Operators -> Variables -> Variables -> -    Var -> VName a -> (StreamableMaps Spec, g) -> (StreamableMaps Spec, g)-addRandomSpec opsF opsF2 opsF3 vs exts v _ (streams, g) =-    let (spec::(Spec a), g') = randomSpec vs exts opsF opsF2 opsF3 g AllSpecSet in-    (updateSubMap (\m -> M.insert v spec m) streams, g')--randomSpec :: forall a g. (Streamable a, RandomGen g, Random a) -           => Variables -> Variables -> Operators -> Operators -              -> Operators -> g -> SpecSet -> (Spec a, g)-randomSpec vs exts opsF opsF2 opsF3 g set =-    let weights = case set of-            AllSpecSet  -> weightsAllSpecSet-            FunSpecSet  -> weightsFunSpecSet-            DropSpecSet -> weightsDropSpecSet-            _           -> weightsAllSpecSet-        (n::Int, g0) = randomWeighted g weights in-    case n of-            0 -> -- PVar-                case getVar g0 exts of-                    (Just v, g1) -> ---                        let (ph, g2) = randomR (1, maxSamplePhase)  g1 in-                        (PVar (atomType (unit::a)) (ExtV v), g1)-                    (Nothing, g1) -> randomSpec' g1 set-            1 -> -- Var-                case getVar g0 vs of-                    (Just v, g1) -> (Var v, g1)-                    (Nothing, g1) -> randomSpec' g1 set-            2 -> -- Const-                let (e, g1) = random g0 in-                (Const e, g1)-            3 -> -- F-                getOpStream opsF g0-            4 -> -- F2-                getOpStream opsF g0-            5 -> -- F3-                getOpStream opsF g0-            6 -> -- Append-                let (ls, g1) = random g0-                    (s', g2) = randomSpec' g1 set in-                (Append ls s', g2)-            7 -> -- Drop-                let (i, g1) = randomR (1::Int, maxDrop) g0-                    (s', g2) = randomSpec' g1 DropSpecSet in-                (Drop i s', g2)-            _ -> error "Impossible"-    where -        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 =-            let m = getSubMap ops-                ks = M.keys m-                len = length ks-            in-            if len > 0-                then-                    let (i, g1) = randomR (0::Int, len - 1) g0-                        k = ks !! i in-                    case fromJust $ M.lookup k m of-                        Operator op -> op randomSpec' g1-                else randomSpec' g0 set-        getVar :: g -> Variables -> (Maybe Var, g)-        getVar g0 variables =-            let m :: M.Map Var (VName a)-                m = getSubMap variables-                ks = M.keys m-                len = length ks-            in-            if len > 0 -                then -                    let (i, g1) = randomR (0::Int, len - 1) g0 in-                    (Just  (ks !! i), g1)-                else (Nothing, g0)-                -addRandomExternal :: forall a g. (Streamable a, Random a, RandomGen g) => -    Var -> VName a -> (Vars, g) -> (Vars, g)-addRandomExternal v _ (vars, g) =-    let (vals::[a], g') = randomExternalValues g in-    (updateSubMap (\m -> M.insert v vals m) vars, g')--randomExternalValues :: (Streamable a, Random a, RandomGen g) => g -> ([a], g)-randomExternalValues g  =-    let (oldG, newG) = split g in-    (randoms oldG, newG)

@@ -1,235 +0,0 @@-*******************************************************************************-Overview-*******************************************************************************--Copilot: A (Haskell DSL) stream language for generating hard real-time C code.--Can you write a list in Haskell? Then you can write embedded C code using-Copilot. Here's a Copilot program that computes the Fibonacci sequence (over-Word 64s) and tests for even numbers:--fib :: Streams-fib = do-  let f = varW64 "f"-  let t   = varB "t"-  f .= [0,1] ++ f + (drop 1 f)-  t .= even f-    where even :: Spec Word64 -> Spec Bool-          even w' = w' `mod` 2 == 0--Copilot contains an interpreter, a compiler, and uses a model-checker to check-the correctness of your program. The compiler generates constant time and-constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was-originally developed to write embedded monitors for more complex embedded-systems, but it can be used to develop a variety of functional-style embedded-code.--The documentation for the language itself is mainly at--  Copilot/doc/Language-Copilot-Language.html --and there are numerous examples in--  Copilot/Language/Copilot/Examples --*******************************************************************************-Download-*******************************************************************************--Please visit <http://leepike.github.com/Copilot/> for more information about-installing and using Copilot.--The page is also available as index.html in the gh-pages branch of the Copilot-repo.  In your local repo,--  > git checkout gh-pages --and you should see index.html.---*******************************************************************************-Release notes-*******************************************************************************--* Copilot-1.0.2-  * Fixed a major compilation bug.-  * Upgraded to GHC 7.0.2 (Haskell Platform).--* Copilot-1.0.1-  * Removed send operators---use triggers instead (see the distributed voting-  * example in VoteExamples.hs.--* Copilot-1.0-  * Language frozen. -  * Added sampling functions and returning arrays.--* Copilot-0.29--  * Refactor Language.hs into submodules.-  * Removed the notion of phases from sampling.  That is a compiler-level-    concern.-  -* Copilot-0.28-  -  * Make triggers part of the Copilot language (see example t5 in Examples.hs).- -* Copilot-0.27--  * Changed syntax and semantics of the 'send' function (Language.hs) for-    sending Copilot values on ports.  An example is in Example.hs (grep for-    'send').--* Copilot-0.26--  * Variables are now specs, not strings.  This gives stream expressions a type,-    so no need for constant functions, monomorphic cast functions, or var-    annotations in expressions.  Examples updated to reflect the change.--* Copilot-0.25--  * Added true, false Specs (Spec Bool)-  * Removed generic const -- unneeded, since Spec instantiates Num.-  * Change casting to only allow casts that (1) are guaranteed not to change the-    sign and (2) are to a larger type.-  * Removed libs from Copilot.hs.  You must import these explicitly.-  * Fixed buts with LTL and ptLTL libraries and examples and added documentation.--* Copilot-0.24--  * Fixed a bug in external array analysis for computing the minimum period-    size.-  * Added the ability to specify a HW clock for Atom.--* 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---*******************************************************************************-Modifying the Compiler-*******************************************************************************--This document is intended as a help for whoever wants to hack the internals of-Copilot.  It is up-to-date on August 2010, the 17th.--I will first explain what each module does, then where to look to do some simple-modifications.--*** Modules ***--Core :-Defines all the important data-structures.-Especially interestings are :-- Spec, the AST of the streams specifications.-    Notice that the operators on streams (F, F2, F3) actually holds functions-    that helps interpreting/compiling them-- Streamable, a type class whose instances are all the possible types of output -    for a stream-- StreamableMaps, a generic container for holding pairs of key/values, with -    values of different types--Compiler :-Does all the scheduling, and translates a Copilot specification, to an Atom-program. More information on its algorithm can be found in the paper "Copilot: A-Hard Real-Time Runtime Monitor".--Interpreter :-Provides a small interpreter, mostly for checking the compiler against it.  Its-design is very concise, because all the hard scheduling work is done by the-Haskell runtime. The streams are indeed translated to mutually recursives-infinite lists, and the lazyness of Haskell spare us from having to schedule-their computation. There is no specific code for each operator either, as-operators hold the function to be applied to their argument.--Analyser :-There are several kinds of restrictions on the inputs accepted by Copilot.-Some of them are catched by the Haskell compiler (for example bad typing into-a stream specification), but others aren't :-- Bad typing across stream boundaries-- Specifications which doesn't obey the syntax of Copilot (it could have been-    checked by Haskell too, but would have greatly complicated the Spec type)-- All kinds of properties on the dependency graph of the specification.-All these additional restrictions are checked by the Analyser.--PrettyPrinter :-Just allows to print the structure of a specification--Tests.Random :-Generates random streams and random input values, for easily checking the-compiler against the interpreter in an automated way. Currently a bit ugly,-would probably have benefited from using the QuickCheck library, rather than the-lower-level Random library. All the parameters of the random generation are near-the top of the file.--Language :-Defines all the different operators of the language. These are defined through a-F, F2 or F3 constructor, a function on how to compile them, and a function on-how to interpret them. These are also packed in a Operators data structure for-use in the random streams generator.  Also contains some monomorphic versions of-the polymorphic language constructs, to help the type inferer.--AdHocC :-A small number of uninteresting functions to output C code. Used by AtomToC.--AtomToC :-Adds to the atom-generated code a main function and some initialisation stuff.--Main :-"Plumbing" module. Makes the analyser/interpreter/compiler, atom, gcc, and the-generated C program interact. Takes its arguments in a very heavy format (not-very convenient for fast testing).  Warning : it is rather easy to desynchronyze-the generated C program and the interpreter with very small modifications-(leading to strange bugs).--Interface :-Is a wrapper around Main. Writing its argument is usually much easier, thanks-to the provided combinators and the reasonable defaults. All it does is -translating those into the numerous and verbose arguments Main expects.--Libs.* :-As Copilot is embedded in Haskell, it is very easy to write libraries of "macros"-that simplify the writing of some specifications. Thus these files, that holds -for example functions for easily writing LTL and PTLTL formulas.--Examples.* :-Self-explanatory.--*** Simple modifications ***--Add an example :-In Examples.Examples, or if related to a library, in Examples.LibraryName--Add some high-level combinator on streams :-In a library, in Lib.*-Should not call Atom, should only use other combinators and base operators.--Add some operator in the base language :-Write in Language.hs, from F, F2 or F3 (see examples) Would be nice to also add-to the corresponding Operators set (opsF, opsF2 or opsF3), so that it could be-automatically checked. This last point obviously require that the interpreted-and compiled semantics are equivalents.--Add some possible types for the streams :-Add a new instance of Stremable in Core.hs-Add a new record to StreamableMaps in Core.hs-Update foldStreamableMaps, mapStreamableMaps, mapStreamableMapsM, -and filterStreamableMaps in Core.hs-Update foldRandomableMaps in Tests/Random.hs--Authorise a new type to be exchanged by monitors :-Add a new instance of Sendable in Core.hs-Update foldSendableMaps in Core.hs--Add a new option to Copilot :-Add a new field to the Options record in Interface.hs-Add a new combinator for that field in Interface.hs-Update the baseOptions in Interface.hs-Implement it (probably in Main.hs).-Update interface in Interface.hs to convey it to the Main.-

@@ -0,0 +1,88 @@+Copilot: a stream DSL+====================================+Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+Haskell that compiles into embedded C.  Copilot is similar in spirit to+languages like Lustre.  Copilot contains an interpreter, multiple back-end+compilers, and other verification tools.++Resources+=========+Copilot is comprised of a number of sub-projects which are automatically+installed when you install Copilot from Hackage, as described below:++* [copilot-language](http://hackage.haskell.org/package/copilot-language) The+  front-end of Copilot defining the user language.++* [copilot-libraries](http://hackage.haskell.org/package/copilot-libraries)+  User-supplied libraries for Copilot, including linear-temporal logic,+  fault-tolerant voting, regular expressions, etc.++* [copilot-core](http://hackage.haskell.org/package/copilot-core) The core+  language, which efficiently represents Copilot expressions.  The core is only+  of interest to implementers wishing to add a new back-end to Copilot.++* [copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to+  generate a driver using CBMC, a third-party tool (see Dependencies below) that+  proves that the code generated by different C back-ends is equivalent.+  Currently, this includes the C99 back-end and the SBV back-end.++* [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that+  translates to [Atom](http://hackage.haskell.org/package/copilot-cbmc) to+  generate hard real-time C code.++Optionally, you may which also to install++* [copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end+  that translates to [SBV](http://hackage.haskell.org/package/sbv), using its+  code generator to generate hard real-time C code as well.  The ad++* [copilot-discussion](https://github.com/niswegmann/copilot-discussion)+  Contains a tutorial, todos, and other items regarding the Copilot system.++**Sources** for each package are available on Github as well.  Just go to+[Github](github.com) and search for the package of interest.  Feel free to fork!++Comments, bug reports, and patches are always welcome.  Send them to leepike @+gmail.com++Examples+=========+Please see the files under the Examples directory for a number of examples+showing the syntax, use of libraries, and use of the interpreter and back-ends.+The examples is the best way to start.++Installation+============+The Copilot library is cabalized. Assuming you have cabal and the GHC compiler+installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the+easiest way to obtain these), it should merely be a matter of running +     +         cabal install copilot+	 +with an Internet connection.  Please see the INSTALL file for installation+details.++Once the installation is done, you can run the executable `XXX` which will+execute the regression test suite for sbv on your machine.++Dependencies+=============+copilot-cbmc depends on the C model-checker, CBMC.+[CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code.  We+use CBMC to prove that two back-ends generating C generate semantically+equivalent C, to help detect bugs in C back-ends.++Copyright, License+==================+Copilot is distributed with the BSD3 license. The license file contains the+[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.++Thanks+======+Copilot was developed, in part, with support from NASA's Aviation Safety+Program, Contract #NNL08AD13T.  Copilot was developed jointly by Galois,+Inc. and the National Institute of Aerospace.++The following people have contributed to Copilot: Lee Pike, Nis Wegmann,+Sebastian Niller, Robin Morisset, Alwyn Goodloe, and Levent Erkok.+

@@ -0,0 +1,11 @@+import Distribution.Simple+import System.Exit (exitWith, ExitCode(..))++main :: IO ()+main = defaultMainWithHooks simpleUserHooks{ postInst = msg }+  where +  msg _ _ _ _ = do+    putStrLn "Execute \"<Your install location>/.cabal/bin/copilot-regression\" to run some very simple tests to ensure your installation built correctly."+    putStrLn "To QuickCheck the Atom backend, execute \"<Your install location>/.cabal/bin/copilot-c99-qc .\""+    exitWith ExitSuccess+

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

@@ -0,0 +1,127 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | A very small test suite to check for basic functionality.++{-# LANGUAGE RebindableSyntax #-}++module Main where++import qualified Prelude as P+import Language.Copilot hiding (even, odd)+import Copilot.Compile.C99++import System.Directory (removeFile)+--------------------------------------------------------------------------------++--+-- Some utility functions:+--++flipflop :: Stream Bool -> Stream Bool+flipflop x = y+  where+    y = [False] ++ if x then not y else y++nats :: Stream Word64+nats = [0] ++ nats + 1++even :: (P.Integral a, Typed a) => Stream a -> Stream Bool+even x = x `mod` 2 == 0++odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool+odd = not . even++counter :: (Num a, Typed a) => Stream Bool -> Stream a+counter reset = y+  where+    zy = [0] ++ y+    y  = if reset then 0 else zy + 1++booleans :: Stream Bool+booleans = [True, True, False] ++ booleans++fib :: Stream Word64+fib = [1, 1] ++ fib + drop 1 fib++bitWise :: Stream Word8+bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )+          .^.+          ( let b = [ 0, 1, 1 ] ++ b in b )++sumExterns :: Stream Word64+sumExterns =+  let+    ex1 = extern "e1"+    ex2 = extern "e2"+  in+    ex1 + ex2++--------------------------------------------------------------------------------++--+-- An example of a complete copilot specification.+++-- A specification:+spec :: Spec +spec =+  do+    -- A trigger with four arguments:+    trigger "e" booleans+      [ arg fib, arg nats, arg sumExterns, arg bitWise ]++    -- A trigger with two arguments:+    trigger "f" booleans+      [ arg fib, arg sumExterns ]++    -- A trigger with a single argument:+    trigger "g" (flipflop booleans)+      [ arg (sumExterns + counter false + 25) ]++    -- A trigger with a single argument (should never fire):+    trigger "h" (extern "e3" /= fib)+      [ arg (0 :: Stream Int8) ]++    observer "i" (odd nats)++--- Some infinite lists for simulating external variables:+e1, e2, e3 :: [Word64]+e1 = [0..]+e2 = 5 : 4 : e2+e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)++main :: IO ()+main = do+  putStrLn "PrettyPrinter:"+  putStrLn ""+  prettyPrint spec+  putStrLn ""+  putStrLn ""+  putStrLn "Interpreter:"+  putStrLn ""+  interpret 10 [var "e1" e1, var "e2" e2, var "e3" e3] spec+  putStrLn ""+  putStrLn ""+  putStrLn "Atom compilation:"+  reify spec >>= compile defaultParams +  cleanUp +  putStrLn "*********************************"+  putStrLn " Ok, things seem to work.  Enjoy!"+  putStrLn "*********************************"++  -- Don't assume SBV is installed.+  -- putStrLn "Check equivalence:"+  -- putStrLn ""+  -- putStrLn ""+  -- reify spec >>= +  --   C.genCBMC C.defaultParams {C.numIterations = 20}++--------------------------------------------------------------------------------++cleanUp :: IO ()+cleanUp = do+  removeFile "copilot.c"+  removeFile "copilot.h"+  return ()

@@ -1,79 +1,49 @@ name:                copilot-version:             1.0.2-cabal-version:       >= 1.6+version:             2.0+cabal-version:       >= 1.10 license:             BSD3 license-file:        LICENSE-author:              Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller-synopsis:            A stream DSL for writing embedded C monitors.+author:              Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe+synopsis:            A stream DSL for writing embedded C programs. build-type:          Simple maintainer:          Lee Pike <leepike@galois.com> category:            Language, Embedded homepage:            http://leepike.github.com/Copilot/-description:         Can you write a list in Haskell? Then you can write embedded C code using-                     Copilot. Here's a Copilot program that computes the Fibonacci sequence (over-                     Word 64s) and tests for even numbers:-                     .-                     > fib :: Streams-                     > fib = do-                     >  let f = varW64 "fib"-                     >  let t = varB "t"-                     >  f .= [0,1] ++ f + (drop 1 f)-                     >  t .= even f-                     >    where even :: Spec Word64 -> Spec Bool-                     >          even w' = w' `mod` 2 == 0-                     .-                     Copilot contains an interpreter, a compiler, and uses a model-checker to check-                     the correctness of your program. The compiler generates constant time and-                     constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was-                     originally developed to write embedded monitors for more complex embedded-                     systems, but it can be used to develop a variety of functional-style embedded-                     code.+stability:           Experimental+description:         Documentation is available at the website, and see the included examples. -extra-source-files:  README+extra-source-files:  README.md  source-repository head     type:       git     location:   git://github.com/leepike/Copilot.git  library-    ghc-options:     -Wall-    -- These build depends represent my current system.  This will probably-    -- build on packages outside these constraints.-    build-depends:     -                       base >= 4.0 && < 6-                     , atom >= 1.0.8-                     , containers >= 0.2.0.1-                     , process >= 1.0.0.0-                     , random >= 1.0.0.0-                     , directory >= 1.0.0.0-                     , mtl >= 1.0.0.0-                     , filepath >= 1.0.0.0--    extensions:+    hs-source-dirs: src+    default-language:  Haskell2010+    ghc-options:     +      -Wall+      -fwarn-tabs+      -auto-all+      -caf-all+      -fno-warn-orphans+    build-depends:+                       base >= 4.0 && <5+                     , copilot-core+                     , copilot-language+                     , copilot-libraries+                     , copilot-cbmc     exposed-modules: Language.Copilot-                     Language.Copilot.AdHocC-                     Language.Copilot.Core-                     Language.Copilot.Language-                     Language.Copilot.Language.Sampling-                     Language.Copilot.Language.FunctionCalls-                     Language.Copilot.Language.RandomOps-                     Language.Copilot.Language.Casting-                     Language.Copilot.AtomToC-                     Language.Copilot.Compiler-                     Language.Copilot.Interpreter-                     Language.Copilot.Help-                     Language.Copilot.Analyser-                     Language.Copilot.PrettyPrinter-                     Language.Copilot.Tests.Random-                     Language.Copilot.Dispatch-                     Language.Copilot.Interface-                     Language.Copilot.Libs.ErrorChks-                     Language.Copilot.Libs.PTLTL-                     Language.Copilot.Libs.LTL-                     Language.Copilot.Libs.Indexes-                     Language.Copilot.Libs.Statistics-                     Language.Copilot.Libs.Vote-                     Language.Copilot.Examples.Examples-                     Language.Copilot.Examples.LTLExamples-                     Language.Copilot.Examples.PTLTLExamples-                     Language.Copilot.Examples.StatExamples++executable copilot-regression+  default-language        : Haskell2010+  hs-source-dirs          : Tests, src+  ghc-options             : -Wall -fwarn-tabs+  main-is                 : Test.hs+  build-depends:+                     base >= 4.0+                   , copilot-core+                   , copilot-language+                   , copilot-libraries+                   , copilot-c99+                   , directory >= 1.1

@@ -0,0 +1,39 @@+module Language.Copilot +  (+    module Copilot.Language+  , module Copilot.Language.Prelude +  , module Copilot.Language.Reify++  -- Code generators+  -- , module Copilot.Compile.C99+  -- , module Copilot.Compile.SBV++  -- Libraries+  , module Copilot.Library.Clocks+  , module Copilot.Library.LTL+  , module Copilot.Library.PTLTL+  , module Copilot.Library.Statistics+  , module Copilot.Library.RegExp+  , module Copilot.Library.Utils+  , module Copilot.Library.Voting+  , module Copilot.Library.Stacks+  ) where++import Copilot.Language+import Copilot.Language.Prelude +import Copilot.Language.Reify++-- Code generators+-- import Copilot.Compile.C99+-- import Copilot.Compile.SBV++-- Libraries+import Copilot.Library.Clocks+import Copilot.Library.LTL+import Copilot.Library.PTLTL+import Copilot.Library.Statistics+import Copilot.Library.RegExp+import Copilot.Library.Utils+import Copilot.Library.Voting+import Copilot.Library.Stacks+