copilot 0.26 → 0.27
raw patch · 11 files changed
+309/−124 lines, 11 files
Files
- Language/Copilot/Compiler.hs +22/−9
- Language/Copilot/Core.hs +88/−36
- Language/Copilot/Dispatch.hs +4/−3
- Language/Copilot/Examples/Examples.hs +11/−10
- Language/Copilot/Interface.hs +17/−13
- Language/Copilot/Language.hs +21/−41
- Language/Copilot/Libs/LTL.hs +2/−2
- Language/Copilot/Libs/PTLTL.hs +2/−2
- Language/Copilot/PrettyPrinter.hs +3/−5
- README +138/−2
- copilot.cabal +1/−1
Language/Copilot/Compiler.hs view
@@ -15,7 +15,7 @@ -- | 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 +copilotToAtom :: StreamableMaps Spec -> StreamableMaps Send -> Maybe Period -> [(Var, String)] -> (Period, A.Atom ()) copilotToAtom streams sends p triggers = (p', A.period p' $ do@@ -39,14 +39,14 @@ outputIndexes) streams (return ()) - foldSendableMaps (makeSend outputs) sends (return ())+ foldStreamableMaps (makeSend outputs) sends (return ()) -- Sampling of the external variables. Remove redundancies. sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ foldStreamableMaps (\_ -> sampleExts tmpSamples) streams [] ) where- optP = getOptimalPeriod streams+ optP = getOptimalPeriod streams sends p' = case p of Nothing -> optP@@ -217,11 +217,19 @@ Append _ s0 -> streamDep s0 i Drop _ s0 -> streamDep s0 i -makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom ()-makeSend outputs name (Send (v, ph, port)) r = do+-- makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom ()+-- makeSend outputs name (Send (v, ph, port)) r = do+-- r +-- A.exactPhase ph $ A.atom ("__send_" ++ name) $+-- send ((A.value (getElem v outputs))::(A.E a)) port+makeSend :: forall a. Streamable a + => Outputs -> String -> Send a -> A.Atom () -> A.Atom ()+makeSend outputs name (Send v ph port portName) r = do r A.exactPhase ph $ A.atom ("__send_" ++ name) $- send ((A.value (getElem v outputs))::(A.E a)) port+ mkSend (A.value (notVarErr v (\var -> getElem var outputs)) :: A.E a) + port + portName -- What we really should be doing is just folding over the TmpSamples, since -- that data should contain all the info we need to construct external variable@@ -274,9 +282,11 @@ _ -> error $ "Expecing either a variable or constant for the index " ++ "in the external array access for array " ++ arr ++ "." -getOptimalPeriod :: StreamableMaps Spec -> Period-getOptimalPeriod streams =- foldStreamableMaps getMaximumSamplingPhase streams 2+-- XXX bound min, max send phases+getOptimalPeriod :: StreamableMaps Spec -> StreamableMaps Send -> Period+getOptimalPeriod streams sends =+ max (foldStreamableMaps getMaximumSamplingPhase streams 2)+ (foldStreamableMaps getMaxSendPhase sends 0) where getMaximumSamplingPhase :: Var -> Spec a -> Period -> Period getMaximumSamplingPhase _ spec n =@@ -299,3 +309,6 @@ Drop _ s -> getMaximumSamplingPhase "" s n Append _ s -> getMaximumSamplingPhase "" s n _ -> n++ getMaxSendPhase :: Var -> Send a -> Period -> Period+ getMaxSendPhase _ (Send _ ph _ _) n = max (ph+1) n
Language/Copilot/Core.hs view
@@ -9,17 +9,21 @@ -- 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,+ Var, Name, Period, Phase, Port(..),+ Spec(..), Streams, Stream, Send(..), --DistributedStreams,+ notVarErr, Both(..), -- * General functions on 'Streams' and 'StreamableMaps'- Streamable(..), Sendable(..), StreamableMaps(..), emptySM,+ Streamable(..), sendKey, mkSend, -- Sendable(..)+ StreamableMaps(..), emptySM, isEmptySM, getMaybeElem, getElem, - foldStreamableMaps, foldSendableMaps, mapStreamableMaps, mapStreamableMapsM,+ foldStreamableMaps, --foldSendableMaps, + mapStreamableMaps, mapStreamableMapsM, filterStreamableMaps, normalizeVar, getVars, Vars, -- compiler BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..),- tmpVarName, tmpArrName, getAtomType+ tmpVarName, tmpArrName, getAtomType,+ getSpecs, getSends ) where import qualified Language.Atom as A@@ -41,7 +45,7 @@ -- | Phase of an Atom phase type Phase = Int -- | Port over which to broadcast information-type Port = Int+data Port = Port Int -- | Specification of a stream, parameterized by the type of the values of the stream. -- The only requirement on @a@ is that it should be 'Streamable'.@@ -101,17 +105,36 @@ (==) (Drop i s) (Drop i' s') = i == i' && s == s' (==) _ _ = False +-- | An instruction to send data on a port at a given phase. Uses a phantom type.+-- data Send a = Sendable a => Send (Var, Phase, Port)+data Send a = + Send { sendVar :: Spec a + , sendPh :: Phase+ , sendPort :: Port+ , sendName :: String}++data Both a b = Both a b+ -- | Container for mutually recursive streams, whose specifications may be -- parameterized by different types-type Streams = Writer (StreamableMaps Spec) ()+type Streams = Writer (Both (StreamableMaps Spec) (StreamableMaps Send)) ()++getSpecs :: Streams -> StreamableMaps Spec+getSpecs streams = + let (Both strms _) = execWriter streams+ in strms++getSends :: Streams -> StreamableMaps Send+getSends streams = + let (Both _ snds) = execWriter streams+ in snds+ -- | 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)+-- type DistributedStreams = (Streams, Sends) ---- General functions on streams ---------------------------------------------- @@ -163,9 +186,32 @@ -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom () -class Streamable a => Sendable a where- send :: A.E a -> Port -> 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]++notVarErr :: Streamable a => Spec a -> (Var -> b) -> b+notVarErr s f =+ case s of+ Var v -> f v+ _ -> error $ "You provided specification \n" ++ show s + ++ "\n where you needed to give a variable."++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]+ instance Streamable Bool where getSubMap = bMap updateSubMap f sm = sm {bMap = f $ bMap sm}@@ -289,11 +335,6 @@ showAsC x = printf "%.10f" x makeTrigger _ _ _ _ _ _ _ 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)@@ -336,15 +377,23 @@ -- 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+-- {-# 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) -> @@ -415,21 +464,24 @@ 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 " +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') ++overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s +overlap x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) + y@(SM bm' i8m' i16m' i32m' i64m' w8m' w16m' w32m' w64m' fm' dm') =+ let multDefs = (getVars x `intersect` getVars y)+ in if null multDefs then union+ else error $ "Copilot error: The variables " ++ show multDefs ++ " have multiple definitions."- union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m') + where union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m') (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m') (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m') (M.union fm fm') (M.union dm dm') -- | Get the Copilot variables.-getVars :: StreamableMaps Spec -> [Var]+getVars :: StreamableMaps s -> [Var] getVars streams = foldStreamableMaps (\k _ ks -> k:ks) streams [] -- | An empty streamableMaps.
Language/Copilot/Dispatch.hs view
@@ -70,7 +70,8 @@ -- @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 :: StreamableMaps Spec -> StreamableMaps Send -> Vars + -> BackEnd -> Iterations -> Verbose -> IO () dispatch streams sends inputExts backEnd iterations verbose = do hSetBuffering stdout LineBuffering@@ -146,8 +147,8 @@ in if t /= A.Bool && v `elem` (map fst trigs) then (v, t):ls else ls badTypes = foldStreamableMaps listAtomTypes streams [] -copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, ExtVars)] -> Vars - -> AtomToC -> Bool -> IO ()+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) cFileName = cName opts
Language/Copilot/Examples/Examples.hs view
@@ -11,7 +11,6 @@ import Data.Map (fromList) import Data.Maybe (Maybe (..)) import System.Random-import Data.Int import Language.Copilot -- import Language.Copilot.Variables@@ -111,16 +110,18 @@ overTemp .= drop 2 temps > 2.3 + temps trigger .= overTemp ==> shutoff --- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist"--- s at phase 2 on port 1. Not stable.-dist :: DistributedStreams-dist = +-- | distributed streams. +distrib :: Streams+distrib = do+ -- vars let a = varW8 "a"- in - ( a .= [0,1] ++ a + 1- , sendW8 a (2, 1)- ..| emptySM- )+ let b = varB "b"+ -- spec+ a .= [0,1] ++ a + 1+ b .= mod a 2 == 0 + -- sends+ send "portA" (port 2) a 1+ send "portB" (port 1) b 2 -- greatest common divisor. gcd :: Word16 -> Word16 -> Streams
Language/Copilot/Interface.hs view
@@ -19,12 +19,13 @@ import System.Exit import System.Cmd import Data.Maybe-import Control.Monad-import Control.Monad.Writer (execWriter)+import Control.Monad (when) data Options = Options {- optStreams :: Maybe Streams, -- ^ If there's no Streams, then generate random streams.- optSends :: Sends, -- ^ For distributed monitors.+ optStreams :: Maybe (StreamableMaps Spec), -- ^ If there's no Streams,+ -- then generate random+ -- streams.+ optSends :: StreamableMaps Send, -- ^ For distributed monitors. optExts :: Maybe Vars, -- ^ Assign values to external variables. optCompile :: Maybe String, -- ^ Set gcc options. optPeriod :: Maybe Period, -- ^ Set the period. If none is given, then@@ -83,15 +84,17 @@ 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}+interpret streams n opts = + interface $ setI $ setN n $ opts {optStreams = Just (getSpecs streams)} compile :: Streams -> Name -> Options -> IO () compile streams fileName opts = - interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams}+ interface $ setC "-Wall" $ setO fileName $ setS (getSends streams) $+ opts {optStreams = Just (getSpecs streams)} verify :: FilePath -> Int -> IO () verify file n = do- putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke "+ 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"@@ -118,8 +121,9 @@ -- Small functions for easy modification of the Options record -setS :: DistributedStreams -> Options -> Options-setS (streams, sends) opts = opts {optStreams = Just streams, optSends = sends}+-- | Set the directives for sending stream values on ports.+setS :: StreamableMaps Send -> Options -> Options+setS sends opts = opts {optSends = sends} -- | Sets the environment for simulation by giving a mapping of external -- variables to lists of values. E.g.,@@ -200,7 +204,7 @@ where vars = map fst trigs repeats = vars \\ Set.toList (Set.fromList vars) --- | The "main" function+-- | The "main" function that dispatches. interface :: Options -> IO () interface opts = do@@ -225,15 +229,15 @@ return . fst . random $ g Just i -> return i +-- | Were streams given? If not, just make random streams. getStreamsVars :: Options -> Int -> (StreamableMaps Spec, Vars) getStreamsVars opts seed = case optStreams opts of Nothing -> randomStreams opsF opsF2 opsF3 (mkStdGen seed) Just s -> case optExts opts of- Nothing -> (s', emptySM)- Just vs -> (s', vs)- where s' = execWriter s+ Nothing -> (s, emptySM)+ Just vs -> (s, vs) getBackend :: Options -> Int -> BackEnd getBackend opts seed =
Language/Copilot/Language.hs view
@@ -15,8 +15,9 @@ Num(..), -- * Division Fractional((/)),- mux,- varB, varI8, varI16, varI32, varI64,+ mux, + -- * Copilot variable declarations.+ var, varB, varI8, varI16, varI32, varI64, varW8, varW16, varW32, varW64, varF, varD, -- * The next functions provide easier access to typed external variables. extB, extI8, extI16, extI32, extI64,@@ -27,11 +28,11 @@ -- * Set of operators from which to choose during the generation of random streams opsF, opsF2, opsF3, -- * Constructs of the copilot language- drop, (++), (.=), (..|), + drop, (++), (.=), -- (..|), -- * 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+ send, port, -- , sendW16, sendW32, sendW64, sendF, sendD -- * Safe casting cast, -- * Boolean stream constants@@ -432,6 +433,11 @@ -- If a generic 'var' declaration is insufficient for the type-checker to -- determine the type, a monomorphic var operator can be used.++-- | Useful for writing libraries.+var :: Streamable a => Var -> Spec a+var = Var+ varB :: Var -> Spec Bool varB = Var varI8 :: Var -> Spec Int8@@ -455,34 +461,17 @@ 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 :: Spec Word8 -> (Phase, Port) -> Send Word8-sendW8 s (ph, port) = - case s of- Var v -> Send (v, ph, port)- _ -> error $ "You provided spec " P.++ show s - P.++ " where you needed to give a variable."-{- 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) -}+port :: Int -> Port+port = Port +-- | Takes a function @name@, a port @number@, a Copilot variable @v@, and a+-- phase @ph@, and constructs a call to the C function @name(x,y)@ where @x@ is+-- the value of the Copilot stream @v@ and @y@ is the port number. The sending+-- of the value on the port occurs at phase @ph@.+send :: Streamable a => String -> Port -> Spec a -> Phase -> Streams+send portName port s ph = + tell $ Both emptySM (updateSubMap (M.insert (sendKey sending) sending) emptySM)+ where sending = Send s ph port portName true, false :: Spec Bool true = Const True@@ -499,20 +488,11 @@ -- | Define a stream variable. (.=) :: Streamable a => Spec a -> Spec a -> Streams v .= s = - case v of- Var var -> tell (updateSubMap (M.insert var s) emptySM) - _ -> error $ "Copilot error: you tried to use specification " P.++ show v - P.++ " where you need to use a variable."+ notVarErr v (\var -> tell $ Both (updateSubMap (M.insert var s) emptySM) 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 --------------------------------------------------------
Language/Copilot/Libs/LTL.hs view
@@ -42,8 +42,8 @@ tmpName :: Spec Bool -> String -> Spec Bool tmpName v name = case v of - Var var -> varB (var P.++ "_" P.++ name)- _ -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs."+ Var v' -> varB (v' P.++ "_" P.++ name)+ _ -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs." -- | Property @s@ holds for the next @n@ periods. We require @n >= 0@. If @n == -- 0@, then @s@ holds in the current period. E.g., if @p = always 2 s@, then we
Language/Copilot/Libs/PTLTL.hs view
@@ -22,8 +22,8 @@ tmpName :: Spec Bool -> String -> Spec Bool tmpName v name = case v of- Var var -> varB (var P.++ "_" P.++ name)- _ -> error "Copilot error in tmpName in PTLTL.hs."+ Var v' -> varB (v' P.++ "_" P.++ name)+ _ -> error "Copilot error in tmpName in PTLTL.hs." ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams ptltl v f = f v
Language/Copilot/PrettyPrinter.hs view
@@ -7,7 +7,6 @@ import Data.Int import Data.Word import Data.Map as M-import Control.Monad.Writer (execWriter) import Language.Copilot.Core @@ -32,8 +31,7 @@ showVal v val string = v ++ " .= " ++ show val ++ "\n" ++ string instance Show Streams where- show s = show (execWriter s) + show s = show (getSpecs s) --- instance Show (StreamableMaps Spec) where--- show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =--- show bm++
README view
@@ -1,3 +1,7 @@+*******************************************************************************+Overview+*******************************************************************************+ Copilot: A (Haskell DSL) stream language for generating hard real-time C code. Can you write a list in Haskell? Then you can write embedded C code using@@ -22,11 +26,14 @@ *******************************************************************************+Download+*******************************************************************************+ 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,+The page is also available as index.html in the gh-pages branch of the Copilot+repo. In your local repo, > git checkout gh-pages @@ -35,8 +42,15 @@ ******************************************************************************* Release notes+*******************************************************************************+* Copilot-0.27 + * Changed syntax and semantics of the 'send' function (Language.hs) for+ sending Copilot values on ports. An example is in Example.hs (grep for+ 'send').+ * Copilot-0.26+ * Variables are now specs, not strings. This gives stream expressions a type, so no need for constant functions, monomorphic cast functions, or var annotations in expressions. Examples updated to reflect the change.@@ -66,4 +80,126 @@ * Copilot-0.22: initial release ++*******************************************************************************+Modifying the Compiler+*******************************************************************************++This document is intended as a help for whoever wants to hack the internals of+Copilot. It is up-to-date on August 2010, the 17th.++I will first explain what each module does, then where to look to do some simple+modifications.++*** Modules ***++Core :+Defines all the important data-structures.+Especially interestings are :+- Spec, the AST of the streams specifications.+ Notice that the operators on streams (F, F2, F3) actually holds functions+ that helps interpreting/compiling them+- Streamable, a type class whose instances are all the possible types of output + for a stream+- StreamableMaps, a generic container for holding pairs of key/values, with + values of different types++Compiler :+Does all the scheduling, and translates a Copilot specification, to an Atom+program. More information on its algorithm can be found in the paper "Copilot: A+Hard Real-Time Runtime Monitor".++Interpreter :+Provides a small interpreter, mostly for checking the compiler against it. Its+design is very concise, because all the hard scheduling work is done by the+Haskell runtime. The streams are indeed translated to mutually recursives+infinite lists, and the lazyness of Haskell spare us from having to schedule+their computation. There is no specific code for each operator either, as+operators hold the function to be applied to their argument.++Analyser :+There are several kinds of restrictions on the inputs accepted by Copilot.+Some of them are catched by the Haskell compiler (for example bad typing into+a stream specification), but others aren't :+- Bad typing across stream boundaries+- Specifications which doesn't obey the syntax of Copilot (it could have been+ checked by Haskell too, but would have greatly complicated the Spec type)+- All kinds of properties on the dependency graph of the specification.+All these additional restrictions are checked by the Analyser.++PrettyPrinter :+Just allows to print the structure of a specification++Tests.Random :+Generates random streams and random input values, for easily checking the+compiler against the interpreter in an automated way. Currently a bit ugly,+would probably have benefited from using the QuickCheck library, rather than the+lower-level Random library. All the parameters of the random generation are near+the top of the file.++Language :+Defines all the different operators of the language. These are defined through a+F, F2 or F3 constructor, a function on how to compile them, and a function on+how to interpret them. These are also packed in a Operators data structure for+use in the random streams generator. Also contains some monomorphic versions of+the polymorphic language constructs, to help the type inferer.++AdHocC :+A small number of uninteresting functions to output C code. Used by AtomToC.++AtomToC :+Adds to the atom-generated code a main function and some initialisation stuff.++Main :+"Plumbing" module. Makes the analyser/interpreter/compiler, atom, gcc, and the+generated C program interact. Takes its arguments in a very heavy format (not+very convenient for fast testing). Warning : it is rather easy to desynchronyze+the generated C program and the interpreter with very small modifications+(leading to strange bugs).++Interface :+Is a wrapper around Main. Writing its argument is usually much easier, thanks+to the provided combinators and the reasonable defaults. All it does is +translating those into the numerous and verbose arguments Main expects.++Libs.* :+As Copilot is embedded in Haskell, it is very easy to write libraries of "macros"+that simplify the writing of some specifications. Thus these files, that holds +for example functions for easily writing LTL and PTLTL formulas.++Examples.* :+Self-explanatory.++*** Simple modifications ***++Add an example :+In Examples.Examples, or if related to a library, in Examples.LibraryName++Add some high-level combinator on streams :+In a library, in Lib.*+Should not call Atom, should only use other combinators and base operators.++Add some operator in the base language :+Write in Language.hs, from F, F2 or F3 (see examples) Would be nice to also add+to the corresponding Operators set (opsF, opsF2 or opsF3), so that it could be+automatically checked. This last point obviously require that the interpreted+and compiled semantics are equivalents.++Add some possible types for the streams :+Add a new instance of Stremable in Core.hs+Add a new record to StreamableMaps in Core.hs+Update foldStreamableMaps, mapStreamableMaps, mapStreamableMapsM, +and filterStreamableMaps in Core.hs+Update foldRandomableMaps in Tests/Random.hs++Authorise a new type to be exchanged by monitors :+Add a new instance of Sendable in Core.hs+Update foldSendableMaps in Core.hs++Add a new option to Copilot :+Add a new field to the Options record in Interface.hs+Add a new combinator for that field in Interface.hs+Update the baseOptions in Interface.hs+Implement it (probably in Main.hs).+Update interface in Interface.hs to convey it to the Main.
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 0.26+version: 0.27 cabal-version: >= 1.2 license: BSD3 license-file: LICENSE