copilot 0.27 → 0.28
raw patch · 10 files changed
+291/−246 lines, 10 filesdep ~atomdep ~base
Dependency ranges changed: atom, base
Files
- Language/Copilot/AtomToC.hs +1/−1
- Language/Copilot/Compiler.hs +9/−7
- Language/Copilot/Core.hs +109/−83
- Language/Copilot/Dispatch.hs +17/−39
- Language/Copilot/Examples/Examples.hs +48/−45
- Language/Copilot/Help.hs +0/−19
- Language/Copilot/Interface.hs +32/−29
- Language/Copilot/Language.hs +65/−18
- README +4/−0
- copilot.cabal +6/−5
Language/Copilot/AtomToC.hs view
@@ -140,4 +140,4 @@ => Var -> Spec a -> [String] -> [String] decl v _ ls = (" " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ " ") - [vPre cName ++ "outputVal__" ++ v]) : ls+ [vPre cName ++ v]) : ls
Language/Copilot/Compiler.hs view
@@ -15,9 +15,8 @@ -- | 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 -> StreamableMaps Send -> Maybe Period - -> [(Var, String)] -> (Period, A.Atom ())-copilotToAtom streams sends p triggers = +copilotToAtom :: LangElems -> Maybe Period -> (Period, A.Atom ())+copilotToAtom (LangElems streams sends triggers) p = (p', A.period p' $ do prophArrs <- mapStreamableMapsM initProphArr streams@@ -35,10 +34,13 @@ updateIndexes outputIndexes) streams (return ()) - foldStreamableMaps (makeTrigger triggers streams prophArrs tmpSamples- outputIndexes)- streams (return ())+ -- foldStreamableMaps (makeTrigger streams prophArrs tmpSamples+ -- outputIndexes)+ -- triggers (return ()) + M.fold (makeTrigger streams prophArrs tmpSamples outputIndexes) + (return ()) triggers+ foldStreamableMaps (makeSend outputs) sends (return ()) -- Sampling of the external variables. Remove redundancies.@@ -75,7 +77,7 @@ initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) initOutput v _ = do- atomConstructor ("outputVal__" ++ normalizeVar v) (unit::a)+ atomConstructor (normalizeVar v) (unit::a) tmpSampleStr :: String tmpSampleStr = "tmpSampleVal__"
Language/Copilot/Core.hs view
@@ -11,9 +11,9 @@ -- * Type hierarchy for the copilot language Var, Name, Period, Phase, Port(..), Spec(..), Streams, Stream, Send(..), --DistributedStreams,- notVarErr, Both(..),+ Trigger(..), Triggers, notVarErr, LangElems(..), -- * General functions on 'Streams' and 'StreamableMaps'- Streamable(..), sendKey, mkSend, -- Sendable(..)+ Streamable(..), mkSend, -- Sendable(..) StreamableMaps(..), emptySM, isEmptySM, getMaybeElem, getElem, foldStreamableMaps, --foldSendableMaps, @@ -23,16 +23,17 @@ BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..), tmpVarName, tmpArrName, getAtomType,- getSpecs, getSends+ getSpecs, getSends, getTriggers, makeTrigger -- XXX compiler ) where import qualified Language.Atom as A+ import Data.Int import Data.Word import Data.List hiding (union) import qualified Data.Map as M import Text.Printf-import Control.Monad.Writer +import Control.Monad.Writer (Writer, Monoid(..), execWriter) ---- Type hierarchy for the copilot language ----------------------------------- @@ -113,22 +114,55 @@ , sendPort :: Port , sendName :: String} -data Both a b = Both a b+instance Streamable a => Show (Send a) where + show (Send s ph (Port port) portName) = + notVarErr s (\var -> (portName ++ "_port_" ++ show port ++ "_var_" + ++ var ++ "_ph_" ++ show ph))+data Trigger =+ Trigger { trigVar :: Spec Bool+ , trigName :: String+ -- We carry around both the value and the vars of the arguments to be+ -- passed to the trigger. The vars are used to put the arguments in+ -- the correct order, since the values are stored in a map, destroying+ -- their order.+ , trigArgs :: ([Var], StreamableMaps Spec)} +type Triggers = M.Map String Trigger++instance Show Trigger where + show (Trigger s fnName _) =+ notVarErr s (\var -> ("trigger_" ++ var ++ "_" ++ fnName ++ "_")) -- XXX add args+-- ++ map (\x -> if x == ' ' then '_' else x) +-- (concatMap show args)))++-- | Holds all the different kinds of language elements that are pushed into the+-- Writer monad. This currently includes the actual specs, "send" directives,+-- and trigger directives. (Use the functions in Language.hs to make sends and+-- triggers.)+data LangElems = LangElems + { strms :: StreamableMaps Spec+ , snds :: StreamableMaps Send+ , trigs :: Triggers}+ -- | Container for mutually recursive streams, whose specifications may be -- parameterized by different types-type Streams = Writer (Both (StreamableMaps Spec) (StreamableMaps Send)) ()+type Streams = Writer LangElems () getSpecs :: Streams -> StreamableMaps Spec getSpecs streams = - let (Both strms _) = execWriter streams+ let (LangElems strms _ _) = execWriter streams in strms getSends :: Streams -> StreamableMaps Send getSends streams = - let (Both _ snds) = execWriter streams+ let (LangElems _ snds _) = execWriter streams in snds +getTriggers :: Streams -> Triggers+getTriggers streams = + let (LangElems _ _ triggers) = execWriter streams+ in triggers+ -- | A named stream type Stream a = Streamable a => (Var, Spec a) @@ -141,16 +175,17 @@ -- | 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)+-- 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+ -- | 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@@ -161,8 +196,8 @@ -- | 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+ -- | 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@@ -175,25 +210,13 @@ -- 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.+ -- | 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 throw an error).- -- XXX make them throw errors!- makeTrigger :: [(Var, String)] -> StreamableMaps Spec - -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a - -> A.Atom () -> A.Atom ()---- class Streamable a => Sendable a where--- send :: A.E a -> Port -> A.Atom ()---- instance Sendable Word8 where--- send e port =--- A.action (\ [ueString] -> "sendW8_port" ++ show port --- ++ "(" ++ ueString ++ ")") [A.ue e]-+-- | If the 'Spec' isn't a 'Var', then throw an error; otherwise, apply the+-- function. notVarErr :: Streamable a => Spec a -> (Var -> b) -> b notVarErr s f = case s of@@ -201,16 +224,11 @@ _ -> error $ "You provided specification \n" ++ show s ++ "\n where you needed to give a variable." -sendKey :: Streamable a => Send a -> String-sendKey (Send s ph (Port port) portName) = - notVarErr - s- (\var -> (portName ++ "_port_" ++ show port ++ "_var_" ++ var ++ "_ph_" ++ show ph))- -- | Sending data over ports. mkSend :: (Streamable a) => A.E a -> Port -> String -> A.Atom () mkSend e (Port port) portName =- A.action (\[ueStr] -> portName ++ "(" ++ ueStr ++ "," ++ show port ++ ")") [A.ue e]+ A.action (\[ueStr] -> portName ++ "(" ++ ueStr ++ "," ++ show port ++ ")") + [A.ue e] instance Streamable Bool where getSubMap = bMap@@ -221,17 +239,6 @@ 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 - trig = case M.lookup v (M.fromList triggers) of- Nothing -> ""- Just fn -> fn- instance Streamable Int8 where getSubMap = i8Map updateSubMap f sm = sm {i8Map = f $ i8Map sm}@@ -241,7 +248,6 @@ typeId _ = "%d" atomType _ = A.Int8 showAsC x = printf "%d" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int16 where getSubMap = i16Map updateSubMap f sm = sm {i16Map = f $ i16Map sm}@@ -251,7 +257,6 @@ typeId _ = "%d" atomType _ = A.Int16 showAsC x = printf "%d" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int32 where getSubMap = i32Map updateSubMap f sm = sm {i32Map = f $ i32Map sm}@@ -261,7 +266,6 @@ typeId _ = "%d" atomType _ = A.Int32 showAsC x = printf "%d" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int64 where getSubMap = i64Map updateSubMap f sm = sm {i64Map = f $ i64Map sm}@@ -271,7 +275,6 @@ typeId _ = "%lld" atomType _ = A.Int64 showAsC x = printf "%d" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word8 where getSubMap = w8Map updateSubMap f sm = sm {w8Map = f $ w8Map sm}@@ -281,7 +284,6 @@ typeId _ = "%u" atomType _ = A.Word8 showAsC x = printf "%u" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word16 where getSubMap = w16Map updateSubMap f sm = sm {w16Map = f $ w16Map sm}@@ -291,7 +293,6 @@ typeId _ = "%u" atomType _ = A.Word16 showAsC x = printf "%u" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word32 where getSubMap = w32Map updateSubMap f sm = sm {w32Map = f $ w32Map sm}@@ -301,7 +302,6 @@ typeId _ = "%u" atomType _ = A.Word32 showAsC x = printf "%u" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word64 where getSubMap = w64Map updateSubMap f sm = sm {w64Map = f $ w64Map sm}@@ -311,7 +311,6 @@ typeId _ = "%llu" atomType _ = A.Word64 showAsC x = printf "%u" (toInteger x)- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Float where getSubMap = fMap updateSubMap f sm = sm {fMap = f $ fMap sm}@@ -322,7 +321,6 @@ typeIdPrec _ = "%.5f" atomType _ = A.Float showAsC x = printf "%.5f" x- makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Double where getSubMap = dMap updateSubMap f sm = sm {dMap = f $ dMap sm}@@ -333,7 +331,6 @@ typeIdPrec _ = "%.10lf" atomType _ = A.Double showAsC x = printf "%.10f" x- makeTrigger _ _ _ _ _ _ _ r = r >> return () -- | Lookup into the map of the right type in @'StreamableMaps'@ {-# INLINE getMaybeElem #-}@@ -374,26 +371,6 @@ acc10 = M.foldWithKey f acc9 dm in acc10 --- XXX only sends Word8s right now--- | This function is used to iterate on all the values in all the maps stored--- by a @'StreamableMaps'@, accumulating a value over time--- {-# INLINE foldSendableMaps #-}--- foldSendableMaps :: forall b c. --- (forall a. Sendable a => Var -> c a -> b -> b) -> --- StreamableMaps c -> b -> b--- --foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =--- foldSendableMaps f (SM _ _ _ _ _ w8m _ _ _ _ _) acc =--- let acc1 = M.foldWithKey f acc w8m--- in acc1--- foldSendableMaps :: forall b c. --- (forall a. Streamable a => Var -> c a -> b -> b) -> --- StreamableMaps c -> b -> b--- --foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =--- foldSendableMaps f (SM _ _ _ _ _ w8m _ _ _ _ _) 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) -> @@ -464,10 +441,14 @@ dMap :: M.Map Var (a Double) } -instance Monoid (Both (StreamableMaps Spec) (StreamableMaps Send)) where- mempty = Both emptySM emptySM- mappend (Both x y) (Both x' y') = Both (overlap x x') (overlap y y') +instance Monoid (StreamableMaps Spec) where+ mempty = emptySM+ mappend x y = overlap x y +instance Monoid LangElems where+ mempty = LangElems emptySM emptySM M.empty+ mappend (LangElems x y z) (LangElems x' y' z') = + LangElems (overlap x x') (overlap y y') (M.union z z') -- XXX should we test for the same key? overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s overlap x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) y@(SM bm' i8m' i16m' i32m' i64m' w8m' w16m' w32m' w64m' fm' dm') =@@ -574,8 +555,53 @@ +-- XXX -- Compiler: the code below really belongs in Compiler.hs, but its called by -- makeTrigger, which is a method of the class Streamable.++-- XXX+-- Check that a trigger references a Copilot variable of type 'Spec' 'Bool'.+-- checkTrigger :: forall a m. (Monad m, Streamable a) +-- => Trigger a -> StreamableMaps Spec -> m ()+-- checkTrigger (Trigger var _ args) streams =+-- if null badDefs+-- then if getAtomType var == A.Bool+-- then return ()+-- else error $ "Copilot error in defining triggers: the variable " +-- ++ show var ++ " are of a type other than Bool."+-- else error $ "Copilot error in defining triggers: the variables " ++ show badDefs +-- ++ "don't define streams in-scope."+-- where varChk v = case getMaybeElem v streams :: Maybe (Spec a) of+-- Nothing -> [v]+-- Just _ -> []+-- badDefs = notVarErr var varChk ++ concatMap varChk args+++-- | To make customer C triggers. Only for Spec Bool (others throw an+-- error). XXX make them throw errors!+makeTrigger :: StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes + -> Trigger -> A.Atom () -> A.Atom ()++makeTrigger streams prophArrs tmpSamples outputIndexes + trigger@(Trigger s fnName (vars,args)) r = + do r + A.liftIO $ putStrLn ("len" ++ (show $ length vars)) +-- checkTrigger trigger streams+ (A.exactPhase 0 $ A.atom (show trigger) $ + do A.cond (nextSt streams prophArrs tmpSamples outputIndexes s 0)+ A.action (\ues -> fnName ++ "(" ++ unwords (intersperse "," ues) ++ ")")+ (reorder vars []+ (foldStreamableMaps + (\v argSpec ls -> (v,next argSpec):ls) args [])))+ where next :: Streamable a => Spec a -> A.UE + next a = A.ue $ nextSt streams prophArrs + tmpSamples outputIndexes a 0+ reorder [] acc _ = reverse $ snd (unzip acc)+ reorder (v:vs) acc ls = + case lookup v ls of+ Nothing -> error "Error in makeTrigger in Core.hs."+ Just x -> let n = (v,x)+ in reorder vs (n:acc) ls -- For the prophecy arrays type ArrIndex = Word64
Language/Copilot/Dispatch.hs view
@@ -20,7 +20,6 @@ import qualified Language.Atom as A import qualified Data.Map as M-import Data.List ((\\)) import System.Directory import System.Process@@ -35,11 +34,11 @@ , outputDir :: String -- ^ Where to put the executable , compiler :: String -- ^ Which compiler to use , prePostCode :: Maybe (String, String) -- ^ Code to replace the default initialization and main- , triggers :: [(Var, String)] -- ^ A list of Copilot variable C function- -- name pairs. The C funciton is called if- -- the Copilot stream becomes True. The- -- Stream must be of Booleans and the C- -- function must be of type void @foo(void)@.+ -- , triggers :: [(Var, String)] -- ^ A list of Copilot variable C function+ -- -- name pairs. The C funciton is called if+ -- -- the Copilot stream becomes True. The+ -- -- Stream must be of Booleans and the C+ -- -- function must be of type void @foo(void)@. , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we -- don't know how large external arrays are, so -- we cannot declare them. Passing in pairs@@ -70,19 +69,18 @@ -- @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 -> StreamableMaps Send -> Vars - -> BackEnd -> Iterations -> Verbose -> IO ()-dispatch streams sends inputExts backEnd iterations verbose =+dispatch :: LangElems -> Vars -> BackEnd -> Iterations -> Verbose -> IO ()+dispatch elems inputExts backEnd iterations verbose = do hSetBuffering stdout LineBuffering mapM_ putStrLn preludeText isValid <-- case check streams of+ case check (strms elems) 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) + let interpretedLines = showVars (interpretStreams (strms elems) trueInputExts) iterations in case backEnd of Interpreter -> @@ -99,8 +97,7 @@ putStrLn $ "Trying to create the directory " ++ dirName ++ " (if missing) ..." createDirectoryIfMissing False dirName- checkTriggerVars streams (triggers opts) - copilotToC streams sends allExts trueInputExts opts isVerbose+ copilotToC elems allExts trueInputExts opts isVerbose let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext) let delete ext = do @@ -117,7 +114,7 @@ when (prePostCode opts == Nothing) $ gccCall (Opts opts) when ((isInterpreted || isExecuted) && not allInputsPresents) $ error errMsg- when isExecuted $ execute streams (dirName ++ cName opts) + when isExecuted $ execute (strms elems) (dirName ++ cName opts) trueInputExts isInterpreted interpretedLines iterations isSilent where@@ -125,37 +122,18 @@ isVerbose = verbose == Verbose isSilent = verbose == OnlyErrors isExecuted = iterations /= 0- allExts = getExternalVars streams+ allExts = getExternalVars (strms elems) (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts --- Check that each trigger references an actual Copilot variable of type Bool.-checkTriggerVars :: StreamableMaps Spec -> [(Var, String)] -> IO ()-checkTriggerVars streams trigs = - 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 trigs \\ getVars streams- listAtomTypes :: Streamable a => Var -> Spec a -> [(Var, A.Type)] -> [(Var, A.Type)]- listAtomTypes v s ls = - let t = getAtomType s - in if t /= A.Bool && v `elem` (map fst trigs) then (v, t):ls else ls- badTypes = foldStreamableMaps listAtomTypes streams []--copilotToC :: StreamableMaps Spec -> StreamableMaps Send - -> [(A.Type, Var, ExtVars)] -> Vars -> AtomToC -> Bool -> IO ()-copilotToC streams sends allExts trueInputExts opts isVerbose =- let (p', program) = copilotToAtom streams sends (getPeriod opts) (triggers opts)+copilotToC :: LangElems -> [(A.Type, Var, ExtVars)] -> Vars -> AtomToC -> Bool -> IO ()+copilotToC elems allExts trueInputExts opts isVerbose =+ let (p', program) = copilotToAtom elems (getPeriod opts) cFileName = cName opts (preCode, postCode) = case (prePostCode opts) of Nothing -> - getPrePostCode cFileName streams allExts (arrDecs opts) trueInputExts p'+ getPrePostCode cFileName (strms elems) allExts + (arrDecs opts) trueInputExts p' Just (pre, post) -> (pre, post) atomConfig = A.defaults { A.cCode = \_ _ _ -> (preCode, postCode)
Language/Copilot/Examples/Examples.hs view
@@ -25,14 +25,15 @@ even w' = w' `mod` 2 == 0 t1 :: Streams-t1 = +t1 = do let x = varI32 "x"- y = varB "y"- z = varB "z"- in do- x .= [0, 1, 2] ++ x - (drop 1 x)- y .= [True, False] ++ y ^ z- z .= x <= drop 1 x+ let y = varB "y"+ let z = varB "z"+ let w = varB "w"+ x .= [0, 1, 2] ++ x - (drop 1 x)+ y .= [True, False] ++ y ^ z+ z .= x <= drop 1 x+ w .= 3 == x -- t2 :: Streams -- t2 = do@@ -41,58 +42,60 @@ -- t3 :: use an external variable called ext, typed Word32 t3 :: Streams-t3 = +t3 = do let a = varW32 "a"- b = varB "b"- ext8 = extW32 "ext" 8- ext1 = extW32 "ext" 1- in do- a .= [0,1] ++ a + ext8 + ext8 + ext1- b .= [True, False] ++ 2 + a < 5 + ext1+ let b = varB "b"+ let ext8 = extW32 "ext" 8+ let ext1 = extW32 "ext" 1+ a .= [0,1] ++ a + ext8 + ext8 + ext1+ b .= [True, False] ++ 2 + a < 5 + ext1 t4 :: Streams-t4 = let- a = varB "a"- b = varB "b"- in do- a .= [True,False] ++ not a- b .= drop 1 a+t4 = do+ let a = varB "a"+ let b = varB "b"+ a .= [True,False] ++ not a+ b .= drop 1 a t5 :: Streams-t5 = - let x = varB "x"- y = varB "y"- w = varB "w"- z = varB "z"- in do- x .= drop 3 y- y .= [True, True] ++ not z- z .= [False, False] ++ not z- w .= x || y-+t5 = do+ let x = varW16 "x"+ let t = varF "t"+ let y = varB "y"+ let w = varB "w"+ let z = varB "z"+ x .= cast (drop 3 y)+ t .= [0] ++ t+ y .= [True, True] ++ not z+ z .= [False] ++ false+ w .= z || y+ -- triggers+ trigger y "w_trigger" (w <> x <> x <>> t) -- XXX wrong arg seem generated for x+ trigger z "y_trigger" void+ trigger w "z_trigger" (x <> y <> z <>> x)+ yy :: Streams yy = let a = varW64 "a" in do a .= 4 zz :: Streams-zz = +zz = do let a = varW32 "a"- b = varW32 "b"- in do --a .= [0..4] ++ drop 4 (varW32 a) + 1- a .= a + 1- b .= drop 3 a+ let b = varW32 "b"+ --a .= [0..4] ++ drop 4 (varW32 a) + 1+ a .= a + 1+ b .= drop 3 a xx :: Streams-xx = +xx = do let a = varW32 "a"- b = varW32 "b"- c = varW32 "c"- ext = extW32 "ext" 1- in do - a .= ext- b .= [3] ++ a- c .= [0, 1, 3, 4] ++ drop 1 b+ let b = varW32 "b"+ let c = varW32 "c"+ let ext = extW32 "ext" 1+ a .= ext+ b .= [3] ++ a+ c .= [0, 1, 3, 4] ++ drop 1 b -- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the -- engine is immediately shut off. From the paper.@@ -110,7 +113,7 @@ overTemp .= drop 2 temps > 2.3 + temps trigger .= overTemp ==> shutoff --- | distributed streams. +-- | Sending over ports. distrib :: Streams distrib = do -- vars
Language/Copilot/Help.hs view
@@ -123,17 +123,6 @@ , " 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."- , "" , " setArrs :: [(String,Int)] -> Options -> Options (c)" , " default: Nothing" , " When generating C programs to test, we don't know how large external"@@ -169,14 +158,6 @@ , " 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"
Language/Copilot/Interface.hs view
@@ -1,8 +1,8 @@ -- | 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, setArrs, setClock,+ , help , setE, setC, setO, setP, setI, setPP, setN, setV, setR+ , setDir, setGCC, setArrs, setClock, module Language.Copilot.Dispatch ) where @@ -13,12 +13,11 @@ import Language.Copilot.Help import qualified Language.Atom as A (Clock) -import Data.Set as Set (fromList, toList)-import Data.List ((\\)) import System.Random import System.Exit import System.Cmd import Data.Maybe+import qualified Data.Map as M (empty) import Control.Monad (when) data Options = Options {@@ -38,16 +37,14 @@ 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 :: [(Var, String)], -- ^ A list of Copilot variable C- -- function name pairs. The C funciton- -- is called if the Copilot stream- -- becomes True. The Stream must be of- -- Booleans and the C function must be- -- of type void @foo(void)@. There- -- should be no more than one function- -- per trigger variable. Triggers fire- -- in the same phase (1) that output- -- vars are assigned.+ optTriggers :: Triggers, -- ^ A list of Copilot variable C function name+ -- pairs. The C funciton is called if the+ -- Copilot stream becomes True. The Stream+ -- must be of Booleans and the C function must+ -- be of type void @foo(void)@. There should+ -- be no more than one function per trigger+ -- variable. Triggers fire in the same phase+ -- (1) that output vars are assigned. optArrs :: [(String, Int)], -- ^ When generating C programs to test, we -- don't know how large external arrays are, -- so we cannot declare them. Passing in@@ -72,7 +69,7 @@ optCompiler = "gcc", optOutputDir = "./", optPrePostCode = Nothing,- optTriggers = [],+ optTriggers = M.empty, optArrs = [], optClock = Nothing }@@ -89,8 +86,9 @@ compile :: Streams -> Name -> Options -> IO () compile streams fileName opts = - interface $ setC "-Wall" $ setO fileName $ setS (getSends streams) $- opts {optStreams = Just (getSpecs streams)}+ interface $ setC "-Wall" $ setO fileName $ setS (getSends streams)+ $ setTriggers (getTriggers streams) + $ opts {optStreams = Just (getSpecs streams)} verify :: FilePath -> Int -> IO () verify file n = do@@ -125,6 +123,10 @@ setS :: StreamableMaps Send -> Options -> Options setS sends opts = opts {optSends = sends} +-- | Set the directives for sending stream values on ports.+setTriggers :: Triggers -> Options -> Options+setTriggers triggers opts = opts {optTriggers = triggers}+ -- | Sets the environment for simulation by giving a mapping of external -- variables to lists of values. E.g., -- @@ -193,16 +195,16 @@ setPP :: (String, String) -> Options -> Options setPP pp opts = opts {optPrePostCode = Just pp} --- | Give C function triggers for Copilot Boolean streams. The tiggers fire if--- the stream becoms true.-setTriggers :: [(Var, String)] -> Options -> Options-setTriggers trigs opts = - if null repeats - then opts {optTriggers = trigs}- else error $ "Error: only one trigger per Copilot variable. Variables "- ++ show (Set.fromList repeats) ++ " are given multiple triggers."- where vars = map fst trigs- repeats = vars \\ Set.toList (Set.fromList vars)+-- -- | Give C function triggers for Copilot Boolean streams. The tiggers fire if+-- -- the stream becoms true.+-- setTriggers :: [(Var, String)] -> Options -> Options+-- setTriggers trigs opts = opts {optTriggers = trigs}+-- -- if null repeats +-- -- then +-- -- else error $ "Error: only one trigger per Copilot variable. Variables "+-- -- ++ show (Set.fromList repeats) ++ " are given multiple triggers."+-- -- where vars = map fst trigs+-- -- repeats = vars \\ Set.toList (Set.fromList vars) -- | The "main" function that dispatches. interface :: Options -> IO ()@@ -211,6 +213,7 @@ seed <- createSeed opts let (streams, vars) = getStreamsVars opts seed sends = optSends opts+ triggers = optTriggers opts backEnd = getBackend opts seed iterations = optIterations opts verbose = optVerbose opts@@ -218,7 +221,7 @@ 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 + dispatch (LangElems streams sends triggers) vars backEnd iterations verbose createSeed :: Options -> IO Int createSeed opts =@@ -255,7 +258,7 @@ outputDir = optOutputDir opts, compiler = optCompiler opts, prePostCode = optPrePostCode opts,- triggers = optTriggers opts,+-- triggers = optTriggers opts, arrDecs = optArrs opts, clock = optClock opts }
Language/Copilot/Language.hs view
@@ -33,10 +33,12 @@ -- Warning: there is no typechecking of that yet -- sendB, sendI8, sendI16, sendI32, sendI64, send, port, -- , sendW16, sendW32, sendW64, sendF, sendD+ -- * Triggers+ trigger, void, (<>), (<>>), -- * Safe casting cast, -- * Boolean stream constants- true, false+ const, true, false ) where import qualified Language.Atom as A@@ -47,7 +49,7 @@ import Prelude ( Bool(..), Num(..), Float, Double, (.), String, error, ($) , Fractional(..), fromInteger, zip, Show(..)) import qualified Prelude as P-import Control.Monad.Writer+import Control.Monad.Writer (tell) import Language.Copilot.Core import Language.Copilot.Analyser@@ -75,6 +77,10 @@ else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d) + +-- class (Streamable a, A.OrdE a) => SpecOrd a where+-- (<)+ (<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool (<) = F2 (P.<) (A.<.) (<=) = F2 (P.<=) (A.<=.)@@ -105,19 +111,19 @@ instance Castable Bool where castFrom = F (\b -> if b then 1 else 0)- (\b -> A.mux b 1 0)+ (\b -> A.mux b 1 0) cast x = error $ castErr "Bool" (getAtomType x) instance Castable Word8 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x t -> error $ castErr "Word8" t instance Castable Word16 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Word8 -> castFrom x@@ -125,7 +131,7 @@ instance Castable Word32 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Word8 -> castFrom x@@ -134,7 +140,7 @@ instance Castable Word64 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Word8 -> castFrom x@@ -144,14 +150,14 @@ instance Castable Int8 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x t -> error $ castErr "Int8" t instance Castable Int16 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Int8 -> castFrom x@@ -160,7 +166,7 @@ instance Castable Int32 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Int8 -> castFrom x@@ -171,7 +177,7 @@ instance Castable Int64 where castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue)+ (A.Retype . A.ue) cast x = case getAtomType x of A.Bool -> castFrom x A.Int8 -> castFrom x@@ -461,6 +467,14 @@ varD :: Var -> Spec Double varD = Var +-- | Define a stream variable.+(.=) :: Streamable a => Spec a -> Spec a -> Streams+v .= s = + notVarErr v (\var -> tell $ LangElems + (updateSubMap (M.insert var s) emptySM) + emptySM + M.empty)+ port :: Int -> Port port = Port @@ -470,9 +484,43 @@ -- of the value on the port occurs at phase @ph@. send :: Streamable a => String -> Port -> Spec a -> Phase -> Streams send portName port s ph = - tell $ Both emptySM (updateSubMap (M.insert (sendKey sending) sending) emptySM)+ tell $ LangElems + emptySM + (updateSubMap (M.insert (show sending) sending) emptySM) + M.empty where sending = Send s ph port portName +type TriggerLst = ([Var], StreamableMaps Spec)++-- | No C arguments +void :: TriggerLst+void = ([],emptySM)++-- | Turn a @Spec Var@ into an arguement for a C function.+(<>) :: Streamable a => Spec a -> TriggerLst -> TriggerLst+s <> (vars,sm) = notVarErr s (\v -> (v:vars, updateSubMap (\m -> M.insert v s m) sm))++-- | Turn a @Spec Var@ into an arguement for a C function.+(<>>) :: (Streamable a, Streamable b) => Spec a -> Spec b + -> TriggerLst+s <>> s' = (update s (update s' void))+ where update x (vars,sm) = + notVarErr x (\v -> (v:vars,updateSubMap (\m -> M.insert v x m) sm))++-- | Takes a Boolean stream, +trigger :: Spec Bool -> String -> TriggerLst -> Streams+trigger var fnName args =+ tell $ LangElems + emptySM + emptySM +-- (updateSubMap (M.insert (show trigger) trigger) emptySM) + (M.insert (show trigger) trigger M.empty)+ where trigger = Trigger var fnName args++-- | Coerces a type that is 'Streamable' into a Copilot constant.+const :: Streamable a => a -> Spec a+const = Const+ true, false :: Spec Bool true = Const True false = Const False@@ -485,14 +533,10 @@ (++) :: Streamable a => [a] -> Spec a -> Spec a ls ++ s = Append ls s --- | Define a stream variable.-(.=) :: Streamable a => Spec a -> Spec a -> Streams-v .= s = - notVarErr v (\var -> tell $ Both (updateSubMap (M.insert var s) emptySM) emptySM) - infixr 3 ++ infixr 2 .=+infixr 1 <> ---- Optimisation rules -------------------------------------------------------- @@ -522,4 +566,7 @@ "Copilot.Language MuxF" forall s0 s1. mux (Const False) s0 s1 = s1 "Copilot.Language MuxT" forall s0 s1. mux (Const True) s0 s1 = s0 "Copilot.Language ImpliesDef" forall s0 s1. (||) s1 (not s0) = s0 ==> s1- #-}+ #-}++-- "Copilot.Language CastLift" forall s i. drop i (cast s) = cast (drop i s)+
README view
@@ -43,6 +43,10 @@ ******************************************************************************* Release notes *******************************************************************************+* Copilot-0.28+ + * Make triggers part of the Copilot language (see example t5 in Examples.hs).+ * Copilot-0.27 * Changed syntax and semantics of the 'send' function (Language.hs) for
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 0.27+version: 0.28 cabal-version: >= 1.2 license: BSD3 license-file: LICENSE@@ -7,7 +7,7 @@ synopsis: A stream DSL for writing embedded C monitors. build-type: Simple maintainer: Lee Pike <leepike@galois.com>-category: Language+category: Language, Embedded homepage: http://leepike.github.com/Copilot/ description: Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here's a Copilot program that computes the Fibonacci sequence (over@@ -19,7 +19,7 @@ > let t = varB "t" > f .= [0,1] ++ f + (drop 1 f) > t .= even f- > where even :: Spaec Word64 -> Spec Bool+ > where even :: Spec Word64 -> Spec Bool > even w' = w' `mod` 2 == 0 . Copilot contains an interpreter, a compiler, and uses a model-checker to check@@ -35,8 +35,9 @@ ghc-options: -Wall -- These build depends represent my current system. This will probably -- build on packages outside these constaints.- build-depends: base > 4 && < 6- , atom >= 1.0.7+ build-depends: + base >= 4.2 && < 6+ , atom >= 1.0.8 , containers >= 0.2.0.1 , process >= 1.0.0.0 , random >= 1.0.0.0