copilot (empty) → 0.21
raw patch · 27 files changed
+3476/−0 lines, 27 filesdep +atomdep +basedep +containerssetup-changed
Dependencies added: atom, base, containers, directory, filepath, mtl, process, random
Files
- LICENSE +29/−0
- Language/Copilot.hs +36/−0
- Language/Copilot/AdHocC.hs +45/−0
- Language/Copilot/Analyser.hs +238/−0
- Language/Copilot/AtomToC.hs +123/−0
- Language/Copilot/Compiler.hs +211/−0
- Language/Copilot/Core.hs +542/−0
- Language/Copilot/Dispatch.hs +262/−0
- Language/Copilot/Examples/Examples.hs +188/−0
- Language/Copilot/Examples/LTLExamples.hs +61/−0
- Language/Copilot/Examples/PTLTLExamples.hs +60/−0
- Language/Copilot/Examples/StatExamples.hs +21/−0
- Language/Copilot/Help.hs +178/−0
- Language/Copilot/Interface.hs +243/−0
- Language/Copilot/Interpreter.hs +34/−0
- Language/Copilot/Language.hs +509/−0
- Language/Copilot/Libs/ErrorChks.hs +30/−0
- Language/Copilot/Libs/Indexes.hs +52/−0
- Language/Copilot/Libs/LTL.hs +57/−0
- Language/Copilot/Libs/PTLTL.hs +39/−0
- Language/Copilot/Libs/Statistics.hs +43/−0
- Language/Copilot/PrettyPrinter.hs +39/−0
- Language/Copilot/Tests/Random.hs +303/−0
- Language/Copilot/Variables.hs +32/−0
- README +33/−0
- Setup.hs +2/−0
- copilot.cabal +66/−0
+ LICENSE view
@@ -0,0 +1,29 @@+2009+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Language/Copilot.hs view
@@ -0,0 +1,36 @@+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.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.Examples.Examples+ -- , module Language.Copilot.Examples.LTLExamples+ -- , module Language.Copilot.Examples.PTLTLExamples+ ) where++import Language.Copilot.Core+import Language.Copilot.Analyser+import Language.Copilot.Interpreter+import Language.Copilot.Help+import Language.Copilot.AtomToC+import Language.Copilot.Compiler+import Language.Copilot.Language (opsF, opsF2, opsF3)+import Language.Copilot.PrettyPrinter()+import Language.Copilot.Tests.Random+import Language.Copilot.Dispatch+import Language.Copilot.Interface+import Language.Copilot.Libs.Indexes+import Language.Copilot.Libs.LTL+import Language.Copilot.Libs.PTLTL+-- import Language.Copilot.Examples.Examples+-- import Language.Copilot.Examples.LTLExamples+-- import Language.Copilot.Examples.PTLTLExamples
+ Language/Copilot/AdHocC.hs view
@@ -0,0 +1,45 @@+-- TODO-Robin : Improve a lot that -> new package in Hackage ?+-- generate C-Code with combinators, high-level, safe haskell.++-- | Helper functions for writing free-form C code.+module Language.Copilot.AdHocC (+ varDecl, includeBracket, includeQuote,+ printf, printfNewline+ ) 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)) ++ ";"+ where+ cType' Bool = "int"+ cType' typ = cType typ+++-- | 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)
+ Language/Copilot/Analyser.hs view
@@ -0,0 +1,238 @@+{-# OPTIONS_GHC -XRelaxedPolyRec #-}++-- | This module provides a way to check that a /Copilot/ specification is compilable+module Language.Copilot.Analyser(+ -- * Main error checking functions+ check, Error(..), SpecSet(..),+ -- * Varied other things+ getExternalVars, getAtomType+ {-+ -- * Dependency Graphs (experimental)+ Weight, Node(..), DependencyGraph,+ mkDepGraph, showDG -}+ ) where+ +import Language.Copilot.Core++import qualified Language.Atom as A++import Data.List++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+ | BadSamplingPhase Var Var Phase -- ^ if an external variable is sampled at phase 0 then there is no time for the stream to be updated+ | BadType Var Var -- ^ either a variable is not defined, or not with the good type ; there is no implicit conversion of types in /Copilot/+ | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile /Copilot/ specification can only work if there is no negative weighted closed path in the specification, as described in the original research paper+ | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but would need bigger prophecyArrays+ | DependsOnFuture [Var] Var Weight-- ^ If an output depends of a future of an input it will be hard to compile to say the least++instance Show Error where+ show (BadSyntax s v) = + "Error syntax : " ++ s ++ "is not allowed in that position in stream " ++ v ++ "\n"+ show (BadDrop i v) = + "Error : a Drop in stream " ++ v ++ "drops the number " ++ show i ++ + "of elements. " ++ show i ++ " is negative, and Drop only accepts positive arguments. \n"+ show (BadSamplingPhase v v' ph) = + "Error : the external variable " ++ v' ++ " is sampled at phase " ++ show ph ++ + " in the stream" ++ v ++ ". Sampling can only occur from phase 1 onwards. \n"+ show (BadType v v') =+ "Error : the monitor variable " ++ v ++ ", called in the stream " ++ v' +++ " either does not exist, or don't have the right type (there is no implicit conversion)\n"+ show (NonNegativeWeightedClosedPath vs w) =+ "Error : the following path is closed in the dependency graph of this "+ ++ "specification and have weight " ++ show w ++ " which is positive (append decrease the weight, "+ ++ "while drop increase it). This is forbidden to avoid streams which could "+ ++ "take 0 or several different values. Try adding some initial elements (e.g., [0,0,0] ++ ...) "+ ++ "to the offending streams. \n"+ ++ "Path : " ++ show (reverse vs) ++ "\n"+ show (DependsOnClosePast vs v w len) =+ "Error : the following path is of weight " ++ show w ++ " ending in "+ ++ "the external variable " ++ v ++ " while the first variable of that path "+ ++ "has a prophecy array of length " ++ show len ++ ", which is strictly greater "+ ++ "than the weight. This is forbidden. \n"+ ++ "Path : " ++ show (reverse vs) ++ "\n" + show (DependsOnFuture vs v w) =+ "Error : the following path is of weight " ++ show w ++ " which is strictly positive. "+ ++ "This means that the first variable depends on the future of the external variable "+ ++ v ++ " which is quoted in the last variable of the path. This is obviously impossible. \n"+ ++ "Path : " ++ show (reverse vs) ++ "\n"++(&&>) :: 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++-- 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+ PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph+ Var _ -> Nothing+ Const _ -> Nothing+ F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v &&>+ (checkSyntaxSpec FunSpecSet v s0 Nothing)+ F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v &&>+ (checkSyntaxSpec FunSpecSet v s0 Nothing) &&>+ checkSyntaxSpec FunSpecSet v s1 Nothing+ F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v &&>+ (checkSyntaxSpec FunSpecSet v s0 Nothing) &&> + (checkSyntaxSpec FunSpecSet v s1 Nothing) &&>+ checkSyntaxSpec FunSpecSet v s2 Nothing + Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v &&> + checkSyntaxSpec AllSpecSet v s0 Nothing+ Drop i s0 -> (0 <= i) ||> BadDrop i v &&> + (checkSyntaxSpec DropSpecSet v s0 Nothing)++-- checks that streams are well defined (ie can be compiled)+-- Currently very inefficient (for simplicity's sake), +-- could probably be optimized if need be+-- by keeping weights of paths in a matrix and doing some linear algebra+-- (fast exponentiation could give some nice results)+-- could also reuse the dependency graph (see below)+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 $ BadType v (head vs)+ _ -> Nothing+ 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++getAtomType :: Streamable a => Spec a -> A.Type+getAtomType s =+ let unitElem = unit+ _ = (Const unitElem) `asTypeOf` s -- to help the typechecker+ in atomType unitElem++getExternalVars :: StreamableMaps Spec -> [(A.Type, Var, Phase)]+getExternalVars streams =+ nub $ foldStreamableMaps decl streams []+ where+ decl :: Streamable a => Var -> Spec a -> [(A.Type, Var, Phase)] -> [(A.Type, Var, Phase)]+ decl _ s ls =+ case s of+ PVar t v ph -> (t, v, ph) : 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++---- 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 -}
+ Language/Copilot/AtomToC.hs view
@@ -0,0 +1,123 @@+{-# 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 qualified Language.Atom as A++import Data.List++-- allExts represents all the variables to monitor (used for declaring them)+-- inputExts represents the monitored variables which are to be feed to the standard input of the C program.+-- only used for the testing with random streams and values.+getPrePostCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> (String, String)+getPrePostCode cName streams allExts inputExts p =+ (preCode $ extDecls allExts, postCode cName streams allExts inputExts p)++-- Make the declarations for external vars+extDecls :: [(A.Type, Var, Phase)] -> [String]+extDecls allExtVars =+ let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars in+ map (\ (t, v, _) -> varDecl t [v]) uniqueExtVars++preCode :: [String] -> String+preCode extDeclarations = unlines $+ [ includeBracket "stdio.h"+ , includeBracket "stdlib.h"+ , includeBracket "string.h"+ , includeBracket "inttypes.h"+ , ""+ , "unsigned long long rnd;"+ ]+ ++ extDeclarations+ +vPre :: Name -> String+vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "."++postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> String+postCode cName streams allExts inputExts p = + unlines $+ (if isEmptySM inputExts+ then []+ else cleanString)+ +++ [ "// #pragma GCC diagnostic ignored \"-Wformat\""+ , "int main(int argc, char *argv[]) {"+ , " 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]);"+ ]+ +++ inputExtVars inputExts " "+ +++ sampleExtVars allExts cName+ +++ [ " int i = 0;"+ , " for(; i < rnd ; i++) {"+ ]+ +++ inputExtVars inputExts " "+ +++ [ " int j = 0;"+ , " for (; j < " ++ show p ++ " ; j++) {"+ , " " ++ cName ++ "();"+ , " }"+ , " " ++ printf "period: %i " ["i"]+ ]+ +++ 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++sampleExtVars :: [(A.Type, Var, Phase)] -> Name -> [String]+sampleExtVars allExts cName =+ map sample allExts+ where+ sample :: (A.Type, Var, Phase) -> String+ sample (_, v, ph) =+ " " ++ vPre cName ++ "tmpSampleVal__" ++ v ++ "_" ++ show ph ++ " = " ++ v ++ ";"++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 ++ "outputVal__" ++ v]) : ls
+ Language/Copilot/Compiler.hs view
@@ -0,0 +1,211 @@+{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}++-- Note : for now, the initial state is computed during the first tick++-- | Transform the copilot specification in an atom one, and then compile that one.+module Language.Copilot.Compiler(copilotToAtom) where++import Language.Copilot.Core++import Data.Word+import Data.Maybe+import Data.Map as M+import Data.List+import Control.Monad (when) ++import qualified Language.Atom as A+import Language.Copilot.Analyser (getAtomType)++getValue :: PhasedValue a -> A.V a+getValue (Ph _ val) = val++-- | Compiles an /Copilot/ specification to an /Atom/ one.+--+-- The period is given as a Maybe : if it is Nothing, an optimal period will be chosen.+copilotToAtom :: StreamableMaps Spec -> Sends -> Maybe Period -> Maybe [(Var, String)] -> (Period, A.Atom ())+copilotToAtom streams sends p triggers = + (p', A.period p' $ do+ -- Three streamableMaps : + -- prophecy arrays (Int, A.A a), outputs (A.V a), temporary samples (Phase, A.V a)+ prophArrs <- mapStreamableMapsM initProphArr streams+ outputs <- mapStreamableMapsM initOutput streams+ tmpSamples <- foldStreamableMaps initTmpSamples streams (return emptySM)+ updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty)+ outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty)++ -- One atom rule for each stream+ foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples + updateIndexes outputIndexes) + streams (return ())++ foldStreamableMaps (makeTrigger triggers streams prophArrs tmpSamples+ outputIndexes)+ streams (return ())++ foldSendableMaps (makeSend outputs) sends (return ())++ -- Sampling of the external variables+ sampleVars tmpSamples)+ where+ optP = getOptimalPeriod streams+ p' = + case p of+ Nothing -> optP+ Just i -> if i >= optP + then i + else error $ "Copilot error: the period is too short, " + ++ "it should be at least " ++ show optP ++ " ticks."++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''+ _ -> []++initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a)+initOutput v s = streamToUnitValue ("outputVal__" ++ normalizeVar v) s++initTmpSamples :: forall a. Streamable a => Var -> Spec a -> A.Atom TmpSamples -> A.Atom TmpSamples+initTmpSamples _ s tmpSamples =+ case s of+ Const _ -> tmpSamples+ Var _ -> tmpSamples+ Drop _ s' -> initTmpSamples undefined s' tmpSamples+ Append _ s' -> initTmpSamples undefined s' tmpSamples+ F _ _ s0 -> initTmpSamples undefined s0 tmpSamples+ F2 _ _ s0 s1 -> initTmpSamples undefined s0 $+ initTmpSamples undefined s1 tmpSamples+ F3 _ _ s0 s1 s2 -> initTmpSamples undefined s0 $+ initTmpSamples undefined s1 $+ initTmpSamples undefined s2 tmpSamples+ PVar _ v ph -> + do+ ts <- tmpSamples+ let v' = normalizeVar v ++ "_" ++ show ph+ maybeElem = (getMaybeElem v' ts)::(Maybe (PhasedValue a))+ name = "tmpSampleVal__" ++ normalizeVar v'+ case maybeElem of+ Nothing -> + do+ val <- streamToUnitValue name s+ let m' = M.insert v' (Ph ph val) (getSubMap ts)+ return $ updateSubMap (\_ -> m') ts+ Just _ -> return ts -- to avoid duplicates. + -- Beware : crashes if "tmpSamples" instead of "return ts" ++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++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 Spec -> Outputs -> ProphArrs -> TmpSamples -> + Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()+makeRule streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do+ r + let B n maybeArr = (getElem v prophArrs)::(BoundedArray a)+ 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 0 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do+ ((getElem v outputs)::(A.V a)) A.<== nextSt'++ Just arr -> do+ let updateIndex = fromJust $ M.lookup v updateIndexes+ outputIndex = fromJust $ M.lookup v outputIndexes++ A.exactPhase 0 $ A.atom ("update__" ++ normalizeVar v) $ do+ arr A.! (A.VRef updateIndex) A.<== nextSt'+ + A.exactPhase 1 $ A.atom ("output__" ++ normalizeVar v) $ do+ ((getElem v outputs)::(A.V a)) A.<== arr A.!. (A.VRef outputIndex)+ outputIndex A.<== (A.VRef outputIndex + A.Const 1) `A.mod_` A.Const (n + 1)+ + A.phase 1 $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do+ updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1)++-- A.phase 2 $ A.atom ("incrOutputIndex__" ++ normalizeVar v) $ do+++ where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0++makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom ()+makeSend outputs name (Send (v, ph, port)) r =+ r >>+ do+ A.exactPhase ph $ A.atom ("__send_" ++ name) $+ send ((A.value (getElem v outputs))::(A.E a)) port++sampleVars :: TmpSamples -> A.Atom ()+sampleVars tmpSamples = + sequence_ $ foldStreamableMaps sample tmpSamples []+ where+ sample :: Streamable a => Var -> PhasedValue a -> [A.Atom ()] -> [A.Atom ()]+ sample v' (Ph ph val) xs = + (A.exactPhase ph $ + A.atom ("sample__" ++ normalizeVar v') $ + val A.<== (A.value $ externalAtomConstructor v)+ ) : xs+ where+ -- TODO : fix this mess+ v0 = reverse (tail (dropWhile (\c -> c /= '_') (reverse v')))+ (v1, n_final) = foldl (\ (s, n) c -> + if c == '_' + then (s, n + 1) + else (s ++ underscoreNumber2Symbol n ++ [c],0)+ ) ("", 0) v0+ v = v1 ++ underscoreNumber2Symbol n_final+ underscoreNumber2Symbol 0 = ""+ underscoreNumber2Symbol 1 = "_"+ underscoreNumber2Symbol 2 = "."+ underscoreNumber2Symbol 3 = "["+ underscoreNumber2Symbol 4 = "]"+ underscoreNumber2Symbol _ = undefined++getOptimalPeriod :: StreamableMaps Spec -> Period+getOptimalPeriod streams =+ foldStreamableMaps getMaximumSamplingPhase streams 2+ where+ getMaximumSamplingPhase :: Var -> Spec a -> Period -> Period + getMaximumSamplingPhase _ spec n =+ case spec of+ PVar _ _ p -> max (p + 1) n+ F _ _ s -> getMaximumSamplingPhase "" s n+ F2 _ _ s0 s1 -> maximum [n,+ (getMaximumSamplingPhase "" s0 n),+ (getMaximumSamplingPhase "" s1 n)]+ F3 _ _ s0 s1 s2 -> maximum [n,+ (getMaximumSamplingPhase "" s0 n), + (getMaximumSamplingPhase "" s1 n), + (getMaximumSamplingPhase "" s2 n)]+ Drop _ s -> getMaximumSamplingPhase "" s n+ Append _ s -> getMaximumSamplingPhase "" s n+ _ -> n
+ Language/Copilot/Core.hs view
@@ -0,0 +1,542 @@+{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, + FlexibleInstances #-}++-- | 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 (+ -- * Type hierarchy for the copilot language+ Var, Name, Period, Phase, Port,+ Spec(..), Streams, Stream, Sends, Send(..), DistributedStreams,+ -- * General functions on 'Streams' and 'StreamableMaps'+ Streamable(..), Sendable(..), StreamableMaps(..), emptySM,+ isEmptySM, getMaybeElem, getElem, streamToUnitValue,+ foldStreamableMaps, foldSendableMaps, mapStreamableMaps, mapStreamableMapsM,+ filterStreamableMaps, normalizeVar, getVars,+ Vars+ -- Compiler+ , nextSt, BoundedArray(..), Outputs, TmpSamples+ , PhasedValue(..), ProphArrs, Indexes+ ) where++import qualified Language.Atom as A+import Data.Int+import Data.Word+import Data.Maybe+import Data.List+import qualified Data.Map as M+import Text.Printf+import Control.Monad.Writer ++---- Type hierarchy for the copilot language -----------------------------------++-- | Names of the streams or external variables+type Var = String+-- | C file name+type Name = String+-- | Atom period+type Period = Int+-- | Phase of an Atom phase+type Phase = Int+-- | Port over which to broadcast information+type 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+ PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a+ Var :: Streamable a => Var -> Spec a+ Const :: Streamable a => a -> 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++{-# 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 ph) (PVar t' v' ph') = t == t' && v == v' && 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++-- | Container for mutually recursive streams, whose specifications may be+-- parameterized by different types+--type Streams = StreamableMaps Spec+type Streams = Writer (StreamableMaps Spec) ()+-- | A named stream+type Stream a = Streamable a => (Var, Spec a)+-- | An instruction to send data on a port at a given phase+data Send a = Sendable a => Send (Var, Phase, Port)+-- | Container for all the instructions sending data, parameterised by different types+type Sends = StreamableMaps Send +-- | 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++ -- | To make customer C triggers. Only for Spec Bool (others through an error).+ makeTrigger :: Maybe [(Var, String)] -> StreamableMaps Spec + -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a + -> A.Atom () -> A.Atom ()+++class Streamable a => Sendable a where+ send :: A.E a -> Port -> A.Atom ()++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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >>+ if trig /= ""+ then (A.exactPhase 0 $ A.atom ("trigger__" ++ normalizeVar v) $ do+ A.cond (nextSt streams prophArrs tmpSamples outputIndexes s 0)+ A.call trig)+ else return ()+ where trigs = case triggers of+ Nothing -> []+ Just t -> t+ trig = case M.lookup v (M.fromList trigs) of+ Nothing -> ""+ Just fn -> fn++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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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)+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()+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+ makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return ()++instance Sendable Word8 where+ send e port =+ A.action (\ [ueString] -> "sendW8_port" ++ show port + ++ "(" ++ ueString ++ ")") [A.ue e]++-- | 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 = fromJust $ getMaybeElem v sm++-- | Just produce an @Atom@ value named after its first argument,+-- with an unspecified value. The second argument only coerces the type, it is discarded+{-# INLINE streamToUnitValue #-}+streamToUnitValue :: Streamable a => Var -> Spec a -> A.Atom (A.V a)+streamToUnitValue v _ = atomConstructor v unit++-- | This function is used to iterate on all the values in all the maps stored+-- by a @'StreamableMaps'@, accumulating a value over time+{-# INLINE foldStreamableMaps #-}+foldStreamableMaps :: forall b c. + (forall a. Streamable a => Var -> c a -> b -> b) -> + StreamableMaps c -> b -> b+foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =+ let acc0 = M.foldWithKey f acc bm+ acc1 = M.foldWithKey f acc0 i8m + acc2 = M.foldWithKey f acc1 i16m+ acc3 = M.foldWithKey f acc2 i32m+ acc4 = M.foldWithKey f acc3 i64m+ acc5 = M.foldWithKey f acc4 w8m+ acc6 = M.foldWithKey f acc5 w16m+ acc7 = M.foldWithKey f acc6 w32m+ acc8 = M.foldWithKey f acc7 w64m+ acc9 = M.foldWithKey f acc8 fm + acc10 = M.foldWithKey f acc9 dm+ in acc10++-- | This function is used to iterate on all the values in all the maps stored+-- by a @'StreamableMaps'@, accumulating a value over time+{-# INLINE foldSendableMaps #-}+foldSendableMaps :: forall b c. + (forall a. Sendable a => Var -> c a -> b -> b) -> + StreamableMaps c -> b -> b+foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =+ let acc1 = M.foldWithKey f acc w8m+ in acc1++{-# 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 => + (forall a. 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. StreamableMaps c -> [(A.Type, Var, Phase)] -> (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@(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') = overlap+ where overlap = let multDefs = (getVars x `intersect` getVars y)+ in if null multDefs then union+ else error $ "Copilot error: The variables " + ++ show multDefs ++ " have multiple definitions."+ 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 Spec -> [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 =+ foldl (\ acc c -> acc ++ case c of '.' -> "__" ; '[' -> "___" ; ']' -> "____" ; _ -> [c]) "" v++-- | For each typed variable, this type holds all its successive values in an infinite list+-- Beware : each element of one of those lists corresponds to a full @Atom@ period, +-- 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 ph) _ = "PVar " ++ show t ++ " " ++ v ++ " " ++ show ph+showRaw (Var v) _ = "Var " ++ v+showRaw (Const e) _ = "Const " ++ 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 " ") ++ ")"+++-- Compiler: the code below really belongs in Core.hs, but its called by+-- makeTrigger, which is a method of the class Streamable.++type ArrIndex = Word64++type ProphArrs = StreamableMaps BoundedArray+type Outputs = StreamableMaps A.V+type TmpSamples = StreamableMaps PhasedValue+type Indexes = M.Map Var (A.V ArrIndex)+data PhasedValue a = Ph Phase (A.V a)+-- important invariant : the maybe is Nothing iff the int is 0+data BoundedArray a = B ArrIndex (Maybe (A.A a))++getValue :: PhasedValue a -> A.V a+getValue (Ph _ val) = val++nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes + -> Spec a -> ArrIndex -> A.E a+nextSt streams prophArrs tmpSamples outputIndexes s index =+ case s of+ PVar _ v ph -> A.value . getValue + $ getElem (normalizeVar v ++ "_" ++ show ph) tmpSamples+ Var v -> let B initLen maybeArr = getElem v prophArrs in+ -- This check is extremely important+ -- It means that if x at time n depends on y at time n+ -- then x is obtained not by y, but by inlining the definition of y+ -- so it increases the size of code (sadly),+ -- but is the only thing preventing race conditions from occuring+ if index < initLen+ -- if maybeArr == Nothing, then initLen == 0 and is <= index+ then+ let outputIndex = fromJust $ M.lookup v outputIndexes in+ (fromJust maybeArr) A.!. + ((A.Const index + A.VRef outputIndex) `A.mod_` + (A.Const (initLen + 1)))+ else next (getElem v streams) (index - initLen)+ Const e -> A.Const e+ F _ f s0 -> f $ next s0 index+ F2 _ f s0 s1 ->+ f (next s0 index) (next s1 index)+ F3 _ f s0 s1 s2 ->+ f (next s0 index) (next s1 index) (next s2 index)+ Append _ s' -> next s' index+ Drop i s' -> next s' (fromInteger (toInteger i) + index)+ where+ next :: Streamable b => Spec b -> ArrIndex -> A.E b+ next = nextSt streams prophArrs tmpSamples outputIndexes+
+ Language/Copilot/Dispatch.hs view
@@ -0,0 +1,262 @@+{-# 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+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 Data.List ((\\))++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+ , prePostCode :: Maybe (String, String) -- ^ Code to replace the default initialization and main+ , triggers :: Maybe [(Var, String)] -- ^ A list of Copilot variable C+ -- function name pairs. The C+ -- funciton is called if the+ -- Copilot stream becomes True.+ -- The Stream must be of Booleans+ -- and the C function must be of+ -- type void @foo(void)@.++ }++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 :: StreamableMaps Spec -> Sends -> Vars -> BackEnd -> Iterations -> Verbose -> IO ()+dispatch streams sends inputExts backEnd iterations verbose =+ do+ hSetBuffering stdout LineBuffering+ when isVerbose $ mapM_ putStrLn preludeText + isValid <-+ case check streams of+ Just x -> putStrLn (show x) >> return False+ Nothing -> return True+ when isValid $+ -- because haskell is lazy, will only get computed if later used+ let interpretedLines = showVars (interpretStreams streams trueInputExts) iterations + in case backEnd of+ Interpreter -> + do+ when (not allInputsPresents) $ error + "the interpreter don't have the values for some of the external variables"+ mapM_ putStrLn interpretedLines+ Opts opts ->+ let isInterpreted =+ case (interpreted opts) of+ Interpreted -> True+ NotInterpreted -> False+ dirName = outputDir opts+ in do+ putStrLn $ "Trying to create (if missing) " ++ dirName ++ " ..."+ createDirectoryIfMissing False dirName+ checkTriggerVars streams (triggers opts) + copilotToC streams sends allExts trueInputExts + (cName opts) (getPeriod opts) (prePostCode opts) + (triggers opts) isVerbose+ let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext)+ let delete ext = do + f0 <- canonicalizePath (cName opts ++ ext) + f1 <- canonicalizePath (dirName ++ cName opts ++ ext)+ if f0 == f1 then return ()+ else removeFile (cName opts ++ ext)+ putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts ++ ".h to " + ++ dirName ++ " ..."+ copy ".c"+ copy ".h"+ delete ".c"+ delete ".h"+ when (prePostCode opts == Nothing) $ gccCall (Opts opts)+ when ((isInterpreted || isExecuted) && not allInputsPresents) $ error + "The interpreter doesn't have the values for some of the external variables."+ when isExecuted $ execute streams (dirName ++ cName opts) trueInputExts isInterpreted + interpretedLines iterations isSilent+ where+ isVerbose = verbose == Verbose+ isSilent = verbose == OnlyErrors+ isExecuted = iterations /= 0+ allExts = getExternalVars streams+ (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts++-- Check that each trigger references an actual Copilot variable of type Bool.+checkTriggerVars :: StreamableMaps Spec -> Maybe [(Var, String)] -> IO ()+checkTriggerVars streams triggers = + if null badDefs+ then if null badTypes+ then return ()+ else error $ "Copilot error in defining triggers: the variables " + ++ show (map fst badTypes)+ ++ " are of a type other than Bool."+ else error $ "Copilot error in defining triggers: the variables " ++ show badDefs + ++ " are given triggers but "+ ++ "don't define streams in-scope."+ where badDefs = map fst bareTriggers \\ getVars streams+ listAtomTypes :: Streamable a => Var -> Spec a -> [(Var, A.Type)] -> [(Var, A.Type)]+ listAtomTypes v s ls = + let t = getAtomType s + in if t /= A.Bool && v `elem` (map fst bareTriggers) then (v, t):ls else ls+ badTypes = foldStreamableMaps listAtomTypes streams []+ bareTriggers = + case triggers of+ Nothing -> []+ Just t -> t++copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, Phase)] -> Vars + -> Name -> Maybe Period -> Maybe (String, String) -> Maybe [(Var, String)] -> Bool -> IO ()+copilotToC streams sends allExts trueInputExts cFileName p prePostC triggers isVerbose =+ let (p', program) = copilotToAtom streams sends p triggers+ (preCode, postCode) = + case prePostC of+ Nothing -> getPrePostCode cFileName streams allExts trueInputExts p'+ Just (pre, post) -> (pre, post)+ atomConfig = A.defaults + {A.cCode = \_ _ _ -> (preCode, postCode),+ A.cRuleCoverage = False,+ A.cAssert = False,+ A.cStateName = "copilotState" ++ cFileName}+ in do+ putStrLn $ "Compiling Copilot specs to C ..."+ (sched, _, _, _, _) <- A.compile cFileName atomConfig program+ if isVerbose + then putStrLn $ A.reportSchedule sched+ else return ()+ putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"++gccCall :: BackEnd -> IO ()+gccCall backend = + 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"+ putStrLn $ show 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 = + (when (not 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]+-- XXX TODO : fill the blanks in the text below+preludeText = + [ "================================================================="+ , " CoPilot, a stream language for generating "+ , " hard real-time C monitors."+ , "================================================================="+ , "Built on the Atom, for generating deterministic time and space"+ , "embedded C programs."+ , "BSD3 License" + , "<Some copyright text.>"+ , "<Website.>"+ , "Lee Pike, Robin Morisset, and Sebastian Niller"+ , "Usage: <help>"+ , ""+ ]
+ Language/Copilot/Examples/Examples.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE FlexibleContexts #-}++module Language.Copilot.Examples.Examples where++import Data.Word+import Prelude (($))+import qualified Prelude as P+import qualified Prelude as Prelude++-- for specifying options+import Data.Map (fromList) +import Data.Maybe (Maybe (..))+import System.Random+import Data.Int++import Language.Copilot.Core+import Language.Copilot.Language+import Language.Copilot.Interface+import Language.Copilot.Variables+import Language.Copilot.PrettyPrinter++import Language.Copilot.Libs.LTL++fib :: Streams+fib = do+ "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")+ "t" .= even (var "fib")+ where even :: Spec Word64 -> Spec Bool+ even w' = w' `mod` const 2 == const 0++t1 :: Streams+t1 = do+ x .= [0, 1, 2] ++ var x - (drop 1 $ varI32 x)+ y .= [True, False] ++ var y ^ var z+ z .= varI32 "x" <= drop 1 (var 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+ a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1+ b .= [True, False] ++ 2 + var a < 5 + extW32 "ext" 1++t4 :: Streams+t4 = do+ a .= [True,False] ++ not (var a)+ b .= drop 1 (varB a)++t5 :: Streams+t5 = do+ x .= drop 3 (varB y)+ y .= [True, True] ++ not (var z)+ z .= [False, False] ++ not (var z)+ w .= varB x || var y++yy :: Streams+yy = do a .= constW64 4 ++zz :: Streams+zz = do --a .= [0..4] ++ drop 4 (varW32 a) + 1+ a .= (varW32 a) + 1+ b .= drop 3 (varW32 a)++xx :: Streams+xx = do + a .= extW32 "ext" 5 + b .= [3] ++ (varW32 a)+ c .= [0, 1, 3, 4] ++ drop 1 (varW32 b)++-- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the+-- engine is immediately shut off. From the paper.+engine :: Streams+engine = do+ "temps" .= [0, 0, 0] ++ extF "temp" 1+ "overTempRise" .= drop 2 (varF "temps") > const 2.3 + var "temps"+ "trigger" .= (var "overTempRise") ==> (extB "shutoff" 2) ++-- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist"+-- s at phase 2 on port 1. Not stable.+dist :: DistributedStreams+dist = + ( a .= [0,1] ++ (var a) + constW8 1+ , sendW8 a (2, 1)+ ..| emptySM+ )++-- greatest common divisor.+gcd :: Word16 -> Word16 -> Streams+gcd n0 n1 = do + a .= alg n0 a b+ b .= alg n1 b a+ "ans" .= varW16 a == var b+ where alg x0 x1 x2 = [x0] ++ mux (varW16 x1 > var x2) (var x1 - var x2) (var 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 + a .= alg "n" (sub a b)+ b .= alg "m" (sub b a)+ "ans" .= varW16 a == varW16 b && not (var "init")+ "init" .= [True] ++ const False+ where sub hi lo = mux (varW16 hi > var lo) (var hi - var lo) (var hi)+ alg ext ex = [0] ++ mux (var "init") (extW16 ext 1) ex++testCoercions :: Streams+testCoercions = do+ "short" .= ((cast (varW64 "fib"))::(Spec Word8)) + "long" .= ((cast (varW8 "short"))::(Spec Word32))++testCoercionsInt :: Streams+testCoercionsInt = do+ "counter" .= [0] ++ varW8 "counter" + 1 + "int" .= ((cast (varW8 "counter"))::(Spec Int8)) ++testRules :: Streams+testRules = do+ "v1" .= (not (Const True)) || Var "v2" + "v2" .= [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 + "v3" .= 0 + drop 3 (int8 6) + "v4" .= always 5 (Var "v1") ++i8 :: Streams+i8 = do+ v .= [0, 1] ++ (varI8 v) + 1 + +trap :: Streams+trap = do+ "target" .= [0] ++ varW32 "target" + 1 + "x" .= [0,0] ++ var "y" + varW32 "target" + "y" .= [0,0] ++ var "x" + varW32 "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")
+ Language/Copilot/Examples/LTLExamples.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE FlexibleContexts #-}++module Language.Copilot.Examples.LTLExamples () where++import Prelude (replicate, Int)++import Language.Copilot.Core+import Language.Copilot.Language +import Language.Copilot.Variables+import Language.Copilot.Libs.LTL+import Language.Copilot.Libs.Indexes++----------------+-- LTL tests ---+----------------++test, output :: Var+test = "test"+output = "output"+++-- Can be tested with various values of n. Use the interpreter to see the outputs.++tSoonest :: Int -> Streams+tSoonest n = do test .= (replicate (n+2) False) ++ const True+ output .= soonest n (var test)+ ++tLatest :: Int -> Streams+tLatest n = do test .= (replicate (n-2) False) ++ const True+ output .= latest n (var test)+ ++tAlways :: Int -> Streams+tAlways n = do test .= (replicate (n+3) True) ++ const False+ output .= always n (varB test)+ ++tFuture :: Int -> Streams+tFuture n = do test .= (replicate (n+3) False) ++ varB a+ a .= [False] ++ not (var a)+ output .= eventually n (varB test)+ ++tUntil :: Int -> Streams+tUntil n = do "t1" .= (replicate (n+2) False) ++ varB c+ c .= [True] ++ not (var c)+ "t0" .= const True+ output .= until n (varB "t0") (varB "t1")+ ++tRelease0 :: Int -> Streams+tRelease0 n = do output .= release n (const False) (const True)+ ++tRelease1 :: Int -> Streams+tRelease1 n = do "t1" .= (replicate (n+2) True) ++ varB c+ c .= [False] ++ not (var c)+ "t0" .= const True+ output .= release n (varB "t0") (varB "t1")+
+ Language/Copilot/Examples/PTLTLExamples.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE FlexibleContexts #-}++module Language.Copilot.Examples.PTLTLExamples where++import Prelude ()++import Language.Copilot.Core+import Language.Copilot.Language+import Language.Copilot.Interface +import Language.Copilot.Variables+import Language.Copilot.PrettyPrinter+import Language.Copilot.Libs.PTLTL++-- Next examples are for testing of the ptLTL library++-- test of previous+tstdatprv :: Streams+tstdatprv = a .= [True, False] ++ varB a + +tprv :: Streams+tprv = do+ tstdatprv + c `previous` (varB a) ++-- test of alwaysBeen+tstdatAB :: Streams+tstdatAB = d .= [True, True, True, True, True, True, True, False] ++ varB d++tAB :: Streams+tAB = do+ tstdatAB + f `alwaysBeen` (var d) ++-- test of eventuallyPrev+tstdatEP :: Streams+tstdatEP = g .= [False, False, False, False, False, True, False] ++ varB g ++tEP :: Streams+tEP = do+ tstdatEP + h `eventuallyPrev` (varB g) ++-- test of since+tstdat1Sin :: Streams+tstdat1Sin = "q1" .= [True, True, True, True, True, True, False ] ++ varB "q1"++tstdat2Sin :: Streams+tstdat2Sin = "q2" .= [False, False, True, False, False, False, False ] ++ varB "q2"+ +tSin :: Streams +tSin = do + tstdat1Sin + tstdat2Sin + "z1" `since` (varB "q1", varB "q2") ++-- with external variables+-- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20+tSinExt :: Streams +tSinExt = do+ "z1" `since` (extB "e1" 2, extB "q2" 3)
+ Language/Copilot/Examples/StatExamples.hs view
@@ -0,0 +1,21 @@+module Language.Copilot.Examples.StatExamples where++import Prelude ()+import Language.Copilot.Core+import Language.Copilot.Language+import Language.Copilot.Interface+import Language.Copilot.Variables+import Language.Copilot.PrettyPrinter+import Language.Copilot.Libs.Statistics++t0 :: Streams+t0 = do+ a .= [0..5] ++ (varW16 a) + 6+ "min" .= min 3 (varW16 a)+ "max" .= max 3 (varW16 a)+ "sum" .= sum 3 (varW16 a)++tMean :: Streams+tMean = do+ a .= [0..5] ++ (varD a) + 6+ "out" .= mean 4 (varD a)
+ Language/Copilot/Help.hs view
@@ -0,0 +1,178 @@+-- | 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 RNDS [$ OPTS] baseOpts"+ , " Executes the interpreter for the Copilot specification STREAMS of type"+ , " 'Streams', where the specification is interpreted as a set of mutually-"+ , " recursive Haskell infinite lists. The output from the lists is given"+ , " for RNDS indexes. RNDS must be greater than 0."+ , ""+ , " > compile STREAMS FILENAME [$ OPTS] baseOpts"+ , " Compiles the Copilot specification STREAMS to constant-time & constant-"+ , " constant-space C program named FILENAME.c with header FILENAME.h"+ , " and executable FILENAME."+ , ""+ , " > test RNDS [$ OPTS] baseOpts"+ , " 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."+ , ""+ , " > Prelude.putStr $ Prelude.show STREAMS -- or simply"+ , " > STREAMS -- in ghci"+ , " Pretty-prints the parsed Copilot specification of type 'Streams'."+ , ""+ , " > verify PATH/FILE.c"+ , " 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. 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, that is included in baseOpts. For"+ , "each option, we describe the default."+ , ""+ , " 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."+ , ""+ , " setPP :: (String, String) -> Options -> Options (c)"+ , " default: Nothing. The default generates a main() function that calls"+ , " Copilot code to run simulations."+ , ""+ , " Sets C code to pretty-print before and after the generated Copilot"+ , " code: the before code is the first element of the tuple and the after"+ , " code is the second element. 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. ('PP' stands for 'pretty-print'.)" + , ""+ , " NOTE: when the pre-/post-code is anything but Nothing, the C compiler"+ , " is NOT called---we assume you're doing a custom build. We do NOT"+ , " instrument your code with a 'main()' function simulator. Use this"+ , " function to generate embedded programs."+ , "" + , " setTriggers :: [(Var, String)] -> Options -> Options (c)"+ , " Provide a list of pairs '(v, n)', where 'v' is a Copilot variable"+ , " (a String) denoting a stream of Booleans, and 'n' is the name of a C"+ , " function to call if that stream ever takes the value True. The"+ , " declaration of the C function must be 'void n(void)'. 'n()' is called"+ , " in phase 0, the same phase that the state is updated (that is, the"+ , " trigger fires at the soonest phase possible."+ , ""+ , " setTriggers MUST be used in conjunction with the setPP option, as the"+ , " simulator does not know about custom trigger functions."+ , ""+ , " setO :: Name -> Options -> Options (t)"+ , " default: \"copilotProgram\""+ , " Sets the name of the executable (e.g., -o) generated by the C"+ , " compiler."+ , ""+ , ""+ , "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 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()."+ , ""+ , " > compile t2 \"t2\" $ setTriggers [(\"b0\",\"foo0\"), (\"b1\",\"foo1\")]"+ , " $ setPP (pre, post) baseOpts"+ , " Compile Copilot spec t2 to t2.c, with triggers void 'foo0(void)' and"+ , " 'void foo1(void)' for Boolean Copilot streams \"b0\" and \"b1\","+ , " respectively. 'pre' and 'post' are constants that (at least) provide"+ , " headers for foo0 and foo1 (in 'pre') and definitions for foo0 and foo1"+ , " in 'post'." + , ""+ , " > test 1000 baseOpts"+ , " Compare the compiler and interpreter for a randomly-generated Copilot"+ , " spec for 1000 iterations."+ , ""+ , " > Prelude.sequence_ [test 100 $ setR x baseOpts | x <- [0..100]]"+ , " Compare the compiler and interpreter on 100 randomly-generated Copilot"+ , " specs, for 100 iterations each."+ , ""+ , " > verify \"foo.c\""+ , " Calls cbmc on foo.c (where foo.c is in the current directory)."+ ]
+ Language/Copilot/Interface.hs view
@@ -0,0 +1,243 @@+-- | Used by the end-user to easily give its arguments to dispatch.+module Language.Copilot.Interface (+ Options(), baseOpts, test, interpret, compile, verify, interface+ , help , setS, setE, setC, setO, setP, setI, setPP, setN, setV, setR+ , setDir, setGCC, setTriggers,+ module Language.Copilot.Dispatch+ ) where++import Language.Copilot.Core+import Language.Copilot.Language (opsF, opsF2, opsF3)+import Language.Copilot.Tests.Random+import Language.Copilot.Dispatch+import Language.Copilot.Help++import Data.Set as Set (fromList, toList)+import Data.List ((\\))+import System.Random+import System.Exit+import System.FilePath (takeBaseName)+import System.Cmd+import Data.Maybe+import Control.Monad+import Control.Monad.Writer (execWriter)++data Options = Options {+ optStreams :: Maybe Streams, -- ^ If there's no Streams, then generate random streams.+ optSends :: Sends, -- ^ 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, String), -- ^ Code to append above and below the C file.+ optTriggers :: Maybe [(Var, String)] -- ^ A list of Copilot variable C+ -- function name pairs. The C+ -- funciton is called if the+ -- Copilot stream becomes True.+ -- The Stream must be of Booleans+ -- and the C function must be of+ -- type void @foo(void)@. There+ -- should be no more than one+ -- function per trigger variable.+ -- Triggers fire in the same phase (1)+ -- that output vars are assigned.+ }++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,+ optTriggers = 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 $ opts ++interpret :: Streams -> Int -> Options -> IO ()+interpret streams n opts = interface $ setI $ setN n $ opts {optStreams = Just streams}++compile :: Streams -> Name -> Options -> IO ()+compile streams fileName opts = + interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams}++verify :: FilePath -> IO ()+verify file = 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 " ++ theMain ++ " as the entry point:"+ putStrLn cmd+ code <- system cmd+ case code of+ ExitSuccess -> return ()+ _ -> do putStrLn $ "cbmc could not be called on file " ++ file ++ "."+ putStrLn "Perhaps cbmc is not installed on your system, is"+ putStrLn "not in your path, cbmc cannot be called from the"+ putStrLn $ "command line on your system, or " ++ file + putStrLn $ "does not exist, or the dispatch function in" ++ file+ putStrLn $ "is not called " ++ theMain ++ "." + putStrLn "See <http://www.cprover.org/cbmc/>"+ putStrLn "for more information on cbmc."+ where theMain = takeBaseName file+ cmd = unwords ("cbmc" : args)+ args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"+ , "--nan-check", "--pointer-check"+ , "--function " ++ theMain, file] + +++-- Small functions for easy modification of the Options record++setS :: DistributedStreams -> Options -> Options+setS (streams, sends) opts = opts {optStreams = Just streams, optSends = sends}++-- | Sets the environment for simulation by giving a mapping of external variables to lists of values. E.g., +-- +-- @ 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}++-- | 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}++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+setPP :: (String, String) -> Options -> Options+setPP pp opts = opts {optPrePostCode = Just pp}++-- | Give C function triggers for Copilot Boolean streams. The tiggers fire if+-- the stream becoms true.+setTriggers :: [(Var, String)] -> Options -> Options+setTriggers triggers opts = + if null repeats + then opts {optTriggers = Just triggers}+ else error $ "Error: only one trigger per Copilot variable. Variables "+ ++ show (Set.fromList repeats) ++ " are given multiple triggers."+ where vars = map fst triggers+ repeats = vars \\ Set.toList (Set.fromList vars)++-- | The "main" function+interface :: Options -> IO ()+interface opts =+ do+ seed <- createSeed opts + let (streams, vars) = getStreamsVars opts seed+ sends = optSends 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 streams sends 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++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)+ where s' = execWriter s+ +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,+ triggers = optTriggers opts+ }++help :: IO ()+help = putStrLn helpStr
+ Language/Copilot/Interpreter.hs view
@@ -0,0 +1,34 @@+-- | This interpreter is mostly used for checking the /Copilot/ implementation.+-- But it can also be used for quick testing of a /Copilot/ design+module Language.Copilot.Interpreter(interpretStreams) where++import Language.Copilot.Core++import Data.List +import Prelude++-- | The main function of this module.+-- It takes a /Copilot/ specification, the values of the monitored values,+-- and returns the values of the streams.+interpretStreams :: StreamableMaps Spec -> Vars -> Vars+interpretStreams streams moVs =+ inVs+ where + inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams++interpret :: Streamable a => Vars -> Vars -> Spec a -> [a]+interpret inVs moVs s =+ case s of+ Const c -> repeat c+ Var v -> getElem v inVs+ PVar _ v _ -> getElem v moVs+ Append ls s' -> ls ++ interpret inVs moVs s'+ Drop i s' -> drop i $ interpret inVs moVs s'+ F f _ s' -> map f (interpret inVs moVs s')+ F2 f _ s0 s1 -> zipWith f + (interpret inVs moVs s0)+ (interpret inVs moVs s1)+ F3 f _ s0 s1 s2 -> zipWith3 f + (interpret inVs moVs s0) + (interpret inVs moVs s1)+ (interpret inVs moVs s2)
+ Language/Copilot/Language.hs view
@@ -0,0 +1,509 @@+{-# LANGUAGE NoImplicitPrelude, Rank2Types, ScopedTypeVariables, FlexibleContexts #-}++-- | 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,+ CastIntTo(..),+ -- * The next functions are used only to coerce the type of their argument+ bool, int8, int16, int32, int64,+ word8, word16, word32, word64, float, double,+ -- * The next functions provide easier access to typed external variables.+ extB, extI8, extI16, extI32, extI64,+ extW8, extW16, extW32, extW64, extF, extD,+ -- * Set of operators from which to choose during the generation of random streams+ opsF, opsF2, opsF3,+ -- * Constructs of the copilot language+ var, const, drop, (++), (.=), (..|), + -- * The next functions are typed variable declarations to help the type-checker.+ varB, varI8, varI16, varI32, varI64,+ varW8, varW16, varW32, varW64, varF, varD,+ -- * The next functions help typing the send operations+ -- Warning: there is no typechecking of that yet+ -- sendB, sendI8, sendI16, sendI32, sendI64,+ sendW8, -- , sendW16, sendW32, sendW64, sendF, sendD+ -- * Typed constant declarations.+ constB, constI8, constI16, constI32, constI64,+ constW8, constW16, constW32, constW64, constF, constD+ ) where++import qualified Language.Atom as A+import Data.Int+import Data.Word+import Data.Monoid+import Data.List(elem)+import System.Random+import qualified Data.Map as M+import Prelude ( Fractional((/)), Bool(..), Num(..), Float, Double+ , Fractional(..), fromInteger, fail, zip, (>>=), Show(..), error, ($))+import qualified Prelude as P+import Control.Monad.Writer++import Language.Copilot.Core+import Language.Copilot.Analyser+import Language.Copilot.Tests.Random++---- Operators and functions ---------------------------------------------------++not :: Spec Bool -> Spec Bool+not = F P.not A.not_++instance (Streamable a, A.NumE a) => P.Num (Spec a) where+ (+) = F2 (P.+) (P.+) -- A.NumE a => E a is an instance of Num+ (*) = F2 (P.*) (P.*)+ (-) = F2 (P.-) (P.-)+ negate = F P.negate P.negate+ abs = F P.abs P.abs+ signum = F P.signum P.signum+ fromInteger i = Const (P.fromInteger i)++instance (Streamable a, A.NumE a, P.Fractional a) => P.Fractional (Spec a) where+ (/) = F2 (P./) (P./)+ recip = F P.recip P.recip+ fromRational r = Const (P.fromRational r)++-- | Beware : crash without any possible recovery if a division by 0 happens.+-- Same risk with mod. Use div0 and mod0 if unsure.+mod, div :: (Streamable a, A.IntegralE a) => Spec a -> Spec a -> Spec a+mod = F2 P.mod A.mod_+div = F2 P.mod A.div_++-- | As mod and div, except that if the division would be by 0, it is instead by the first argument.+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)++(<), (<=), (>=), (>) :: (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++class (Streamable a, P.Integral a) => CastIntTo a where+ cast :: (Streamable b, A.IntegralE b) => Spec b -> Spec a++instance CastIntTo Word8 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (`A.mod_` (256::(A.E Word64))) P.. A.Retype P.. A.ue)+instance CastIntTo Word16 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (`A.mod_` (65536::(A.E Word64))) P.. A.Retype P.. A.ue)+instance CastIntTo Word32 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ 32)::(A.E Word64))) P.. A.Retype P.. A.ue)+instance CastIntTo Word64 where+ cast = F (P.fromInteger P.. P.toInteger) (A.Retype P.. A.ue)++instance CastIntTo Int8 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+instance CastIntTo Int16 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^15)::(A.E Word64))) `A.mod_` (2 P.^ 16)) P.- (2 P.^ 15)) P.. A.Retype P.. A.ue)+instance CastIntTo Int32 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+instance CastIntTo Int64 where+ cast = F (P.fromInteger P.. P.toInteger) (+ A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+++-- | 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 ||, &&, ^, ==>++-- Used for helping ghc in infering the type of the streams+bool :: Spec Bool -> Spec Bool+int8 :: Spec Int8 -> Spec Int8+int16 :: Spec Int16 -> Spec Int16+int32 :: Spec Int32 -> Spec Int32+int64 :: Spec Int64 -> Spec Int64+word8 :: Spec Word8 -> Spec Word8+word16 :: Spec Word16 -> Spec Word16+word32 :: Spec Word32 -> Spec Word32+word64 :: Spec Word64 -> Spec Word64+float :: Spec Float -> Spec Float+double :: Spec Double -> Spec Double+bool = P.id+int8 = P.id+int16 = P.id+int32 = P.id+int64 = P.id+word8 = P.id+word16 = P.id+word32 = P.id+word64 = P.id+float = P.id+double = P.id++-- Used for easily producing, and coercing PVars+extB :: Var -> Phase -> Spec Bool+extB = PVar A.Bool+extI8 :: Var -> Phase -> Spec Int8+extI8 = PVar A.Int8+extI16 :: Var -> Phase -> Spec Int16+extI16 = PVar A.Int16+extI32 :: Var -> Phase -> Spec Int32+extI32 = PVar A.Int32+extI64 :: Var -> Phase -> Spec Int64+extI64 = PVar A.Int64+extW8 :: Var -> Phase -> Spec Word8+extW8 = PVar A.Word8+extW16 :: Var -> Phase -> Spec Word16+extW16 = PVar A.Word16+extW32 :: Var -> Phase -> Spec Word32+extW32 = PVar A.Word32+extW64 :: Var -> Phase -> Spec Word64+extW64 = PVar A.Word64+extF :: Var -> Phase -> Spec Float+extF = PVar A.Float+extD :: Var -> Phase -> Spec Double+extD = PVar A.Double++---- Sets of operators for Tests.Random.hs -------------------------------------++---- Helper functions++mkOp :: (Random arg1, Streamable arg1) =>+ (Spec arg1 -> Spec r) -> Operator r+mkOp op =+ Operator (\ rand g ->+ let (s0, g0) = rand g FunSpecSet in+ (op s0, g0)+ )++mkOp2 :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>+ (Spec arg1 -> Spec arg2 -> Spec r) -> Operator r+mkOp2 op =+ Operator (\ rand g ->+ let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet in+ (op s0 s1, g1)+ )+ +mkOp3 :: (Random arg1, Random arg2, Random arg3, + Streamable arg1, Streamable arg2, Streamable arg3) =>+ (Spec arg1 -> Spec arg2 -> Spec arg3 -> Spec r) -> Operator r+mkOp3 op =+ Operator (\ rand g ->+ let (s0, g0) = rand g FunSpecSet+ (s1, g1) = rand g0 FunSpecSet+ (s2, g2) = rand g1 FunSpecSet in+ (op s0 s1 s2, g2)+ )++mkOp2Coerce :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) =>+ (Spec arg1 -> Spec arg2 -> Spec r) -> arg1 -> arg2 -> Operator r+mkOp2Coerce op c0 c1 =+ Operator (\ rand g ->+ let (s0, g0) = rand g FunSpecSet+ (s1, g1) = rand g0 FunSpecSet in+ (op (s0 `P.asTypeOf` (Const c0)) (s1 `P.asTypeOf` (Const c1)), g1)+ )++mkOp2Ord :: forall r. (forall arg. + (Random arg, A.OrdE arg, Streamable arg) =>+ (Spec arg -> Spec arg -> Spec r)) + -> Operator r+mkOp2Ord op =+ let opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)+ opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8)+ opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16)+ opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32)+ opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64)+ opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8)+ opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16)+ opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32)+ opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64)+ opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float)+ opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in+ Operator (\ rand g ->+ let (t, g0) = randomR (A.Int8, A.Double) g in+ case t of+ A.Int8 -> opI8 rand g0+ A.Int16 -> opI16 rand g0+ A.Int32 -> opI32 rand g0+ A.Int64 -> opI64 rand g0+ A.Word8 -> opW8 rand g0+ A.Word16 -> opW16 rand g0+ A.Word32 -> opW32 rand g0+ A.Word64 -> opW64 rand g0+ A.Float -> opF rand g0+ A.Double -> opD rand g0+ _ -> P.error "Impossible"+ )++mkOp2Eq :: forall r. (forall arg. + (Random arg, A.EqE arg, Streamable arg) =>+ (Spec arg -> Spec arg -> Spec r)) + -> Operator r+mkOp2Eq op =+ let opB, opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g)+ opB = fromOp P.$ mkOp2Coerce op (unit::Bool) (unit::Bool)+ opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8)+ opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16)+ opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32)+ opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64)+ opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8)+ opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16)+ opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32)+ opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64)+ opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float)+ opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in+ Operator (\ rand g ->+ let (t, g0) = random g in+ case t of+ A.Bool -> opB rand g0+ A.Int8 -> opI8 rand g0+ A.Int16 -> opI16 rand g0+ A.Int32 -> opI32 rand g0+ A.Int64 -> opI64 rand g0+ A.Word8 -> opW8 rand g0+ A.Word16 -> opW16 rand g0+ A.Word32 -> opW32 rand g0+ A.Word64 -> opW64 rand g0+ A.Float -> opF rand g0+ A.Double -> opD rand g0+ )++---- Definition of each operator++not_ :: Operator Bool+not_ = mkOp not + +(+$), (-$), (*$) :: (Streamable a, A.NumE a, Random a) => Operator a+(+$) = mkOp2 (P.+)+(-$) = mkOp2 (P.-)+(*$) = mkOp2 (P.*)++(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a+(/$) = mkOp2 (P./)++(<$), (<=$), (>=$), (>$) :: Operator Bool+(<$) = mkOp2Ord (<)+(<=$) = mkOp2Ord (<=)+(>=$) = mkOp2Ord (>=)+(>$) = mkOp2Ord (>)++(==$), (/=$) :: Operator Bool+(==$) = mkOp2Eq (==)+(/=$) = mkOp2Eq (/=)++(||$), (&&$), (^$), (==>$) :: Operator Bool+(||$) = mkOp2 (||)+(&&$) = mkOp2 (&&)+(^$) = mkOp2 (^)+(==>$) = mkOp2 (==>)++mux_ :: (Streamable a, Random a) => Operator a+mux_ = mkOp3 mux++-- Packing of the operators in StreamableMaps++createMapFromElems :: [val] -> M.Map Var val+createMapFromElems vals =+ let ks = [[x] | x <- ['a'..]]+ l = zip ks vals in+ M.fromAscList l++-- | opsF, opsF2 and opsF3 are feeded to Tests.Random.randomStreams.+-- They allows the random generated streams to include lots of operators.+-- If you add a new operator to Copilot, it would be nice to add it to one of those,+-- that way it could be used in the random streams used for testing.+-- opsF holds all the operators of arity 1, opsF2 of arity 2 and opsF3 of arity3+-- They are StreamableMaps, because operators are sorted based on their return type.+opsF, opsF2, opsF3 :: Operators+opsF = emptySM {bMap = createMapFromElems [not_]}++opsF2 = emptySM {+ bMap = createMapFromElems [(<$), (<=$), (>=$), (>$), (==$), (/=$), (||$), (&&$), (^$), (==>$)],+ i8Map = createMapFromElems [(+$), (-$), (*$)],+ i16Map = createMapFromElems [(+$), (-$), (*$)],+ i32Map = createMapFromElems [(+$), (-$), (*$)],+ i64Map = createMapFromElems [(+$), (-$), (*$)],+ w8Map = createMapFromElems [(+$), (-$), (*$)],+ w16Map = createMapFromElems [(+$), (-$), (*$)],+ w32Map = createMapFromElems [(+$), (-$), (*$)],+ w64Map = createMapFromElems [(+$), (-$), (*$)],+ fMap = createMapFromElems [(+$), (-$), (*$), (/$)],+ dMap = createMapFromElems [(+$), (-$), (*$), (/$)]+ }++opsF3 = emptySM {+ bMap = createMapFromElems [mux_],+ i8Map = createMapFromElems [mux_],+ i16Map = createMapFromElems [mux_],+ i32Map = createMapFromElems [mux_],+ i64Map = createMapFromElems [mux_],+ w8Map = createMapFromElems [mux_],+ w16Map = createMapFromElems [mux_],+ w32Map = createMapFromElems [mux_],+ w64Map = createMapFromElems [mux_],+ fMap = createMapFromElems [mux_],+ dMap = createMapFromElems [mux_]+ }++---- Constructs of the language ------------------------------------------------++-- | Stream variable reference+var :: Streamable a => Var -> Spec a+var v = Var v++-- If a generic 'var' declaration is insufficient for the type-checker to determine the type, a monomorphic var operator can be used+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++{-+sendB :: Var -> (Phase, Port) -> Send Bool+sendB v (ph, port) = Send (v, ph, port)+sendI8 :: Var -> (Phase, Port) -> Send Int8+sendI8 v (ph, port) = Send (v, ph, port)+sendI16 :: Var -> (Phase, Port) -> Send Int16+sendI16 v (ph, port) = Send (v, ph, port)+sendI32 :: Var -> (Phase, Port) -> Send Int32+sendI32 v (ph, port) = Send (v, ph, port)+sendI64 :: Var -> (Phase, Port) -> Send Int64+sendI64 v (ph, port) = Send (v, ph, port) -}+sendW8 :: Var -> (Phase, Port) -> Send Word8+sendW8 v (ph, port) = Send (v, ph, port)+{- sendW16 :: Var -> (Phase, Port) -> Send Word16+sendW16 v (ph, port) = Send (v, ph, port)+sendW32 :: Var -> (Phase, Port) -> Send Word32+sendW32 v (ph, port) = Send (v, ph, port)+sendW64 :: Var -> (Phase, Port) -> Send Word64+sendW64 v (ph, port) = Send (v, ph, port)+sendF :: Var -> (Phase, Port) -> Send Float+sendF v (ph, port) = Send (v, ph, port)+sendD :: Var -> (Phase, Port) -> Send Double+sendD v (ph, port) = Send (v, ph, port) -}++-- | A constant stream+const :: Streamable a => a -> Spec a+const x = Const x++constB :: Bool -> Spec Bool+constB = 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+++-- | 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++-- | Define a stream variable.+(.=) :: Streamable a => Var -> Spec a -> Streams+v .= s = tell (updateSubMap (M.insert v s) emptySM) ++-- | Allows to build a @'Sends'@ from specification+(..|) :: Sendable a => Send a -> Sends -> Sends+sendStmt@(Send (v, ph, port)) ..| sends = + updateSubMap (M.insert name sendStmt) sends+ where name = v P.++ "_" P.++ show ph P.++ "_" P.++ show port++infixr 3 +++infixr 2 .=+infixr 1 ..|++---- 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+ #-}
+ Language/Copilot/Libs/ErrorChks.hs view
@@ -0,0 +1,30 @@+-- | Basic error checking for other libraries.++module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where++import Prelude (Num, Integral, Int, String, error, ($), show, maxBound, toInteger)+import qualified Prelude as P +import Data.Int (Int16)++import Language.Copilot.Core++chk :: String -> Int -> Spec a -> Int -> Spec a+chk name n s m = + if n P.< m + then error $ "Value " P.++ show n P.++ " in operator " P.++ name + P.++ " must be greater than or equal to " P.++ show m P.++ "."+ 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) P.> max+ then error $ "Offset " P.++ show n P.++ " in operator " P.++ name + P.++ " is larger than the Int16 maxBound, " P.++ show max P.++ "."+ else s+ where max = toInteger (maxBound::Int16)
+ Language/Copilot/Libs/Indexes.hs view
@@ -0,0 +1,52 @@+-- | 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 (Integral, Bool(..), id, Int, String, error, fromIntegral, ($), show)+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 const (-1)+ else mux (f $ drop m s) (const $ 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 const (-1)+ else mux (f $ drop m s) (const $ 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+++ +
+ Language/Copilot/Libs/LTL.hs view
@@ -0,0 +1,57 @@+-- | Bounded Linear Temporal Logic (LTL) operators.++module Language.Copilot.Libs.LTL(always, next, eventually, until, release) where++import Prelude (Int, ($))+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++-- | Property @s@ holds for the next @n@ periods. If @n == 0@, then @s@ holds+-- in the current period. We require @n >= 0@.+-- E.g., if @p = always 2 s@, then we have the following relationship between the streams generated:+-- @+-- s => T T T T F F F F ...+-- p => T T F F F F F F ...+-- @+always :: Int -> Spec Bool -> Spec Bool+always n s = nPosChk "always" n $ foldl1 (&&) [drop x s | x <- [0..n]]++-- | Property @s@ holds at the next period.+next :: Spec Bool -> Spec Bool+next s = drop 1 s++-- | 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 F T F T F ...+-- p => F F T T T T T T ...+-- @+eventually :: Int -> Spec Bool -> Spec Bool+eventually n s = nPosChk "eventually" n $ foldl1 (||) [drop x s | x <- [0..n]] ++-- | @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+until n s0 s1 = + nPosChk "until" n $ ( (whenS0 < const 0) -- s0 didn't fail within n periods.+ || (soonest n s1 <= whenS0)) -- s0 failed at some point before n.+ && eventually n s1 -- guarantees that soonest n s1 >= 0+ where 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+release n s0 s1 = + nPosChk "release" n $ (whenS1 < const 0) -- s1 never fails+ || ( (whenS0 >= const 0) -- s0 becomes true at some point+ && (whenS0 < whenS1)) -- and when s0 becomes true,+ -- is strictly sooner than+ -- whne s1 fails.+ where whenS1 = soonestFail n s1+ whenS0 = soonest n s0
+ Language/Copilot/Libs/PTLTL.hs view
@@ -0,0 +1,39 @@+-- | Provides past-time linear-temporal logic (ptLTL operators).++-- XXX won't make unique tmp stream names if you use the same operator twice in+-- one stream definition.++module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where++import Prelude ()+import qualified Prelude as P++import Language.Copilot.Core+import Language.Copilot.Language++-- | Did @s@ hold in the previous period?+previous :: Var -> Spec Bool -> Streams+previous v s = do+ v .= [False] ++ s + +-- | Has @s@ always held?+alwaysBeen :: Var -> Spec Bool -> Streams+alwaysBeen v s = do+ tmp .= [True] ++ (var tmp) && s + v .= s && varB tmp+ where tmp = "alwaysBeenTmp_" P.++ v+ +-- | Did @s@ hold at some time in the past (including the current state)?+eventuallyPrev :: Var -> Spec Bool -> Streams+eventuallyPrev v s = do+ tmp .= [False] ++ (var tmp) || s+ v .= s || varB tmp+ where tmp = "eventuallyPrevTmp_" P.++ v++-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?+since :: Var -> (Spec Bool, Spec Bool) -> Streams+since v (s1, s2) = do+ tmp .= [False] ++ (s2 || (s1 && varB v)) + v .= varB tmp && s1+ where tmp = "sinceTmp_" P.++ v+
+ Language/Copilot/Libs/Statistics.hs view
@@ -0,0 +1,43 @@+-- | 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) where++import Prelude (Int, ($), foldl1, fromIntegral)+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) / (const $ fromIntegral n)++-- majority :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a+-- majority n s =
+ Language/Copilot/PrettyPrinter.hs view
@@ -0,0 +1,39 @@+{-# 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 Control.Monad.Writer (execWriter)++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.foldWithKey showVal "" bm+ acc1 = M.foldWithKey showVal acc0 i8m + acc2 = M.foldWithKey showVal acc1 i16m+ acc3 = M.foldWithKey showVal acc2 i32m+ acc4 = M.foldWithKey showVal acc3 i64m+ acc5 = M.foldWithKey showVal acc4 w8m+ acc6 = M.foldWithKey showVal acc5 w16m+ acc7 = M.foldWithKey showVal acc6 w32m+ acc8 = M.foldWithKey showVal acc7 w64m+ acc9 = M.foldWithKey showVal acc8 fm + acc10 = M.foldWithKey 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 (execWriter s) ++-- instance Show (StreamableMaps Spec) where+-- show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =+-- show bm
+ Language/Copilot/Tests/Random.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, GADTs, RankNTypes #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++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, maxSamplePhase :: 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.foldWithKey f acc bm+ acc1 = M.foldWithKey f acc0 i8m + acc2 = M.foldWithKey f acc1 i16m+ acc3 = M.foldWithKey f acc2 i32m+ acc4 = M.foldWithKey f acc3 i64m+ acc5 = M.foldWithKey f acc4 w8m+ acc6 = M.foldWithKey f acc5 w16m+ acc7 = M.foldWithKey f acc6 w32m+ acc8 = M.foldWithKey f acc7 w64m+ acc9 = M.foldWithKey f acc8 fm + acc10 = M.foldWithKey f acc9 dm+ 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+ (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)) v ph, g2)+ (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)
+ Language/Copilot/Variables.hs view
@@ -0,0 +1,32 @@+-- | Variable names++module Language.Copilot.Variables where++a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z :: String++a = "a"+b = "b"+c = "c"+d = "d"+e = "e"+f = "f"+g = "g"+h = "h"+i = "i"+j = "j"+k = "k"+l = "l"+m = "m"+n = "n"+o = "o"+p = "p"+q = "q"+r = "r"+s = "s"+t = "t"+u = "u"+v = "v"+w = "w"+x = "x"+y = "y"+z = "z"
+ README view
@@ -0,0 +1,33 @@+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+ "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")+ "t" .= even (var "fib")+ where even :: Spec Word64 -> Spec Bool+ even w = w `mod` const 2 == const 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.+++********+Please visit <http://leepike.github.com/Copilot/> for more information about+installing and using Copilot.++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.+********
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot.cabal view
@@ -0,0 +1,66 @@+name: copilot+version: 0.21+cabal-version: >= 1.2+license: BSD3+license-file: LICENSE+author: Lee Pike <leepike@gmail.com>, Robin Morisset, Alwyn Goodloe, Sebastian Niller+synopsis: A lazy-list language for generating constant-time and constant-space C programs. Uses Atom as a backend.+build-type: Simple+maintainer: Lee Pike <leepike@gmail.com>+category: Language+homepage: http://leepike.github.com/Copilot/+description: Can you write a list in Haskell? Then you can write embedded C code using+ Copilot. Here's a Copilot program that computes the Fibonacci sequence (over+ Word 64s) and tests for even numbers:+ .+ > fib :: Streams+ > fib = do+ > "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")+ > "t" .= even (var "fib")+ > where even :: Spec Word64 -> Spec Bool+ > even w = w `mod` const 2 == const 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.++extra-source-files: README++library+ ghc-options: -Wall+ build-depends: base > 4 && < 5+ , atom >= 1.0.5+ , containers >= 0.2.0.1+ , process >= 1.0.0.0+ , random >= 1.0.0.0+ , directory+ , mtl >= 1.0.0.0 + , filepath >= 1.0.0.0++ extensions:+ exposed-modules: Language.Copilot+ Language.Copilot.AdHocC+ Language.Copilot.Core+ Language.Copilot.Language+ 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.Variables+ Language.Copilot.Libs.ErrorChks+ Language.Copilot.Libs.PTLTL+ Language.Copilot.Libs.LTL+ Language.Copilot.Libs.Indexes+ Language.Copilot.Libs.Statistics+ Language.Copilot.Examples.Examples+ Language.Copilot.Examples.LTLExamples+ Language.Copilot.Examples.PTLTLExamples+ Language.Copilot.Examples.StatExamples