Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge branch 'development' of github.com:leepike/Copilot into develop…

…ment
  • Loading branch information...
commit 98504dac976b7098c06034b3b583acc635037ec0 2 parents ef88edc + edff052
@leepike authored
View
14 Language/Copilot/AdHocC.hs
@@ -6,18 +6,18 @@ module Language.Copilot.AdHocC (
, includeBracket, includeQuote, printf, printfNewline
) where
-import Data.List (intersperse)
+import Data.List (intersperse)
import Language.Atom (Type(..))
import Language.Atom.Code (cType) -- C99
-- | Takes a type and a list of variable names and declares them.
varDecl :: Type -> [String] -> String
-varDecl t vars =
+varDecl t vars =
cType t ++ " " ++ unwords (intersperse "," vars) ++ ";"
-- | Takes a type and a list of array names and their sizes declares them.
arrDecl :: Type -> [(String, Int)] -> String
-arrDecl t arrs =
+arrDecl t arrs =
cType t ++ " " ++ unwords (intersperse "," mkArrs) ++ ";"
where mkArrs = map (\(a,size) -> a ++ "[" ++ show size ++ "]") arrs
@@ -29,10 +29,10 @@ varInit t var val = cType t ++ " " ++ var ++ " = " ++ show val ++ ";"
-- | Takes a type and an array and initializes it. It is YOUR responsibility to
-- ensure that @vals@ is of type @t@.
arrayInit :: Show a => Type -> String -> [a] -> String
-arrayInit t var vals =
+arrayInit t var vals =
cType t ++ " " ++ var ++ "[" ++ show (length vals)
++ "] = " ++ bracesListShow ++ ";"
- where
+ where
-- Show a list with braces {} rather than brackets [].
bracesListShow :: String
bracesListShow =
@@ -59,8 +59,8 @@ printfPre :: String -> String
printfPre = ("printf(\"" ++)
printfPost :: [String] -> String
-printfPost vars =
- let sep = if null vars then " " else ", "
+printfPost vars =
+ let sep = if null vars then " " else ", "
in "\"" ++ sep ++ unwords (intersperse "," vars) ++ ");"
newline :: String
View
8 Language/Copilot/Analyser.hs
@@ -310,8 +310,9 @@ checkInitsArgs streams =
(_, Fun _ args, _) ->
mapMaybe (\arg ->
case arg of
- C _ -> Nothing
V v0 -> Just v0
+ C _ -> Nothing
+ S _ -> Nothing
) args
(_, ExtV _, _) -> [])
(getExternalVars streams)
@@ -320,7 +321,9 @@ checkInitsArgs streams =
(_,_,ExtRetA idx) ->
case idx of
V v' -> Just v'
- C _ -> Nothing)
+ C _ -> Nothing
+ S _ -> Nothing
+ )
(getExternalVars streams)
in foldStreamableMaps checkInits streams Nothing
@@ -412,7 +415,6 @@ checkVarName varName =
let checkVarName' = nondigit
>> many ( nondigit <|> digit )
>> eof
- >> return ()
nondigit = char '_' <|> letter
in
case parse checkVarName' varName varName of
View
98 Language/Copilot/AtomToC.hs
@@ -1,49 +1,70 @@
{-# LANGUAGE ScopedTypeVariables #-}
-- | Defines a main() and print statements to easily execute generated Copilot specs.
-module Language.Copilot.AtomToC(getPrePostCode) where
+module Language.Copilot.AtomToC(getPrePostCode, preHCode, AtomToC(..)) where
import Language.Copilot.AdHocC
import Language.Copilot.Core
-import Language.Atom (Type(Bool))
+import Language.Atom (Type(Bool), Clock)
import Data.Maybe (fromMaybe)
import Data.List
+-- | Datatype corresponding to the 'Options' datatype in 'Interface.hs', but
+-- only including the compilation-relevant fields.
+data AtomToC = AtomToC
+ { cName :: Name -- ^ Name of the C file to generate
+ , gccOpts :: String -- ^ Options to pass to the compiler
+ , getPeriod :: Maybe Period -- ^ The optional period
+ , outputDir :: String -- ^ Where to put the executable
+ , compiler :: String -- ^ Which compiler to use
+ , randomProg :: Bool -- ^ Was the program randomly generated?
+ , sim :: Bool -- ^ Are we running a C simulator?
+ , prePostCode :: (Maybe String, Maybe String) -- ^ Code to replace the default
+ -- initialization and main
+ , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we
+ -- don't know how large external arrays are, so
+ -- we cannot declare them. Passing in pairs
+ -- containing the name of the array and it's
+ -- size allows them to be declared.
+ , clock :: Maybe Clock -- ^ Use the hardware clock to drive the timing
+ -- of the program.
+ }
+
-- allExts represents all the variables to monitor (used for declaring them)
-- inputExts represents the monitored variables which are to be fed to the
-- standard input of the C program. only used for the testing with random
-- streams and values.
-getPrePostCode :: Bool -> (Maybe String, Maybe String) -> Name
- -> StreamableMaps Spec -> [Exs] -> [(Ext,Int)] -> SimValues
+getPrePostCode :: Bool -> (Maybe String, Maybe String) -> Name
+ -> StreamableMaps Spec -> [Exs] -> [(Ext,Int)] -> SimValues
-> Period -> (String, String)
-getPrePostCode simulatation (pre, post) cName streams allExts
- arrDecs inputExts p =
- ( (if simulatation then preCode (extDecls allExts arrDecs)
+getPrePostCode simulatation (pre, post) cname streams allExts
+ arrdecs inputExts p =
+ ( (if simulatation then preCode (extDecls allExts arrdecs)
else "") ++ fromMaybe "" pre
- , fromMaybe "" post ++ periodLoop cName p
- ++ if simulatation then (postCode cName streams inputExts)
+ , fromMaybe "" post ++ periodLoop cname p
+ ++ if simulatation then (postCode cname streams inputExts)
else ""
)
-- Make the declarations for external vars
extDecls :: [Exs] -> [(Ext,Int)] -> [String]
-extDecls allExtVars arrDecs =
- let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y')
- allExtVars
+extDecls allExtVars arrdecs =
+ let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y')
+ allExtVars
getDec :: Exs -> String
getDec (t, (ExtV v), ExtRetV) = varDecl t [v]
getDec (_, (Fun _ _), ExtRetV) = ""
- getDec (t, arr, ExtRetA _) =
- case getIdx arr of
+ getDec (t, arr, ExtRetA _) =
+ case getIdx arr of
Nothing -> error $ "Please use the setArrs option to provide a list of " ++
"pairs (a,idx) where a is the name of an external array and idx " ++
"is its static size to declare. There is no size for array " ++
show arr ++ "."
- Just idx -> arrDecl t [(show arr, idx)]
- getIdx arr = lookup arr arrDecs
- in
+ Just idx -> arrDecl t [(show arr, idx)]
+ getIdx arr = lookup arr arrdecs
+ in
map getDec uniqueExtVars
preCode :: [String] -> String
@@ -57,23 +78,28 @@ preCode extDeclarations = unlines $
]
++ extDeclarations
--- | Generate a temporary C file name.
+-- | Export the period loop function in the header file
+preHCode :: String -> String
+preHCode cname =
+ "void " ++ tmpCFileName cname ++ " ();\n"
+
+-- | Generate a temporary C file name.
tmpCFileName :: String -> String
tmpCFileName name = "__" ++ name
periodLoop :: Name -> Period -> String
-periodLoop cName p = unlines
+periodLoop cname p = unlines
[ "\n"
- , "void " ++ tmpCFileName cName ++ "(void) {"
+ , "void " ++ tmpCFileName cname ++ "(void) {"
, " int i;"
, " for(i = 0; i < " ++ show p ++ "; i++) {"
- , " " ++ cName ++ "();"
+ , " " ++ cname ++ "();"
, " }"
, "}"
]
postCode :: Name -> StreamableMaps Spec -> SimValues -> String
-postCode cName streams inputExts =
+postCode cname streams inputExts =
unlines $
[""] ++
-- (if isEmptySM inputExts
@@ -82,7 +108,7 @@ postCode cName streams inputExts =
-- make a loop to complete a period of computation.
[ "int main(int argc, char *argv[]) {"
, " if (argc != 2) {"
- , " " ++ printfNewline
+ , " " ++ printfNewline
( "Please pass a single argument to the simulator"
++ " containing the number of rounds to execute it.")
[]
@@ -95,9 +121,9 @@ postCode cName streams inputExts =
, " " ++ printf "period: %i " ["i"]
]
++ inputExtVars inputExts " "
- ++ [" " ++ tmpCFileName cName ++ "();"]
- ++ outputVars cName streams
- ++
+ ++ [" " ++ tmpCFileName cname ++ "();"]
+ ++ outputVars cname streams
+ ++
[ " }"
, " //Important to let the Haskell program know we're done with stdout."
, " " ++ printfNewline "" []
@@ -112,30 +138,30 @@ inputExtVars exts indent =
where
decl :: Streamable a => Var -> [a] -> [String] -> [String]
decl v l ls =
- let spec = if null l then error "Impossible error in inputExtVars"
+ let spec = if null l then error "Impossible error in inputExtVars"
else head l
- (frmt, mMacro) = scnId spec
+ (frmt, mMacro) = scnId spec
aBool = atomType spec == Bool
mTmp = if aBool then "__tmpCopilotBool_" ++ v else v
- scan = indent ++ "scanf(" ++ "\"" ++ frmt ++ "\"" ++ mMacro
+ scan = indent ++ "scanf(" ++ "\"" ++ frmt ++ "\"" ++ mMacro
++ ", " ++ "&" ++ mTmp ++ ");" in
- (if aBool
+ (if aBool
then indent ++"//We can't scanf directly into a Bool, "
- ++ "so we get an int then cast.\n"
+ ++ "so we get an int then cast.\n"
++ (indent ++ "int " ++ mTmp ++ ";\n")
++ scan ++ "\n"
++ indent ++ v ++ " = (bool) " ++ mTmp ++ ";"
-
+
else scan) : ls
-- | Print the Copilot stream values to standard out.
outputVars :: Name -> StreamableMaps Spec -> [String]
-outputVars cName streams =
+outputVars cname streams =
foldStreamableMaps decl streams []
where
decl :: forall a. Streamable a => Var -> Spec a -> [String] -> [String]
decl v _ ls =
- let (frmt, mMacro) = prtIdPrec (unit::a)
- prtf = printf (v ++ ": " ++ frmt ++ "\" " ++ mMacro ++ "\" ")
- [vPre cName ++ v] in
+ let (frmt, mMacro) = prtIdPrec (unit::a)
+ prtf = printf (v ++ ": " ++ frmt ++ "\" " ++ mMacro ++ "\" ")
+ [vPre cname ++ v] in
(" " ++ prtf) : ls
View
184 Language/Copilot/Core.hs
@@ -1,20 +1,20 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts,
+{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts,
FlexibleInstances, TypeSynonymInstances #-}
-- | Provides basic types and functions for other parts of /Copilot/.
--
-- If you wish to add a new type, you need to make it an instance of @'Streamable'@,
--- to add it to @'foldStreamableMaps'@, @'mapStreamableMaps'@, and optionnaly
+-- to add it to @'foldStreamableMaps'@, @'mapStreamableMaps'@, and optionnaly
-- to add an ext[Type], a [type] and a var[Type]
--- functions in Language.hs to make it easier to use.
+-- functions in Language.hs to make it easier to use.
module Language.Copilot.Core (
Period, Var, Name, Port(..), Ext(..),
Exs, ExtRet(..), Args, ArgConstVar(..),
- Spec(..), Streams, Stream,
+ Spec(..), Streams, Stream,
Trigger(..), Triggers, LangElems(..),
Streamable(..), StreamableMaps(..), emptySM,
- isEmptySM, getMaybeElem, getElem,
- foldStreamableMaps,
+ isEmptySM, getMaybeElem, getElem,
+ foldStreamableMaps,
mapStreamableMaps, mapStreamableMapsM,
filterStreamableMaps, normalizeVar, getVars, SimValues,
getAtomType, getSpecs, getTriggers, vPre, funcShow,
@@ -25,6 +25,7 @@ import qualified Language.Atom as A
import Data.Int
import Data.Word
+import Data.Char
import Data.List hiding (union)
import qualified Data.Map as M
import Text.Printf
@@ -50,33 +51,36 @@ data Spec a where
Const :: Streamable a => a -> Spec a
ExtVar :: Streamable a => A.Type -> Ext -> Spec a
- ExtArr :: (Streamable a, Streamable b, A.IntegralE b)
+ ExtArr :: (Streamable a, Streamable b, A.IntegralE b)
=> A.Type -> (Ext, Spec b) -> Spec a
- F :: (Streamable a, Streamable b)
+ F :: (Streamable a, Streamable b)
=> (b -> a) -> (A.E b -> A.E a) -> Spec b -> Spec a
- F2 :: (Streamable a, Streamable b, Streamable c)
- => (b -> c -> a) -> (A.E b -> A.E c -> A.E a)
+ F2 :: (Streamable a, Streamable b, Streamable c)
+ => (b -> c -> a) -> (A.E b -> A.E c -> A.E a)
-> Spec b -> Spec c -> Spec a
- F3 :: (Streamable a, Streamable b, Streamable c, Streamable d)
- => (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a)
+ F3 :: (Streamable a, Streamable b, Streamable c, Streamable d)
+ => (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a)
-> Spec b -> Spec c -> Spec d -> Spec a
Append :: Streamable a => [a] -> Spec a -> Spec a
Drop :: Streamable a => Int -> Spec a -> Spec a
--- | Arguments to be passed to a C function. Either a Copilot variable or a
--- constant. A little hacky that I store constants as strings so we don't have
--- to pass around types. However, these data are just used to make external C
--- calls, for which we have no type info anyway, so it's a bit of a moot point.
+-- | Arguments to be passed to a C function. Either a Copilot variable, a
+-- constant or a string for messages. 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
+ | S String
deriving Eq
-instance Show ArgConstVar where
+instance Show ArgConstVar where
show args = case args of
V v -> normalizeVar v
C c -> "_const_" ++ c ++ "_"
+ S s -> "_string_const_" ++ normalizeVar' s
type Args = [ArgConstVar]
@@ -87,17 +91,17 @@ data Trigger =
-- 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}
+ , trigArgs :: Args}
type Triggers = M.Map String Trigger
-instance Show Trigger where
+instance Show Trigger where
show (Trigger s fnName args) =
"trigger_" ++ notConstVarErr s show ++ "_" ++ fnName ++ "_" ++ normalizeVar (show args)
-- getMaybeVar :: Streamable a => Spec a -> Var
-- getMaybeVar (Var v) = v
- -- getMaybeVar s =
+ -- getMaybeVar s =
-- error $ "Expected a Copilot variable but provided " ++ show s ++ " instead."
-- XXX change the constructors to SimpleVar and Function (or something like that)
@@ -116,22 +120,23 @@ instance Show Ext where
-- | External variable, function, or array, together with it's type
type Exs = (A.Type, Ext, ExtRet)
-data ExtRet = ExtRetV
+data ExtRet = ExtRetV
| ExtRetA ArgConstVar
deriving Eq
-- | For calling a function with Atom variables.
funcShow :: Name -> String -> Args -> String
-funcShow cName fname args =
- fname ++ "(" ++ (unwords $ intersperse ","
+funcShow cName fname args =
+ fname ++ "(" ++ (unwords $ intersperse ","
(map (\arg -> case arg of
v@(V _) -> vPre cName ++ show v
C c -> c
+ S s -> "\"" ++ s ++ "\""
) args)) ++ ")"
instance Eq Ext where
(==) (ExtV v0) (ExtV v1) = v0 == v1
- (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1
+ (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1
(==) _ _ = False
-- These belong in Language.hs, but we don't want orphan instances.
@@ -160,7 +165,7 @@ instance (Streamable a, A.NumE a, Fractional a) => Fractional (Spec a) where
instance Eq a => Eq (Spec a) where
(==) (ExtVar t v) (ExtVar t' v') = t == t' && v == v' -- && ph == ph'
- (==) (ExtArr t (v, idx)) (ExtArr t' (v', idx')) =
+ (==) (ExtArr t (v, idx)) (ExtArr 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'
@@ -175,21 +180,21 @@ instance Eq a => Eq (Spec a) where
vPre :: Name -> String
vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "."
--- -- | An instruction to send data on a port at a given phase.
+-- -- | 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
+-- data Send a =
+-- Send { sendVar :: Spec a
-- , sendPort :: Port
-- , sendName :: String}
--- instance Streamable a => Show (Send a) where
--- show (Send s (Port port) portName) =
+-- instance Streamable a => Show (Send a) where
+-- show (Send s (Port port) portName) =
-- portName ++ "_port_" ++ show port ++ "_var_" ++ getMaybeVar s
-
+
-- | Holds all the different kinds of language elements that are pushed into the
-- Writer monad. This currently includes the actual specs and trigger
-- directives. (Use the functions in Language.hs to make sends and triggers.)
-data LangElems = LangElems
+data LangElems = LangElems
{ strms :: StreamableMaps Spec
, trigs :: Triggers}
@@ -198,12 +203,12 @@ data LangElems = LangElems
type Streams = Writer LangElems ()
getSpecs :: Streams -> StreamableMaps Spec
-getSpecs streams =
+getSpecs streams =
let (LangElems ss _) = execWriter streams
in ss
getTriggers :: Streams -> Triggers
-getTriggers streams =
+getTriggers streams =
let (LangElems _ triggers) = execWriter streams
in triggers
@@ -217,7 +222,7 @@ notConstVarErr s f = f $
case s of
Var v -> V v
Const c -> C (showAsC c)
- _ -> error $ "You provided specification \n" ++ " " ++ show s
+ _ -> error $ "You provided specification \n" ++ " " ++ show s
++ "\n where you needed to give a Copilot variable or constant."
@@ -227,7 +232,7 @@ notConstVarErr s f = f $
---- General functions on streams ----------------------------------------------
-- | A type is streamable iff a stream may emit values of that type
---
+--
-- There are very strong links between @'Streamable'@ and @'StreamableMaps'@ :
-- the types aggregated in @'StreamableMaps'@ are exactly the @'Streamable'@
-- types and that invariant should be kept (see methods)
@@ -238,12 +243,12 @@ class (A.Expr a, A.Assign a, Show a) => Streamable a where
-- | Provides a way to modify (mostly used for insertions) the Map in a
-- StreamableMaps which store values of the type
- updateSubMap :: (M.Map Var (b a) -> M.Map Var (b a))
+ updateSubMap :: (M.Map Var (b a) -> M.Map Var (b a))
-> StreamableMaps b -> StreamableMaps b
-- | A default value for the type @a@. Its value is not important.
unit :: a
-
+
-- | A constructor to produce an 'Atom' value
atomConstructor :: Var -> a -> A.Atom (A.V a)
@@ -256,20 +261,20 @@ class (A.Expr a, A.Assign a, Show a) => Streamable a where
-- printing and scanning, respectively.
prtId :: a -> (String, String)
scnId :: a -> (String, String)
-
+
-- | The same, only adds the wanted precision for floating points.
prtIdPrec :: a -> (String, String)
prtIdPrec x = prtId x
-
+
-- | The argument only coerces the type, it is discarded.
-- Returns the corresponding 'Atom' type.
atomType :: a -> A.Type
-
+
-- | Like Show, except that the formatting is exactly the same as the one of
-- C for example the booleans are first converted to 0 or 1, and floats and
-- doubles have the good precision.
showAsC :: a -> String
-
+
instance Streamable Bool where
getSubMap = bMap
updateSubMap f sm = sm {bMap = f $ bMap sm}
@@ -402,7 +407,7 @@ getMaybeElem v sm = M.lookup v $ getSubMap sm
-- Launch an exception if the index is not in it
{-# INLINE getElem #-}
getElem :: Streamable a => Var -> StreamableMaps b -> b a
-getElem v sm =
+getElem v sm =
case getMaybeElem v sm of
Nothing -> error $ "Error in application of getElem from Core.hs for variable "
++ v ++ "."
@@ -417,12 +422,12 @@ getAtomType s =
-- | This function is used to iterate on all the values in all the maps stored
-- by a @'StreamableMaps'@, accumulating a value over time
{-# INLINE foldStreamableMaps #-}
-foldStreamableMaps :: forall b c.
- (Streamable a => Var -> c a -> b -> b) ->
+foldStreamableMaps :: forall b c.
+ (Streamable a => Var -> c a -> b -> b) ->
StreamableMaps c -> b -> b
foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =
let acc0 = M.foldrWithKey f acc bm
- acc1 = M.foldrWithKey f acc0 i8m
+ acc1 = M.foldrWithKey f acc0 i8m
acc2 = M.foldrWithKey f acc1 i16m
acc3 = M.foldrWithKey f acc2 i32m
acc4 = M.foldrWithKey f acc3 i64m
@@ -430,13 +435,13 @@ foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =
acc6 = M.foldrWithKey f acc5 w16m
acc7 = M.foldrWithKey f acc6 w32m
acc8 = M.foldrWithKey f acc7 w64m
- acc9 = M.foldrWithKey f acc8 fm
+ acc9 = M.foldrWithKey f acc8 fm
acc10 = M.foldrWithKey f acc9 dm
in acc10
{-# INLINE mapStreamableMaps #-}
-mapStreamableMaps :: forall s s'.
- (forall a. Streamable a => Var -> s a -> s' a) ->
+mapStreamableMaps :: forall s s'.
+ (forall a. Streamable a => Var -> s a -> s' a) ->
StreamableMaps s -> StreamableMaps s'
mapStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
SM {
@@ -454,8 +459,8 @@ mapStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
}
{-# INLINE mapStreamableMapsM #-}
-mapStreamableMapsM :: forall s s' m. Monad m =>
- (Streamable a => Var -> s a -> m (s' a)) ->
+mapStreamableMapsM :: forall s s' m. Monad m =>
+ (Streamable a => Var -> s a -> m (s' a)) ->
StreamableMaps s -> m (StreamableMaps s')
mapStreamableMapsM f sm =
foldStreamableMaps (
@@ -468,14 +473,14 @@ mapStreamableMapsM f sm =
-- | Only keeps in @sm@ the values whose key+type are in @l@. Also returns a
-- bool saying whether all the elements in sm were in l. Works even if some
-- elements in @l@ are not in @sm@. Not optimised at all.
-filterStreamableMaps ::
+filterStreamableMaps ::
forall c b. StreamableMaps c -> [(A.Type, Var, b)] -> (StreamableMaps c, Bool)
filterStreamableMaps sm l =
let (sm2, l2) = foldStreamableMaps filterElem sm (emptySM, []) in
(sm2, (l' \\ nub l2) == [])
where
- filterElem :: forall a. Streamable a => Var -> c a ->
- (StreamableMaps c, [(A.Type, Var)]) ->
+ filterElem :: forall a. Streamable a => Var -> c a ->
+ (StreamableMaps c, [(A.Type, Var)]) ->
(StreamableMaps c, [(A.Type, Var)])
filterElem v s (sm', l2) =
let x = (atomType (unit::a), v) in
@@ -510,29 +515,29 @@ instance Monoid (StreamableMaps Spec) where
instance Monoid LangElems where
mempty = LangElems emptySM M.empty
- mappend (LangElems x z) (LangElems x' z') =
- LangElems (overlap x x') (M.union z z')
-overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s
-overlap x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm)
+ mappend (LangElems x z) (LangElems x' z') =
+ LangElems (overlap x x') (M.union z z')
+overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s
+overlap x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm)
y@(SM bm' i8m' i16m' i32m' i64m' w8m' w16m' w32m' w64m' fm' dm') =
let multDefs = (getVars x `intersect` getVars y)
in if null multDefs then union
- else error $ "Copilot error: The variables "
+ else error $ "Copilot error: The variables "
++ show multDefs ++ " have multiple definitions."
- where union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m')
- (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m')
- (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m')
+ where union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m')
+ (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m')
+ (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m')
(M.union fm fm') (M.union dm dm')
-- | Get the Copilot variables.
getVars :: StreamableMaps s -> [Var]
-getVars streams = foldStreamableMaps (\k _ ks -> k:ks) streams []
+getVars streams = foldStreamableMaps (\k _ ks -> k:ks) streams []
--- | An empty streamableMaps.
+-- | An empty streamableMaps.
emptySM :: StreamableMaps a
emptySM = SM
{
- bMap = M.empty,
+ bMap = M.empty,
i8Map = M.empty,
i16Map = M.empty,
i32Map = M.empty,
@@ -542,12 +547,12 @@ emptySM = SM
w32Map = M.empty,
w64Map = M.empty,
fMap = M.empty,
- dMap = M.empty
+ dMap = M.empty
}
-- | Verifies if its argument is equal to emptySM
isEmptySM :: StreamableMaps a -> Bool
-isEmptySM (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
+isEmptySM (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
M.null bm &&
M.null i8m &&
M.null i16m &&
@@ -558,13 +563,18 @@ isEmptySM (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
M.null w32m &&
M.null w64m &&
M.null fm &&
- M.null dm
+ M.null dm
--- | Replace all accepted special characters by sequences of underscores.
+-- | Replace all accepted special characters by sequences of underscores.
normalizeVar :: Var -> Var
-normalizeVar v =
+normalizeVar v =
map (\c -> if (c `elem` ".[]()") then '_' else c)
- (filter (\c -> c /= ',' && c /= ' ') v)
+ (filter (\c -> c /= ',' && c /= ' ') v)
+
+-- | Replace special characters by sequences of underscores, for string
+-- parameters of triggers.
+normalizeVar' :: String -> String
+normalizeVar' = map ( \ c -> if ( isAlpha c ) then c else '_' )
-- | For each typed variable, this type holds all its successive values in a
-- (probably) infinite list.
@@ -582,32 +592,32 @@ showIndented s n =
showRaw :: Spec a -> Int -> String
showRaw (ExtVar t v) _ = "ExtVar " ++ show t ++ " " ++ show v -- ++ " " ++ show ph
-showRaw (ExtArr t (v, idx)) _ =
+showRaw (ExtArr t (v, idx)) _ =
"ExtArr " ++ show t ++ " (" ++ show v ++ " ! (" ++ show idx ++ "))" -- ++ show ph
showRaw (Var v) _ = "Var " ++ v
showRaw (Const e) _ = show e
-showRaw (F _ _ s0) n =
- "F op? (\n" ++
- showIndented s0 (n + 1) ++ "\n" ++
+showRaw (F _ _ s0) n =
+ "F op? (\n" ++
+ showIndented s0 (n + 1) ++ "\n" ++
(concat $ replicate n " ") ++ ")"
-showRaw (F2 _ _ s0 s1) n =
+showRaw (F2 _ _ s0 s1) n =
"F2 op? (\n" ++
- showIndented s0 (n + 1) ++ "\n" ++
- showIndented s1 (n + 1) ++ "\n" ++
+ showIndented s0 (n + 1) ++ "\n" ++
+ showIndented s1 (n + 1) ++ "\n" ++
(concat $ replicate n " ") ++ ")"
-showRaw (F3 _ _ s0 s1 s2) n =
- "F3 op? (\n" ++
- showIndented s0 (n + 1) ++ "\n" ++
- showIndented s1 (n + 1) ++ "\n" ++
- showIndented s2 (n + 1) ++ "\n" ++
+showRaw (F3 _ _ s0 s1 s2) n =
+ "F3 op? (\n" ++
+ showIndented s0 (n + 1) ++ "\n" ++
+ showIndented s1 (n + 1) ++ "\n" ++
+ showIndented s2 (n + 1) ++ "\n" ++
(concat $ replicate n " ") ++ ")"
-showRaw (Append ls s0) n =
+showRaw (Append ls s0) n =
"Append " ++ show ls ++ " (\n" ++
- showIndented s0 (n + 1) ++ "\n" ++
+ showIndented s0 (n + 1) ++ "\n" ++
(concat $ replicate n " ") ++ ")"
-showRaw (Drop i s0) n =
+showRaw (Drop i s0) n =
"Drop " ++ show i ++ " (\n" ++
- showIndented s0 (n + 1) ++ "\n" ++
+ showIndented s0 (n + 1) ++ "\n" ++
(concat $ replicate n " ") ++ ")"
View
212 Language/Copilot/Dispatch.hs
@@ -8,7 +8,7 @@
-- used to check automatically the equivalence between the interpreter and the
-- compiler. The Dispatch module only parses the command-line arguments before
-- calling that module.
-module Language.Copilot.Dispatch
+module Language.Copilot.Dispatch
(dispatch, BackEnd(..), AtomToC(..), Iterations, Verbose(..)) where
import Language.Copilot.Core
@@ -16,51 +16,26 @@ import Language.Copilot.Analyser (check, getExternalVars)
import Language.Copilot.Interpreter
import Language.Copilot.AtomToC
import Language.Copilot.Compiler
+import Language.Copilot.Tests.Test
import Language.Copilot.PrettyPrinter ()
import qualified Language.Atom as A
import qualified Data.Map as M
-import System.Directory
-import System.Process
+import System.Directory
+import System.Process
import Control.Concurrent (threadDelay)
-import System.IO
- (stderr, hSetBuffering, hClose, hGetLine, hPutStrLn, BufferMode(..), Handle)
import Control.Monad
-import Data.Maybe (isJust, fromJust)
-
-data AtomToC = AtomToC
- { cName :: Name -- ^ Name of the C file to generate
- , gccOpts :: String -- ^ Options to pass to the compiler
- , getPeriod :: Maybe Period -- ^ The optional period
- , outputDir :: String -- ^ Where to put the executable
- , compiler :: String -- ^ Which compiler to use
- , randomProg :: Bool -- ^ Was the program randomly generated?
- , sim :: Bool -- ^ Are we running a C simulator?
- , prePostCode :: (Maybe String, Maybe String) -- ^ Code to replace the default
- -- initialization and main
- , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we
- -- don't know how large external arrays are, so
- -- we cannot declare them. Passing in pairs
- -- containing the name of the array and it's
- -- size allows them to be declared.
- , clock :: Maybe A.Clock -- Use the hardware clock to drive the timing
- -- of the program.
- }
data BackEnd = Interpreter -- Just interpret
- | Compile AtomToC -- Just compile
+ | Compile AtomToC -- Just compile
| Test AtomToC -- Interpret and compile (and test, with random programs)
---data Interpreted = Interpreted | NotInterpreted
-type Iterations = Int
-data Verbose = OnlyErrors | DefaultVerbose | Verbose deriving Eq
-
-- | This function is the core of /Copilot/ : it glues together analyser,
-- interpreter and compiler, and does all the IO. It can be called either from
-- interface (which justs decodes the command-line argument) or directly from
-- the interactive prompt in ghci.
--- @elems@ is a specification (and possible triggers),
+-- @elems@ is a specification (and possible triggers),
-- @inputExts@ allows the user to give at runtime values for
-- the monitored variables. Useful for testing on randomly generated values
-- and specifications, or for the interpreted version.
@@ -83,17 +58,17 @@ dispatch elems inputExts backEnd mIterations verbose = do
case backEnd of
Interpreter -> do
mapM_ putStrLn preludeText
- extVarValuesChks
+ extVarValuesChks
mapM_ putStrLn interpretedLines
- Compile opts -> do
+ Compile opts -> do
mapM_ putStrLn preludeText
makeCFiles elems simExtValues allExts opts verbose
-- Did the user ask us to execute the code, too?
- when (sim opts) $ do extVarValuesChks
+ when (sim opts) $ do extVarValuesChks
gccCall opts
-- Don't check against interpreter
- simC opts Nothing
+ simC opts Nothing
Test opts -> do
unless (randomProg opts) (mapM_ putStrLn preludeText)
extVarValuesChks
@@ -104,11 +79,11 @@ dispatch elems inputExts backEnd mIterations verbose = do
where
-- Do all the checks for feeding in external variable values for
-- interpreting.
- extVarValuesChks = do
+ extVarValuesChks = do
unless allInputsPresent $ error missingExtVars
unless (null inputsTooShort) $ error missingExtValues
-- Simulate the generated C code, possibly checking it against the interpreter.
- simC opts interps =
+ simC opts interps =
simCCode (strms elems) (outputDir opts ++ cName opts) simExtValues
interps iterations verbose
iterations = case mIterations of
@@ -116,45 +91,45 @@ dispatch elems inputExts backEnd mIterations verbose = do
Just i -> i
-- Call the interpreter and pass the result to showVars, which prettyprints
-- the results.
- interpretedLines = showVars (interpretStreams (strms elems) simExtValues)
- iterations
- missingExtVars =
+ interpretedLines = showVars (interpretStreams (strms elems) simExtValues)
+ iterations
+ missingExtVars =
"The interpreter does not have values for some of the external variables."
missingExtValues =
- "Error: the input values given for the external streams "
- ++ show inputsTooShort ++ " must contain at least " ++ show iterations
+ "Error: the input values given for the external streams "
+ ++ show inputsTooShort ++ " must contain at least " ++ show iterations
++ " (the number of iterations) elements."
-- collect all the external variables from the Copilot program.
allExts = getExternalVars (strms elems)
-- check that all the external variables have streams given for them for
-- simulation.
- (simExtValues :: SimValues , allInputsPresent :: Bool) =
+ (simExtValues :: SimValues , allInputsPresent :: Bool) =
filterStreamableMaps inputExts (map (\(a,v,r) -> (a, show v, r)) allExts)
-- check that enough values are given for each external-variable
-- value-stream. (Can't just use length, since lists might be infinite.)
- inputsTooShort =
+ inputsTooShort =
foldStreamableMaps (\v ls vs -> if length (take iterations ls) < iterations
- then v:vs else vs)
- simExtValues []
+ then v:vs else vs)
+ simExtValues []
-- | Make and possibly move C files. (We make them in the current directory,
-- | then move them.)
makeCFiles :: LangElems -> SimValues -> [Exs] -> AtomToC -> Verbose -> IO ()
makeCFiles elems simExtValues allExts opts verbose = do
let dirName = outputDir opts
- unless (last dirName == '/')
+ unless (last dirName == '/')
(error $ "Error: directory name for C files must contain a final '/'. "
++ "The directory name " ++ dirName ++ " does not.")
- putStrLn $ "Trying to create the directory " ++ dirName
+ putStrLn $ "Trying to create the directory " ++ dirName
++ " (if missing) ..."
createDirectoryIfMissing False dirName
copilotToC elems allExts simExtValues opts verbose
let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext)
- let delete ext = do f0 <- canonicalizePath (cName opts ++ ext)
+ let delete ext = do f0 <- canonicalizePath (cName opts ++ ext)
f1 <- canonicalizePath (dirName ++ cName opts ++ ext)
-- We might not have to move them!
unless (f0 == f1) $ removeFile f0
- putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts
+ putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts
++ ".h to " ++ dirName ++ " ..."
copy ".c"
copy ".h"
@@ -165,7 +140,7 @@ makeCFiles elems simExtValues allExts opts verbose = do
removeCFiles :: AtomToC -> IO ()
removeCFiles opts = do
putStrLn "Removing random program files..."
- let delete ext = do
+ let delete ext = do
f1 <- canonicalizePath (outputDir opts ++ cName opts ++ ext)
removeFile f1
delete ".c"
@@ -177,12 +152,14 @@ copilotToC :: LangElems -> [Exs] -> SimValues -> AtomToC -> Verbose -> IO ()
copilotToC elems allExts simExtValues opts verbose =
let cFileName = cName opts
(p', program) = copilotToAtom elems (getPeriod opts) cFileName
- (preCode, postCode) =
- getPrePostCode (sim opts) (prePostCode opts) cFileName
- (strms elems) allExts (map (\(x,y) -> (ExtV x,y))
+ (preCode, postCode) =
+ getPrePostCode (sim opts) (prePostCode opts) cFileName
+ (strms elems) allExts (map (\(x,y) -> (ExtV x,y))
(arrDecs opts)) simExtValues p'
- atomConfig = A.defaults
+ preHCode' = preHCode cFileName
+ atomConfig = A.defaults
{ A.cCode = \_ _ _ -> (preCode, postCode)
+ , A.hCode = \_ _ _ -> (preHCode', "")
, A.cRuleCoverage = False
, A.cAssert = False
, A.hardwareClock = clock opts
@@ -191,7 +168,7 @@ copilotToC elems allExts simExtValues opts verbose =
compileA = A.compile cFileName atomConfig program
in do
putStrLn $ "Compiling Copilot specs to C ..."
- (sched, _, _, _, _) <-
+ (sched, _, _, _, _) <-
-- Can fail with openFile: resource exhausted (Cannot allocate memory)
-- after thousands of compiles during random testing.
catch compileA (\_ -> threadDelay 10000 >> compileA)
@@ -200,140 +177,45 @@ copilotToC elems allExts simExtValues opts verbose =
-- | Call the C compiler.
gccCall :: AtomToC -> IO ()
-gccCall opts =
+gccCall opts =
let dirName = outputDir opts
- programName = cName opts
- command = compiler opts ++ " " ++ dirName ++ cName opts
- ++ ".c" ++ " -o " ++ dirName ++ programName
+ programName = cName opts
+ command = compiler opts ++ " " ++ dirName ++ cName opts
+ ++ ".c" ++ " -o " ++ dirName ++ programName
++ " " ++ gccOpts opts
in do putStrLn "Calling the C compiler ..."
putStrLn command
_ <- system command
return ()
--- | Execute the generated C code using provided values for external
--- variables. (And possibly execute the interpreter, and compare the results, if
--- interpretedLines is defined .)
-simCCode :: StreamableMaps Spec -> String -> SimValues -> Maybe [String]
- -> Iterations -> Verbose -> IO ()
-simCCode streams programName simExtValues mbInterpretedLines
- iterations verbose = do
- (Just hin, Just hout, _, prc) <- createProcess processConfig
-
- when (verbose == Verbose) (putStrLn $ "\nTesting program:\n"
- ++ unlines showStreams)
-
- -- Buffer by lines
- hSetBuffering hin LineBuffering
-
- -- Make the initial set of external variable values to send to the C program.
- inputVals <- foldStreamableMaps (inputVar hin) simExtValues (return emptySM)
-
- -- -1 Because we did an initial set of external vars.
- executePeriod (hin, hout, prc) inputVals mbInterpretedLines (iterations - 1)
-
- hClose hout
- _ <- waitForProcess prc
- putStrLn "Execution complete."
-
- where
-
- -- Create a subprocess to execute the C program. stdin and stdout for the C
- -- program, executed as a subprocess, will be redirected to hin and hout,
- -- respectively. We'll keep stderr (for the C program) pointed at stderr.
- processConfig =
- (shell $ programName ++ " " ++ show iterations)
- {std_in = CreatePipe, std_out = CreatePipe, std_err = UseHandle stderr}
-
- -- inputVar is folded over the set of input values (as lists) given for
- -- external variables. It returns a set of IO actions: for each external
- -- variable, the actions pipe the head of the list to the C simulator, then
- -- update the external variable map with the tail of the list.
- inputVar :: Streamable a
- => Handle -> Var -> [a] -> IO SimValues -> IO SimValues
- inputVar _ _ [] _ =
- error "Error: no more input values for external variables exist!"
- inputVar hin v (val:vals) ioSimVals = do
- _ <- hPutStrLn hin (showAsC val)
- valMap <- ioSimVals
- return $ updateSubMap (\m -> M.insert v vals m) valMap
-
- -- Execute the C program for the specified number of periods, comparing the
- -- outputs to the results of the interpreter at each period, if we're in
- -- testing mode.
- --
- -- XXX The code below works, but don't change it unless you know what you're
- -- doing. A less fragile version might use temporary files.
- executePeriod :: (Handle, Handle, ProcessHandle) -> SimValues -> Maybe [String]
- -> Int -> IO ()
- executePeriod (hin, hout, _) _ mbInLines 0 = do
- hClose hin -- Important to close hin before getting hout.
- cLines <- hGetLine hout
- when (isJust mbInLines)
- (compareOutputs ((concat . fromJust) mbInLines) cLines)
-
- executePeriod ps@(hin, _, _) inputVals mbInLines n = do
- nextInputVals <-
- foldStreamableMaps (inputVar hin) inputVals (return emptySM)
- let nextLines = case mbInLines of
- Nothing -> Nothing
- Just [] -> error "Impossible : empty ExecutePeriod"
- Just xs -> Just xs
- executePeriod ps nextInputVals nextLines (n - 1)
-
- showStreams =
- [ "****************************************************************\n"
- , show streams
- , "****************************************************************\n"
- ]
-
- -- Checking the compiler and interpreter.
- -- XXX This is pretty fragile, and depends on the string representations given
- -- by the interpreter and parser. Ideally, this would be made more robust.
- compareOutputs :: String -> String -> IO ()
- compareOutputs inLine line = do
- unless (inLine == line)
- -- Print to standard error, so you can push the testing to /dev/null.
- (hPutStrLn stderr failure >> error "Aborted testing on failure.")
- where
- failure = unlines
- [ "\n*** Failed on the Copilot specification: ***\n"
- , unlines showStreams
- , ""
- , "Failure: interpreter /= compiler"
- , " program name: " ++ programName
- , " interpreter: " ++ inLine
- , " compiler: " ++ line
- ]
-
-- | Prettyprint the interpreted values.
showVars :: SimValues -> Int-> [String]
showVars interpretedVars n = showVarsLine interpretedVars 0
where
showVarsLine copilotVs i =
- if i == n
+ if i == n
then []
- else let (string, copilotVs') =
- foldStreamableMaps prettyShow copilotVs ("", emptySM)
- endString = showVarsLine copilotVs' (i + 1)
+ else let (string, copilotVs') =
+ foldStreamableMaps prettyShow copilotVs ("", emptySM)
+ endString = showVarsLine copilotVs' (i + 1)
beginString = "period: " ++ show i ++ " " ++ string in
beginString:endString
- prettyShow v l (s, vs) =
+ prettyShow v l (s, vs) =
let s' = v ++ ": " ++ showAsC head' ++ " " ++ s
- head' = if null l
+ head' = if null l
then error "Copilot: internal error in the interpreter."
else head l
vs' = updateSubMap (\ m -> M.insert v (tail l) m) vs in
- (s', vs')
-
+ (s', vs')
+
preludeText :: [String]
-preludeText =
+preludeText =
[ ""
, "========================================================================="
, " CoPilot, a stream language for generating hard real-time C monitors. "
, "========================================================================="
, "Copyright, Galois, Inc. 2010"
- , "BSD3 License"
+ , "BSD3 License"
, "Website: http://leepike.github.com/Copilot/"
, "Maintainer: Lee Pike <leepike--at--gmail.com> (remove dashes)."
, "Usage: > help"
View
6 Language/Copilot/Examples/ClockExamples.hs
@@ -10,9 +10,11 @@ clkTest :: Streams
clkTest = do
let x = varB "x"
let y = varB "y"
+ let z = varB "z"
let a = varW8 "a"
let b = varW8 "b"
- x `clock` (period 3, phase 1)
- y `clock` (period 4, phase 3)
+ x `clk` (period 3, phase 1)
+ y `clk` (period 4, phase 3)
a .= [0] ++ mux x (a + 2) a
b .= [1] ++ mux y (b + 2) b
+ z `clk1` ("zclock", period 4, phase 3)
View
103 Language/Copilot/Examples/Examples.hs
@@ -4,21 +4,25 @@ module Language.Copilot.Examples.Examples where
import Data.Word
import Prelude (($))
-import qualified Prelude as Prelude
import qualified Prelude as P
-- for specifying options
--- import Data.Map (fromList)
+-- import Data.Map (fromList)
--import Data.Maybe (Maybe (..))
--import System.Random
-import Language.Copilot
+import Language.Copilot
-- import Language.Copilot.Variables
+aa :: Streams
+aa = do
+ let x = varW64 "x"
+ x .= [0] ++ x + 2
+
fib :: Streams
fib = do
let f = varW64 "f"
- t = varB "t"
+ t = varB "t"
f .= [0,1] ++ f + (drop 1 f)
t .= even f
where even :: Spec Word64 -> Spec Bool
@@ -77,7 +81,7 @@ t6 = do
let x = extB "x"
y = varB "y"
y .= x
-
+
yy :: Streams
yy = do
let a = varW32 "a"
@@ -108,8 +112,8 @@ xx = do
c = varW32 "c"
e = extW32 "ext"
d = varB "d"
- f = extW32 (fun "fun1" void)
- h = extArrW16 (fun "g" b) a
+ 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
@@ -130,9 +134,9 @@ distrib = do
b = varB "b"
-- spec
a .= [0,1] ++ a + 1
- b .= mod a 2 == 0
+ b .= mod a 2 == 0
-- sends
- trigger true "portA" a
+ trigger true "portA" a
trigger true "portB" b
monitor :: Streams
@@ -159,15 +163,15 @@ gcd n0 n1 = do
where alg x0 x1 x2 = [x0] ++ mux (x1 > x2) (x1 - x2) x1
-- greatest common divisor of two external vars. Compare to
--- Language.Atom.Example Try
+-- Language.Atom.Example Try
--
--- interpret gcd' 40 $ setE (emptySM {w16Map =
--- fromList [("n", [9,9..]), ("m", [7,7..])]}) baseOpts
+-- interpret gcd' 40 $ setE (emptySM {w16Map =
+-- fromList [("n", [9,9..]), ("m", [7,7..])]}) baseOpts
--
-- Note we have to start streams a and b with a dummy value 0 before they can
-- sample the external variables.
gcd' :: Streams
-gcd' = do
+gcd' = do
-- externals
let n = extW16 "n"
m = extW16 "m"
@@ -176,7 +180,7 @@ gcd' = do
b = varW16 "b"
init = varB "init"
ans = varB "ans"
-
+
a .= alg n (sub a b) init
b .= alg m (sub b a) init
ans .= a == b && not init
@@ -212,12 +216,12 @@ testCoercions3 = do
z .= cast (not true)
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
let target = varW32 "target"
- target .= [0] ++ target + 1
+ target .= [0] ++ target + 1
let x = varW32 "x"
let y = varW32 "y"
@@ -225,14 +229,14 @@ trap = do
y .= [0,0] ++ x + target
-- vicious :: Streams
--- vicious = do
--- "varExt" .= extW32 "ext" 5
--- "vicious" .= [0,1,2,3] ++ drop 4 (varW32 "varExt") + drop 1 (var "varExt") + var "varExt"
+-- vicious = do
+-- "varExt" .= extW32 "ext" 5
+-- "vicious" .= [0,1,2,3] ++ drop 4 (varW32 "varExt") + drop 1 (var "varExt") + var "varExt"
-- testVicious :: Streams
-- testVicious = do
--- "counter" .= [0] ++ varW32 "counter" + 1
--- "testVicious" .= [0,0,0,0,0,0,0,0,0,0] ++ drop 8 (varW32 "counter")
+-- "counter" .= [0] ++ varW32 "counter" + 1
+-- "testVicious" .= [0,0,0,0,0,0,0,0,0,0] ++ drop 8 (varW32 "counter")
-- -- The issue is when a variable v with a prophecy array of length n deps on
-- -- an external variable pv with a weight w, and that w > - n + 1 Here, w = 0 and
@@ -247,9 +251,9 @@ trap = do
-- -- easier for now to just forbid it. But it could become an issue.
-- isBugged :: Streams
-- isBugged = do
--- "v" .= extW16 "ext" 5
--- "v2" .= [0,1,3] ++ drop 1 (varW16 "v")
-
+-- "v" .= extW16 "ext" 5
+-- "v2" .= [0,1,3] ++ drop 1 (varW16 "v")
+
-- -- The next two examples are currently refused, because they include a
-- -- non-negative weighted closed path. But they could be compiled. More
@@ -261,29 +265,29 @@ trap = do
-- -- requirement of a Copilot monitor.
-- shouldBeRight :: Streams
-- shouldBeRight = do
--- "v1" .= [0] ++ varI32 "v1" + 1
--- "v2" .= drop 2 (varI32 "v1")
+-- "v1" .= [0] ++ varI32 "v1" + 1
+-- "v2" .= drop 2 (varI32 "v1")
-- shouldBeRight2 :: Streams
-- shouldBeRight2 = do
--- "loop1" .= [0] ++ varI32 "loop2" + 2
--- "loop2" .= [1] ++ varI32 "loop1" - 1
--- "other" .= drop 3 (varI32 "loop1")
+-- "loop1" .= [0] ++ varI32 "loop2" + 2
+-- "loop2" .= [1] ++ varI32 "loop1" - 1
+-- "other" .= drop 3 (varI32 "loop1")
-- testing external array references
testArr :: Streams
-testArr = do
- -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1
+testArr = do
+ -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1
-- && extArrB ("ff", varW16 b) 2
- -- b .= [7] ++ varW16 b + 3 + extArrW16 ("gg", varW16 f) 2
- -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4
+ -- b .= [7] ++ varW16 b + 3 + extArrW16 ("gg", varW16 f) 2
+ -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4
-- c .= [True] ++ var c
- -- d .= varB c
+ -- d .= varB c
let e = varW16 "e"
e .= [6,7,8] ++ 3 -- + extArrW16 ("gg", varW16 b) 2
--- f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2
+-- f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2
let g = varB "g"
- let gg = extArrW16 "gg" e
+ let gg = extArrW16 "gg" e
g .= gg < 13
-- h .= [0] ++ drop 1 (varW16 g)
@@ -293,10 +297,10 @@ t99 :: Streams
t99 = do
let ext = extW32 "ext"
a = varW32 "a"
- a .= [0,1] ++ a + ext + ext + ext
+ a .= [0,1] ++ a + ext + ext + ext
let b = varB "b"
- b .= [True, False] ++ 2 + a < 5 + ext
+ b .= [True, False] ++ 2 + a < 5 + ext
t11 :: Streams
t11 = do
@@ -314,12 +318,12 @@ extT :: Streams
extT = do
let x = extW16 "x"
let y = varW16 "y"
- y .= x
+ y .= x
-- Examples:
-interpretExtT :: Prelude.IO ()
+interpretExtT :: P.IO ()
interpretExtT =
- interpret extT 10 $
+ interpret extT 10 $
-- setE (emptySM {w16Map = fromList [("x", [8,9..])]})
setEW16 "x" [8,9..]
baseOpts
@@ -334,14 +338,14 @@ extT2 :: Streams
extT2 = do
let y = varW16 "y"
x = extW16 (fun "f" y)
- y .= x
+ y .= x
-- Should pass.
extT3 :: Streams
extT3 = do
let y = varW16 "y"
x = extW16 (fun "f" y)
- y .= [3] ++ x
+ y .= [3] ++ x
-- Should fail.
extT4 :: Streams
@@ -373,7 +377,16 @@ extT6 = do
y .= [7] ++ z
w .= x
-
+foo :: Streams
+foo = do
+ let x = varW16 "x"
+ let y = varW16 "y"
+ let z = varW16 "z"
+ let w = varW16 "w"
+ x .= [1,2] ++ x
+ y .= [3,4] ++ y
+ z .= x + y
+ w .= z + z
-- test external idx before after and in the stream it references
-- test multiple defs
View
26 Language/Copilot/Examples/RegExpExample.hs
@@ -3,10 +3,10 @@ module Language.Copilot.Examples.RegExpExample where
import Language.Copilot.Core
import qualified Language.Copilot.Language as C
import Language.Copilot.Interface
-import Language.Copilot.Libs.RegExp ( copilotRegexp )
+import Language.Copilot.Libs.RegExp ( copilotRegexp, copilotRegexpB )
-testRegExp :: Streams
-testRegExp = do
+testRegExp1 :: Streams
+testRegExp1 = do
let input = C.varI64 "input"
output = C.varB "output"
reset = C.varB "reset"
@@ -14,7 +14,23 @@ testRegExp = do
reset C..= [ True ] C.++ C.false
copilotRegexp input "<0><1><2>*|<-3>+" output reset
+testRegExp2 :: Streams
+testRegExp2 = do
+ let b1 = C.varB "b1"
+ b2 = C.varB "b2"
+ b3 = C.varB "b3"
+ output = C.varB "output"
+ reset = C.varB "reset"
+ b1 C..= [ True, False, False ] C.++ b2
+ b2 C..= [ False, True, False ] C.++ b3
+ b3 C..= [ False, False, True ] C.++ b1
+ reset C..= [ True ] C.++ C.false
+ copilotRegexpB "<b1><b2><b3>(<b1>|<b2>|<b3>)*" output reset
+
main :: IO ()
main = do
- interpret testRegExp 10 baseOpts
- compile testRegExp "testRegExp" baseOpts
+ interpret testRegExp1 10 baseOpts
+ compile testRegExp1 "testRegExp" baseOpts
+
+ interpret testRegExp2 10 baseOpts
+ compile testRegExp2 "testRegExp" baseOpts
View
57 Language/Copilot/Interface.hs
@@ -13,7 +13,7 @@ module Language.Copilot.Interface (
import Language.Copilot.Core
import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3)
import Language.Copilot.Tests.Random
-import Language.Copilot.Dispatch
+import Language.Copilot.Dispatch
import Language.Copilot.Help
import qualified Language.Atom as A (Clock)
@@ -47,6 +47,8 @@ data Options = Options {
-- binary).
optPrePostCode :: (Maybe String, Maybe String), -- ^ Code to append above and
-- below the C file.
+ optPrePostHCode :: (Maybe String, Maybe String), -- ^ Code to append above and
+ -- below the header file.
optSimulate :: Bool, -- ^ Do we want a simulation driver?
optTriggers :: Triggers, -- ^ A list of Copilot variable C function name
-- pairs. The C funciton is called if the Copilot
@@ -78,6 +80,7 @@ baseOpts = Options {
optCompiler = "gcc",
optOutputDir = "./",
optPrePostCode = (Nothing, Nothing),
+ optPrePostHCode = (Nothing, Nothing),
optSimulate = False,
optTriggers = M.empty,
optArrs = [],
@@ -89,16 +92,16 @@ baseOpts = Options {
-- | Run 'randomTest' @n@ iterations on each of @i@ random programs.
randomTests :: Int -> Int -> Options -> IO ()
-randomTests n i opts = do
+randomTests n i opts = do
randomTests' i
- where
- randomTests' 0 = do putStrLn
+ where
+ randomTests' 0 = do putStrLn
$ "Executed " ++ show i ++ " tests without an error."
- randomTests' j = do
- catch (randomTest n opts)
- (\_ -> error $ "Executed " ++ show (i-j)
+ randomTests' j = do
+ catch (randomTest n opts)
+ (\_ -> error $ "Executed " ++ show (i-j)
++ " tests before an unexpected system error.")
- randomTests' (j-1)
+ randomTests' (j-1)
-- | Generate a random Copilot program and compare the interpreter against the
-- compiler on that program.
@@ -106,25 +109,25 @@ randomTest :: Int -> Options -> IO ()
randomTest n opts = do
r <- randomRIO (0, maxBound)
interface $ setI $ setR r $ setSim n opts
-
+
-- | Compare the interpreter and the compiler on a specific program, possibly
-- using @gcov@ <http://gcc.gnu.org/onlinedocs/gcc/Gcov.html> to check coverage
-- of the generated C program.
test :: Streams -> Name -> Int -> Bool -> Options -> IO ()
test streams fileName n b opts = do
interface $ setO fileName $ setSim n
- $ setTriggers (getTriggers streams)
+ $ setTriggers (getTriggers streams)
$ setI $ opts { optStreams = Just (getSpecs streams)
, optCompile = copts}
- when b (do h <- runCommand ("gcov -b " ++ fileName)
+ when b (do h <- runCommand ("gcov -b " ++ fileName)
putStrLn ""
putStrLn "***********************************"
putStrLn " Coverage statistics from gcov:"
putStrLn "***********************************"
_ <- waitForProcess h
return ())
- where
- copts = if b then "-Wall -fprofile-arcs -ftest-coverage"
+ where
+ copts = if b then "-Wall -fprofile-arcs -ftest-coverage"
else optCompiler opts
-- | Interpret a program.
@@ -134,9 +137,9 @@ interpret streams n opts =
-- | Compile a program.
compile :: Streams -> Name -> Options -> IO ()
-compile streams fileName opts =
- interface $ setO fileName
- $ setTriggers (getTriggers streams)
+compile streams fileName opts =
+ interface $ setO fileName
+ $ setTriggers (getTriggers streams)
$ opts {optStreams = Just (getSpecs streams)}
-- | Verify the output of a compiled program using @CBMC@.
@@ -150,19 +153,19 @@ verify file n opts = do
putStrLn " --overflow-check enable arithmetic over- and underflow checks"
putStrLn " --nan-check check floating-point for NaN"
putStrLn ""
- putStrLn $ "Assuming main() as the entry point unless specified otherwise "
+ putStrLn $ "Assuming main() as the entry point unless specified otherwise "
++ "(--function f)"
putStrLn cmd
code <- system cmd
case code of
ExitSuccess -> return ()
_ -> do putStrLn ""
- putStrLn $ "An error was returned by cbmc. This may have "
- ++ "be due to cbmc not finding the file "
+ 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
+ ++ " on your system, or " ++ file
++ " does not exist. See "
++ "<http://www.cprover.org/cbmc/> "
++ "for more information on cbmc."
@@ -179,7 +182,7 @@ setTriggers :: Triggers -> Options -> Options
setTriggers triggers opts = opts {optTriggers = triggers}
setE :: Streamable a => Var -> [a] -> Options -> Options
-setE v ls opts =
+setE v ls opts =
opts {optSimVals = Just $ updateSubMap (\m -> insert v ls m) mp}
where mp = if isNothing (optSimVals opts) then emptySM
else fromJust $ optSimVals opts
@@ -195,7 +198,7 @@ setEI32 = setE
setEI64 :: Var -> [Int64] -> Options -> Options
setEI64 = setE
setEW8 :: Var -> [Word8] -> Options -> Options
-setEW8 = setE
+setEW8 = setE
setEW16 :: Var -> [Word16] -> Options -> Options
setEW16 = setE
setEW32 :: Var -> [Word32] -> Options -> Options
@@ -297,7 +300,7 @@ interface opts =
-- putStrLn $ "Random seed :" ++ show seed
-- dispatch is doing all the heavy plumbing between
-- analyser, compiler, interpreter, gcc and the generated program
- dispatch (LangElems streams triggers) vars backEnd iterations verbose
+ dispatch (LangElems streams triggers) vars backEnd iterations verbose
createSeed :: Options -> IO Int
createSeed opts =
@@ -326,12 +329,12 @@ getBackend opts seed =
then Test backendOpts
else Interpreter
else Compile backendOpts
- where
+ where
backendOpts =
- AtomToC { cName =
- optCName opts ++ if isJust $ optRandomSeed opts
+ AtomToC { cName =
+ optCName opts ++ if isJust $ optRandomSeed opts
then show seed else ""
- , randomProg = isJust $ optRandomSeed opts
+ , randomProg = isJust $ optRandomSeed opts
, gccOpts = optCompile opts
, getPeriod = optPeriod opts
, outputDir = optOutputDir opts
View
32 Language/Copilot/Language.hs
@@ -17,7 +17,7 @@ module Language.Copilot.Language (
Num(..),
-- * Division
Fractional((/)),
- mux,
+ mux,
-- * Copilot variable declarations.
var, varB, varI8, varI16, varI32, varI64,
varW8, varW16, varW32, varW64, varF, varD,
@@ -31,7 +31,7 @@ module Language.Copilot.Language (
true, false,
module Language.Copilot.Language.Sampling,
-- * Constructs of the copilot language
- drop, (++), (.=), -- (..|),
+ drop, (++), (.=), -- (..|),
-- * Triggers
module Language.Copilot.Language.FunctionCalls,
-- * Safe casting
@@ -70,14 +70,14 @@ div = F2 P.div A.div_
-- | As mod and div, except that if the division would be by 0, the first
-- argument is used as a default.
mod0, div0 :: (Streamable a, A.IntegralE a) => a -> Spec a -> Spec a -> Spec a
-mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d
- else x0 `P.div` x1)
+mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d
+ else x0 `P.div` x1)
(\ e0 e1 -> A.mod0_ e0 e1 d)
-div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d
- else x0 `P.mod` x1)
+div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d
+ else x0 `P.mod` x1)
(\ e0 e1 -> A.div0_ e0 e1 d)
-
+
-- class (Streamable a, A.OrdE a) => SpecOrd a where
-- (<)
@@ -94,8 +94,8 @@ div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d
(||), (&&), (^), (==>) :: Spec Bool -> Spec Bool -> Spec Bool
(||) = F2 (P.||) (A.||.)
(&&) = F2 (P.&&) (A.&&.)
-(^) = F2
- (\ x y -> (x P.&& P.not y) P.|| (y P.&& P.not x))
+(^) = F2
+ (\ x y -> (x P.&& P.not y) P.|| (y P.&& P.not x))
(\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x))
(==>) = F2 (\ x y -> y P.|| P.not x) A.imply
@@ -128,7 +128,7 @@ varI32 = Var
varI64 :: Var -> Spec Int64
varI64 = Var
varW8 :: Var -> Spec Word8
-varW8 = Var
+varW8 = Var
varW16 :: Var -> Spec Word16
varW16 = Var
varW32 :: Var -> Spec Word32
@@ -142,11 +142,11 @@ varD = Var
-- | Define a stream variable.
(.=) :: Streamable a => Spec a -> Spec a -> Streams
-v .= s =
+v .= s =
case v of
- (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM)
+ (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM)
M.empty
- _ -> error $ "Given spec " P.++ show v
+ _ -> error $ "Given spec " P.++ show v
P.++ " but expected a variable in a Copilot definition (.=)."
-- | Coerces a type that is 'Streamable' into a Copilot constant.
@@ -162,7 +162,7 @@ constI32 = Const
constI64 :: Int64 -> Spec Int64
constI64 = Const
constW8 :: Word8 -> Spec Word8
-constW8 = Const
+constW8 = Const
constW16 :: Word16 -> Spec Word16
constW16 = Const
constW32 :: Word32 -> Spec Word32
@@ -201,8 +201,8 @@ infixr 2 .=
"Copilot.Language Times1L" forall s. (P.*) (Const 1) s = s
"Copilot.Language Times0R" forall s. (P.*) s (Const 0) = Const 0
"Copilot.Language Times0L" forall s. (P.*) (Const 0) s = Const 0
-"Copilot.Language FracBy0" forall s. (P./) s (Const 0.0) = P.error "division by zero !"
-"Copilot.Language FracBy1" forall s. (P./) s (Const 1.0) = s
+"Copilot.Language FracBy0" forall s. (P./) s (Const 0.0) = P.error "division by zero !"
+"Copilot.Language FracBy1" forall s. (P./) s (Const 1.0) = s
"Copilot.Language Frac0" forall s. (P./) (Const 0.0) s = (Const 0.0)
"Copilot.Language OrFR" forall s. (||) s (Const False) = s
"Copilot.Language OrFL" forall s. (||) (Const False) s = s
View
51 Language/Copilot/Language/FunctionCalls.hs
@@ -1,6 +1,7 @@
{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
-module Language.Copilot.Language.FunctionCalls
+module Language.Copilot.Language.FunctionCalls
((<>), trigger, void, fun) where
import Language.Copilot.Core
@@ -8,39 +9,63 @@ import Language.Copilot.Core
import Control.Monad.Writer (tell)
import qualified Data.Map as M
--- | No C arguments
+-- | No C arguments
void :: Args
void = []
-class ArgCl a where
- (<>) :: Streamable b => Spec b -> a -> Args
+
+class ArgFunCl a where
trigger :: Spec Bool -> String -> a -> Streams
fun :: String -> a -> Ext
-instance ArgCl Args where
- s <> args = argUpdate s args
+instance ArgFunCl Args where
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 =
+instance Streamable a => ArgFunCl ( Spec a ) where
+ trigger v fnName arg =
let arg' = argUpdate arg [] in
trigger' v fnName arg'
- fun f arg =
+ fun f arg =
let arg' = argUpdate arg [] in
Fun f arg'
+instance ArgFunCl String where
+ trigger v fnName arg = trigger' v fnName [ S arg ]
+ fun f arg = Fun f [ S arg ]
+
+
+class ArgListCl a b where
+ (<>) :: a -> b -> Args
+
+instance Streamable a => ArgListCl ( Spec a ) Args where
+ s <> args = argUpdate s args
+
+instance ArgListCl String Args where
+ s <> args = ( S s ) : args
+
+instance ( Streamable a, Streamable b ) => ArgListCl ( Spec a ) ( Spec b ) where
+ s <> s' = (argUpdate s (argUpdate s' []))
+
+instance ( Streamable a ) => ArgListCl ( Spec a ) String where
+ s <> s' = argUpdate s [ S s' ]
+
+instance ( Streamable a ) => ArgListCl String ( Spec a ) where
+ s <> s' = ( S s ) : argUpdate s' []
+
+instance ArgListCl String String where
+ s <> s' = [ S s, S s' ]
+
+
infixr 1 <>
-- | XXX document
trigger' :: Spec Bool -> String -> Args -> Streams
trigger' v fnName args =
- tell $ LangElems
- emptySM
+ tell $ LangElems
+ emptySM
(M.insert (show trig) trig M.empty)
where trig = Trigger v fnName args
argUpdate :: Streamable a => Spec a -> Args -> Args
argUpdate s args = notConstVarErr s (\v -> v:args)
-
View
49 Language/Copilot/Libs/Clocks.hs
@@ -19,20 +19,19 @@
-- The phase must be less than the period.
module Language.Copilot.Libs.Clocks
- ( clock, period, phase
+ ( clk, clk1, period, phase
) where
-import Prelude (Int, error, String, show, (.), fromIntegral)
-import Prelude (($))
+import Prelude (error, show, fromIntegral, String)
import qualified Prelude as P
import Data.List (replicate)
import Data.Int
-import Language.Copilot
-import Language.Copilot.Core hiding (Period)
+import Language.Copilot
+-- import Language.Copilot.Core hiding (Period)
-- For testing.
-import Language.Copilot.Interface (interpret, baseOpts)
+-- import Language.Copilot.Interface (interpret, baseOpts)
data Period = Period Int
data Phase = Phase Int
@@ -43,10 +42,10 @@ period = Period
phase :: Int -> Phase
phase = Phase
--- clock generates a clock that counts n ticks by using a
+-- clk generates a clock that counts n ticks by using a
-- prophecy array of size n
-clock :: Spec Bool -> (Period, Phase) -> Streams
-clock v (Period per, Phase ph) =
+clk :: Spec Bool -> (Period, Phase) -> Streams
+clk v (Period per, Phase ph) =
if (per P.< 1) then error ("Error in stream " P.++ (show v)
P.++ ": period must be 1 or greater.")
else if (ph P.< 0) then error ("Error in stream " P.++ (show v)
@@ -56,20 +55,20 @@ clock v (Period per, Phase ph) =
else v .= ((replicate ph False)
P.++ (True : (replicate ((per - ph) - 1) False)) ++ v)
--- -- clock generates a clock that counts n ticks by using a
--- -- 32 bit counter variable
--- clock' :: String -> Spec Bool -> (Period, Phase) -> Streams
--- clock' clockName v (Period per, Phase ph) = do
--- { let counter = varI32 ( clockName P.++ "_counter" )
--- ; counter .= [ 0 ] ++ ( mux ( counter /= ( fromIntegral ) per - 1 )
--- ( counter + 1 )
--- ( 0 ) )
--- ; if (per P.< 1) then error ("Error in stream " P.++ (show v)
--- P.++ ": period must be 1 or greater.")
--- else if (ph P.< 0) then error ("Error in stream " P.++ (show v)
--- P.++ ": phase must be 0 or greater.")
--- else if (ph P.>= per) then error ("Error in stream " P.++ (show v)
--- P.++ ": phase must be less than period.")
--- else v .= counter == ( fromIntegral ) ph
--- }
+-- clk1 generates a clock that counts n ticks by using a
+-- 32 bit counter variable
+clk1 :: Spec Bool -> (String, Period, Phase) -> Streams
+clk1 v (clockName, Period per, Phase ph) = do
+ { let counter = varI32 ( clockName P.++ "_counter" )
+ ; counter .= [ 0 ] ++ ( mux ( counter /= ( fromIntegral per ) - 1 )
+ ( counter + 1 )
+ ( 0 ) )
+ ; if (per P.< 1) then error ("Error in stream " P.++ (show v)
+ P.++ ": period must be 1 or greater.")
+ else if (ph P.< 0) then error ("Error in stream " P.++ (show v)
+ P.++ ": phase must be 0 or greater.")
+ else if (ph P.>= per) then error ("Error in stream " P.++ (show v)
+ P.++ ": phase must be less than period.")
+ else v .= counter == ( fromIntegral ph )
+ }
View
119 Language/Copilot/Libs/RegExp.hs
@@ -1,8 +1,9 @@
-module Language.Copilot.Libs.RegExp ( copilotRegexp ) where
+module Language.Copilot.Libs.RegExp ( copilotRegexp, copilotRegexpB ) where
import Text.ParserCombinators.Parsec
- ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser
- , optionMaybe, chainr1, chainr, many1, digit, eof, parse, SourceName)
+-- ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser
+-- , optionMaybe, chainr1, chainr, many1, digit, letter, alphaNum, eof, parse
+-- , mappend, SourceName)
import Data.Int
import Data.Word
import Data.List
@@ -14,6 +15,7 @@ import Control.Monad.State (evalState, get, modify)
import Language.Copilot.Core
import qualified Language.Copilot.Language as C
+
-- The symbols in a regular expression, "Any" is any value of type t
-- (matches any symbol, the "point" character in a regular expression).
-- Start is used only for a start state in the generated NFA, that
@@ -37,10 +39,10 @@ data NumSym t = NumSym { symbolNum :: Maybe Int
-- symbol type into a valid C identifier string to be used as a
-- Copilot variable name
instance Show t => Show ( NumSym t ) where
- show s = "rsym_"
- ++ ( replace '-' '_' . show . symbol ) s
- ++ "_"
- ++ show ( fromJust $ symbolNum s )
+ show s = "rsym_"
+ ++ ( replace '-' '_' . show . symbol ) s
+ ++ "_"
+ ++ show ( fromJust $ symbolNum s )
where replace c1 c2 = map ( \ c -> if c == c1 then c2 else c )
-- The regular expression data type. For our use
@@ -58,7 +60,8 @@ data RegExp t = REpsilon
-- Parsers for single characters.
lquote, rquote, lparen, rparen,
- star, plus, qmark, point, minus :: CharParser () Char
+ star, plus, qmark, point, minus,
+ nondigit :: CharParser () Char
lquote = char '<'
rquote = char '>'
lparen = char '('
@@ -69,6 +72,7 @@ qmark = char '?'
point = char '.'
minus = char '-'
+nondigit = char '_' <|> letter
-- A "followedBy" combinator for parsing, parses
-- p, then p' and returns the result of p.
@@ -77,12 +81,17 @@ followedBy :: GenParser tok () a
-> GenParser tok () a
followedBy p p' = p >>= \ r -> p' >> return r
+
+-- Parsing a string p' with prefix p, returning
+-- both in order
+cPrefix, optCPrefix :: GenParser tok () Char
+ -> GenParser tok () String
+ -> GenParser tok () String
+cPrefix p p' = p >>= \ c -> fmap ( c : ) p'
+
-- Parsing a string p' with the character p as an
-- optional prefix, return the result with the
-- optional prefix.
-optCPrefix :: GenParser tok () Char
- -> GenParser tok () String
- -> GenParser tok () String
optCPrefix p p' = optionMaybe p
>>= \ r -> case r of
Nothing -> p'
@@ -115,8 +124,9 @@ anySym :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
anySym = point >> ( return . RSymbol ) ( NumSym Nothing Any )
-class Streamable t => SymbolParser t where
- parseSym :: GenParser Char () ( RegExp t )
+class SymbolParser t where
+ parseSym :: GenParser Char () ( RegExp t )
+
instance SymbolParser Bool where
parseSym = do { truth <- ( ci "t" >> optional ( ci "rue" )
@@ -129,14 +139,14 @@ instance SymbolParser Bool where
}
-parseWordSym :: ( Integral t, Streamable t )
+parseWordSym :: ( Integral t )
=> GenParser Char () ( RegExp t )
parseWordSym = do { num <- between lquote rquote $ many1 digit
; return . RSymbol . NumSym Nothing . Sym
$ fromIntegral ( read num :: Integer )
}
-parseIntSym :: ( Integral t, Streamable t )
+parseIntSym :: ( Integral t )
=> GenParser Char () ( RegExp t )
parseIntSym = do { num <- between lquote rquote $
optCPrefix minus ( many1 digit )
@@ -144,6 +154,20 @@ parseIntSym = do { num <- between lquote rquote $
$ fromIntegral ( read num :: Integer )
}
+newtype VarName = VarName { getVarName :: Var }
+ deriving Eq
+
+instance Show VarName where
+ show s = getVarName s
+
+parseVarSym :: GenParser Char () ( RegExp VarName )
+parseVarSym = do { varName <- between lquote rquote $
+ cPrefix nondigit ( many $ nondigit <|> digit )
+ ; return . RSymbol . NumSym Nothing . Sym
+ $ VarName varName
+ }
+
+
instance SymbolParser Word8 where
parseSym = parseWordSym
@@ -168,6 +192,9 @@ instance SymbolParser Int32 where
instance SymbolParser Int64 where
parseSym = parseIntSym
+instance SymbolParser VarName where
+ parseSym = parseVarSym
+
opOr :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
opOr = char '|' >> return ROr
@@ -277,7 +304,8 @@ enumSyms rexp = evalState ( enumSyms' rexp ) 0
enumSyms' other =
return other
-regexp2CopilotNFA :: (Streamable t, C.EqE t)
+
+regexp2CopilotNFA :: ( Streamable t, C.EqE t )
=> Spec t -> RegExp t -> Spec Bool -> Spec Bool -> Streams
regexp2CopilotNFA inStream rexp outStream reset =
let symbols = getSymbols rexp
@@ -303,7 +331,7 @@ regexp2CopilotNFA inStream rexp outStream reset =
spec numSym = [ False ] C.++
C.mux ( C.drop 1 reset )
- C.false
+ C.false
( transition numSym )
stream numSym = ref numSym C..= spec numSym
@@ -311,7 +339,7 @@ regexp2CopilotNFA inStream rexp outStream reset =
in foldl ( >> ) startStream streams >> outStream'
-copilotRegexp :: (SymbolParser t, C.EqE t)
+copilotRegexp :: (Streamable t, SymbolParser t, C.EqE t)
=> Spec t -> SourceName -> Spec Bool -> Spec Bool -> Streams
copilotRegexp inStream rexp outStream reset =
case parse start rexp rexp of
@@ -331,3 +359,58 @@ copilotRegexp inStream rexp outStream reset =
, "on infinite streams, since we do not have "
, "a distinct end-of-input symbol."]
else regexp2CopilotNFA inStream nrexp outStream reset
+
+
+regexp2CopilotNFAB :: RegExp VarName -> Spec Bool -> Spec Bool -> Streams
+regexp2CopilotNFAB rexp outStream reset =
+ let symbols = getSymbols rexp
+ ref = C.var . show
+ startRef = C.var "start"
+ startStream = startRef C..= reset
+ outStream' = outStream C..=
+ foldl ( C.|| ) reset ( map ref symbols )
+
+ preceding' rexp' numSym = case preceding rexp' numSym of
+ [] -> [ startRef ]
+ other -> map ref other
+
+ matchesInput numSym = case symbol numSym of
+ Start -> error
+ "start matched"
+ Any -> C.true
+ Sym ( VarName t ) -> C.var t
+
+ transition numSym = matchesInput numSym
+ C.&&
+ foldl1 ( C.|| )
+ ( preceding' rexp numSym )
+
+ spec numSym = [ False ] C.++
+ C.mux ( C.drop 1 reset )
+ C.false
+ ( transition numSym )
+
+ stream numSym = ref numSym C..= spec numSym
+ streams = map stream symbols
+ in foldl ( >> ) startStream streams >> outStream'
+
+
+copilotRegexpB :: SourceName -> Spec Bool -> Spec Bool -> Streams
+copilotRegexpB rexp outStream reset =
+ case parse start rexp rexp of
+ Left err ->
+ error $ "parse error: " ++ show err
+ Right rexp' -> let nrexp = enumSyms rexp' in
+ if hasFinitePath nrexp then
+ error $
+ concat [ "The regular expression contains a finite path "
+ , "which is something that will fail to match "
+ , "since we do not have a distinct end-of-input "
+ , "symbol on infinite streams." ]
+ else if hasEpsilon nrexp then
+ error $
+ concat [ "The regular expression matches a language "
+ , "that contains epsilon. This cannot be handled "
+ , "on infinite streams, since we do not have "
+ , "a distinct end-of-input symbol."]
+ else regexp2CopilotNFAB nrexp outStream reset
View
6 Language/Copilot/PrettyPrinter.hs
@@ -11,11 +11,11 @@ import Data.Map as M
import Language.Copilot.Core
instance (Show (a Bool), Show (a Int8), Show (a Int16), Show (a Int32), Show (a Int64),
- Show (a Word8), Show (a Word16), Show (a Word32), Show (a Word64),
+ Show (a Word8), Show (a Word16), Show (a Word32), Show (a Word64),
Show (a Float), Show (a Double)) => Show (StreamableMaps a) where
show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) =
let acc0 = M.foldrWithKey showVal "" bm
- acc1 = M.foldrWithKey showVal acc0 i8m
+ acc1 = M.foldrWithKey showVal acc0 i8m
acc2 = M.foldrWithKey showVal acc1 i16m
acc3 = M.foldrWithKey showVal acc2 i32m
acc4 = M.foldrWithKey showVal acc3 i64m
@@ -23,7 +23,7 @@ instance (Show (a Bool), Show (a Int8), Show (a Int16), Show (a Int32), Show (a
acc6 = M.foldrWithKey showVal acc5 w16m
acc7 = M.foldrWithKey showVal acc6 w32m
acc8 = M.foldrWithKey showVal acc7 w64m
- acc9 = M.foldrWithKey showVal acc8 fm
+ acc9 = M.foldrWithKey showVal acc8 fm
acc10 = M.foldrWithKey showVal acc9 dm
in acc10
where
View
104 Language/Copilot/Tests/Random.hs
@@ -3,16 +3,16 @@
-- | Generate random specs for testing. We do not generate external array indexes.
-module Language.Copilot.Tests.Random
+module Language.Copilot.Tests.Random
(randomStreams, Operator(..), Operators, fromOp) where
-import Language.Copilot.Core
+import Language.Copilot.Core
import Language.Copilot.Analyser
import qualified Language.Atom as A
import qualified Data.Map as M
-import Prelude
+import Prelude
import System.Random
import Data.Int
import Data.Word
@@ -30,15 +30,17 @@ weightsContinueVar, weightsContinueExtVar :: [(Bool, Int)]
weightsContinueVar = [(True, 3), (False, 1)]
weightsContinueExtVar = [(True, 1), (False, 1)]
--- These determines the frequency of each atom type for the streams and the monitored variables
+-- These determines the frequency of each atom type for the streams and the
+-- monitored variables XXX We're not testing floats and doubles, because it's
+-- impossible to guarantee precision.
weightsVarTypes, weightsExtVarTypes :: [(A.Type, Int)]
-weightsVarTypes =
- [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4),
+weightsVarTypes =
+ [(A.Bool, 1), (A.Word64, 1), (A.Int64, 1), (A.Float, 0), (A.Double, 0),
(A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)]
-weightsExtVarTypes =
- [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4),
+weightsExtVarTypes =
+ [(A.Bool, 1), (A.Word64, 1), (A.Int64, 1), (A.Float, 0), (A.Double, 0),
(A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)]
-
+
-- These determines the frequency of each constructor in the random streams
-- 0 -> ExtVar
-- 1 -> Var
@@ -55,28 +57,28 @@ weightsDropSpecSet = [(1,2),(2,6),(7,1)]
---- Tools ---------------------------------------------------------------------
-data Operator a =
- Operator (forall g . RandomGen g =>
- (forall a' g'. (Streamable a', Random a', RandomGen g') =>
- g' -> SpecSet -> (Spec a', g')) ->
+data Operator a =
+ Operator (forall g . RandomGen g =>
+ (forall a' g'. (Streamable a', Random a', RandomGen g') =>
+ g' -> SpecSet -> (Spec a', g')) ->
g -> (Spec a, g))
type Operators = StreamableMaps Operator
-fromOp :: Operator a ->
- (forall g. RandomGen g =>
- (forall a' g'. (Streamable a', Random a', RandomGen g') =>
- g' -> SpecSet -> (Spec a', g')) ->
+fromOp :: Operator a ->
+ (forall g. RandomGen g =>
+ (forall a' g'. (Streamable a', Random a', RandomGen g') =>
+ g' -> SpecSet -> (Spec a', g')) ->
g -> (Spec a, g))
fromOp op =
case op of
Operator x -> x
-foldRandomableMaps :: forall b c.
- (forall a. (Streamable a, Random a) => Var -> c a -> b -> b) ->
+foldRandomableMaps :: forall b c.
+ (forall a. (Streamable a, Random a) => Var -> c a -> b -> b) ->
StreamableMaps c -> b -> b
foldRandomableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =
let acc0 = M.foldrWithKey f acc bm
- acc1 = M.foldrWithKey f acc0 i8m
+ acc1 = M.foldrWithKey f acc0 i8m
acc2 = M.foldrWithKey f acc1 i16m
acc3 = M.foldrWithKey f acc2 i32m
acc4 = M.foldrWithKey f acc3 i64m
@@ -84,7 +86,7 @@ foldRandomableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =
acc6 = M.foldrWithKey f acc5 w16m
acc7 = M.foldrWithKey f acc6 w32m
acc8 = M.foldrWithKey f acc7 w64m