diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,61 +1,33 @@ [![Build Status](https://travis-ci.org/Copilot-Language/copilot-core.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-core) -Overview -======== -[copilot-core](http://hackage.haskell.org/package/copilot-core) The core -language, which efficiently represents Copilot expressions. The core is only of -interest to implementers wishing to add a new back-end to Copilot. +# Copilot: a stream DSL +The core language, which efficiently represents Copilot expressions. The core +is only of interest to implementers wishing to add a new back-end to Copilot. -Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in -Haskell that compiles into embedded C. Copilot is similar in spirit to -languages like Lustre. Copilot contains an interpreter, multiple back-end -compilers, and other verification tools. +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. -Installation -============ -The Copilot library is cabalized. Assuming you have cabal and the GHC compiler -installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the -easiest way to obtain these), it should merely be a matter of running - - cabal install copilot-core +Programs can be interpreted for testing, or translated C99 code to be +incorporated in a project, or as a standalone application. The C99 backend +ensures us that the output is constant in memory and time, making it suitable +for systems with hard realtime requirements. -However, we strongly recommend you install Copilot, which installs copilot-c99 -and other packages automatically. Execute - cabal install copilot +## Installation +Copilot-core can be found on +[Hackage](https://hackage.haskell.org/package/copilot-core). It is typically +only installed as part of the complete Copilot distribution. For installation +instructions, please refer to the [Copilot +website](https://copilot-language.github.io). -Resources -========= -To understand our use of Dynamic typing, please consult the following, -particularly the last document: -+ Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh, - "*Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages*", - Journal of Functional Programming vol. 19, p. 509-543, 2009. +## Further information +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) -+ Guillemette, Louis-Julien and Monnier, Stefan, - "*Type-Safe Code Transformations in Haskell*", - Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007. -+ Baars, Arthur I. and Swierstra, S. Doaitse, - "*Typing dynamic typing*", - ACM SIGPLAN Notices vol. 37, p. 157-166, 2002 - -Resources -========= -[copilot-core](http://hackage.haskell.org/package/copilot-core) is available on -Hackage. - -**Sources** for each package are available on Github as well. Just go to -[Github](github.com) and search for the package of interest. Feel free to fork! - -Copyright, License -================== -Copilot is distributed with the BSD3 license. The license file contains the -[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage. - -Thanks -====== -We are grateful for NASA Contract NNL08AD13T to [Galois, -Inc](http://corp.galois.com/) and the [National Institute of -Aerospace](http://www.nianet.org/), which partially supported this work. +## License +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot-core/master/LICENSE). diff --git a/copilot-core.cabal b/copilot-core.cabal --- a/copilot-core.cabal +++ b/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 2.2.1 +version: 3.0 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. @@ -9,16 +9,16 @@ Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at - . + . . Examples are available at - . + . -author: Lee Pike, Robin Morisset, Alwyn Goodloe, +author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller, Nis Nordbyop Wegmann license: BSD3 license-file: LICENSE -maintainer: leepike@gmail.com +maintainer: Frank Dedden stability: Experimental category: Language, Embedded build-type: Simple @@ -26,7 +26,7 @@ source-repository head type: git - location: git://github.com/leepike/copilot-core.git + location: https://github.com/Copilot-Language/copilot-core.git library @@ -37,28 +37,18 @@ ghc-options: -Wall -fwarn-tabs - -auto-all - -caf-all -fno-warn-orphans - -fpackage-trust - -trust=array - -trust=base - -trust=containers - -trust=random - build-depends: - containers >= 0.4, - base >= 4.0 && < 5, - pretty >= 1.0, - random > 1.0, - pretty-ncols >= 0.1, - mtl >= 2.0, + base >= 4.9 && < 5, + containers >= 0.4 && < 0.7, + pretty >= 1.0 && < 1.2, + random > 1.0 && < 1.2, + mtl >= 2.0 && < 2.3, dlist exposed-modules: - Copilot.Compile.Header.C99 Copilot.Core Copilot.Core.Error Copilot.Core.Expr @@ -74,6 +64,7 @@ Copilot.Core.Random.Gen Copilot.Core.Random.Weights Copilot.Core.Type + Copilot.Core.Type.Array Copilot.Core.Type.Dynamic Copilot.Core.Type.Equality Copilot.Core.Type.Eq diff --git a/src/Copilot/Compile/Header/C99.hs b/src/Copilot/Compile/Header/C99.hs deleted file mode 100644 --- a/src/Copilot/Compile/Header/C99.hs +++ /dev/null @@ -1,223 +0,0 @@ --------------------------------------------------------------------------------- --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. --------------------------------------------------------------------------------- - --- | Generates a C99 header from a copilot-specification. The functionality --- provided by the header must be implemented by back-ends targetting C99. - -{-# LANGUAGE Safe #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE Rank2Types #-} - -module Copilot.Compile.Header.C99 - ( genC99Header - , c99HeaderName - ) where - -import Copilot.Core -import Data.List (intersperse, nubBy) -import Text.PrettyPrint.HughesPJ -import Prelude hiding (unlines) - --------------------------------------------------------------------------------- - -genC99Header :: Maybe String -> FilePath -> Spec -> IO () -genC99Header mprefix path spec = - let - filePath = path ++ "/" ++ prefix ++ "copilot.h" - prefix = case mprefix of - Just cs -> cs ++ "_" - _ -> "" - in - writeFile filePath (c99Header prefix spec) - -c99HeaderName :: Maybe String -> String -c99HeaderName (Just cs) = cs ++ "_" ++ "copilot.h" -c99HeaderName _ = "copilot.h" - -c99Header :: String -> Spec -> String -c99Header prefix spec = render $ vcat $ - [ text "/* Generated by Copilot Core." <+> text "*/" - , text "" - , ppHeaders - , text "" - , text "/* Observers (defined by Copilot): */" - , text "" - , ppObservers prefix (specObservers spec) - , text "" - , text "/* Triggers (must be defined by user): */" - , text "" - , ppTriggerPrototypes prefix (specTriggers spec) - , text "" - , text "/* External structs (must be defined by user): */" - , text "" - , ppExternalStructs (externStructs spec) - , text "" - , text "/* External variables (must be defined by user): */" - , text "" - , ppExternalVariables (externVars spec) - , text "" - , text "/* External arrays (must be defined by user): */" - , text "" - , ppExternalArrays (externArrays spec) - , text "" - , text "/* External functions (must be defined by user): */" - , text "" - , ppExternalFunctions (externFuns spec) - , text "" - , text "/* Step function: */" - , text "" - , ppStep prefix - ] - --------------------------------------------------------------------------------- - -ppHeaders :: Doc -ppHeaders = unlines - [ "#include " - , "#include " - ] - --------------------------------------------------------------------------------- - -ppObservers :: String -> [Observer] -> Doc -ppObservers prefix = vcat . map ppObserver - - where - - ppObserver :: Observer -> Doc - ppObserver - Observer - { observerName = name - , observerExprType = t } = - text "extern" <+> text (typeSpec (UType t)) <+> - text (prefix ++ name) <> text ";" - --------------------------------------------------------------------------------- - -ppTriggerPrototypes :: String -> [Trigger] -> Doc -ppTriggerPrototypes prefix = vcat . map ppTriggerPrototype - - where - - ppTriggerPrototype :: Trigger -> Doc - ppTriggerPrototype - Trigger - { triggerName = name - , triggerArgs = args } = - text "void" <+> text (prefix ++ name) <> - text "(" <> ppArgs args <> text ");" - - where - ppArgs :: [UExpr] -> Doc - ppArgs = hcat . intersperse (text ", ") . map ppArg - - ppArg :: UExpr -> Doc - ppArg UExpr { uExprType = t } = text (typeSpec (UType t)) - --------------------------------------------------------------------------------- - -ppExternalVariables :: [ExtVar] -> Doc -ppExternalVariables = vcat . map ppExternalVariable - -ppExternalVariable :: ExtVar -> Doc -ppExternalVariable - ExtVar - { externVarName = name - , externVarType = t } = - text "extern" <+> text (typeSpec t) <+> text name <> text ";" - --------------------------------------------------------------------------------- - -ppExternalArrays :: [ExtArray] -> Doc -ppExternalArrays = vcat . map ppExternalArray . nubBy eq - where - eq ExtArray { externArrayName = name1 } ExtArray { externArrayName = name2 } = - name1 == name2 - -ppExternalArray :: ExtArray -> Doc -ppExternalArray - ExtArray - { externArrayName = name - , externArrayElemType = t - , externArraySize = size } - = - text "extern" <+> text (typeSpec (UType t)) - <+> text name <> lbrack <> int size <> rbrack - <> text ";" - --------------------------------------------------------------------------------- - -ppExternalFunctions :: [ExtFun] -> Doc -ppExternalFunctions = vcat . map ppExternalFunction . nubBy eq - where - eq ExtFun { externFunName = name1 } ExtFun { externFunName = name2 } = - name1 == name2 - -ppExternalFunction :: ExtFun -> Doc -ppExternalFunction - ExtFun - { externFunName = name - , externFunType = t - , externFunArgs = args } = - text (typeSpec (UType t)) <+> text name <> - text "(" <> ppArgs args <> text ");" - - where - ppArgs :: [UExpr] -> Doc - ppArgs = hcat . intersperse (text ",") . map ppArg - - ppArg :: UExpr -> Doc - ppArg UExpr { uExprType = t1 } = text (typeSpec (UType t1)) - --------------------------------------------------------------------------------- - -ppExternalStructs :: [ExtStruct] -> Doc -ppExternalStructs = vcat . map ppExternalStruct . nubBy eq - where - eq ExtStruct { externStructName = name1 } ExtStruct { externStructName = name2 } = - name1 == name2 - -ppExternalStruct :: ExtStruct -> Doc -ppExternalStruct - ExtStruct - { externStructName = name - , externStructArgs = args } = - hang (hang (text "struct" <+> text name <+> text "{") 1 (nest 1 (ppStructArgs args))) 1 (text "};") - - where - ppStructArgs :: [(Name, UExpr)] -> Doc - ppStructArgs = vcat . map ppStructArg - - ppStructArg :: (Name, UExpr) -> Doc - ppStructArg (name', UExpr { uExprType = t1 }) = text (typeSpec (UType t1)) <+> - text name' <> text ";" - --------------------------------------------------------------------------------- - -typeSpec :: UType -> String -typeSpec UType { uTypeType = t } - = case t of - Bool -> "bool" - Int8 -> "int8_t" - Int16 -> "int16_t" - Int32 -> "int32_t" - Int64 -> "int64_t" - Word8 -> "uint8_t" - Word16 -> "uint16_t" - Word32 -> "uint32_t" - Word64 -> "uint64_t" - Float -> "float" - Double -> "double" - --------------------------------------------------------------------------------- - -ppStep :: String -> Doc -ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "(void);" - --------------------------------------------------------------------------------- - -unlines :: [String] -> Doc -unlines = vcat . map text - --------------------------------------------------------------------------------- diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs --- a/src/Copilot/Core.hs +++ b/src/Copilot/Core.hs @@ -32,6 +32,7 @@ , module Copilot.Core.Operators , module Copilot.Core.Spec , module Copilot.Core.Type + , module Copilot.Core.Type.Array , module Copilot.Core.Type.Uninitialized , module Data.Int , module Data.Word @@ -44,6 +45,7 @@ import Copilot.Core.Operators import Copilot.Core.Spec import Copilot.Core.Type +import Copilot.Core.Type.Array import Copilot.Core.Type.Uninitialized import Data.Int import Data.Word diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs --- a/src/Copilot/Core/Expr.hs +++ b/src/Copilot/Core/Expr.hs @@ -10,7 +10,6 @@ , Name , Expr (..) , UExpr (..) - , SExpr (..) , DropIdx , Tag ) where @@ -19,6 +18,8 @@ import Copilot.Core.Type (Type) import Data.Word (Word32) +import Data.Typeable (Typeable) + -------------------------------------------------------------------------------- -- | A stream identifier. @@ -42,28 +43,21 @@ -------------------------------------------------------------------------------- data Expr a where - Const :: Type a -> a -> Expr a - Drop :: Type a -> DropIdx -> Id -> Expr a - Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b - Var :: Type a -> Name -> Expr a - ExternVar :: Type a -> Name -> Maybe [a] -> Expr a - ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) + Const :: Typeable a => Type a -> a -> Expr a + Drop :: Typeable a => Type a -> DropIdx -> Id -> Expr a + Local :: Typeable a => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b + Var :: Typeable a => Type a -> Name -> Expr a + ExternVar :: Typeable a => Type a -> Name -> Maybe [a] -> Expr a + ExternFun :: Typeable a => Type a -> Name -> [UExpr] -> Maybe (Expr a) -> Maybe Tag -> Expr a - ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a - -> Maybe [[b]] -> Maybe Tag -> Expr b - ExternStruct :: Type a -> Name -> [(Name, UExpr)] -> Maybe Tag -> Expr a - GetField :: Type a -> Type b -> Expr a -> Name -> Expr b - Op1 :: Op1 a b -> Expr a -> Expr b - Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c - Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d - Label :: Type a -> String -> Expr a -> Expr a + Op1 :: Typeable a => Op1 a b -> Expr a -> Expr b + Op2 :: (Typeable a, Typeable b) => Op2 a b c -> Expr a -> Expr b -> Expr c + Op3 :: (Typeable a, Typeable b, Typeable c) => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d + Label :: Typeable a => Type a -> String -> Expr a -> Expr a -------------------------------------------------------------------------------- -- | A untyped expression (no phantom type). -data UExpr = forall a. UExpr +data UExpr = forall a. Typeable a => UExpr { uExprType :: Type a , uExprExpr :: Expr a } - --- | An expression for Struct args -data SExpr = SExpr { sname :: String, uexpr :: UExpr } diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs --- a/src/Copilot/Core/External.hs +++ b/src/Copilot/Core/External.hs @@ -7,8 +7,8 @@ {-# LANGUAGE Rank2Types #-} module Copilot.Core.External - ( ExtVar (..), ExtArray (..), ExtFun (..), ExtStruct (..) - , externVars, externArrays, externFuns, externStructs + ( ExtVar (..), ExtFun (..) + , externVars, externFuns ) where import Copilot.Core.Expr @@ -18,31 +18,20 @@ import Data.List (nubBy) import Prelude hiding (all, concat, foldr) +import Data.Typeable (Typeable) + -------------------------------------------------------------------------------- data ExtVar = ExtVar { externVarName :: Name , externVarType :: UType } -data ExtArray = forall a b . Integral a => ExtArray - { externArrayName :: Name - , externArrayElemType :: Type b - , externArrayIdx :: Expr a - , externArrayIdxType :: Type a - , externArraySize :: Int - , externArrayTag :: Maybe Tag } - -data ExtFun = forall a . ExtFun +data ExtFun = forall a . Typeable a => ExtFun { externFunName :: Name , externFunType :: Type a , externFunArgs :: [UExpr] , externFunTag :: Maybe Tag } -data ExtStruct = ExtStruct - { externStructName :: Name - , externStructArgs :: [(Name, UExpr)] - , externStructTag :: Maybe Tag } - -------------------------------------------------------------------------------- externVars :: Spec -> [ExtVar] @@ -59,10 +48,7 @@ Local _ _ _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 Var _ _ -> empty ExternVar t name _ -> singleton (ExtVar name (UType t)) - ExternArray _ _ _ _ e _ _ -> externVarsExpr e ExternFun _ _ ues _ _ -> concat (map externVarsUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty Op1 _ e -> externVarsExpr e Op2 _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 Op3 _ e1 e2 e3 -> externVarsExpr e1 `append` @@ -75,33 +61,6 @@ -------------------------------------------------------------------------------- -externArrays :: Spec -> [ExtArray] -externArrays = toList . all externArraysExpr - -externArraysExpr :: Expr a -> DList ExtArray -externArraysExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ e1 e2 -> externArraysExpr e1 `append` externArraysExpr e2 - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternArray t1 t2 name - size idx _ tag -> singleton (ExtArray name t2 idx t1 size tag) - ExternFun _ _ ues _ _ -> concat (map externArraysUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty - Op1 _ e -> externArraysExpr e - Op2 _ e1 e2 -> externArraysExpr e1 `append` externArraysExpr e2 - Op3 _ e1 e2 e3 -> externArraysExpr e1 `append` - externArraysExpr e2 `append` - externArraysExpr e3 - Label _ _ e -> externArraysExpr e - -externArraysUExpr :: UExpr -> DList ExtArray -externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e - --------------------------------------------------------------------------------- - externFuns :: Spec -> [ExtFun] externFuns = toList . all externFunsExpr @@ -112,10 +71,7 @@ Local _ _ _ e1 e2 -> externFunsExpr e1 `append` externFunsExpr e2 Var _ _ -> empty ExternVar _ _ _ -> empty - ExternArray _ _ _ _ idx _ _ -> externFunsExpr idx ExternFun t name ues _ tag -> concat $ singleton (ExtFun name t ues tag) : (map externFunsUExpr ues) - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty Op1 _ e -> externFunsExpr e Op2 _ e1 e2 -> externFunsExpr e1 `append` externFunsExpr e2 Op3 _ e1 e2 e3 -> externFunsExpr e1 `append` @@ -126,28 +82,6 @@ externFunsUExpr :: UExpr -> DList ExtFun externFunsUExpr UExpr { uExprExpr = e } = externFunsExpr e - --------------------------------------------------------------------------------- - -externStructs :: Spec -> [ExtStruct] -externStructs = toList . all externStructsExpr - -externStructsExpr :: Expr a -> DList ExtStruct -externStructsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ _ _ -> empty - Var _ _ -> empty - ExternVar _ _ _ -> empty - ExternArray _ _ _ _ _ _ _ -> empty - ExternFun _ _ _ _ _ -> empty - ExternStruct _ name ses tag -> singleton (ExtStruct name ses tag) - -- all expressions in a struct are typed - GetField _ _ _ _ -> empty - Op1 _ _ -> empty - Op2 _ _ _ -> empty - Op3 _ _ _ _ -> empty - Label _ _ e -> externStructsExpr e -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs --- a/src/Copilot/Core/Interpret/Eval.hs +++ b/src/Copilot/Core/Interpret/Eval.hs @@ -16,7 +16,6 @@ ) where import Copilot.Core -import Copilot.Core.Type.Dynamic import Copilot.Core.Type.Show (showWithType, ShowType) import Prelude hiding (id) @@ -28,8 +27,10 @@ import Data.Maybe (fromJust) import Data.Bits import Control.Exception (Exception, throw) -import Data.Typeable +import Data.Dynamic (Dynamic, fromDynamic, toDyn) +import Data.Typeable (Typeable) + -------------------------------------------------------------------------------- data InterpException @@ -84,7 +85,7 @@ -------------------------------------------------------------------------------- -type Env nm = [(nm, DynamicF [] Type)] +type Env nm = [(nm, Dynamic)] -- -- | External arrays environment. -- type ArrEnv = [(Name, [DynamicF [] Type])] @@ -153,28 +154,24 @@ -------------------------------------------------------------------------------- -type LocalEnv = [(Name, Dynamic Type)] +type LocalEnv = [(Name, Dynamic)] -evalExpr_ :: Int -> Expr a -> LocalEnv -> Env Id -> a +evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a evalExpr_ k e0 locs strms = case e0 of Const _ x -> x Drop t i id -> - let Just xs = lookup id strms >>= fromDynF t in - reverse xs !! (fromIntegral i + k) + let Just buff = lookup id strms >>= fromDynamic in + reverse buff !! (fromIntegral i + k) Local t1 _ name e1 e2 -> let x = evalExpr_ k e1 locs strms in - let locs' = (name, toDyn t1 x) : locs in + let locs' = (name, toDyn x) : locs in x `seq` locs' `seq` evalExpr_ k e2 locs' strms - Var t name -> fromJust $ lookup name locs >>= fromDyn t + Var t name -> fromJust $ lookup name locs >>= fromDynamic ExternVar _ name xs -> evalExternVar k name xs ExternFun _ name _ expr _ -> --evalFunc k t name expr case expr of Nothing -> throw (NoExtsInterp name) Just e -> evalExpr_ k e locs strms - ExternArray _ _ name size idx xs _ -> evalArray k name evalIdx xs size - where evalIdx = evalExpr_ k idx locs strms - ExternStruct _ _ _ _ -> error "unimplemented" - GetField _ _ _ _ -> error "unimplemented" Op1 op e1 -> let ev1 = evalExpr_ k e1 locs strms in let op1 = evalOp1 op in @@ -231,25 +228,6 @@ -------------------------------------------------------------------------------- -evalArray :: Integral b => Int -> Name -> b -> Maybe [[a]] -> Int -> a -evalArray k name idx exts size = - case exts of - Nothing -> throw (NoExtsInterp name) - Just xs -> - case safeIndex k xs of - Nothing -> throw (NotEnoughValues name k) - Just arr -> -- convoluted form in case the array is env of infinite - -- length. - if length (take size arr) == size - && length (take (size+1) arr) == size - then case safeIndex (fromIntegral idx) arr of - Nothing -> throw (ArrayIdxOutofBounds - name (fromIntegral idx) size) - Just x -> x - else throw (ArrayWrongSize name size) - --------------------------------------------------------------------------------- - evalOp1 :: Op1 a b -> (a -> b) evalOp1 op = case op of Not -> P.not @@ -284,7 +262,7 @@ Sub _ -> (-) Mul _ -> (*) Mod _ -> (catchZero P.mod) - Div _ -> (catchZero P.div) + Div _ -> (catchZero P.quot) Fdiv _ -> (P./) Pow _ -> (P.**) Logb _ -> P.logBase @@ -311,11 +289,11 @@ -------------------------------------------------------------------------------- -initStrm :: Stream -> (Id, DynamicF [] Type) +initStrm :: Stream -> (Id, Dynamic) initStrm Stream { streamId = id , streamBuffer = buffer , streamExprType = t } = - (id, toDynF t (reverse buffer)) + (id, toDyn (reverse buffer)) -- XXX actually only need to compute until shortest stream is of length k -- XXX this should just be a foldl' over [0,1..k] @@ -332,10 +310,10 @@ evalStream Stream { streamId = id , streamExpr = e , streamExprType = t } = - let xs = fromJust $ lookup id strms >>= fromDynF t in + let xs = fromJust $ lookup id strms >>= fromDynamic in let x = evalExpr_ k e [] strms in let ls = x `seq` (x:xs) in - (id, toDynF t ls) + (id, toDyn ls) -------------------------------------------------------------------------------- @@ -375,7 +353,7 @@ -------------------------------------------------------------------------------- -evalExprs_ :: Int -> Expr a -> Env Id -> [a] +evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a] evalExprs_ k e strms = map (\i -> evalExpr_ i e [] strms) [0..(k-1)] @@ -388,4 +366,4 @@ if length ls' > i then Just (ls' !! i) else Nothing --------------------------------------------------------------------------------- +------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs --- a/src/Copilot/Core/Interpret/Render.hs +++ b/src/Copilot/Core/Interpret/Render.hs @@ -15,40 +15,43 @@ import Data.Maybe (catMaybes) import Copilot.Core.Interpret.Eval (Output, ExecTrace (..)) import qualified Data.Map as M -import Text.PrettyPrint.NCol (asColumns) +-- TODO: pretty-ncols is not updated yet to support >=base-4.11 +-- import Text.PrettyPrint.NCol (asColumns) import Text.PrettyPrint (Doc, ($$), (<>), text, render, empty) +import Prelude hiding ((<>)) + -------------------------------------------------------------------------------- renderAsTable :: ExecTrace -> String renderAsTable ExecTrace { interpTriggers = trigs - , interpObservers = obsvs } = - ( render - . asColumns - . transpose - . (:) (ppTriggerNames ++ ppObserverNames) - . transpose - ) (ppTriggerOutputs ++ ppObserverOutputs) + , interpObservers = obsvs } = "Rendering as table is not support, because pretty-ncols is not updated (yet) to newer base versions." + -- ( render + -- . asColumns + -- . transpose + -- . (:) (ppTriggerNames ++ ppObserverNames) + -- . transpose + -- ) (ppTriggerOutputs ++ ppObserverOutputs) - where + -- where - ppTriggerNames :: [Doc] - ppTriggerNames = map (text . (++ ":")) (M.keys trigs) + -- ppTriggerNames :: [Doc] + -- ppTriggerNames = map (text . (++ ":")) (M.keys trigs) - ppObserverNames :: [Doc] - ppObserverNames = map (text . (++ ":")) (M.keys obsvs) + -- ppObserverNames :: [Doc] + -- ppObserverNames = map (text . (++ ":")) (M.keys obsvs) - ppTriggerOutputs :: [[Doc]] - ppTriggerOutputs = map (map ppTriggerOutput) (M.elems trigs) + -- ppTriggerOutputs :: [[Doc]] + -- ppTriggerOutputs = map (map ppTriggerOutput) (M.elems trigs) - ppTriggerOutput :: Maybe [Output] -> Doc - ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")" - ppTriggerOutput Nothing = text "--" + -- ppTriggerOutput :: Maybe [Output] -> Doc + -- ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")" + -- ppTriggerOutput Nothing = text "--" - ppObserverOutputs :: [[Doc]] - ppObserverOutputs = map (map text) (M.elems obsvs) + -- ppObserverOutputs :: [[Doc]] + -- ppObserverOutputs = map (map text) (M.elems obsvs) -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Locals.hs b/src/Copilot/Core/Locals.hs --- a/src/Copilot/Core/Locals.hs +++ b/src/Copilot/Core/Locals.hs @@ -12,7 +12,7 @@ , locals ) where -import Copilot.Core +import Copilot.Core hiding (toList) import Data.DList (DList, empty, singleton, append, concat, toList) import Data.List (nubBy) import Prelude hiding (concat, foldr) @@ -78,9 +78,6 @@ Var _ _ -> empty ExternVar _ _ _ -> empty ExternFun _ _ _ _ _ -> empty - ExternArray _ _ _ _ _ _ _ -> empty - ExternStruct _ _ _ _ -> empty - GetField _ _ _ _ -> empty Op1 _ e -> locsExpr e Op2 _ e1 e2 -> locsExpr e1 `append` locsExpr e2 Op3 _ e1 e2 e3 -> locsExpr e1 `append` locsExpr e2 diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs --- a/src/Copilot/Core/MakeTags.hs +++ b/src/Copilot/Core/MakeTags.hs @@ -91,12 +91,6 @@ e' <- mkTagsExpr (propertyExpr p) return $ p { propertyExpr = e' } -mkTagsSExpr :: (Name, UExpr) -> State Int (Name, UExpr) -mkTagsSExpr (name, UExpr { uExprExpr = e, uExprType = t }) = - do - e' <- mkTagsExpr e - return (name, UExpr { uExprExpr = e', uExprType = t }) - mkTagsUExpr :: UExpr -> State Int UExpr mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } = do @@ -113,14 +107,6 @@ ExternFun t name args expr _ -> do args' <- mapM mkTagsUExpr args k <- next return $ ExternFun t name args' expr (Just k) - ExternArray t1 t2 name - size idx e _ -> do idx' <- mkTagsExpr idx - k <- next - return $ ExternArray t1 t2 name size idx' e (Just k) - ExternStruct t name sargs _ -> do args' <- mapM mkTagsSExpr sargs - k <- next - return $ ExternStruct t name args' (Just k) - GetField ts tf id name -> return $ GetField ts tf id name Op1 op e -> liftM (Op1 op) (mkTagsExpr e) Op2 op e1 e2 -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2) Op3 op e1 e2 e3 -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3) diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs --- a/src/Copilot/Core/Operators.hs +++ b/src/Copilot/Core/Operators.hs @@ -11,8 +11,10 @@ , Op3 (..) ) where -import Copilot.Core.Type (Type) +import Copilot.Core.Type (Type(..)) +import Copilot.Core.Type.Array (Array) import Data.Bits +import Data.Word (Word32) -------------------------------------------------------------------------------- @@ -45,6 +47,8 @@ BwNot :: Bits a => Type a -> Op1 a a -- Casting operator. Cast :: (Integral a, Num b) => Type a -> Type b -> Op1 a b + -- Struct operator. + GetField :: Type a -> Type b -> String -> Op1 a b -- | Binary operators. data Op2 a b c where @@ -77,6 +81,8 @@ BwXor :: Bits a => Type a -> Op2 a a a BwShiftL :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a BwShiftR :: ( Bits a, Integral b ) => Type a -> Type b -> Op2 a b a + -- Array operator. + Index :: Type (Array n t) -> Op2 (Array n t) Word32 t -- | Ternary operators. data Op3 a b c d where diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs --- a/src/Copilot/Core/PrettyDot.hs +++ b/src/Copilot/Core/PrettyDot.hs @@ -14,7 +14,7 @@ import Copilot.Core import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) -import Prelude hiding (id) +import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse) import Text.Printf @@ -45,20 +45,6 @@ (if bb then (text (printf "%s [label=\"externF: %s\",color=cyan4, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) <> (hcat (r1))) else (text (printf "%s [label=\"%s\",color=cyan4, style=filled]\n" (show ii::String) (mkExtTmpTag name tag))<> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) ,i1) - ExternArray _ _ name - _ idx _ tag -> let (r1,i1) = ppExprDot (ii+1) ii bb idx - in (if bb then (text (printf "%s [label=\"externA: %s\",color=cyan3, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> r1) else (text (printf "%s [label=\"%s\",color=cyan3, style=filled]\n" (show ii::String) (mkExtTmpTag name tag)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))) - ,i1) - - ExternStruct _ name args _ -> let (r1, i1) = ppUExprL (ii+1) ii bb (map snd $args) in - (text (printf "%s [label=\"externS: %s\",color=dodgerblue2, style=filled]\n" (show ii::String) (name::String)) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)) - <> (hcat (r1)),i1) - - GetField _ _ _ name -> (text (printf "%s [label=\"field: %s\",color=dodgerblue3, style=filled]\n" (show ii::String) (name::String) ) - <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1) - Local _ _ name e1 e2 -> let (r1, i1) = ppExprDot (ii+2) (ii+1) bb e1 in let (r2, i2) = ppExprDot (i1) ii bb e2 in (text (printf "%s [label=\"local:\",color=blue, style=filled]\n" (show ii::String) ) diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs --- a/src/Copilot/Core/PrettyPrint.hs +++ b/src/Copilot/Core/PrettyPrint.hs @@ -14,7 +14,7 @@ import Copilot.Core import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) -import Prelude hiding (id) +import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse) @@ -35,12 +35,6 @@ text "Extf_" <> (text name) <> lparen <> (hcat (punctuate (comma <> space) (map ppUExpr args)) <> rparen) - ExternArray _ _ name - _ idx _ _ -> text "Exta_" <> (text name) <> lbrack - <> ppExpr idx <> rbrack - ExternStruct _ name args _ -> text "struct" <+> doubleQuotes (text name <> lbrace - <> vcat (punctuate (semi <> space) (map ppSExpr $ args)) <> rbrace) - GetField _ _ _ name -> text "field" <+> doubleQuotes (text name) Local _ _ name e1 e2 -> text "local" <+> doubleQuotes (text name) <+> equals <+> ppExpr e1 $$ text "in" <+> ppExpr e2 Var _ name -> text "var" <+> doubleQuotes (text name) @@ -48,9 +42,6 @@ Op2 op e1 e2 -> ppOp2 op (ppExpr e1) (ppExpr e2) Op3 op e1 e2 e3 -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3) Label _ s e -> text "label "<> doubleQuotes (text s) <+> (ppExpr e) - -ppSExpr :: (Name, UExpr) -> Doc -ppSExpr (_, UExpr { uExprExpr = e0 }) = ppExpr e0 ppUExpr :: UExpr -> Doc ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0 diff --git a/src/Copilot/Core/Random.hs b/src/Copilot/Core/Random.hs --- a/src/Copilot/Core/Random.hs +++ b/src/Copilot/Core/Random.hs @@ -22,6 +22,8 @@ import System.Random (StdGen) import Control.Monad.Reader +import Data.Typeable (Typeable) + -------------------------------------------------------------------------------- randomSpec :: Int -> Weights -> StdGen -> Spec @@ -166,7 +168,7 @@ -------------------------------------------------------------------------------- -genExpr :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) +genExpr :: Typeable a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) genExpr extVars ss t = do dp <- depth ws <- weights @@ -261,7 +263,7 @@ ew <- genExpr extVars ss (typeOf :: Type Bool) return $ Op1 Not ew -genOp1Num :: Num a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) +genOp1Num :: (Typeable a, Num a) => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) genOp1Num extVars ss t = do ew <- genExpr extVars ss t opw <- elements [Abs t, Sign t] @@ -303,7 +305,7 @@ _ -> False in filter (not . p) ss -genOp2Num :: [DynExtVar] -> [StreamInfo] -> Type a -> NumWit a -> Gen (Expr a) +genOp2Num :: Typeable a => [DynExtVar] -> [StreamInfo] -> Type a -> NumWit a -> Gen (Expr a) genOp2Num extVars ss t NumWit = do ew1 <- genExpr extVars ss t ew2 <- genExpr extVars ss t @@ -312,7 +314,7 @@ , (Mul t) ] return $ Op2 opw ew1 ew2 -genOp2Integral :: +genOp2Integral :: Typeable a => [DynExtVar] -> [StreamInfo] -> Type a -> IntegralWit a -> Gen (Expr a) genOp2Integral extVars ss t IntegralWit = do ew1 <- genExpr extVars ss t @@ -321,7 +323,7 @@ , (Mod t) ] return $ Op2 opw ew1 ew2 -genOp3Mux :: [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) +genOp3Mux :: Typeable a => [DynExtVar] -> [StreamInfo] -> Type a -> Gen (Expr a) genOp3Mux extVars ss t = do ew1 <- genExpr extVars ss (typeOf :: Type Bool) ew2 <- genExpr extVars ss t diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs --- a/src/Copilot/Core/Spec.hs +++ b/src/Copilot/Core/Spec.hs @@ -11,16 +11,16 @@ , Trigger (..) , Spec (..) , Property (..) - , StructData (..) ) where import Copilot.Core.Expr (Name, Id, Expr, UExpr) import Copilot.Core.Type (Type, Typed) +import Data.Typeable (Typeable) -------------------------------------------------------------------------------- -- | A stream. -data Stream = forall a. Typed a => Stream +data Stream = forall a. (Typeable a, Typed a) => Stream { streamId :: Id , streamBuffer :: [a] , streamExpr :: Expr a @@ -29,7 +29,7 @@ -------------------------------------------------------------------------------- -- | An observer. -data Observer = forall a. Observer +data Observer = forall a. Typeable a => Observer { observerName :: Name , observerExpr :: Expr a , observerExprType :: Type a } @@ -48,13 +48,6 @@ data Property = Property { propertyName :: Name , propertyExpr :: Expr Bool } - --------------------------------------------------------------------------------- - --- | Struct representation as a bit array. -data StructData = StructData - { structName :: Name - , structFields :: [(Name, UExpr)] } -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs --- a/src/Copilot/Core/Type.hs +++ b/src/Copilot/Core/Type.hs @@ -5,19 +5,71 @@ -- | Typing for Core. {-# LANGUAGE Safe #-} -{-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-} +{-# LANGUAGE ExistentialQuantification + , GADTs + , KindSignatures + , ScopedTypeVariables + , UndecidableInstances + , FlexibleContexts + , DataKinds + , FlexibleInstances +#-} module Copilot.Core.Type ( Type (..) , Typed (..) , UType (..) - , SimpleType(..) + , SimpleType (..) + + , tysize + , tylength + + , Value (..) + , toValues + , Field (..) + , typename + + , Struct + , fieldname + , accessorname ) where import Data.Int import Data.Word import Copilot.Core.Type.Equality +import Copilot.Core.Type.Array +import Data.Typeable (Typeable, typeRep) + +import GHC.TypeLits (KnownNat, natVal, Symbol, KnownSymbol, symbolVal) +import Data.Proxy (Proxy (..)) + +import Data.List (intercalate) + + +class Struct a where + typename :: a -> String + toValues :: a -> [Value a] + +data Value a = forall s t. (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t) + +data Field (s :: Symbol) t = Field t + +fieldname :: forall s t. KnownSymbol s => Field s t -> String +fieldname _ = symbolVal (Proxy :: Proxy s) + +accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String +accessorname _ = symbolVal (Proxy :: Proxy s) + +instance (KnownSymbol s, Show t) => Show (Field s t) where + show f@(Field v) = fieldname f ++ ":" ++ show v + +instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where + show t = "<" ++ fields ++ ">" where + fields = intercalate "," $ map showfield (toValues t) + showfield (Value _ field) = show field + + data Type :: * -> * where Bool :: Type Bool Int8 :: Type Int8 @@ -30,7 +82,22 @@ Word64 :: Type Word64 Float :: Type Float Double :: Type Double + Array :: forall n t. ( KnownNat n + , Typed t + , Typed (InnerType t) + , Flatten t (InnerType t) + ) => Type t -> Type (Array n t) + Struct :: (Typed a, Struct a) => a -> Type a +-- Get the length of an array from its type +tylength :: forall n t. KnownNat n => Type (Array n t) -> Int +tylength _ = fromIntegral $ natVal (Proxy :: Proxy n) + +-- Get the total (nested) size of an array from its type +tysize :: forall n t. KnownNat n => Type (Array n t) -> Int +tysize ty@(Array ty'@(Array _)) = tylength ty * tylength ty' +tysize ty@(Array _ ) = tylength ty + instance EqualType Type where (=~=) Bool Bool = Just Refl (=~=) Int8 Int8 = Just Refl @@ -47,24 +114,45 @@ -------------------------------------------------------------------------------- -data SimpleType = SBool - | SInt8 - | SInt16 - | SInt32 - | SInt64 - | SWord8 - | SWord16 - | SWord32 - | SWord64 - | SFloat - | SDouble - deriving Eq +data SimpleType where + SBool :: SimpleType + SInt8 :: SimpleType + SInt16 :: SimpleType + SInt32 :: SimpleType + SInt64 :: SimpleType + SWord8 :: SimpleType + SWord16 :: SimpleType + SWord32 :: SimpleType + SWord64 :: SimpleType + SFloat :: SimpleType + SDouble :: SimpleType + SArray :: Type t -> SimpleType + SStruct :: SimpleType +{- This instance is necessary, otherwise the type of SArray can't be inferred -} +instance Eq SimpleType where + SBool == SBool = True + SInt8 == SInt8 = True + SInt16 == SInt16 = True + SInt32 == SInt32 = True + SInt64 == SInt64 = True + SWord8 == SWord8 = True + SWord16 == SWord16 = True + SWord32 == SWord32 = True + SWord64 == SWord64 = True + SFloat == SFloat = True + SDouble == SDouble = True + (SArray t1) == (SArray t2) | Just Refl <- t1 =~= t2 = True + | otherwise = False + SStruct == SStruct = True + _ == _ = False + -------------------------------------------------------------------------------- -class Typed a where - typeOf :: Type a +class (Show a, Typeable a) => Typed a where + typeOf :: Type a simpleType :: Type a -> SimpleType + simpleType _ = SStruct -------------------------------------------------------------------------------- @@ -101,10 +189,16 @@ instance Typed Double where typeOf = Double simpleType _ = SDouble +instance (Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) where + typeOf = Array typeOf + simpleType (Array t) = SArray t -------------------------------------------------------------------------------- -- | A untyped type (no phantom type). -data UType = forall a . UType { uTypeType :: Type a } +data UType = forall a . Typeable a => UType { uTypeType :: Type a } + +instance Eq UType where + UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2 -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Core/Type/Array.hs @@ -0,0 +1,70 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE Safe #-} + +-- | Implementation of an array that uses type literals to store length. No +-- explicit indexing is used for the input data. Supports arbitrary nesting of +-- arrays. + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} + +module Copilot.Core.Type.Array + ( Array + , array + , flatten + , size + , Flatten + , InnerType + , arrayelems + ) where + +import GHC.TypeLits (Nat, KnownNat, natVal) +import Data.Proxy (Proxy (..)) + +data Array (n :: Nat) t where + Array :: [t] -> Array n t + +instance Show t => Show (Array n t) where + show (Array xs) = show xs + +array :: forall n t. KnownNat n => [t] -> Array n t +array xs | datalen == typelen = Array xs + | otherwise = error errmsg where + datalen = length xs + typelen = fromIntegral $ natVal (Proxy :: Proxy n) + errmsg = "Length of data (" ++ show datalen ++ + ") does not match length of type (" ++ show typelen ++ ")." + + +type family InnerType x where + InnerType (Array _ x) = InnerType x + InnerType x = x + + +class Flatten a b where + flatten :: Array n a -> [b] + +instance Flatten a a where + flatten (Array xs) = xs + +instance Flatten a b => Flatten (Array n a) b where + flatten (Array xss) = concat $ map flatten xss + +instance Foldable (Array n) where + foldr f base (Array xs) = foldr f base xs + + +size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int +size xs = length $ (flatten xs :: [b]) + +arrayelems :: Array n a -> [a] +arrayelems (Array xs) = xs diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs --- a/src/Copilot/Core/Type/Show.hs +++ b/src/Copilot/Core/Type/Show.hs @@ -35,6 +35,8 @@ Word64 -> ShowWit Float -> ShowWit Double -> ShowWit + Array t -> ShowWit + Struct t -> ShowWit -------------------------------------------------------------------------------- @@ -52,6 +54,8 @@ Word64 -> "Word64" Float -> "Float" Double -> "Double" + Array t -> "Array " ++ showType t + Struct t -> "Struct" --------------------------------------------------------------------------------