diff --git a/Language/Copilot.hs b/Language/Copilot.hs --- a/Language/Copilot.hs +++ b/Language/Copilot.hs @@ -1,37 +1,43 @@ module Language.Copilot - ( module Language.Copilot.Core + ( module Language.Copilot.Core , module Language.Copilot.Analyser , module Language.Copilot.Interpreter , module Language.Copilot.Help , module Language.Copilot.AtomToC , module Language.Copilot.Compiler , module Language.Copilot.Language + -- , module Language.Copilot.Sampling + -- , module Language.Copilot.Casting -- , module Language.Copilot.Dispatch , module Language.Copilot.Interface , module Language.Copilot.Tests.Random -- , module Language.Copilot.Libs.Indexes -- , module Language.Copilot.Libs.LTL -- , module Language.Copilot.Libs.PTLTL + -- , module Language.Copilot.Libs.Clocks -- , module Language.Copilot.AdHocC -- , module Language.Copilot.Examples.Examples -- , module Language.Copilot.Examples.LTLExamples -- , module Language.Copilot.Examples.PTLTLExamples ) where -import Language.Copilot.Core +import Language.Copilot.Core (Streams, Spec, emptySM, StreamableMaps(..)) -- XXX for libs, probably need to export all the maps. Maybe put in a different file? import Language.Copilot.Analyser import Language.Copilot.Interpreter import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler -import Language.Copilot.Language -- (opsF, opsF2, opsF3) -import Language.Copilot.PrettyPrinter() import Language.Copilot.Tests.Random +import Language.Copilot.Language +-- import Language.Copilot.Language.Sampling +-- import Language.Copilot.Language.Casting +-- import Language.Copilot.PrettyPrinter() -- import Language.Copilot.Dispatch import Language.Copilot.Interface -- import Language.Copilot.Libs.Indexes -- import Language.Copilot.Libs.LTL -- import Language.Copilot.Libs.PTLTL +-- import Language.Copilot.Libs.Clocks -- import Language.Copilot.AdHocC -- import Language.Copilot.Examples.Examples -- import Language.Copilot.Examples.LTLExamples diff --git a/Language/Copilot/Analyser.hs b/Language/Copilot/Analyser.hs --- a/Language/Copilot/Analyser.hs +++ b/Language/Copilot/Analyser.hs @@ -6,7 +6,7 @@ -- * Main error checking functions check, Error(..), SpecSet(..), -- * Varied other things - getExternalVars, ExtVars(..) + getExternalVars {- -- * Dependency Graphs (experimental) Weight, Node(..), DependencyGraph, @@ -15,8 +15,6 @@ import Language.Copilot.Core -import qualified Language.Atom as A - import Data.List type Weight = Int @@ -25,17 +23,20 @@ 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 - | BadSamplingArrPhase Var Var Phase -- ^ if an external variable is sampled at - -- phase 0 then there is no time for the - -- stream to be updated - | BadPArrSpec Var Var String -- ^ External array indexes can only take + -- | BadSamplingPhase Var Ext -- ^ if an external variable is sampled at phase + -- -- 0 then there is no time for the stream to be + -- -- updated + -- | BadSamplingArrPhase Var Ext -- ^ if an external variable is sampled at + -- -- phase 0 then there is no time for the + -- -- stream to be updated + | BadPArrSpec Var Ext String -- ^ External array indexes can only take -- variables or constants as indexes. | BadType Var Var -- ^ either a variable is not defined, or not with the -- good type ; there is no implicit conversion of types in -- /Copilot/ + | BadTypeExt Ext Var -- ^ either an external variable is not defined, or not + -- with the good type; there is no implicit conversion + -- of types in /Copilot/ | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile -- /Copilot/ specification can -- only work if there is no @@ -43,10 +44,10 @@ -- path in the specification, -- as described in the original -- research paper - | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but + | DependsOnClosePast [Var] Ext Weight Weight -- ^ Could be compiled, but -- would need bigger -- prophecyArrays - | DependsOnFuture [Var] Var Weight -- ^ If an output depends of a future of + | DependsOnFuture [Var] Ext Weight -- ^ If an output depends of a future of -- an input it will be hard to compile to -- say the least @@ -61,24 +62,24 @@ "of elements.\n" , show i ++ " is negative, and Drop only accepts positive arguments.\n" ] - show (BadSamplingPhase v v' ph) = - unlines - [ "Error : the external variable " ++ v' ++ " is sampled at phase " ++ - show ph ++ " in the stream " ++ v ++ "." - , "Sampling can only occur from phase 1 onwards.\n" - ] - show (BadSamplingArrPhase v arr ph) = - unlines - [ "Error : the external array " ++ arr ++ " is sampled at phase " ++ - show ph ++ " in the stream " ++ v ++ "." - , " Sampling can only occur from phase 1 onwards.\n" - ] + -- show (BadSamplingPhase v v' ph) = + -- unlines + -- [ "Error : the external variable " ++ show v' ++ " is sampled at phase " ++ + -- show ph ++ " in the stream " ++ v ++ "." + -- , "Sampling can only occur from phase 1 onwards.\n" + -- ] + -- show (BadSamplingArrPhase v arr ph) = + -- unlines + -- [ "Error : the external array " ++ show arr ++ " is sampled at phase " ++ + -- show ph ++ " in the stream " ++ v ++ "." + -- , " Sampling can only occur from phase 1 onwards.\n" + -- ] show (BadPArrSpec v arr idx) = unlines [ "Error : the index into an external array can only take a " ++ "variable or a constant. The index\n" , idx ++ "\n\n in external array " - ++ arr ++ "in the definition of stream " ++ v ++ " is not of that " + ++ show arr ++ "in the definition of stream " ++ v ++ " is not of that " ++ "form.\n" ] show (BadType v v') = @@ -88,6 +89,13 @@ , "does not exist, or don't have the right type (there is no implicit " ++ "conversion).\n" ] + show (BadTypeExt v v') = + unlines + [ "Error : the external call " ++ show v ++ ", called in the stream " + ++ v' ++ ", either" + , "does not exist, or don't have the right type (there is no implicit " + ++ "conversion).\n" + ] show (NonNegativeWeightedClosedPath vs w) = unlines [ "Error : the following path is closed in the dependency graph of the " @@ -103,7 +111,7 @@ show (DependsOnClosePast vs v w len) = unlines [ "Error : the following path is of weight " ++ show w ++ " ending in " - ++ "the external variable " ++ v + ++ "the external variable " ++ show v , "while the first variable of that path has a prophecy array of length " ++ show len ++ "," , "which is strictly greater than the weight. This is forbidden." @@ -114,7 +122,7 @@ [ "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 + ++ "external variable " ++ show v , "which is quoted in the last variable of the path. This is " ++ "obviously impossible." , "Path : " ++ show (reverse vs) ++ "\n" @@ -161,9 +169,9 @@ case s of Var _ -> Nothing Const _ -> Nothing - PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph - PArr _ (arr,s0) ph -> checkIndex v arr s0 - &&> ph > 0 ||> BadSamplingArrPhase v arr ph + PVar _ _ -> Nothing -- ph > 0 ||> BadSamplingPhase v v' ph + PArr _ (arr,s0) -> checkIndex v arr s0 +-- &&> ph > 0 ||> BadSamplingArrPhase v arr ph &&> checkSyntaxSpec PArrSet v s0 Nothing F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v &&> checkSyntaxSpec FunSpecSet v s0 Nothing @@ -196,24 +204,27 @@ checkPath :: Streamable a => Int -> [Var] -> Spec a -> Maybe Error checkPath n vs s = case s of - PVar t v _ -> case () 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) + | t /= getAtomType s -> + Just $ BadTypeExt v (head vs) _ -> Nothing - PArr t (arr, idx) _ + PArr t (arr, idx) | n > 0 -> Just $ DependsOnFuture vs arr n | n > negate (prophecyArrayLength idx) -> Just $ DependsOnClosePast vs arr n (prophecyArrayLength idx) - | t /= getAtomType s -> Just $ BadType arr (head vs) + | t /= getAtomType s -> + Just $ BadTypeExt arr (head vs) | otherwise -> case idx of Const _ -> checkPath n vs idx Var _ -> checkPath n vs idx - _ -> Just $ BadPArrSpec v0 arr (show idx) + _ -> + Just $ BadPArrSpec v0 arr (show idx) Var v -> if elem v vs then if n >= 0 @@ -233,12 +244,6 @@ Drop i s' -> checkPath (n + i) vs s' in foldStreamableMaps checkPathsFromSpec streams Nothing -type Exs = (A.Type, Var, ExtVars) - -data ExtVars = ExtV Phase - | ExtA Phase String - deriving Eq - getExternalVars :: StreamableMaps Spec -> [Exs] getExternalVars streams = nub $ foldStreamableMaps decl streams [] @@ -247,8 +252,8 @@ => Var -> Spec a -> [Exs] -> [Exs] decl _ s ls = case s of - PVar t v ph -> (t, v, ExtV ph) : ls - PArr t (arr, s0) ph -> (t, arr, ExtA ph (show s0)) : ls + PVar t v -> (t, v, ExtRetV) : ls + PArr t (arr, s0) -> (t, arr, ExtRetA (show s0)) : ls F _ _ s0 -> decl undefined s0 ls F2 _ _ s0 s1 -> decl undefined s0 $ decl undefined s1 ls F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 diff --git a/Language/Copilot/AtomToC.hs b/Language/Copilot/AtomToC.hs --- a/Language/Copilot/AtomToC.hs +++ b/Language/Copilot/AtomToC.hs @@ -3,35 +3,37 @@ -- | Defines a main() and print statements to easily execute generated Copilot specs. module Language.Copilot.AtomToC(getPrePostCode) where -import Language.Copilot.Compiler (tmpSampleStr) +import Language.Copilot.Compiler (tmpSampleStr, tmpArrName, tmpVarName) import Language.Copilot.AdHocC -import Language.Copilot.Core -import Language.Copilot.Analyser (ExtVars(..)) -import qualified Language.Atom as A +import Language.Copilot.Core 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, ExtVars)] - -> [(String,Int)] -> Vars -> Period -> (String, String) +-- allExts represents all the variabbles to monitor (used for declaring them) +-- inputExts represents the monitored variables which are to be fed to the +-- standard input of the C program. only used for the testing with random +-- streams and values. +getPrePostCode :: Name -> StreamableMaps Spec -> [Exs] + -> [(Ext,Int)] -> Vars -> Period -> (String, String) getPrePostCode cName streams allExts arrDecs inputExts p = (preCode $ extDecls allExts arrDecs, postCode cName streams allExts inputExts p) -- Make the declarations for external vars -extDecls :: [(A.Type, Var, ExtVars)] -> [(String,Int)] -> [String] +extDecls :: [Exs] -> [(Ext,Int)] -> [String] extDecls allExtVars arrDecs = - let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars - getDec (t, v, ExtV _) = varDecl t [v] - getDec (t, arr, ExtA _ _) = + let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') + allExtVars + getDec :: Exs -> String + getDec (t, (ExtV v), ExtRetV) = varDecl t [v] + getDec (_, (Fun _ _), ExtRetV) = "" + getDec (t, arr, ExtRetA _) = case getIdx arr of Nothing -> error $ "Please use the setArrs option to provide a list of " ++ "pairs (a,idx) where a is the name of an external array and idx " ++ "is its static size to declare. There is no size for array " ++ - arr ++ "." - Just idx -> arrDecl t [(arr, idx)] + show arr ++ "." + Just idx -> arrDecl t [(show arr, idx)] getIdx arr = lookup arr arrDecs in map getDec uniqueExtVars @@ -47,18 +49,14 @@ ] ++ extDeclarations -vPre :: Name -> String -vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." - -postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] -> Vars -> Period -> String +postCode :: Name -> StreamableMaps Spec -> [Exs] -> 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[]) {" + [ "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." @@ -121,16 +119,19 @@ ++ typeId (head l) ++ "\", &" ++ v ++ ");") : (indent ++ "clean (" ++ string ++ ", stdin);") : ls -sampleExtVars :: [(A.Type, Var, ExtVars)] -> Name -> [String] +sampleExtVars :: [Exs] -> Name -> [String] sampleExtVars allExts cName = map (\ext -> let (v,e) = sample ext in - " " ++ vPre cName ++ tmpSampleStr ++ e + " " ++ vPre cName ++ tmpSampleStr ++ (normalizeVar e) ++ " = " ++ v ++ ";") allExts where - sample :: (A.Type, Var, ExtVars) -> (Var, String) - sample (_, v, ExtV ph) = (v, tmpVarName v ph) - sample (_, v, ExtA ph idx) = (v ++ "[0]", tmpArrName v ph idx) + sample :: Exs -> (Var, String) + sample (_, v, ExtRetV) = ( case v of + ExtV var -> var + Fun fname args -> funcShow cName fname args + , tmpVarName v) + sample (_, v, ExtRetA idx) = (show v ++ "[0]", tmpArrName v idx) outputVars :: Name -> StreamableMaps Spec -> [String] outputVars cName streams = diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs --- a/Language/Copilot/Compiler.hs +++ b/Language/Copilot/Compiler.hs @@ -1,62 +1,130 @@ {-# LANGUAGE ScopedTypeVariables, Rank2Types #-} --- Note : for now, the initial state is computed during the first tick +-- XXX Clean this up! -- | Transform the copilot specification in an atom one, and then compile that one. -module Language.Copilot.Compiler(copilotToAtom, tmpSampleStr) where +module Language.Copilot.Compiler + (copilotToAtom, tmpSampleStr, tmpArrName, tmpVarName + ) where import Language.Copilot.Core import Data.Maybe -import Data.Map as M +import qualified Data.Map as M import Data.List +import Data.Word (Word64) import qualified Language.Atom as A -- | Compiles an /Copilot/ specification to an /Atom/ one. -- The period is given as a Maybe : if it is Nothing, an optimal period will be chosen. -copilotToAtom :: LangElems -> Maybe Period -> (Period, A.Atom ()) -copilotToAtom (LangElems streams sends triggers) p = +copilotToAtom :: LangElems -> Maybe Period -> Name -> (Period, A.Atom ()) +copilotToAtom (LangElems streams sends triggers) p cFileName = (p', A.period p' $ do - prophArrs <- mapStreamableMapsM initProphArr streams outputs <- mapStreamableMapsM initOutput streams - updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty) outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty) - - tmpSamples <- foldStreamableMaps (\_ -> initExtSamples streams prophArrs outputIndexes) + tmpSamples <- foldStreamableMaps + (\_ -> initExtSamples streams outputs prophArrs outputIndexes) streams (return emptyTmpSamples) - -- One atom rule for each stream - foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples + foldStreamableMaps (makeRule p' streams outputs prophArrs tmpSamples updateIndexes outputIndexes) streams (return ()) - -- foldStreamableMaps (makeTrigger streams prophArrs tmpSamples - -- outputIndexes) - -- triggers (return ()) - - M.fold (makeTrigger streams prophArrs tmpSamples outputIndexes) - (return ()) triggers - + M.fold (makeTrigger outputs cFileName) (return ()) triggers + 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 [] + foldStreamableMaps (\_ -> sampleExts outputs tmpSamples cFileName) streams [] ) - where - optP = getOptimalPeriod streams sends - 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." + where p' = period p +-- where +-- optP = getOptimalPeriod streams sends +-- | For period of length n: +-- Phase 0: state update. +-- Phase 1: Compute output variables. +-- Phase 2 - n-2: send values (if any). +-- Phase 2 - n-2: Sample external vars (if any). +-- Phase n-1: update indexes. +period :: Maybe Int -> Int +period p = + case p of + Nothing -> minPeriod + Just i -> if i >= minPeriod + then i + else error $ "Copilot error: the period is too short, " + ++ "it should be at least " ++ show minPeriod ++ " ticks." + where minPeriod :: Int + minPeriod = 4 + +-- For the prophecy arrays +type ArrIndex = Word64 +type ProphArrs = StreamableMaps BoundedArray +type Outputs = StreamableMaps A.V +type Indexes = M.Map Var (A.V ArrIndex) + +-- External variables +data PhasedValueVar a = PhV (A.V a) + +data BoundedArray a = B ArrIndex (Maybe (A.A a)) + +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 -> + let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in + A.value var + PArr _ (v, idx) -> + let PhA var = e tmp (tmpArrs tmpSamples) + tmp = tmpArrName v (show idx) + e a b = case getMaybeElem a b of + Nothing -> + error "Error in application of getElem in nextSt." + Just x -> x + in A.value var + Var v -> let B initLen maybeArr = getElem v prophArrs in + -- This check is extremely important + -- It means that if x at time n depends on y at time n + -- then x is obtained not by y, but by inlining the definition of y + -- so it increases the size of code (sadly), + -- but is the only thing preventing race conditions from occuring + if index < initLen + then getVar v initLen maybeArr + else let s0 = getElem v streams in + next s0 (index - initLen) + Const e -> A.Const e + F _ f s0 -> f $ next s0 index + F2 _ f s0 s1 -> + f (next s0 index) + (next s1 index) + F3 _ f s0 s1 s2 -> + f (next s0 index) + (next s1 index) + (next s2 index) + Append _ s0 -> next s0 index + Drop i s0 -> next s0 (fromInteger (toInteger i) + index) + where + next :: Streamable b => Spec b -> ArrIndex -> A.E b + next = nextSt streams prophArrs tmpSamples outputIndexes + getVar :: Streamable a + => Var -> ArrIndex -> Maybe (A.A a) -> A.E a + getVar v initLen maybeArr = + let outputIndex = case M.lookup v outputIndexes of + Nothing -> error "Error in function getVar." + Just x -> x + arr = case maybeArr of + Nothing -> error "Error in function getVar (maybeArr)." + Just x -> x in + arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_` + (A.Const (initLen + 1))) + initProphArr :: forall a. Streamable a => Var -> Spec a -> A.Atom (BoundedArray a) initProphArr v s = let states = initState s @@ -75,6 +143,26 @@ Append ls s'' -> ls ++ initState s'' _ -> [] + +-- External arrays +data PhasedValueArr a = PhA (A.V a) -- Array name. +data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. + +data TmpSamples = + TmpSamples { tmpVars :: StreamableMaps PhasedValueVar + , tmpArrs :: StreamableMaps PhasedValueArr + , tmpIdxs :: StreamableMaps PhasedValueIdx + } + +emptyTmpSamples :: TmpSamples +emptyTmpSamples = TmpSamples emptySM emptySM emptySM + +tmpVarName :: Ext -> Var +tmpVarName v = show v + +tmpArrName :: Ext -> String -> Var +tmpArrName v idx = (tmpVarName v) ++ "_" ++ normalizeVar idx + initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) initOutput v _ = do atomConstructor (normalizeVar v) (unit::a) @@ -83,9 +171,9 @@ tmpSampleStr = "tmpSampleVal__" initExtSamples :: forall a. Streamable a - => StreamableMaps Spec -> ProphArrs -> Indexes -> Spec a + => StreamableMaps Spec -> Outputs -> ProphArrs -> Indexes -> Spec a -> A.Atom TmpSamples -> A.Atom TmpSamples -initExtSamples streams prophArrs outputIndexes s tmpSamples = do +initExtSamples streams outputs prophArrs outputIndexes s tmpSamples = do case s of Const _ -> tmpSamples Var _ -> tmpSamples @@ -96,23 +184,21 @@ initExtSamples' s1 tmpSamples F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $ initExtSamples' s2 tmpSamples - PVar _ v ph -> - do -- checkVar v - ts <- tmpSamples - let v' = tmpVarName v ph + PVar _ v -> + do ts <- tmpSamples + let v' = tmpVarName v vts = tmpVars ts maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a) name = tmpSampleStr ++ normalizeVar v' case maybeElem of Nothing -> do val <- atomConstructor name (unit::a) - let m' = M.insert v' (PhV ph val) (getSubMap vts) + let m' = M.insert v' (PhV val) (getSubMap vts) return $ ts {tmpVars = updateSubMap (\_ -> m') vts} Just _ -> return ts - PArr _ (arr, idx) ph -> - do --checkVar arr - ts <- tmpSamples - let arr' = tmpArrName arr ph (show idx) + PArr _ (arr, idx) -> + do ts <- tmpSamples + let arr' = tmpArrName arr (show idx) arrts = tmpArrs ts idxts = tmpIdxs ts maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a) @@ -122,29 +208,17 @@ do val <- atomConstructor name (unit::a) let i = case idx of Const e -> PhIdx $ A.Const e - Var _ -> --- let B initLen maybeArr = getElem v prophArrs --- let B initLen maybeArr = --- case getMaybeElem v prophArrs of --- Nothing -> --- error "Error in function initExtSamples." --- Just x -> x - PhIdx $ nextSt streams prophArrs - undefined outputIndexes idx 0 + Var v -> PhIdx $ A.value (getElem v outputs) _ -> error "Unexpected Spec in initExtSamples." - let m' = M.insert arr' (PhA ph val) (getSubMap arrts) + let m' = M.insert arr' (PhA val) (getSubMap arrts) let m'' = M.insert arr' i (getSubMap idxts) return $ ts { tmpArrs = updateSubMap (\_ -> m') arrts , tmpIdxs = updateSubMap (\_ -> m'') idxts } Just _ -> return ts - where - -- checkVar v = when (normalizeVar v /= v) - -- (error $ "Copilot: external variable " ++ v ++ " is not " - -- ++ "a valid C99 variable.") - initExtSamples' :: Streamable b + where initExtSamples' :: Streamable b => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples - initExtSamples' = initExtSamples streams prophArrs outputIndexes + initExtSamples' = initExtSamples streams outputs prophArrs outputIndexes makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes makeUpdateIndex v (B n arr) indexes = @@ -167,9 +241,9 @@ return $ M.insert v index mindexes makeRule :: forall a. Streamable a => - StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples -> + Period -> 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 +makeRule p streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do r let B n maybeArr = getElem v prophArrs::BoundedArray a case maybeArr of @@ -188,51 +262,37 @@ 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) + outputIndex A.<== (A.VRef outputIndex + A.Const 1) + `A.mod_` A.Const (n + 1) - -- Spread these out evenly accross the remaining phases, staring no - -- earlier than phase 1. - A.phase ((maxSampleDep v streams) + 1) + -- XXX For now, we put these all in the last phase. We want better + -- distribution though at some point. + A.phase (p - 1) $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do - updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1) + updateIndex A.<== (A.VRef updateIndex + A.Const 1) + `A.mod_` A.Const (n + 1) where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0 --- | Find the maximum phase as which an array sampling depends on this stream by --- computing it's index in terms of it. Returns zero by default. -maxSampleDep :: Var -> StreamableMaps Spec -> Int -maxSampleDep v streams = - foldStreamableMaps (\_ -> streamDep) streams 0 - where - streamDep :: Streamable b => Spec b -> Int -> Int - streamDep s i = - case s of - Var _ -> i - Const _ -> i - PVar _ _ _ -> i - PArr _ (_, Var v') ph | v == v' -> max ph i - | otherwise -> i - PArr _ _ _ -> i - F _ _ s0 -> streamDep s0 i - F2 _ _ s0 s1 -> streamDep s0 $ streamDep s1 i - F3 _ _ s0 s1 s2 -> streamDep s0 $ streamDep s1 $ streamDep s2 i - Append _ s0 -> streamDep s0 i - Drop _ s0 -> streamDep s0 i - --- makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom () --- makeSend outputs name (Send (v, ph, port)) r = do --- r --- A.exactPhase ph $ A.atom ("__send_" ++ name) $ --- send ((A.value (getElem v outputs))::(A.E a)) port +-- Do sends in phase 2. makeSend :: forall a. Streamable a => Outputs -> String -> Send a -> A.Atom () -> A.Atom () -makeSend outputs name (Send v ph port portName) r = do +makeSend outputs name (Send v port portName) r = do r - A.exactPhase ph $ A.atom ("__send_" ++ name) $ - mkSend (A.value (notVarErr v (\var -> getElem var outputs)) :: A.E a) + A.exactPhase 2 $ A.atom ("__send_" ++ name) $ + mkSend (A.value $ getElem (getMaybeVar v) outputs :: A.E a) port portName +-- | Sending data over ports. +mkSend :: (Streamable a) => A.E a -> Port -> String -> A.Atom () +mkSend e (Port port) portName = + A.action (\ueStr -> portName ++ "(" ++ head ueStr ++ "," ++ show port ++ ")") + [A.ue e] + +sampleStr :: String +sampleStr = "sample__" + -- What we really should be doing is just folding over the TmpSamples, since -- that data should contain all the info we need to construct external variable -- and external array samples. However, there is the issue that for array @@ -240,38 +300,51 @@ -- having the spec available provides typing coercion. We could fold over the -- TmpSamples, passing streams in, and extract the appropriate Spec a. sampleExts :: forall a. Streamable a - => TmpSamples -> Spec a -> [(Var, A.Atom ())] -> [(Var, A.Atom ())] -sampleExts ts s a = do + => Outputs -> TmpSamples -> Name -> Spec a + -> [(Var, A.Atom ())] -> [(Var, A.Atom ())] +sampleExts outputs ts cFileName s a = do case s of Var _ -> a Const _ -> a - PVar _ v ph -> - let v' = tmpVarName v ph - PhV _ var = getElem v' (tmpVars ts)::PhasedValueVar a in - (v', A.exactPhase ph $ - A.atom ("sample__" ++ v') $ - var A.<== (A.value $ externalAtomConstructor v) + PVar _ v -> + let v' = tmpVarName v +-- PhV var = getElem v' (tmpVars ts) :: PhasedValueVar a in + PhV var = case getMaybeElem v' (tmpVars ts) :: Maybe (PhasedValueVar a) of + Nothing -> error $ "Copilot error: variable " ++ v' + ++ " was not defined!." + Just (PhV var') -> PhV var' in + (v', A.exactPhase minSampPh $ + A.atom (sampleStr ++ normalizeVar v') $ + var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v) ) : a - - PArr _ (arr, idx) ph -> - let arr' = tmpArrName arr ph (show idx) + PArr _ (arr, idx) -> + let arr' = tmpArrName arr (show idx) PhIdx i = getIdx arr' idx (tmpIdxs ts) --- PhA _ arrV = getElem arr' (tmpArrs ts)::PhasedValueArr a in - PhA _ arrV = case getMaybeElem arr' (tmpArrs ts)::Maybe (PhasedValueArr a) of - Nothing -> error "Error in fucntion sampleExts." - Just x -> x - in - (arr', A.exactPhase ph $ - A.atom ("sample__" ++ arr') $ - arrV A.<== A.array' arr (atomType (unit::a)) A.!. i - ) : a - F _ _ s0 -> sampleExts ts s0 a - F2 _ _ s0 s1 -> sampleExts ts s0 $ sampleExts ts s1 a - F3 _ _ s0 s1 s2 -> sampleExts ts s0 $ sampleExts ts s1 $ - sampleExts ts s2 a - Append _ s0 -> sampleExts ts s0 a - Drop _ s0 -> sampleExts ts s0 a + PhA arrV = + case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of + Nothing -> error "Error in fucntion sampleExts." + Just x -> x in + (arr', A.exactPhase minSampPh $ + A.atom (sampleStr ++ normalizeVar arr') $ + arrV A.<== A.array' (getSampleFuncVar arr) + (atomType (unit::a)) A.!. i + ) : a + F _ _ s0 -> sampleExts' s0 a + F2 _ _ s0 s1 -> sampleExts' s0 $ sampleExts' s1 a + F3 _ _ s0 s1 s2 -> sampleExts' s0 $ sampleExts' s1 $ + sampleExts' s2 a + Append _ s0 -> sampleExts' s0 a + Drop _ s0 -> sampleExts' s0 a + where minSampPh :: Int + minSampPh = 2 + sampleExts' s' a' = sampleExts outputs ts cFileName s' a' + getSampleFuncVar v = case v of + ExtV extV -> extV + -- XXX A bit of a hack. Atom should be changed to allow + -- "out-of-Atom" assignments. But this works for now. + Fun nm args -> funcShow cFileName nm args + -- lookup the idx for external array accesses in the map. getIdx :: forall a. (Streamable a, A.IntegralE a) => Var -> Spec a -> StreamableMaps PhasedValueIdx -> PhasedValueIdx a @@ -284,33 +357,29 @@ _ -> error $ "Expecing either a variable or constant for the index " ++ "in the external array access for array " ++ arr ++ "." --- 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 = - case spec of - PVar _ _ ph -> max (ph + 1) n - PArr _ (_, Var _) ph -> max (ph + 2) n -- because this may depend on a - -- variable, and if that variable - -- has a prophecy array, it needs - -- an extra phase to update after - -- the index is taken. - PArr _ _ ph -> max (ph + 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 +-- TRIGGERS ----------------------------- - getMaxSendPhase :: Var -> Send a -> Period -> Period - getMaxSendPhase _ (Send _ ph _ _) n = max (ph+1) n +-- | To make customer C triggers. Only for Spec Bool (others throw an +-- error). +makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom () +makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = + do r + (A.exactPhase 2 $ A.atom (show trigger) $ + do A.cond (getOutput outputs s) + fnCall cFileName fnName args) + +-- | Building an external function call in Atom. +fnCall :: Name -> String -> Args -> A.Atom () +fnCall cFileName fnName args = + A.action (\_ -> funcShow cFileName fnName args) [] + +getOutput :: Streamable a => Outputs -> Spec a -> A.E a +getOutput outputs s = + case s of + (Var v) -> A.value + (case getMaybeElem v outputs of + Nothing -> error $ "Copilot error in trigger specification: variable " + ++ v ++ " was not defined!." + Just v' -> v') + (Const c) -> A.Const c + _ -> error "Impossible error in getOutput in Compiler.hs." diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs --- a/Language/Copilot/Core.hs +++ b/Language/Copilot/Core.hs @@ -1,5 +1,5 @@ {-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, - FlexibleInstances #-} + FlexibleInstances, TypeSynonymInstances #-} -- | Provides basic types and functions for other parts of /Copilot/. -- @@ -8,22 +8,17 @@ -- 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, Send(..), --DistributedStreams, - Trigger(..), Triggers, notVarErr, LangElems(..), - -- * General functions on 'Streams' and 'StreamableMaps' - Streamable(..), mkSend, -- Sendable(..) - StreamableMaps(..), emptySM, + Period, Var, Name, Port(..), Ext(..), + Exs, ExtRet(..), Args, ArgConstVar(..), + Spec(..), Streams, Stream, Send(..), + Trigger(..), Triggers, LangElems(..), + Streamable(..), StreamableMaps(..), emptySM, isEmptySM, getMaybeElem, getElem, - foldStreamableMaps, --foldSendableMaps, + foldStreamableMaps, mapStreamableMaps, mapStreamableMapsM, filterStreamableMaps, normalizeVar, getVars, Vars, - -- compiler - BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, - ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..), - tmpVarName, tmpArrName, getAtomType, - getSpecs, getSends, getTriggers, makeTrigger -- XXX compiler + getAtomType, getSpecs, getSends, getTriggers, vPre, funcShow, + getMaybeVar, notConstVarErr ) where import qualified Language.Atom as A @@ -41,10 +36,10 @@ type Var = String -- | C file name type Name = String --- | Atom period +-- | Atom period -- used as an option to control the duration of a Copilot "tick". type Period = Int --- | Phase of an Atom phase -type Phase = Int +-- -- | Phase of an Atom phase +-- type Phase = Int -- | Port over which to broadcast information data Port = Port Int @@ -54,9 +49,9 @@ Var :: Streamable a => Var -> Spec a Const :: Streamable a => a -> Spec a - PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a + PVar :: Streamable a => A.Type -> Ext -> Spec a PArr :: (Streamable a, Streamable b, A.IntegralE b) - => A.Type -> (Var, Spec b) -> Phase -> Spec a + => A.Type -> (Ext, Spec b) -> Spec a F :: (Streamable a, Streamable b) => (b -> a) -> (A.E b -> A.E a) -> Spec b -> Spec a @@ -69,6 +64,68 @@ Append :: Streamable a => [a] -> Spec a -> Spec a Drop :: Streamable a => Int -> Spec a -> Spec a +-- | Arguments to be passed to a C function. Either a Copilot variable or a +-- constant. A little hacky that I store constants as strings so we don't have +-- to pass around types. However, these data are just used to make external C +-- calls, for which we have no type info anyway, so it's a bit of a moot point. +data ArgConstVar = V Var + | C String + deriving Eq + +instance Show ArgConstVar where + show args = case args of + V v -> normalizeVar v + C c -> "_const_" ++ c ++ "_" + +type Args = [ArgConstVar] + +data Trigger = + Trigger { trigVar :: Spec Bool + , trigName :: String + -- We carry around both the value and the vars of the arguments to be + -- passed to the trigger. The vars are used to put the arguments in + -- the correct order, since the values are stored in a map, destroying + -- their order. + , trigArgs :: Args} + +type Triggers = M.Map String Trigger + +instance Show Trigger where + show (Trigger s fnName args) = + "trigger_" ++ getMaybeVar s ++ "_" ++ fnName ++ "_" ++ normalizeVar (show args) + +-- XXX change the constructors to SimpleVar and Function (or something like that) +-- XXX in Ext, we throw away the type info for Args. This is because we're just +-- making external calls, and we don't know anything about the types anyway (we +-- just make strings). Remove from the datatype. +-- | Holds external variables or external functions to call. +data Ext = ExtV Var + | Fun String Args + +type Exs = (A.Type, Ext, ExtRet) + +data ExtRet = ExtRetV + | ExtRetA String + deriving Eq + +instance Show Ext where + show (ExtV v) = v + show (Fun f args) = normalizeVar f ++ show args + +-- | For calling a function with Atom variables. +funcShow :: Name -> String -> Args -> String +funcShow cName fname args = + fname ++ "(" ++ (unwords $ intersperse "," + (map (\arg -> case arg of + v@(V _) -> vPre cName ++ show v + C c -> c + ) args)) ++ ")" + +instance Eq Ext where + (==) (ExtV v0) (ExtV v1) = v0 == v1 + (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1 + (==) _ _ = False + -- These belong in Language.hs, but we don't want orphan instances. instance (Streamable a, A.NumE a) => Num (Spec a) where (+) = F2 (+) (+) -- A.NumE a => E a is an instance of Num @@ -94,9 +151,9 @@ #-} instance Eq a => Eq (Spec a) where - (==) (PVar t v ph) (PVar t' v' ph') = t == t' && v == v' && ph == ph' - (==) (PArr t (v, idx) ph) (PArr t' (v', idx') ph') = - t == t' && v == v' && show idx == show idx' && ph == ph' + (==) (PVar t v) (PVar t' v') = t == t' && v == v' -- && ph == ph' + (==) (PArr t (v, idx)) (PArr t' (v', idx')) = + t == t' && v == v' && show idx == show idx' -- && ph == ph' (==) (Var v) (Var v') = v == v' (==) (Const x) (Const x') = x == x' (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s' @@ -106,35 +163,26 @@ (==) (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. +-- | Get a variable name from a spec; throw an error otherwise. +getMaybeVar :: Streamable a => Spec a -> Var +getMaybeVar (Var v) = v +getMaybeVar s = error $ "Expected a Copilot variable but provided " ++ show s ++ " instead." + +-- | Copilot variable reference, taking the name of the generated C file. +vPre :: Name -> String +vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." + +-- | An instruction to send data on a port at a given phase. -- data Send a = Sendable a => Send (Var, Phase, Port) data Send a = Send { sendVar :: Spec a - , sendPh :: Phase , sendPort :: Port , sendName :: String} 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))) - + show (Send s (Port port) portName) = + portName ++ "_port_" ++ show port ++ "_var_" ++ getMaybeVar s + -- | Holds all the different kinds of language elements that are pushed into the -- Writer monad. This currently includes the actual specs, "send" directives, -- and trigger directives. (Use the functions in Language.hs to make sends and @@ -150,13 +198,13 @@ getSpecs :: Streams -> StreamableMaps Spec getSpecs streams = - let (LangElems strms _ _) = execWriter streams - in strms + let (LangElems ss _ _) = execWriter streams + in ss getSends :: Streams -> StreamableMaps Send getSends streams = - let (LangElems _ snds _) = execWriter streams - in snds + let (LangElems _ sendMap _) = execWriter streams + in sendMap getTriggers :: Streams -> Triggers getTriggers streams = @@ -166,7 +214,17 @@ -- | A named stream type Stream a = Streamable a => (Var, Spec a) +-- | If the 'Spec' isn't a 'Var' or 'Const', then throw an error; otherwise, +-- apply the function. +notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b +notConstVarErr s f = + case s of + Var v -> f (V v) + Const c -> f (C (showAsC c)) + _ -> error $ "You provided specification \n" ++ " " ++ show s + ++ "\n where you needed to give a Copilot variable or constant." + -- | Holds the complete specification of a distributed monitor -- type DistributedStreams = (Streams, Sends) @@ -215,21 +273,6 @@ -- doubles have the good precision. showAsC :: a -> String --- | 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 - Var v -> f v - _ -> error $ "You provided specification \n" ++ show s - ++ "\n where you needed to give a variable." - --- | 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} @@ -341,9 +384,11 @@ -- Launch an exception if the index is not in it {-# INLINE getElem #-} getElem :: Streamable a => Var -> StreamableMaps b -> b a -getElem v sm = case getMaybeElem v sm of - Nothing -> error "Error in application of getElem from Core.hs." - Just x -> x +getElem v sm = + case getMaybeElem v sm of + Nothing -> error $ "Error in application of getElem from Core.hs for variable " + ++ v ++ "." + Just x -> x getAtomType :: Streamable a => Spec a -> A.Type getAtomType s = @@ -499,14 +544,9 @@ -- | Replace all accepted special characters by sequences of underscores. normalizeVar :: Var -> Var -normalizeVar v = - foldl (\ acc c -> acc ++ case c of - '.' -> "_" - '[' -> "_" - ']' -> "_" - ' ' -> "_" - _ -> [c]) - "" v +normalizeVar v = + map (\c -> if (c `elem` ".[]()") then '_' else c) + (filter (\c -> c /= ',' && c /= ' ') v) -- | For each typed variable, this type holds all its successive values in an infinite list -- Beware : each element of one of those lists corresponds to a full @Atom@ period, @@ -524,11 +564,11 @@ tabs ++ showRaw s n showRaw :: Spec a -> Int -> String -showRaw (PVar t v ph) _ = "PVar " ++ show t ++ " " ++ v ++ " " ++ show ph -showRaw (PArr t (v, idx) ph) _ = - "PArr " ++ show t ++ " (" ++ v ++ " ! (" ++ show idx ++ ")) " ++ show ph +showRaw (PVar t v) _ = "PVar " ++ show t ++ " " ++ show v -- ++ " " ++ show ph +showRaw (PArr t (v, idx)) _ = + "PArr " ++ show t ++ " (" ++ show v ++ " ! (" ++ show idx ++ "))" -- ++ show ph showRaw (Var v) _ = "Var " ++ v -showRaw (Const e) _ = "Const " ++ show e +showRaw (Const e) _ = show e showRaw (F _ _ s0) n = "F op? (\n" ++ showIndented s0 (n + 1) ++ "\n" ++ @@ -555,133 +595,3 @@ --- 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 -type ProphArrs = StreamableMaps BoundedArray -type Outputs = StreamableMaps A.V -type Indexes = M.Map Var (A.V ArrIndex) - --- External variables -data PhasedValueVar a = PhV Phase (A.V a) ---type TmpVarSamples = StreamableMaps PhasedValueVar - -tmpVarName :: Var -> Phase -> Var -tmpVarName v ph = normalizeVar v ++ "_" ++ show ph - - --- External arrays -data PhasedValueArr a = PhA Phase (A.V a) -- Array name. -data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. - -data TmpSamples = - TmpSamples { tmpVars :: StreamableMaps PhasedValueVar - , tmpArrs :: StreamableMaps PhasedValueArr - , tmpIdxs :: StreamableMaps PhasedValueIdx - } - -emptyTmpSamples :: TmpSamples -emptyTmpSamples = TmpSamples emptySM emptySM emptySM - -tmpArrName :: Var -> Phase -> String -> Var -tmpArrName v ph idx = (tmpVarName v ph) ++ "_" ++ normalizeVar idx - -data BoundedArray a = B ArrIndex (Maybe (A.A a)) - -nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes - -> Spec a -> ArrIndex -> A.E a -nextSt streams prophArrs tmpSamples outputIndexes s index = - case s of - PVar _ v ph -> - let PhV _ var = getElem (tmpVarName v ph) (tmpVars tmpSamples) in - A.value var - PArr _ (v, idx) ph -> - let PhA _ var = e tmp (tmpArrs tmpSamples) - tmp = tmpArrName v ph (show idx) - e a b = case getMaybeElem a b of - Nothing -> - error "Error in application of getElem in nextSt." - Just x -> x - in A.value var - Var v -> let B initLen maybeArr = getElem v prophArrs in - -- This check is extremely important - -- It means that if x at time n depends on y at time n - -- then x is obtained not by y, but by inlining the definition of y - -- so it increases the size of code (sadly), - -- but is the only thing preventing race conditions from occuring - if index < initLen - then getVar v initLen maybeArr - else let s0 = getElem v streams in - next s0 (index - initLen) - Const e -> A.Const e - F _ f s0 -> f $ next s0 index - F2 _ f s0 s1 -> - f (next s0 index) - (next s1 index) - F3 _ f s0 s1 s2 -> - f (next s0 index) - (next s1 index) - (next s2 index) - Append _ s0 -> next s0 index - Drop i s0 -> next s0 (fromInteger (toInteger i) + index) - where - next :: Streamable b => Spec b -> ArrIndex -> A.E b - next = nextSt streams prophArrs tmpSamples outputIndexes - getVar :: Streamable a - => Var -> ArrIndex -> Maybe (A.A a) -> A.E a - getVar v initLen maybeArr = - let outputIndex = case M.lookup v outputIndexes of - Nothing -> error "Error in function getVar." - Just x -> x - arr = case maybeArr of - Nothing -> error "Error in function getVar (maybeArr)." - Just x -> x in - arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_` - (A.Const (initLen + 1))) diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs --- a/Language/Copilot/Dispatch.hs +++ b/Language/Copilot/Dispatch.hs @@ -12,7 +12,7 @@ (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where import Language.Copilot.Core -import Language.Copilot.Analyser +import Language.Copilot.Analyser (check, getExternalVars) import Language.Copilot.Interpreter import Language.Copilot.AtomToC import Language.Copilot.Compiler @@ -33,12 +33,8 @@ , 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 :: [(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)@. + , prePostCode :: Maybe (String, String) -- ^ Code to replace the default + -- initialization and main , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we -- don't know how large external arrays are, so -- we cannot declare them. Passing in pairs @@ -123,17 +119,19 @@ isSilent = verbose == OnlyErrors isExecuted = iterations /= 0 allExts = getExternalVars (strms elems) - (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts + (trueInputExts :: StreamableMaps [] , allInputsPresents :: Bool) = + filterStreamableMaps inputExts (map (\(a,v,r) -> (a, show v, r)) allExts) -copilotToC :: LangElems -> [(A.Type, Var, ExtVars)] -> Vars -> AtomToC -> Bool -> IO () +copilotToC :: LangElems -> [Exs] -> Vars -> AtomToC -> Bool -> IO () copilotToC elems allExts trueInputExts opts isVerbose = - let (p', program) = copilotToAtom elems (getPeriod opts) - cFileName = cName opts + let cFileName = cName opts + (p', program) = copilotToAtom elems (getPeriod opts) cFileName (preCode, postCode) = case (prePostCode opts) of Nothing -> getPrePostCode cFileName (strms elems) allExts - (arrDecs opts) trueInputExts p' + (map (\(x,y) -> (ExtV x,y)) (arrDecs opts)) + trueInputExts p' Just (pre, post) -> (pre, post) atomConfig = A.defaults { A.cCode = \_ _ _ -> (preCode, postCode) diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs --- a/Language/Copilot/Examples/Examples.hs +++ b/Language/Copilot/Examples/Examples.hs @@ -10,7 +10,7 @@ -- for specifying options import Data.Map (fromList) import Data.Maybe (Maybe (..)) -import System.Random +--import System.Random import Language.Copilot -- import Language.Copilot.Variables @@ -18,7 +18,7 @@ fib :: Streams fib = do let f = varW64 "f" - let t = varB "t" + t = varB "t" f .= [0,1] ++ f + (drop 1 f) t .= even f where even :: Spec Word64 -> Spec Bool @@ -27,9 +27,9 @@ t1 :: Streams t1 = do let x = varI32 "x" - let y = varB "y" - let z = varB "z" - let w = varB "w" + y = varB "y" + z = varB "z" + w = varB "w" x .= [0, 1, 2] ++ x - (drop 1 x) y .= [True, False] ++ y ^ z z .= x <= drop 1 x @@ -44,35 +44,31 @@ t3 :: Streams t3 = do let a = varW32 "a" - let b = varB "b" - let ext8 = extW32 "ext" 8 - let ext1 = extW32 "ext" 1 + b = varB "b" + ext8 = extW32 "ext" + ext1 = extW32 "ext" a .= [0,1] ++ a + ext8 + ext8 + ext1 b .= [True, False] ++ 2 + a < 5 + ext1 t4 :: Streams t4 = do let a = varB "a" - let b = varB "b" + b = varB "b" a .= [True,False] ++ not a b .= drop 1 a t5 :: Streams 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 + y = varB "y" + z = varB "z" + x .= [0] ++ x + 1 + y .= [True, True] ++ y + z .= [False] ++ not z -- 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) + trigger y "y_trigger" void + trigger z "z0_trigger" x + trigger z "z1_trigger" (y <> constW16 3 <> x) yy :: Streams yy = @@ -82,7 +78,7 @@ zz :: Streams zz = do let a = varW32 "a" - let b = varW32 "b" + b = varW32 "b" --a .= [0..4] ++ drop 4 (varW32 a) + 1 a .= a + 1 b .= drop 3 a @@ -90,47 +86,57 @@ xx :: Streams xx = do let a = varW32 "a" - let b = varW32 "b" - let c = varW32 "c" - let ext = extW32 "ext" 1 - a .= ext + b = varW32 "b" + c = varW32 "c" + e = extW32 "ext" + d = varB "d" + f = extW32 (fun "fun1" void) + h = extArrW16 (fun "g" b) a + g = extW16 (fun "fun2" (true <> b <> constW16 3)) + w = varB "w" + a .= e + f b .= [3] ++ a c .= [0, 1, 3, 4] ++ drop 1 b + d .= h < g + -- triggers + trigger d "y_trigger" void + trigger w "z0_trigger" (a <> b <> true) + trigger w "z1_trigger" (d <> constW16 3 <> w) -- 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 -- external vars - let temp = extF "temp" 1 - let shutoff = extB "shutoff" 2 + let temp = extF "temp" + shutoff = extB "shutoff" -- Copilot vars - let temps = varF "temps" - let overTemp = varB "overTemp" - let trigger = varB "trigger" + temps = varF "temps" + overTemp = varB "overTemp" + err = varB "trigger" temps .= [0, 0, 0] ++ temp overTemp .= drop 2 temps > 2.3 + temps - trigger .= overTemp ==> shutoff + err .= overTemp ==> shutoff -- | Sending over ports. distrib :: Streams distrib = do -- vars let a = varW8 "a" - let b = varB "b" + 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 + send "portA" (port 2) a + send "portB" (port 1) b -- greatest common divisor. gcd :: Word16 -> Word16 -> Streams gcd n0 n1 = do let a = varW16 "a" - let b = varW16 "b" + b = varW16 "b" a .= alg n0 a b b .= alg n1 b a @@ -148,18 +154,18 @@ -- sample the external variables. gcd' :: Streams gcd' = do - let n = extW16 "n" 1 - let m = extW16 "m" 1 - - let a = varW16 "a" - let b = varW16 "b" - let init = varB "init" + -- externals + let n = extW16 "n" + m = extW16 "m" + -- copilot vars + a = varW16 "a" + b = varW16 "b" + init = varB "init" + ans = varB "ans" + a .= alg n (sub a b) init b .= alg m (sub b a) init - - let ans = varB "ans" ans .= a == b && not init - init .= [True] ++ false where sub hi lo = mux (hi > lo) (hi - lo) hi @@ -189,8 +195,7 @@ y .= cast x + cast x i8 :: Streams -i8 = - let v = varI8 "v" in v .= [0, 1] ++ v + 1 +i8 = let v = varI8 "v" in v .= [0, 1] ++ v + 1 trap :: Streams trap = do @@ -262,7 +267,7 @@ -- f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 let g = varB "g" let gg = extArrW16 "gg" e - g .= gg 1 == gg 2 + g .= gg < 13 -- h .= [0] ++ drop 1 (varW16 g) @@ -270,11 +275,16 @@ t99 :: Streams t99 = do let ext = extW32 "ext" - let a = varW32 "a" - a .= [0,1] ++ a + ext 8 + ext 8 + ext 1 + a = varW32 "a" + a .= [0,1] ++ a + ext + ext + ext let b = varB "b" - b .= [True, False] ++ 2 + a < 5 + ext 1 + b .= [True, False] ++ 2 + a < 5 + ext + +t11 :: Streams +t11 = do + let v = varB "v" + v .= [False, True, False] ++ v -- test external idx before after and in the stream it references -- test multiple defs diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs --- a/Language/Copilot/Examples/LTLExamples.hs +++ b/Language/Copilot/Examples/LTLExamples.hs @@ -72,12 +72,12 @@ testRules :: Streams testRules = do let v1 = varB "v1" - let v2 = varB "v2" - let v3 = varI16 "v3" - let v4 = varB "v4" - let ext = extI8 "ext" 5 + v2 = varB "v2" + v3 = varI16 "v3" + v4 = varB "v4" + ex = extI8 "ex" v1 .= (not true) || v2 - v2 .= [True, False] ++ [True] ++ v3 < cast ext + v2 .= [True, False] ++ [True] ++ v3 < cast ex v3 .= 0 + drop 3 6 v4 `ltl` always 5 v1 diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs --- a/Language/Copilot/Examples/PTLTLExamples.hs +++ b/Language/Copilot/Examples/PTLTLExamples.hs @@ -20,7 +20,7 @@ tprv :: Streams tprv = do let c = varB "c" - let a = varB "a" + a = varB "a" tstdatprv c `ptltl` previous a @@ -33,7 +33,7 @@ tAB :: Streams tAB = do let f = varB "f" - let d = varB "d" + d = varB "d" tstdatAB f `ptltl` alwaysBeen d @@ -46,7 +46,7 @@ tEP :: Streams tEP = do let h = varB "h" - let g = varB "g" + g = varB "g" tstdatEP h `ptltl` eventuallyPrev g @@ -61,7 +61,6 @@ tstdat2Sin :: Streams tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2 - tSince :: Streams tSince = do @@ -73,19 +72,19 @@ -- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 tSinExt :: Streams tSinExt = do - let e1 = extB "e1" 2 - let e2 = extB "e2" 3 + let e1 = extB "e1" + e2 = extB "e2" z `ptltl` (e1 `since` e2) tSinExt2 :: Streams tSinExt2 = do - let e1 = extB "e1" 2 - let e2 = extB "e2" 2 - let a = varB "a" - let s = varB "s" - let d = varB "d" - let t = varB "t" - let e = varB "e" + let e1 = extB "e1" + e2 = extB "e2" + a = varB "a" + s = varB "s" + d = varB "d" + t = varB "t" + e = varB "e" a .= not e1 s `ptltl` (e2 `since` d) @@ -98,15 +97,15 @@ engine :: Streams engine = do -- external vars - let engineTemp = extW8 "engineTemp" 1 - let engineOff = extB "engineOff" 1 - let coolerOn = extB "coolerOn" 1 + let engineTemp = extW8 "engineTemp" + engineOff = extB "engineOff" + coolerOn = extB "coolerOn" -- Copilot vars - let cnt = varW8 "cnt" - let temp = varB "temp" - let cooler = varB "cooler" - let off = varB "off" - let monitor = varB "monitor" + cnt = varW8 "cnt" + temp = varB "temp" + cooler = varB "cooler" + off = varB "off" + monitor = varB "monitor" temp `ptltl` (alwaysBeen (engineTemp > 250)) cnt .= [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt @@ -122,5 +121,6 @@ , ("coolerOn", replicate 9 False P.++ repeat True) ] , w8Map = fromList [("engineTemp", [99,100..])] - }) baseOpts + }) + baseOpts diff --git a/Language/Copilot/Examples/StatExamples.hs b/Language/Copilot/Examples/StatExamples.hs --- a/Language/Copilot/Examples/StatExamples.hs +++ b/Language/Copilot/Examples/StatExamples.hs @@ -10,9 +10,9 @@ t0 :: Streams t0 = do let minV = varW16 "min" - let maxV = varW16 "max" - let sumV = varW16 "sum" - let a = varW16 "a" + maxV = varW16 "max" + sumV = varW16 "sum" + a = varW16 "a" a .= [0..5] ++ a + 6 minV .= min 3 a @@ -22,7 +22,7 @@ tMean :: Streams tMean = do let a = varD "a" - let out = varD "out" + out = varD "out" a .= [0..5] ++ a + 6 out .= mean 4 a diff --git a/Language/Copilot/Help.hs b/Language/Copilot/Help.hs --- a/Language/Copilot/Help.hs +++ b/Language/Copilot/Help.hs @@ -11,20 +11,20 @@ , "There are 4 essential Copilot commands. Each command may take a variety" , "of options. We describe the commands then list the possible options." , "" - , " interpret :: Streams -> Int -> Options -> IO ()" - , " > interpret STREAMS RNDS [$ OPTS] baseOpts" + , " interpret :: Streams -> Int -> (Options -> Options) -> IO ()" + , " > interpret STREAMS RNDS (noOpts | [$ OPTS])" , " Executes the interpreter for the Copilot specification STREAMS of type" , " 'Streams', where the specification is interpreted as a set of mutually-" , " recursive Haskell infinite lists. The output from the lists is given" , " for RNDS indexes. RNDS must be greater than 0." , "" - , " compile :: Streams -> String -> Options -> IO ()" - , " > compile STREAMS FILENAME [$ OPTS] baseOpts" + , " compile :: Streams -> String -> (Options -> Options) -> IO ()" + , " > compile STREAMS FILENAME (noOpts | [$ OPTS])" , " Compiles the Copilot specification STREAMS to constant-time & constant-" , " constant-space C program named FILENAME.c with header FILENAME.h" , " and executable FILENAME." , "" - , " > test RNDS [$ OPTS] baseOpts" + , " > test RNDS (noOpts | [$ OPTS])" , " Generates a random set of streams & inputs for external variables, and" , " tests the equivalence between the output of the compiled C program and" , " the interpreter over RNDS rounds. RNDS must be greater than 0. This" @@ -37,8 +37,8 @@ , " > STREAMS -- in ghci" , " Pretty-prints the parsed Copilot specification of type 'Streams'." , "" - , " verify :: FilePath -> Int -> IO () (FilePath is a synonym for String)" - , " > verify PATH/FILE.c n" + , " verify :: FilePath -> Int -> String -> IO () (FilePath is a synonym for String)" + , " > verify PATH/FILE.c n opts (opts are additional options for cbmc.)" , " Calls cbmc, developed by Daniel Kroening \& Edmund Clarke" , " on a C file generated by Copilot." , " cbmc is a bounded model-checker that verifies C programs. While there" @@ -64,8 +64,7 @@ , "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." + , "For each option, there is a default described below." , "" , " setE :: Vars -> Options -> Options (i)" , " default: Nothing (no assignments)" @@ -139,7 +138,7 @@ , "The following examples reference Copilot specs defined in" , "Language.Copilot.Examples.Examples." , "" - , " > interpret t0 50 baseOpts" + , " > interpret t0 50 noOpts" , " Interprets t0 for 50 iterations." , "" , " > interpret t3 40" @@ -150,23 +149,24 @@ , " Interpret t3 for 40 iterations, seeding the external variable \"ext\"" , " to [0,1,..], with 'Verbose' verbosity." , "" - , " > compile t1 \"t1\" baseOpts" + , " > compile t1 \"t1\" noOpts" , " 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 t2 \"t2\" $ setC \"-O2\" $ setP 100" , " Compile Copilot spec t2 to t2.c, t2.h, and executable t2 in the default" , " directory, /tmp/copilot/ , with optimization level -02 and period 100." , " This is compiled with a simulation main()." , "" - , " > test 1000 baseOpts" + , " > test 1000" , " Compare the compiler and interpreter for a randomly-generated Copilot" , " spec for 1000 iterations." , "" - , " > Prelude.sequence_ [test 100 $ setR x baseOpts | x <- [0..100]]" + , " > Prelude.sequence_ [test 100 $ setR x | 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)." + , " > verify \"foo.c\" n" + , " Calls cbmc on foo.c (where foo.c is in the current directory) and" + , " unrolls the program n times." ] diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs --- a/Language/Copilot/Interface.hs +++ b/Language/Copilot/Interface.hs @@ -1,13 +1,16 @@ +{-# LANGUAGE FlexibleInstances #-} + -- | Used by the end-user to easily give its arguments to dispatch. module Language.Copilot.Interface ( Options(), baseOpts, test, interpret, compile, verify, interface , help , setE, setC, setO, setP, setI, setPP, setN, setV, setR - , setDir, setGCC, setArrs, setClock, + , setDir, setGCC, setArrs, setClock, noOpts, module Language.Copilot.Dispatch ) where import Language.Copilot.Core -import Language.Copilot.Language (opsF, opsF2, opsF3) +--import Language.Copilot.Language (opsF, opsF2, opsF3) +import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3) import Language.Copilot.Tests.Random import Language.Copilot.Dispatch import Language.Copilot.Help @@ -76,6 +79,9 @@ -- Functions for making it easier for configuring copilot in the frequent use cases +noOpts :: Options -> Options +noOpts = id + test :: Int -> Options -> IO () test n opts = interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts @@ -90,8 +96,8 @@ $ setTriggers (getTriggers streams) $ opts {optStreams = Just (getSpecs streams)} -verify :: FilePath -> Int -> IO () -verify file n = do +verify :: FilePath -> Int -> String -> IO () +verify file n opts = do putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke." putStrLn ", with the following checks:" putStrLn " --bounds-check enable array bounds checks" @@ -100,21 +106,17 @@ putStrLn " --overflow-check enable arithmetic over- and underflow checks" putStrLn " --nan-check check floating-point for NaN" putStrLn "" - putStrLn $ " assuming main() as the entry point:" + putStrLn "Assuming main() as the entry point unless specified otherwise (--function f)" 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. See " - putStrLn "for more information on cbmc." + _ -> do putStrLn "" + putStrLn $ "An error was returned by cbmc. This may have be due to cbmc not finding the file " ++ file ++ ". Perhaps cbmc is not installed on your system, is not in your path, cbmc cannot be called from the command line on your system, or " ++ file ++ " does not exist. See for more information on cbmc." where cmd = unwords ("cbmc" : args) args = ["--div-by-zero-check", "--overflow-check", "--bounds-check" , "--nan-check", "--pointer-check" - , "--unwind " ++ show n, file] + , "--unwind " ++ show n, opts, file] -- Small functions for easy modification of the Options record @@ -123,7 +125,7 @@ setS :: StreamableMaps Send -> Options -> Options setS sends opts = opts {optSends = sends} --- | Set the directives for sending stream values on ports. +-- -- | Set the directives for sending stream values on ports. setTriggers :: Triggers -> Options -> Options setTriggers triggers opts = opts {optTriggers = triggers} @@ -194,17 +196,6 @@ -- 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 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 () diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs --- a/Language/Copilot/Interpreter.hs +++ b/Language/Copilot/Interpreter.hs @@ -1,5 +1,8 @@ +{-# LANGUAGE Rank2Types #-} + -- | The Copilot interpreter. -module Language.Copilot.Interpreter(interpretStreams) where +module Language.Copilot.Interpreter + (interpretStreams) where import Language.Copilot.Core @@ -12,14 +15,15 @@ where inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams -interpret :: Streamable a => Vars -> Vars -> Spec a -> [a] +interpret :: forall a. Streamable a => Vars -> Vars -> Spec a -> [a] interpret inVs moVs s = case s of Const c -> repeat c Var v -> getElem v inVs - PVar _ v _ -> getElem v moVs - PArr _ (v,s') _ -> map (\i -> getElem v moVs !! fromIntegral i) - (interpret inVs moVs s') + PVar _ v -> checkV v (\v' -> (getElem v' moVs)) + PArr _ (v,s') -> checkV v (\v' -> map (\i -> getElem v' moVs + !! fromIntegral i) + (interpret inVs moVs s')) Append ls s' -> ls ++ interpret inVs moVs s' Drop i s' -> drop i $ interpret inVs moVs s' F f _ s' -> map f (interpret inVs moVs s') @@ -29,3 +33,12 @@ (interpret inVs moVs s0) (interpret inVs moVs s1) (interpret inVs moVs s2) + where + checkV :: Ext -> (Var -> [a]) -> [a] + checkV v f = + case v of + ExtV v' -> f v' + -- XXX support this? + Fun _ _ -> error $ "Sampling functions is not currently supported" + ++ " in the Copilot interpreter." + diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs --- a/Language/Copilot/Language.hs +++ b/Language/Copilot/Language.hs @@ -1,9 +1,11 @@ -{-# LANGUAGE NoImplicitPrelude, Rank2Types, ScopedTypeVariables, FlexibleContexts #-} +{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} -- | Describes the language /Copilot/. -- --- If you wish to add a new operator, the only modification needed is adding it in this module. --- But if you want it to be used in the random generated streams, add it to either @'opsF'@, @'opsF2'@ or @'opsF3'@ +-- 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, @@ -19,41 +21,41 @@ -- * 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, - extW8, extW16, extW32, extW64, extF, extD, - -- * The next functions provide easier access to typed external arrays. - extArrB, extArrI8, extArrI16, extArrI32, extArrI64, - extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD, - -- * Set of operators from which to choose during the generation of random streams - opsF, opsF2, opsF3, + -- * Copilot constant declarations. For the most part, these are + -- unnecessary, as constants are automatically lifted in into the * + -- Copilot types. They are useful though for specifying triggers and * + -- function samplings. + const, constI8, constI16, constI32, constI64, + constW8, constW16, constW32, constW64, constF, constD, + -- * Boolean stream constants + true, false, + module Language.Copilot.Language.Sampling, -- * Constructs of the copilot language drop, (++), (.=), -- (..|), -- * The next functions help typing the send operations - -- Warning: there is no typechecking of that yet - -- sendB, sendI8, sendI16, sendI32, sendI64, - send, port, -- , sendW16, sendW32, sendW64, sendF, sendD + send, port, -- * Triggers - trigger, void, (<>), (<>>), + module Language.Copilot.Language.FunctionCalls, +-- trigger, (<>), void, -- * Safe casting - cast, - -- * Boolean stream constants - const, true, false + module Language.Copilot.Language.Casting, + notConstVarErr ) where import qualified Language.Atom as A import Data.Int import Data.Word -import System.Random -import qualified Data.Map as M -import Prelude ( Bool(..), Num(..), Float, Double, (.), String, error, ($) - , Fractional(..), fromInteger, zip, Show(..)) +import Prelude ( Bool(..), Num(..), Float, Double, String, ($), error + , Fractional(..), fromInteger, Show(..)) import qualified Prelude as P import Control.Monad.Writer (tell) +import qualified Data.Map as M import Language.Copilot.Core -import Language.Copilot.Analyser -import Language.Copilot.Tests.Random +import Language.Copilot.Language.Sampling +import Language.Copilot.Language.Casting +import Language.Copilot.Language.FunctionCalls +--import Language.Copilot.Language.RandomOps ---- Operators and functions --------------------------------------------------- @@ -99,95 +101,6 @@ (\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x)) (==>) = F2 (\ x y -> y P.|| P.not x) A.imply --- | Cast 'a' into 'b'. We only allow "safe casts" to larger types. -class Streamable a => Castable a where - castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b - cast :: (Castable b, Streamable b) => Spec b -> Spec a - -castErr :: String -> A.Type -> String -castErr toT fromT = "Error: cannot cast type " P.++ show fromT - P.++ " into " P.++ toT P.++ ". Only casts guarnateed \n" - P.++ "not to change sign and to larger types are allowed." - -instance Castable Bool where - castFrom = F (\b -> if b then 1 else 0) - (\b -> A.mux b 1 0) - cast x = error $ castErr "Bool" (getAtomType x) - -instance Castable Word8 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - t -> error $ castErr "Word8" t - -instance Castable Word16 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - t -> error $ castErr "Word16" t - -instance Castable Word32 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - t -> error $ castErr "Word32" t - -instance Castable Word64 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - A.Word32 -> castFrom x - t -> error $ castErr "Word64" t - -instance Castable Int8 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - t -> error $ castErr "Int8" t - -instance Castable Int16 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Word8 -> castFrom x - t -> error $ castErr "Int16" t - -instance Castable Int32 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Int16 -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - t -> error $ castErr "Int32" t - -instance Castable Int64 where - castFrom = F (P.fromInteger . P.toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Int16 -> castFrom x - A.Int32 -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - A.Word32 -> castFrom x - t -> error $ castErr "Int64" t - -- | 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 @@ -196,244 +109,6 @@ infixr 4 ||, &&, ^, ==> --- Used for easily producing, and coercing PVars - --- for variables -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 - --- for arrays -extArrB :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Bool -extArrB = \v idx ph -> PArr A.Bool (v, idx) ph -extArrI8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int8 -extArrI8 = \v idx ph -> PArr A.Int8 (v, idx) ph -extArrI16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int16 -extArrI16 = \v idx ph -> PArr A.Int16 (v, idx) ph -extArrI32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int32 -extArrI32 = \v idx ph -> PArr A.Int32 (v, idx) ph -extArrI64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Int64 -extArrI64 = \v idx ph -> PArr A.Int64 (v, idx) ph -extArrW8 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word8 -extArrW8 = \v idx ph -> PArr A.Word8 (v, idx) ph -extArrW16 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word16 -extArrW16 = \v idx ph -> PArr A.Word16 (v, idx) ph -extArrW32 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word32 -extArrW32 = \v idx ph -> PArr A.Word32 (v, idx) ph -extArrW64 :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Word64 -extArrW64 = \v idx ph -> PArr A.Word64 (v, idx) ph -extArrF :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Float -extArrF = \v idx ph -> PArr A.Float (v, idx) ph -extArrD :: (Streamable a, A.IntegralE a) => Var -> Spec a -> Phase -> Spec Double -extArrD = \v idx ph -> PArr A.Double (v, idx) ph - - ----- Sets of operators for Tests.Random.hs ------------------------------------- - ----- 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 ------------------------------------------------ @@ -470,57 +145,56 @@ -- | 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) + case v of + (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM) + emptySM + M.empty + _ -> error $ "Given spec " P.++ show v + P.++ " but expected a variable in a Copilot definition (.=)." 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 = +-- | Takes a function @name@, a port @number@, and a Copilot variable @v@ 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. +send :: Streamable a => String -> Port -> Spec a -> Streams +send portName thePort s = 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 + where sending = case s of + v@(Var _) -> Send v thePort portName + _ -> error $ "Expected a Copilot variable but given " + P.++ show s P.++ " instead." -- | Coerces a type that is 'Streamable' into a Copilot constant. const :: Streamable a => a -> Spec a const = Const +constI8 :: Int8 -> Spec Int8 +constI8 = Const +constI16 :: Int16 -> Spec Int16 +constI16 = Const +constI32 :: Int32 -> Spec Int32 +constI32 = Const +constI64 :: Int64 -> Spec Int64 +constI64 = Const +constW8 :: Word8 -> Spec Word8 +constW8 = Const +constW16 :: Word16 -> Spec Word16 +constW16 = Const +constW32 :: Word32 -> Spec Word32 +constW32 = Const +constW64 :: Word64 -> Spec Word64 +constW64 = Const +constF :: Float -> Spec Float +constF = Const +constD :: Double -> Spec Double +constD = Const + + true, false :: Spec Bool true = Const True false = Const False @@ -536,7 +210,6 @@ infixr 3 ++ infixr 2 .= -infixr 1 <> ---- Optimisation rules -------------------------------------------------------- @@ -568,5 +241,4 @@ "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) - +-- "Copilot.Core CastLift" forall s i. drop i (cast s) = cast (drop i s) diff --git a/Language/Copilot/Language/Casting.hs b/Language/Copilot/Language/Casting.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Language/Casting.hs @@ -0,0 +1,99 @@ +-- | Safe casting of values. + +module Language.Copilot.Language.Casting ( cast ) where + +import qualified Language.Atom as A + +import Data.Int +import Data.Word + +import Language.Copilot.Core + +-- | Cast 'a' into 'b'. We only allow "safe casts" to larger types. +class Streamable a => Castable a where + castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b + cast :: (Castable b, Streamable b) => Spec b -> Spec a + +castErr :: String -> A.Type -> String +castErr toT fromT = "Error: cannot cast type " ++ show fromT + ++ " into " ++ toT ++ ". Only casts guarnateed \n" + ++ "not to change sign and to larger types are allowed." + +instance Castable Bool where + castFrom = F (\b -> if b then 1 else 0) + (\b -> A.mux b 1 0) + cast x = error $ castErr "Bool" (getAtomType x) + +instance Castable Word8 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + t -> error $ castErr "Word8" t + +instance Castable Word16 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Word8 -> castFrom x + t -> error $ castErr "Word16" t + +instance Castable Word32 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Word8 -> castFrom x + A.Word16 -> castFrom x + t -> error $ castErr "Word32" t + +instance Castable Word64 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Word8 -> castFrom x + A.Word16 -> castFrom x + A.Word32 -> castFrom x + t -> error $ castErr "Word64" t + +instance Castable Int8 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + t -> error $ castErr "Int8" t + +instance Castable Int16 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Int8 -> castFrom x + A.Word8 -> castFrom x + t -> error $ castErr "Int16" t + +instance Castable Int32 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Int8 -> castFrom x + A.Int16 -> castFrom x + A.Word8 -> castFrom x + A.Word16 -> castFrom x + t -> error $ castErr "Int32" t + +instance Castable Int64 where + castFrom = F (fromInteger . toInteger) + (A.Retype . A.ue) + cast x = case getAtomType x of + A.Bool -> castFrom x + A.Int8 -> castFrom x + A.Int16 -> castFrom x + A.Int32 -> castFrom x + A.Word8 -> castFrom x + A.Word16 -> castFrom x + A.Word32 -> castFrom x + t -> error $ castErr "Int64" t diff --git a/Language/Copilot/Language/FunctionCalls.hs b/Language/Copilot/Language/FunctionCalls.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Language/FunctionCalls.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE TypeSynonymInstances #-} + +module Language.Copilot.Language.FunctionCalls + ((<>), trigger, void, fun) where + +import Language.Copilot.Core + +import Control.Monad.Writer (tell) +import qualified Data.Map as M + +-- | No C arguments +void :: Args +void = [] + +class ArgCl a where + (<>) :: Streamable b => Spec b -> a -> Args + trigger :: Spec Bool -> String -> a -> Streams + fun :: String -> a -> Ext + +instance ArgCl Args where + s <> args = argUpdate s args + trigger v fnName args = trigger' v fnName args + fun = Fun + +instance Streamable b => ArgCl (Spec b) where + s <> s' = (argUpdate s (argUpdate s' [])) + trigger v fnName arg = + let arg' = argUpdate arg [] in + trigger' v fnName arg' + fun f arg = + let arg' = argUpdate arg [] in + Fun f arg' + +infixr 1 <> + +-- | XXX document +trigger' :: Spec Bool -> String -> Args -> Streams +trigger' v fnName args = + tell $ LangElems + emptySM + emptySM + (M.insert (show trig) trig M.empty) + where trig = Trigger v fnName args + +argUpdate :: Streamable a => Spec a -> Args -> Args +argUpdate s args = notConstVarErr s (\v -> v:args) + diff --git a/Language/Copilot/Language/RandomOps.hs b/Language/Copilot/Language/RandomOps.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Language/RandomOps.hs @@ -0,0 +1,206 @@ +{-# LANGUAGE Rank2Types, ScopedTypeVariables #-} + +-- | Sets of operators for Tests.Random.hs + +module Language.Copilot.Language.RandomOps ( +-- mkOp, mkOp2, mkOp3, mkOp2Coerce, mkOp2Ord, mkOp2Eq, + opsF, opsF2, opsF3, + module Language.Copilot.Tests.Random + ) where + +import qualified Language.Atom as A + +import Prelude (($), Float, Double, error, zip, asTypeOf) +import Data.Int +import Data.Word +import System.Random +import Data.Map as M + +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Analyser +import Language.Copilot.Tests.Random + +mkOp :: (Random arg1, Streamable arg1) => + (Spec arg1 -> Spec r) -> Operator r +mkOp op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet in + (op s0, g0) + ) + +mkOp2 :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) => + (Spec arg1 -> Spec arg2 -> Spec r) -> Operator r +mkOp2 op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet in + (op s0 s1, g1) + ) + +mkOp3 :: (Random arg1, Random arg2, Random arg3, + Streamable arg1, Streamable arg2, Streamable arg3) => + (Spec arg1 -> Spec arg2 -> Spec arg3 -> Spec r) -> Operator r +mkOp3 op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet + (s2, g2) = rand g1 FunSpecSet in + (op s0 s1 s2, g2) + ) + +mkOp2Coerce :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) => + (Spec arg1 -> Spec arg2 -> Spec r) -> arg1 -> arg2 -> Operator r +mkOp2Coerce op c0 c1 = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet in + (op (s0 `asTypeOf` (Const c0)) (s1 `asTypeOf` (Const c1)), g1) + ) + +mkOp2Ord :: forall r. + (forall arg. (Random arg, A.OrdE arg, Streamable arg) + => (Spec arg -> Spec arg -> Spec r)) -> Operator r +mkOp2Ord op = + let opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g + => (forall a' g'. (Streamable a', Random a', RandomGen g') + => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g) + opI8 = fromOp $ mkOp2Coerce op (unit::Int8) (unit::Int8) + opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16) + opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32) + opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64) + opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8) + opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16) + opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32) + opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64) + opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float) + opD = fromOp $ mkOp2Coerce op (unit::Double) (unit::Double) in + Operator (\ rand g -> + let (t, g0) = randomR (A.Int8, A.Double) g in + case t of + A.Int8 -> opI8 rand g0 + A.Int16 -> opI16 rand g0 + A.Int32 -> opI32 rand g0 + A.Int64 -> opI64 rand g0 + A.Word8 -> opW8 rand g0 + A.Word16 -> opW16 rand g0 + A.Word32 -> opW32 rand g0 + A.Word64 -> opW64 rand g0 + A.Float -> opF rand g0 + A.Double -> opD rand g0 + _ -> error "Impossible" + ) + +mkOp2Eq :: forall r. (forall arg. + (Random arg, A.EqE arg, Streamable arg) => + (Spec arg -> Spec arg -> Spec r)) + -> Operator r +mkOp2Eq op = + let opB, opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => + g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g) + opB = fromOp $ mkOp2Coerce op (unit::Bool) (unit::Bool) + opI8 = fromOp $ mkOp2Coerce op (unit::Int8) (unit::Int8) + opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16) + opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32) + opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64) + opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8) + opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16) + opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32) + opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64) + opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float) + opD = fromOp $ mkOp2Coerce op (unit::Double) (unit::Double) in + Operator (\ rand g -> + let (t, g0) = random g in + case t of + A.Bool -> opB rand g0 + A.Int8 -> opI8 rand g0 + A.Int16 -> opI16 rand g0 + A.Int32 -> opI32 rand g0 + A.Int64 -> opI64 rand g0 + A.Word8 -> opW8 rand g0 + A.Word16 -> opW16 rand g0 + A.Word32 -> opW32 rand g0 + A.Word64 -> opW64 rand g0 + A.Float -> opF rand g0 + A.Double -> opD rand g0 + ) + +---- Definition of each operator + +not_ :: Operator Bool +not_ = mkOp not + +(+$), (-$), (*$) :: (Streamable a, A.NumE a, Random a) => Operator a +(+$) = mkOp2 (+) +(-$) = mkOp2 (-) +(*$) = mkOp2 (*) + +(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a +(/$) = mkOp2 (/) + +(<$), (<=$), (>=$), (>$) :: Operator Bool +(<$) = mkOp2Ord (<) +(<=$) = mkOp2Ord (<=) +(>=$) = mkOp2Ord (>=) +(>$) = mkOp2Ord (>) + +(==$), (/=$) :: Operator Bool +(==$) = mkOp2Eq (==) +(/=$) = mkOp2Eq (/=) + +(||$), (&&$), (^$), (==>$) :: Operator Bool +(||$) = mkOp2 (||) +(&&$) = mkOp2 (&&) +(^$) = mkOp2 (^) +(==>$) = mkOp2 (==>) + +mux_ :: (Streamable a, Random a) => Operator a +mux_ = mkOp3 mux + +-- Packing of the operators in StreamableMaps + +createMapFromElems :: [val] -> M.Map Var val +createMapFromElems vals = + let ks = [[x] | x <- ['a'..]] + l = zip ks vals in + M.fromAscList l + +-- | opsF, opsF2 and opsF3 are fed to Tests.Random.randomStreams. They allows +-- the random generated streams to include lots of operators. If you add a new +-- operator to Copilot, it would be nice to add it to one of those, that way it +-- could be used in the random streams used for testing. opsF holds all the +-- operators of arity 1, opsF2 of arity 2 and opsF3 of arity3 They are +-- StreamableMaps, because operators are sorted based on their return type. +opsF, opsF2, opsF3 :: Operators +opsF = emptySM {bMap = createMapFromElems [not_]} + +opsF2 = emptySM { + bMap = createMapFromElems [(<$), (<=$), (>=$), (>$), (==$), (/=$), (||$), (&&$), (^$), (==>$)], + i8Map = createMapFromElems [(+$), (-$), (*$)], + i16Map = createMapFromElems [(+$), (-$), (*$)], + i32Map = createMapFromElems [(+$), (-$), (*$)], + i64Map = createMapFromElems [(+$), (-$), (*$)], + w8Map = createMapFromElems [(+$), (-$), (*$)], + w16Map = createMapFromElems [(+$), (-$), (*$)], + w32Map = createMapFromElems [(+$), (-$), (*$)], + w64Map = createMapFromElems [(+$), (-$), (*$)], + fMap = createMapFromElems [(+$), (-$), (*$), (/$)], + dMap = createMapFromElems [(+$), (-$), (*$), (/$)] + } + +opsF3 = emptySM { + bMap = createMapFromElems [mux_], + i8Map = createMapFromElems [mux_], + i16Map = createMapFromElems [mux_], + i32Map = createMapFromElems [mux_], + i64Map = createMapFromElems [mux_], + w8Map = createMapFromElems [mux_], + w16Map = createMapFromElems [mux_], + w32Map = createMapFromElems [mux_], + w64Map = createMapFromElems [mux_], + fMap = createMapFromElems [mux_], + dMap = createMapFromElems [mux_] + } diff --git a/Language/Copilot/Language/Sampling.hs b/Language/Copilot/Language/Sampling.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Language/Sampling.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE TypeSynonymInstances #-} + +-- | Functions for sampling external variables. + +module Language.Copilot.Language.Sampling ( + -- * The next functions provide easier access to typed external variables. + extB, extI8, extI16, extI32, extI64, + extW8, extW16, extW32, extW64, extF, extD, + -- * The next functions provide easier access to typed external arrays. + extArrB, extArrI8, extArrI16, extArrI32, extArrI64, + extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD, + ) where + + +import qualified Language.Atom as A +import Data.Int +import Data.Word + +import Language.Copilot.Core + +class ExtCl a where + extB :: a -> Spec Bool + extI8 :: a -> Spec Int8 + extI16 :: a -> Spec Int16 + extI32 :: a -> Spec Int32 + extI64 :: a -> Spec Int64 + extW8 :: a -> Spec Word8 + extW16 :: a -> Spec Word16 + extW32 :: a -> Spec Word32 + extW64 :: a -> Spec Word64 + extF :: a -> Spec Float + extD :: a -> Spec Double + + -- for arrays + extArrB :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Bool + extArrI8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int8 + extArrI16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int16 + extArrI32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int32 + extArrI64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int64 + extArrW8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word8 + extArrW16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word16 + extArrW32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word32 + extArrW64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word64 + extArrF :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Float + extArrD :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Double + +-- | For global variables. +instance ExtCl String where + extB var = PVar A.Bool (ExtV var) + extI8 var = PVar A.Int8 (ExtV var) + extI16 var = PVar A.Int16 (ExtV var) + extI32 var = PVar A.Int32 (ExtV var) + extI64 var = PVar A.Int64 (ExtV var) + extW8 var = PVar A.Word8 (ExtV var) + extW16 var = PVar A.Word16 (ExtV var) + extW32 var = PVar A.Word32 (ExtV var) + extW64 var = PVar A.Word64 (ExtV var) + extF var = PVar A.Float (ExtV var) + extD var = PVar A.Double (ExtV var) + + -- for arrays + extArrB = \v idx -> PArr A.Bool (ExtV v, idx) + extArrI8 = \v idx -> PArr A.Int8 (ExtV v, idx) + extArrI16 = \v idx -> PArr A.Int16 (ExtV v, idx) + extArrI32 = \v idx -> PArr A.Int32 (ExtV v, idx) + extArrI64 = \v idx -> PArr A.Int64 (ExtV v, idx) + extArrW8 = \v idx -> PArr A.Word8 (ExtV v, idx) + extArrW16 = \v idx -> PArr A.Word16 (ExtV v, idx) + extArrW32 = \v idx -> PArr A.Word32 (ExtV v, idx) + extArrW64 = \v idx -> PArr A.Word64 (ExtV v, idx) + extArrF = \v idx -> PArr A.Float (ExtV v, idx) + extArrD = \v idx -> PArr A.Double (ExtV v, idx) + +-- | For functions. +instance ExtCl Ext where + extB = PVar A.Bool + extI8 = PVar A.Int8 + extI16 = PVar A.Int16 + extI32 = PVar A.Int32 + extI64 = PVar A.Int64 + extW8 = PVar A.Word8 + extW16 = PVar A.Word16 + extW32 = PVar A.Word32 + extW64 = PVar A.Word64 + extF = PVar A.Float + extD = PVar A.Double + -- for arrays + extArrB = \fn idx -> PArr A.Bool (fn, idx) + extArrI8 = \fn idx -> PArr A.Int8 (fn, idx) + extArrI16 = \fn idx -> PArr A.Int16 (fn, idx) + extArrI32 = \fn idx -> PArr A.Int32 (fn, idx) + extArrI64 = \fn idx -> PArr A.Int64 (fn, idx) + extArrW8 = \fn idx -> PArr A.Word8 (fn, idx) + extArrW16 = \fn idx -> PArr A.Word16 (fn, idx) + extArrW32 = \fn idx -> PArr A.Word32 (fn, idx) + extArrW64 = \fn idx -> PArr A.Word64 (fn, idx) + extArrF = \fn idx -> PArr A.Float (fn, idx) + extArrD = \fn idx -> PArr A.Double (fn, idx) + diff --git a/Language/Copilot/Tests/Random.hs b/Language/Copilot/Tests/Random.hs --- a/Language/Copilot/Tests/Random.hs +++ b/Language/Copilot/Tests/Random.hs @@ -3,7 +3,8 @@ -- | Generate random specs for testing. We do not generate external array indexes. -module Language.Copilot.Tests.Random (randomStreams, Operator(..), Operators, fromOp) where +module Language.Copilot.Tests.Random + (randomStreams, Operator(..), Operators, fromOp) where import Language.Copilot.Core import Language.Copilot.Analyser @@ -19,9 +20,9 @@ ---- Parameters of the random generation --------------------------------------- -maxDrop, maxSamplePhase :: Int +maxDrop :: Int maxDrop = 4 -- The maximum value for i in Drop i _ -maxSamplePhase = 8 -- The maximum value for ph in PVar _ _ ph +-- 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 @@ -233,8 +234,9 @@ 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 :: 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 @@ -246,8 +248,8 @@ 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) +-- let (ph, g2) = randomR (1, maxSamplePhase) g1 in + (PVar (atomType (unit::a)) (ExtV v), g1) (Nothing, g1) -> randomSpec' g1 set 1 -> -- Var case getVar g0 vs of diff --git a/README b/README --- a/README +++ b/README @@ -43,6 +43,17 @@ ******************************************************************************* Release notes ******************************************************************************* + +* Copilot-1.0 + * Language frozen. + * Added sampling functions and returning arrays. + +* Copilot-0.29 + + * Refactor Language.hs into submodules. + * Removed the notion of phases from sampling. That is a compiler-level + concern. + * Copilot-0.28 * Make triggers part of the Copilot language (see example t5 in Examples.hs). diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 0.28 +version: 1.0 cabal-version: >= 1.2 license: BSD3 license-file: LICENSE @@ -32,7 +32,7 @@ extra-source-files: README library - ghc-options: -Wall + ghc-options: -Wall -- These build depends represent my current system. This will probably -- build on packages outside these constaints. build-depends: @@ -50,6 +50,10 @@ Language.Copilot.AdHocC Language.Copilot.Core Language.Copilot.Language + Language.Copilot.Language.Sampling + Language.Copilot.Language.FunctionCalls + Language.Copilot.Language.RandomOps + Language.Copilot.Language.Casting Language.Copilot.AtomToC Language.Copilot.Compiler Language.Copilot.Interpreter