copilot-language 2.1.2 → 2.2.0
raw patch · 13 files changed
+617/−242 lines, 13 filesdep +copilot-theoremdep ~copilot-core
Dependencies added: copilot-theorem
Dependency ranges changed: copilot-core
Files
- copilot-language.cabal +8/−5
- src/Copilot/Language.hs +4/−1
- src/Copilot/Language/Analyze.hs +126/−67
- src/Copilot/Language/Operators/BitWise.hs +10/−10
- src/Copilot/Language/Operators/Cast.hs +94/−2
- src/Copilot/Language/Operators/Extern.hs +33/−18
- src/Copilot/Language/Operators/Integral.hs +3/−2
- src/Copilot/Language/Operators/Label.hs +21/−0
- src/Copilot/Language/Operators/Propositional.hs +27/−0
- src/Copilot/Language/Operators/Temporal.hs +9/−0
- src/Copilot/Language/Reify.hs +191/−115
- src/Copilot/Language/Spec.hs +83/−22
- src/Copilot/Language/Stream.hs +8/−0
copilot-language.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language-version: 2.1.2+version: 2.2.0 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description:@@ -37,17 +37,20 @@ , data-reify >= 0.6 , mtl >= 2.0 && < 3 , ghc-prim >= 0.2- , copilot-core >= 0.1+ , copilot-core == 2.2.0+ , copilot-theorem == 0.2 exposed-modules: Copilot , Copilot.Language , Copilot.Language.Operators.BitWise , Copilot.Language.Operators.Boolean+ , Copilot.Language.Operators.Propositional , Copilot.Language.Operators.Cast , Copilot.Language.Operators.Constant , Copilot.Language.Operators.Eq , Copilot.Language.Operators.Extern , Copilot.Language.Operators.Integral , Copilot.Language.Operators.Local+ , Copilot.Language.Operators.Label , Copilot.Language.Operators.Mux , Copilot.Language.Operators.Ord , Copilot.Language.Operators.Temporal@@ -68,8 +71,8 @@ -fpackage-trust -- Trusted packages:- -trust base- -trust containers- -trust array+ -trust=base+ -trust=containers+ -trust=array
src/Copilot/Language.hs view
@@ -18,6 +18,7 @@ , module Copilot.Language.Operators.Eq , module Copilot.Language.Operators.Extern , module Copilot.Language.Operators.Local+ , module Copilot.Language.Operators.Label , module Copilot.Language.Operators.Integral , module Copilot.Language.Operators.Mux , module Copilot.Language.Operators.Ord@@ -30,6 +31,8 @@ , trigger , arg , prop+ , theorem+ , forall, exists , prettyPrint ) where @@ -46,6 +49,7 @@ import Copilot.Language.Operators.Extern import Copilot.Language.Operators.Integral import Copilot.Language.Operators.Local+import Copilot.Language.Operators.Label import Copilot.Language.Operators.Mux import Copilot.Language.Operators.Ord import Copilot.Language.Operators.Temporal@@ -53,7 +57,6 @@ import Copilot.Language.Reify import Copilot.Language.Prelude import Copilot.Language.Spec- (Spec, trigger, arg, observer, prop) import Copilot.Language.Stream (Stream) --------------------------------------------------------------------------------
src/Copilot/Language/Analyze.hs view
@@ -38,7 +38,8 @@ | DropMaxViolation | NestedExternFun | NestedArray- | TooMuchRecussion+ | TooMuchRecursion+ | InvalidField | DifferentTypes String | Redeclared String | BadNumberOfArgs String@@ -49,22 +50,24 @@ show DropAppliedToNonAppend = badUsage $ "Drop applied to non-append operation!" show DropIndexOverflow = badUsage $ "Drop index overflow!" show ReferentialCycle = badUsage $ "Referential cycle!"- show DropMaxViolation = badUsage $ "Maximum drop violation (" ++ + show DropMaxViolation = badUsage $ "Maximum drop violation (" ++ show (maxBound :: DropIdx) ++ ")!"- show NestedExternFun = badUsage $ + show NestedExternFun = badUsage $ "An external function cannot take another external function or external array as an argument. Try defining a stream, and using the stream values in the other definition."- show NestedArray = badUsage $ + show NestedArray = badUsage $ "An external function cannot take another external function or external array as an argument. Try defining a stream, and using the stream values in the other definition."- show TooMuchRecussion = badUsage $ - "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition. Likely, you have accidently defined a circular stream, such as 'x = x'. Another possibility is you have defined a a polymorphic function with type constraints that references other streams. For example,\n\n nats :: (Typed a, Num a) => Stream a\n nats = [0] ++ nats + 1\n\nis not allowed. Make the definition monomorphic, or add a level of indirection, like \n\n nats :: (Typed a, Num a) => Stream a\n nats = n\n where n = [0] ++ nats + 1\n\nFinally, you may have intended to generate a very large expression. You can try shrinking the expression by using local variables. It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."- show (DifferentTypes name) = badUsage $ - "The external symbol " ++ name ++ " has been declared to have two different types!"- show (Redeclared name) = badUsage $ - "The external symbol " ++ name ++ " has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."- show (BadNumberOfArgs name) = badUsage $ - "The function symbol " ++ name ++ " has been redeclared to have different number of arguments."- show (BadFunctionArgType name) = badUsage $ - "The funciton symbol " ++ name ++ " has been redeclared to an argument with different types."+ show TooMuchRecursion = badUsage $+ "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition. Likely, you have accidently defined a circular stream, such as 'x = x'. Another possibility is you have defined a a polymorphic function with type constraints that references other streams. For example,\n\n nats :: (Typed a, Num a) => Stream a\n nats = [0] ++ nats + 1\n\nis not allowed. Make the definition monomorphic, or add a level of indirection, like \n\n nats :: (Typed a, Num a) => Stream a\n nats = n\n where n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression. You can try shrinking the expression by using local variables. It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."+ show InvalidField = badUsage $+ "A struct can only take external variables, arrays, or other structs as fields."+ show (DifferentTypes name) = badUsage $+ "The external symbol \'" ++ name ++ "\' has been declared to have two different types!"+ show (Redeclared name) = badUsage $+ "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."+ show (BadNumberOfArgs name) = badUsage $+ "The function symbol \'" ++ name ++ "\' has been redeclared to have different number of arguments."+ show (BadFunctionArgType name) = badUsage $+ "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types." instance Exception AnalyzeException @@ -77,17 +80,19 @@ -------------------------------------------------------------------------------- -analyze :: Spec -> IO ()+analyze :: Spec' a -> IO () analyze spec = do refStreams <- newIORef M.empty mapM_ (analyzeTrigger refStreams) (triggers $ runSpec spec) mapM_ (analyzeObserver refStreams) (observers $ runSpec spec)- specExts refStreams spec >>= analyzeExts + mapM_ (analyzeProperty refStreams) (properties $ runSpec spec)+ mapM_ (analyzeProperty refStreams) (map fst $ theorems $ runSpec spec)+ specExts refStreams spec >>= analyzeExts -------------------------------------------------------------------------------- analyzeTrigger :: IORef Env -> Trigger -> IO ()-analyzeTrigger refStreams (Trigger _ e0 args) = +analyzeTrigger refStreams (Trigger _ e0 args) = analyzeExpr refStreams e0 >> mapM_ analyzeTriggerArg args where@@ -101,16 +106,22 @@ -------------------------------------------------------------------------------- +analyzeProperty :: IORef Env -> Property -> IO ()+analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e++--------------------------------------------------------------------------------+ data SeenExtern = NoExtern | SeenFun | SeenArr+ | SeenStruct -------------------------------------------------------------------------------- analyzeExpr :: IORef Env -> Stream a -> IO () analyzeExpr refStreams s = do b <- mapCheck refStreams- when b (throw TooMuchRecussion)+ when b (throw TooMuchRecursion) go NoExtern M.empty s where@@ -124,30 +135,41 @@ Const _ -> return () Drop k e1 -> analyzeDrop (fromIntegral k) e1 Extern _ _ -> return ()- ExternFun _ args me -> + ExternFun _ args me -> checkInterp >> checkArgs where- checkInterp = case me of + checkInterp = case me of Nothing -> return () Just e -> go seenExt nodes' e- checkArgs = case seenExt of - NoExtern -> mapM_ (\(Arg a) -> + checkArgs = case seenExt of+ NoExtern -> mapM_ (\(Arg a) -> go SeenFun nodes' a) args SeenFun -> throw NestedExternFun SeenArr -> throw NestedArray- ExternArray _ idx _ _ -> case seenExt of - NoExtern -> go SeenArr nodes' idx- SeenFun -> throw NestedExternFun- SeenArr -> throw NestedArray- Local e f -> go seenExt nodes' e >> + SeenStruct-> throw InvalidField+ ExternArray _ idx _ _ -> case seenExt of+ NoExtern -> go SeenArr nodes' idx+ SeenFun -> throw NestedExternFun+ SeenArr -> throw NestedArray+ SeenStruct-> go SeenStruct nodes' idx+ ExternStruct _ sargs -> case seenExt of+ NoExtern ->+ mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs+ SeenFun -> throw NestedExternFun+ SeenArr -> throw NestedArray+ SeenStruct->+ mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs+ GetField e _ -> analyzeAppend refStreams dstn e () analyzeExpr --Copied from `Append` case+ Local e f -> go seenExt nodes' e >> go seenExt nodes' (f (Var "dummy")) Var _ -> return () Op1 _ e -> go seenExt nodes' e- Op2 _ e1 e2 -> go seenExt nodes' e1 >> + Op2 _ e1 e2 -> go seenExt nodes' e1 >> go seenExt nodes' e2- Op3 _ e1 e2 e3 -> go seenExt nodes' e1 >> - go seenExt nodes' e2 >> + Op3 _ e1 e2 e3 -> go seenExt nodes' e1 >>+ go seenExt nodes' e2 >> go seenExt nodes' e3+ Label _ e -> go seenExt nodes' e -------------------------------------------------------------------------------- @@ -167,7 +189,7 @@ -------------------------------------------------------------------------------- -analyzeAppend :: +analyzeAppend :: IORef Env -> DynStableName -> Stream a -> b -> (IORef Env -> Stream a -> IO b) -> IO b analyzeAppend refStreams dstn e b f = do@@ -194,89 +216,105 @@ -- typed arguments. -------------------------------------------------------------------------------- --- An environment to store external variables, arrays, and functions, so that we+-- An environment to store external variables, arrays, functions and structs, so that we -- can check types in the expression---e.g., if we declare the same external to -- have two different types. data ExternEnv = ExternEnv { externVarEnv :: [(String, C.SimpleType)] , externArrEnv :: [(String, C.SimpleType)]- , externFunEnv :: [(String, C.SimpleType)] - , externFunArgs :: [(String, [C.SimpleType])] + , externFunEnv :: [(String, C.SimpleType)]+ , externFunArgs :: [(String, [C.SimpleType])]+ , externStructEnv :: [(String, C.SimpleType)]+ , externStructArgs :: [(String, [C.SimpleType])] } -------------------------------------------------------------------------------- --- Make sure external variables, functions, and arrays are correctly typed.+-- Make sure external variables, functions, arrays, and structs are correctly typed. analyzeExts :: ExternEnv -> IO () analyzeExts ExternEnv { externVarEnv = vars , externArrEnv = arrs- , externFunEnv = funs - , externFunArgs = args }+ , externFunEnv = funs+ , externFunArgs = args+ , externStructEnv = datastructs+ , externStructArgs = struct_args } = do -- symbol names redeclared? findDups vars arrs findDups vars funs+ --findDups vars struct_args+ findDups vars datastructs findDups arrs funs+ --findDups arrs struct_args+ findDups arrs datastructs+ --findDups funs struct_args+ findDups funs datastructs -- conflicting types? conflictingTypes vars conflictingTypes arrs conflictingTypes funs -- symbol names given different number of args and right types? funcArgCheck args- + --funcArgCheck struct_args+ funcArgCheck struct_args+ where- findDups :: [(String, C.SimpleType)] -> [(String, C.SimpleType)] -> IO ()+ findDups :: [(String, a)] -> [(String, b)] -> IO () findDups ls0 ls1 = mapM_ (\(name,_) -> dup name) ls0 where- dup nm = mapM_ ( \(name',_) -> if name' == nm + dup nm = mapM_ ( \(name',_) -> if name' == nm then throw (Redeclared nm)- else return () + else return () ) ls1 conflictingTypes :: [(String, C.SimpleType)] -> IO ()- conflictingTypes ls = + conflictingTypes ls = let grps = groupByPred ls in mapM_ sameType grps- where + where sameType :: [(String, C.SimpleType)] -> IO ()- sameType grp = foldCheck check grp + sameType grp = foldCheck check grp check name c0 c1 = if c0 == c1 then return (name,c0) -- a dummy---we -- discard the result else throw (DifferentTypes name) funcArgCheck :: [(String, [C.SimpleType])] -> IO ()- funcArgCheck ls = + funcArgCheck ls = let grps = groupByPred ls in mapM_ argCheck grps- where + where argCheck :: [(String, [C.SimpleType])] -> IO () argCheck grp = foldCheck check grp- check name args0 args1 = - if length args0 == length args1 + check name args0 args1 =+ if length args0 == length args1 then if args0 == args1 then return (name,args0) -- a dummy---we discard the -- result else throw (BadFunctionArgType name)- else throw (BadNumberOfArgs name) + else throw (BadNumberOfArgs name) + {-structArgCheck :: [(String, [C.SimpleType])] -> IO ()+ structArgCheck ls = foldr (\sarg' _ -> findDups (getArgName sarg', sarg') (getArgName sarg', sarg'))+ (return ()) $ map snd ls-}+ groupByPred :: [(String, a)] -> [[(String, a)]] groupByPred = groupBy (\(n0,_) (n1,_) -> n0 == n1) foldCheck :: (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()- foldCheck check grp = + foldCheck check grp = foldM_ ( \(name, c0) (_, c1) -> check name c0 c1) (head grp) -- should be typesafe, since this is from groupBy grp -------------------------------------------------------------------------------- -specExts :: IORef Env -> Spec -> IO ExternEnv+specExts :: IORef Env -> Spec' a -> IO ExternEnv specExts refStreams spec = do env <- foldM triggerExts- (ExternEnv [] [] [] []) + (ExternEnv [] [] [] [] [] []) (triggers $ runSpec spec)- foldM observerExts env (observers $ runSpec spec) + foldM observerExts env (observers $ runSpec spec) where observerExts :: ExternEnv -> Observer -> IO ExternEnv@@ -284,14 +322,14 @@ triggerExts :: ExternEnv -> Trigger -> IO ExternEnv triggerExts env (Trigger _ guard args) = do- env' <- collectExts refStreams guard env + env' <- collectExts refStreams guard env foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'') env' args collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv collectExts refStreams stream_ env_ = do b <- mapCheck refStreams- when b (throw TooMuchRecussion)+ when b (throw TooMuchRecursion) go M.empty env_ stream_ where@@ -301,22 +339,22 @@ assertNotVisited stream dstn nodes case stream of- Append _ _ e -> analyzeAppend refStreams dstn e env + Append _ _ e -> analyzeAppend refStreams dstn e env (\refs str -> collectExts refs str env) Const _ -> return env Drop _ e1 -> go nodes env e1- Extern name _ -> + Extern name _ -> let ext = ( name, getSimpleType stream ) in return env { externVarEnv = ext : externVarEnv env } ExternFun name args me -> do env' <- case me of- Nothing -> return env + Nothing -> return env Just e -> go nodes env e env'' <- foldM (\env'' (Arg arg_) -> go nodes env'' arg_)- env' args - let argTypes = map (\(Arg arg_) -> getSimpleType arg_) args - let fun = (name, getSimpleType stream) + env' args+ let argTypes = map (\(Arg arg_) -> getSimpleType arg_) args+ let fun = (name, getSimpleType stream) return env'' { externFunEnv = fun : externFunEnv env'' , externFunArgs = (name, argTypes) : externFunArgs env'' }@@ -326,17 +364,38 @@ let arr = ( name, getSimpleType stream ) return env' { externArrEnv = arr : externArrEnv env' } - Local e _ -> go nodes env e + ExternStruct name sargs -> do+ env' <- foldM (\env' (_, Arg arg_) -> go nodes env' arg_)+ env sargs+ --let argTypes = map (\(Arg arg_) -> (n, getSimpleType arg_)) sargs+ let argTypes = map (\(_, Arg arg_) -> getSimpleType arg_) sargs+ let struct = (name, getSimpleType stream)+ return env' { externStructEnv = struct : externStructEnv env'+ , externStructArgs = (name, argTypes) : externStructArgs env' }++ GetField _ _ -> return env++ Local e _ -> go nodes env e Var _ -> return env- Op1 _ e -> go nodes env e + Op1 _ e -> go nodes env e Op2 _ e1 e2 -> do env' <- go nodes env e1 go nodes env' e2- Op3 _ e1 e2 e3 -> do env' <- go nodes env e1 - env'' <- go nodes env' e2 - go nodes env'' e3 + Op3 _ e1 e2 e3 -> do env' <- go nodes env e1+ env'' <- go nodes env' e2+ go nodes env'' e3+ Label _ e -> go nodes env e ---------------------------------------------------------------------------------+{-+getArgName :: forall a. C.Typed a => Stream a -> String+getArgName arg_stream =+ case arg_stream of+ Extern cs _ -> cs+ ExternFun cs _ _ -> cs+ ExternArray cs _ _ _ -> cs+ ExternStruct cs _ -> cs+ _ -> ""+-} getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)
src/Copilot/Language/Operators/BitWise.hs view
@@ -21,21 +21,21 @@ import Data.Bits instance (Typed a, Bits a) => Bits (Stream a) where- (.&.) = Op2 (Core.BwAnd typeOf)- complement = Op1 (Core.BwNot typeOf)- (.|.) = Op2 (Core.BwOr typeOf)- xor = Op2 (Core.BwXor typeOf)- shiftL = P.error "shiftL undefined, for left-shifting use .<<."- shiftR = P.error "shiftR undefined, for right-shifting use .>>."- rotate = P.error "tbd: rotate"- bitSize = P.error "tbd: bitSize"- isSigned = P.error "tbd: issigned"+ (.&.) = Op2 (Core.BwAnd typeOf)+ complement = Op1 (Core.BwNot typeOf)+ (.|.) = Op2 (Core.BwOr typeOf)+ xor = Op2 (Core.BwXor typeOf)+ shiftL = P.error "shiftL undefined, for left-shifting use .<<."+ shiftR = P.error "shiftR undefined, for right-shifting use .>>."+ rotate = P.error "tbd: rotate"+ bitSize = P.error "tbd: bitSize"+ isSigned = P.error "tbd: issigned" -- Avoid redefinition of the Operators.Boolean xor (.^.) :: Bits a => a -> a -> a (.^.) = xor -(.<<.), (.>>.) :: (Bits a, Typed a, Typed b, P.Integral b) +(.<<.), (.>>.) :: (Bits a, Typed a, Typed b, P.Integral b) => Stream a -> Stream b -> Stream a (.<<.) = Op2 (Core.BwShiftL typeOf typeOf) (.>>.) = Op2 (Core.BwShiftR typeOf typeOf)
src/Copilot/Language/Operators/Cast.hs view
@@ -7,8 +7,8 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE MultiParamTypeClasses #-} -module Copilot.Language.Operators.Cast - ( cast ) where+module Copilot.Language.Operators.Cast+ ( cast, unsafeCast ) where import qualified Copilot.Core.Operators as C import Copilot.Core.Type@@ -22,6 +22,9 @@ class Cast a b where cast :: (Typed a, Typed b) => Stream a -> Stream b +class UnsafeCast a b where+ unsafeCast :: (Typed a, Typed b) => Stream a -> Stream b+ -------------------------------------------------------------------------------- castBool :: (Eq a, Num a, Typed a) => Stream Bool -> Stream a@@ -136,4 +139,93 @@ cast = castIntegral --------------------------------------------------------------------------------+-- | Unsafe downcasting to smaller sizes+-------------------------------------------------------------------------------- +instance UnsafeCast Word64 Word32 where+ unsafeCast = castIntegral+instance UnsafeCast Word64 Word16 where+ unsafeCast = castIntegral+instance UnsafeCast Word64 Word8 where+ unsafeCast = castIntegral+instance UnsafeCast Word32 Word16 where+ unsafeCast = castIntegral+instance UnsafeCast Word32 Word8 where+ unsafeCast = castIntegral+instance UnsafeCast Word16 Word8 where+ unsafeCast = castIntegral++instance UnsafeCast Int64 Int32 where+ unsafeCast = castIntegral+instance UnsafeCast Int64 Int16 where+ unsafeCast = castIntegral+instance UnsafeCast Int64 Int8 where+ unsafeCast = castIntegral+instance UnsafeCast Int32 Int16 where+ unsafeCast = castIntegral+instance UnsafeCast Int32 Int8 where+ unsafeCast = castIntegral+instance UnsafeCast Int16 Int8 where+ unsafeCast = castIntegral++--------------------------------------------------------------------------------+-- | Unsafe unsigned and signed promotion to floating point values+--------------------------------------------------------------------------------++instance UnsafeCast Int64 Float where+ unsafeCast = castIntegral+instance UnsafeCast Int32 Float where+ unsafeCast = castIntegral+instance UnsafeCast Int16 Float where+ unsafeCast = castIntegral+instance UnsafeCast Int8 Float where+ unsafeCast = castIntegral++instance UnsafeCast Int64 Double where+ unsafeCast = castIntegral+instance UnsafeCast Int32 Double where+ unsafeCast = castIntegral+instance UnsafeCast Int16 Double where+ unsafeCast = castIntegral+instance UnsafeCast Int8 Double where+ unsafeCast = castIntegral++instance UnsafeCast Word64 Float where+ unsafeCast = castIntegral+instance UnsafeCast Word32 Float where+ unsafeCast = castIntegral+instance UnsafeCast Word16 Float where+ unsafeCast = castIntegral+instance UnsafeCast Word8 Float where+ unsafeCast = castIntegral++instance UnsafeCast Word64 Double where+ unsafeCast = castIntegral+instance UnsafeCast Word32 Double where+ unsafeCast = castIntegral+instance UnsafeCast Word16 Double where+ unsafeCast = castIntegral+instance UnsafeCast Word8 Double where+ unsafeCast = castIntegral++--------------------------------------------------------------------------------+-- | Signed to unsigned and vice versa+--------------------------------------------------------------------------------++instance UnsafeCast Word64 Int64 where+ unsafeCast = castIntegral+instance UnsafeCast Word32 Int32 where+ unsafeCast = castIntegral+instance UnsafeCast Word16 Int16 where+ unsafeCast = castIntegral+instance UnsafeCast Word8 Int8 where+ unsafeCast = castIntegral++instance UnsafeCast Int64 Word64 where+ unsafeCast = castIntegral+instance UnsafeCast Int32 Word32 where+ unsafeCast = castIntegral+instance UnsafeCast Int16 Word16 where+ unsafeCast = castIntegral+instance UnsafeCast Int8 Word8 where+ unsafeCast = castIntegral
src/Copilot/Language/Operators/Extern.hs view
@@ -32,6 +32,7 @@ , externArrayI64 , externArrayF , externArrayD+ , externStruct , funArg -- * Deprecated. ) where @@ -50,7 +51,7 @@ externFun :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a externFun = ExternFun -externArray :: (Typed a, Typed b, Integral a) +externArray :: (Typed a, Typed b, Integral a) => String -> Stream a -> Size -> Maybe [[b]] -> Stream b externArray = ExternArray @@ -58,12 +59,26 @@ funArg :: Typed a => Stream a -> Arg funArg = Arg +externStruct :: Typed a => String -> [(String, Arg)] -> Stream a+externStruct = ExternStruct++{-(#) :: Typed a => Core.StructData -> String -> Stream a+(Core.StructData {Core.structName = x, Core.structInst = y})#z = getField x z+ where+ getField struct_nm field_nm =+ let test = find (\(Core.StructData name _) -> name == struct_nm) structs in+ case test of+ Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"+ Just element ->+ fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structInst))+ (error "No field by the name of \"" ++ field_nm ++ "\"") element+-} -------------------------------------------------------------------------------- externB :: String -> Maybe [Bool] -> Stream Bool-externB = extern +externB = extern externW8 :: String -> Maybe [Word8] -> Stream Word8-externW8 = extern +externW8 = extern externW16 :: String -> Maybe [Word16] -> Stream Word16 externW16 = extern externW32 :: String -> Maybe [Word32] -> Stream Word32@@ -85,47 +100,47 @@ -------------------------------------------------------------------------------- -externArrayB :: (Typed a, Integral a) - => String -> Stream a -> Size +externArrayB :: (Typed a, Integral a)+ => String -> Stream a -> Size -> Maybe [[Bool]] -> Stream Bool-externArrayB = externArray -externArrayW8 :: (Typed a, Integral a) - => String -> Stream a -> Size +externArrayB = externArray+externArrayW8 :: (Typed a, Integral a)+ => String -> Stream a -> Size -> Maybe [[Word8]] -> Stream Word8-externArrayW8 = externArray +externArrayW8 = externArray externArrayW16 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Word16]] -> Stream Word16 externArrayW16 = externArray externArrayW32 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Word32]] -> Stream Word32 externArrayW32 = externArray externArrayW64 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Word64]] -> Stream Word64 externArrayW64 = externArray externArrayI8 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Int8]] -> Stream Int8 externArrayI8 = externArray externArrayI16 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Int16]] -> Stream Int16 externArrayI16 = externArray externArrayI32 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Int32]] -> Stream Int32 externArrayI32 = externArray externArrayI64 :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Int64]] -> Stream Int64 externArrayI64 = externArray externArrayF :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Float]] -> Stream Float externArrayF = externArray externArrayD :: (Typed a, Integral a)- => String -> Stream a -> Size + => String -> Stream a -> Size -> Maybe [[Double]] -> Stream Double externArrayD = externArray
src/Copilot/Language/Operators/Integral.hs view
@@ -37,10 +37,11 @@ (^) :: (Typed a, Typed b, P.Num a, B.Bits a, P.Integral b) => Stream a -> Stream b -> Stream a-(Const 0) ^ _ = Const 0+(Const 0) ^ (Const 0) = Const 1+(Const 0) ^ x = Op3 (Core.Mux typeOf) (Op2 (Core.Eq typeOf) x 0) (1) (0) (Const 1) ^ _ = Const 1 (Const x) ^ (Const y) = Const (x P.^ y)-(Const 2) ^ y = (Const 2) .<<. y+(Const 2) ^ y = (Const 1) .<<. y x ^ (Const y) = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x) _ ^ _ = Core.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant. (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"
+ src/Copilot/Language/Operators/Label.hs view
@@ -0,0 +1,21 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Let expressions.++{-# LANGUAGE Trustworthy #-}++module Copilot.Language.Operators.Label+ ( label+ ) where++import Copilot.Core (Typed)+import Copilot.Language.Stream (Stream (..))++--------------------------------------------------------------------------------++label :: (Typed a) => String -> Stream a -> Stream a+label = Label++--------------------------------------------------------------------------------
+ src/Copilot/Language/Operators/Propositional.hs view
@@ -0,0 +1,27 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE Trustworthy, FlexibleInstances, GADTs, MultiParamTypeClasses #-}++module Copilot.Language.Operators.Propositional (not) where++import Prelude (($))++import Copilot.Language.Spec (Prop (..))+import qualified Copilot.Language.Operators.Boolean as B++import Copilot.Theorem++--------------------------------------------------------------------------------++class Negatable a b where+ not :: a -> b++instance Negatable (Prop Existential) (Prop Universal) where+ not (Exists p) = Forall $ B.not p++instance Negatable (Prop Universal) (Prop Existential) where+ not (Forall p) = Exists $ B.not p++--------------------------------------------------------------------------------
src/Copilot/Language/Operators/Temporal.hs view
@@ -9,6 +9,7 @@ module Copilot.Language.Operators.Temporal ( (++) , drop+ , (#) ) where import Copilot.Core (Typed)@@ -28,3 +29,11 @@ drop _ ( Const j ) = Const j drop i ( Drop j s ) = Drop (fromIntegral i + j) s drop i s = Drop (fromIntegral i) s++(#) :: (Typed a, Typed b) => Stream a -> String -> Stream b+(#) = GetField+{-(ExternStruct cs sargs) # (Extern nm i) = Extern nm i+(ExternStruct cs sargs) # (ExternFun nm args i) = ExternFun nm args i+(ExternStruct cs sargs) # (ExternArray nm strm j i) = ExternArray nm strm j i+(ExternStruct cs sargs) # (ExternStruct nm args) = ExternStruct nm args-}+--(ExternStruct cs sargs) # name = GetField (ExternStruct cs sargs) name
src/Copilot/Language/Reify.hs view
@@ -20,36 +20,45 @@ import Copilot.Language.Spec import Copilot.Language.Stream (Stream (..), Arg (..)) +import Copilot.Theorem.Prove+ import Prelude hiding (id) import Data.IORef import System.Mem.StableName.Dynamic import System.Mem.StableName.Map (Map) import qualified System.Mem.StableName.Map as M-import Control.Monad (liftM)-+import Control.Monad (liftM, unless) -------------------------------------------------------------------------------- -reify :: Spec -> IO Core.Spec-reify spec =- do - analyze spec- let trigs = triggers $ runSpec spec- let obsvs = observers $ runSpec spec- let props = properties $ runSpec spec- refMkId <- newIORef 0- refVisited <- newIORef M.empty- refMap <- newIORef []- coreTriggers <- mapM (mkTrigger refMkId refVisited refMap) trigs- coreObservers <- mapM (mkObserver refMkId refVisited refMap) obsvs- coreProperties <- mapM (mkProperty refMkId refVisited refMap) props- coreStreams <- readIORef refMap- return $- Core.Spec+reify :: Spec' a -> IO Core.Spec+reify spec = do+ analyze spec+ let trigs = triggers $ runSpec spec+ let obsvs = observers $ runSpec spec+ let props = properties $ runSpec spec+ let thms = reverse $ theorems $ runSpec spec+ --let strs = structs $ runSpec spec+ refMkId <- newIORef 0+ refVisited <- newIORef M.empty+ refMap <- newIORef []+ coreTriggers <- mapM (mkTrigger refMkId refVisited refMap) trigs+ coreObservers <- mapM (mkObserver refMkId refVisited refMap) obsvs+ coreProperties <- mapM (mkProperty refMkId refVisited refMap) $ props ++ (map fst thms)+ --coreStructs <- mapM (mkStruct refMkId refVisited refMap) strs+ coreStreams <- readIORef refMap++ let cspec = Core.Spec { Core.specStreams = reverse coreStreams , Core.specObservers = coreObservers , Core.specTriggers = coreTriggers , Core.specProperties = coreProperties }+ --, Core.specStructs = coreStructs } + results <- sequence $ zipWith (prove cspec) (map (\(Property n _,_) -> n) thms) $ map snd thms+ unless (and results) $ putStrLn "Warning: failed to check some proofs."++ return cspec+ -------------------------------------------------------------------------------- {-# INLINE mkObserver #-}@@ -60,12 +69,11 @@ -> Observer -> IO Core.Observer mkObserver refMkId refStreams refMap (Observer name e) = do- w <- mkExpr refMkId refStreams refMap e- return $- Core.Observer- { Core.observerName = name- , Core.observerExpr = w- , Core.observerExprType = typeOf }+ w <- mkExpr refMkId refStreams refMap e+ return Core.Observer+ { Core.observerName = name+ , Core.observerExpr = w+ , Core.observerExprType = typeOf } -------------------------------------------------------------------------------- @@ -77,20 +85,19 @@ -> Trigger -> IO Core.Trigger mkTrigger refMkId refStreams refMap (Trigger name guard args) = do- w1 <- mkExpr refMkId refStreams refMap guard - args' <- mapM mkTriggerArg args- return $- Core.Trigger- { Core.triggerName = name- , Core.triggerGuard = w1 - , Core.triggerArgs = args' }+ w1 <- mkExpr refMkId refStreams refMap guard+ args' <- mapM mkTriggerArg args+ return Core.Trigger+ { Core.triggerName = name+ , Core.triggerGuard = w1+ , Core.triggerArgs = args' } where mkTriggerArg :: Arg -> IO Core.UExpr mkTriggerArg (Arg e) = do- w <- mkExpr refMkId refStreams refMap e- return $ Core.UExpr typeOf w+ w <- mkExpr refMkId refStreams refMap e+ return $ Core.UExpr typeOf w -------------------------------------------------------------------------------- @@ -102,14 +109,37 @@ -> Property -> IO Core.Property mkProperty refMkId refStreams refMap (Property name guard) = do- w1 <- mkExpr refMkId refStreams refMap guard + w1 <- mkExpr refMkId refStreams refMap guard+ return Core.Property+ { Core.propertyName = name+ , Core.propertyExpr = w1 }++--------------------------------------------------------------------------------++--{-# INLINE mkStruct #-}+{-mkStruct+ :: IORef Int+ -> IORef (Map Core.Id)+ -> IORef [Core.Stream]+ -> StructData+ -> IO Core.StructData+mkStruct refMkId refStreams refMap (StructData name fields) = do+ fields' <- mapM mkStructField fields return $- Core.Property- { Core.propertyName = name- , Core.propertyExpr = w1 }+ Core.StructData+ { Core.structName = name+ , Core.structFields = fields' } + where++ mkStructField :: String -> Arg -> IO (Core.Name, Core.UExpr)+ mkStructField cs (Arg e) = do+ w <- mkExpr refMkId refStreams refMap e+ return (cs, $ Core.UExpr typeOf w)+-} -------------------------------------------------------------------------------- + {-# INLINE mkExpr #-} mkExpr :: Typed a@@ -124,90 +154,139 @@ where go :: Typed a => Stream a -> IO (Core.Expr a)- go e0 =- case e0 of+ go e0 = case e0 of - ------------------------------------------------------+ ------------------------------------------------------ + Append _ _ _ -> do+ s <- mkStream refMkId refStreams refMap e0+ return $ Core.Drop typeOf 0 s++ ------------------------------------------------------++ Drop k e1 -> case e1 of Append _ _ _ -> do- s <- mkStream refMkId refStreams refMap e0- return $ Core.Drop typeOf 0 s+ s <- mkStream refMkId refStreams refMap e1+ return $ Core.Drop typeOf (fromIntegral k) s+ _ -> impossible "mkExpr" "copilot-language" - ------------------------------------------------------+ ------------------------------------------------------ - Drop k e1 ->- case e1 of- Append _ _ _ -> do- s <- mkStream refMkId refStreams refMap e1- return $ Core.Drop typeOf (fromIntegral k) s- _ -> impossible "mkExpr" "copilot-language"+ Const x -> return $ Core.Const typeOf x - ------------------------------------------------------+ ------------------------------------------------------ - Const x -> return $ Core.Const typeOf x+ Local e f -> do+ id <- mkId refMkId+ let cs = "local_" ++ show id+ w1 <- go e+ w2 <- go (f (Var cs))+ return $ Core.Local typeOf typeOf cs w1 w2 - ------------------------------------------------------+ ------------------------------------------------------ - Local e f -> do- id <- mkId refMkId- let cs = "local_" ++ show id- w1 <- go e- w2 <- go (f (Var cs))- return $ Core.Local typeOf typeOf cs w1 w2+ Label s e -> do+ w <- go e+ return $ Core.Label typeOf s w - ------------------------------------------------------+ ------------------------------------------------------ - Var cs -> return $ Core.Var typeOf cs+ Var cs -> return $ Core.Var typeOf cs - ------------------------------------------------------+ ------------------------------------------------------ - Extern cs mXs -> return $ Core.ExternVar typeOf cs mXs+ Extern cs mXs -> return $ Core.ExternVar typeOf cs mXs - ------------------------------------------------------+ ------------------------------------------------------ - ExternFun cs args interpExpr -> do- args' <- mapM mkFunArg args- w <- case interpExpr of- Nothing -> return Nothing- Just e -> liftM Just (go e)- return $ Core.ExternFun typeOf cs args' w Nothing+ ExternFun cs args interpExpr -> do+ args' <- mapM mkFunArg args+ w <- case interpExpr of+ Nothing -> return Nothing+ Just e -> liftM Just (go e)+ return $ Core.ExternFun typeOf cs args' w Nothing - ------------------------------------------------------+ ------------------------------------------------------ - ExternArray cs e size mXs -> do- w <- go e- return $ Core.ExternArray typeOf typeOf cs size w mXs Nothing+ ExternArray cs e size mXs -> do+ w <- go e+ return $ Core.ExternArray typeOf typeOf cs size w mXs Nothing - ------------------------------------------------------+ ------------------------------------------------------ - Op1 op e -> do- w <- go e- return $ Core.Op1 op w+ ExternStruct cs sargs -> do+ args' <- mapM (\(name, Arg e) -> mkStrArg (name, Arg e)) sargs+ return $ Core.ExternStruct typeOf cs args' Nothing - ------------------------------------------------------+ ------------------------------------------------------ - Op2 op e1 e2 -> do- w1 <- go e1- w2 <- go e2- return $ Core.Op2 op w1 w2+ GetField struct field -> do+ s <- go struct+ return $ Core.GetField typeOf typeOf s field+ {- ISSUE: UNLIKE APPEND, GETFIELD DOES NOT HAVE CONSISTENT RETURN TYPE+ --> NEED TO PROPERLY DEFINE GETFIELD IN EXPR+ --> IMPLEMENT GETFIELD FROM CORE THROUGH LANGUAGE -} - ------------------------------------------------------+ ------------------------------------------------------ - Op3 op e1 e2 e3 -> do- w1 <- go e1- w2 <- go e2- w3 <- go e3- return $ Core.Op3 op w1 w2 w3+ Op1 op e -> do+ w <- go e+ return $ Core.Op1 op w - ------------------------------------------------------+ ------------------------------------------------------ + Op2 op e1 e2 -> do+ w1 <- go e1+ w2 <- go e2+ return $ Core.Op2 op w1 w2++ ------------------------------------------------------++ Op3 op e1 e2 e3 -> do+ w1 <- go e1+ w2 <- go e2+ w3 <- go e3+ return $ Core.Op3 op w1 w2 w3++ ------------------------------------------------------+ mkFunArg :: Arg -> IO Core.UExpr mkFunArg (Arg e) = do- w <- mkExpr refMkId refStreams refMap e- return $ Core.UExpr typeOf w+ w <- mkExpr refMkId refStreams refMap e+ return $ Core.UExpr typeOf w + mkStrArg :: (Core.Name, Arg) -> IO (Core.Name, Core.UExpr)+ mkStrArg (name, Arg e) = do+ w <- mkExpr refMkId refStreams refMap e+ return $ (name, Core.UExpr typeOf w)++ {-mkStructArg :: StructArg -> IO Core.SExpr+ mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do+ w <- mkExpr refMkId refStreams refMap a+ return $ Core.SExpr n $ Core.UExpr typeOf w+-} -------------------------------------------------------------------------------- +--{-# INLINE mkStruct #-}+{-mkStruct+ :: IORef Int+ -> IORef (Map Core.Id)+ -> IORef [Core.Stream]+ -> StructData+ -> IO Core.StructData+mkStruct refMkId refStreams refMap (StructData name sargs) = trace (show name) $ do+ args' <- mapM mkStructArg sargs+ return $+ Core.StructData+ { Core.structName = name+ , Core.structInst = Core.ExternStruct typeOf "" args' Nothing }+ where+ mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do+ w <- mkExpr refMkId refStreams refMap a+ return $ Core.SExpr n $ Core.UExpr typeOf w-}++--------------------------------------------------------------------------------+ {-# INLINE mkStream #-} mkStream :: Typed a@@ -216,23 +295,21 @@ -> IORef [Core.Stream] -> Stream a -> IO Id-mkStream refMkId refStreams refMap e0 =- do- dstn <- makeDynStableName e0- let Append buf _ e = e0 -- avoids warning- mk <- haveVisited dstn- case mk of- Just id_ -> return id_- Nothing -> addToVisited dstn buf e+mkStream refMkId refStreams refMap e0 = do+ dstn <- makeDynStableName e0+ let Append buf _ e = e0 -- avoids warning+ mk <- haveVisited dstn+ case mk of+ Just id_ -> return id_+ Nothing -> addToVisited dstn buf e where {-# INLINE haveVisited #-} haveVisited :: DynStableName -> IO (Maybe Int)- haveVisited dstn =- do- tab <- readIORef refStreams- return (M.lookup dstn tab)+ haveVisited dstn = do+ tab <- readIORef refStreams+ return (M.lookup dstn tab) {-# INLINE addToVisited #-} addToVisited@@ -241,18 +318,17 @@ -> [a] -> Stream a -> IO Id- addToVisited dstn buf e =- do- id <- mkId refMkId- modifyIORef refStreams (M.insert dstn id)- w <- mkExpr refMkId refStreams refMap e- modifyIORef refMap $ (:)- Core.Stream- { Core.streamId = id- , Core.streamBuffer = buf- , Core.streamExpr = w- , Core.streamExprType = typeOf }- return id+ addToVisited dstn buf e = do+ id <- mkId refMkId+ modifyIORef refStreams (M.insert dstn id)+ w <- mkExpr refMkId refStreams refMap e+ modifyIORef refMap $ (:)+ Core.Stream+ { Core.streamId = id+ , Core.streamBuffer = buf+ , Core.streamExpr = w+ , Core.streamExprType = typeOf }+ return id --------------------------------------------------------------------------------
src/Copilot/Language/Spec.hs view
@@ -7,56 +7,66 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-} module Copilot.Language.Spec- ( Spec+ ( Spec, Spec' , runSpec , SpecItem , Observer (..)- , observer- , observers+ , observer, observers , Trigger (..)- , triggers- , trigger+ , trigger, triggers , arg , Property (..)- , prop- , properties+ , Prop (..)+ , prop, properties+ , theorem, theorems+ , forall, exists+ , extractProp+ , Universal, Existential ) where +import Prelude hiding (not)+ import Control.Monad.Writer import Data.List (foldl')+--import Data.Maybe (fromMaybe) +--import Copilot.Core (Typed, Struct) import Copilot.Core (Typed) import qualified Copilot.Core as Core import Copilot.Language.Stream +import Copilot.Theorem.Prove+ -------------------------------------------------------------------------------- type Spec = Writer [SpecItem] ()+type Spec' a = Writer [SpecItem] a -------------------------------------------------------------------------------- -runSpec :: Spec -> [SpecItem]-runSpec = execWriter +runSpec :: Spec' a -> [SpecItem]+runSpec = execWriter -------------------------------------------------------------------------------- observers :: [SpecItem] -> [Observer]-observers = +observers = foldl' lets' [] where lets' ls e =- case e of + case e of ObserverItem l -> l : ls _ -> ls triggers :: [SpecItem] -> [Trigger]-triggers = +triggers = foldl' triggers' [] where triggers' ls e =- case e of + case e of TriggerItem t -> t : ls _ -> ls @@ -69,12 +79,22 @@ PropertyItem p -> p : ls _ -> ls +theorems :: [SpecItem] -> [(Property, UProof)]+theorems =+ foldl' theorems' []+ where+ theorems' ls e =+ case e of+ TheoremItem p -> p : ls+ _ -> ls+ -------------------------------------------------------------------------------- data SpecItem = ObserverItem Observer | TriggerItem Trigger | PropertyItem Property+ | TheoremItem (Property, UProof) -------------------------------------------------------------------------------- @@ -83,32 +103,73 @@ -------------------------------------------------------------------------------- +observer :: Typed a => String -> Stream a -> Spec+observer name e = tell [ObserverItem $ Observer name e]++--------------------------------------------------------------------------------++data Trigger where+ Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger++--------------------------------------------------------------------------------++trigger :: String -> Stream Bool -> [Arg] -> Spec+trigger name e args = tell [TriggerItem $ Trigger name e args]++--------------------------------------------------------------------------------+ data Property where Property :: String -> Stream Bool -> Property -------------------------------------------------------------------------------- -prop :: String -> Stream Bool -> Spec-prop name e = tell [PropertyItem $ Property name e]+data Prop a where+ Forall :: Stream Bool -> Prop Universal+ Exists :: Stream Bool -> Prop Existential ---------------------------------------------------------------------------------+forall :: Stream Bool -> Prop Universal+forall = Forall -observer :: Typed a => String -> Stream a -> Spec-observer name e = tell [ObserverItem $ Observer name e]+exists :: Stream Bool -> Prop Existential+exists = Exists +extractProp :: Prop a -> Stream Bool+extractProp (Forall p) = p+extractProp (Exists p) = p+ -------------------------------------------------------------------------------- -data Trigger where- Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger+prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)+prop name e = tell [PropertyItem $ Property name (extractProp e)]+ >> return (PropRef name) -------------------------------------------------------------------------------- -trigger :: String -> Stream Bool -> [Arg] -> Spec-trigger name e args = tell [TriggerItem $ Trigger name e args]+theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)+theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]+ >> return (PropRef name) -------------------------------------------------------------------------------- arg :: Typed a => Stream a -> Arg arg = Arg +--------------------------------------------------------------------------------++{-+-- | Struct operator.++-- Look up the given struct x, and return field y (which should be a stream?)+(#) :: Typed a => Core.StructData -> String -> Stream a+(Core.StructData {Core.structName = x, Core.structArgs = y})#z = getField x z+ where+ getField struct_nm field_nm =+ let test = find (\(Core.StructData name _) -> name == struct_nm) structs in+ case test of+ Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"+ Just element ->+ fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structArgs))+ (error "No field by the name of \"" ++ field_nm ++ "\"") element+--(Core.StructData l m)#n = Op2 (Core.GetField Core.typeOf) (Core.StructData l m) n+-} --------------------------------------------------------------------------------
src/Copilot/Language/Stream.hs view
@@ -12,6 +12,7 @@ module Copilot.Language.Stream ( Stream (..) , Arg (..) + , StructArg (..) ) where import Copilot.Core (Typed, typeOf)@@ -34,6 +35,10 @@ => String -> [Arg] -> Maybe (Stream a) -> Stream a ExternArray :: (Typed a, Typed b, Integral a) => String -> Stream a -> Int -> Maybe [[b]] -> Stream b+ ExternStruct:: Typed a+ => String -> [(String, Arg)] -> Stream a+ GetField :: (Typed a, Typed b)+ => Stream a -> String -> Stream b Local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b Var :: Typed a @@ -44,11 +49,14 @@ => Core.Op2 a b c -> Stream a -> Stream b -> Stream c Op3 :: (Typed a, Typed b, Typed c, Typed d) => Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d+ Label :: Typed a => String -> Stream a -> Stream a -------------------------------------------------------------------------------- data Arg where Arg :: Typed a => Stream a -> Arg++data StructArg = StructArg { name_ :: String, arg' :: Arg } --------------------------------------------------------------------------------