copilot-core 2.2.1 → 3.0

raw patch · 18 files changed

+300/−520 lines, 18 filesdep −pretty-ncolsdep ~basedep ~containersdep ~mtlnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies removed: pretty-ncols

Dependency ranges changed: base, containers, mtl, pretty, random

API changes (from Hackage documentation)

Files

• README.md +23/−51
• copilot-core.cabal +12/−21
• src/Copilot/Compile/Header/C99.hs +0/−223
• src/Copilot/Core.hs +2/−0
• src/Copilot/Core/Expr.hs +13/−19
• src/Copilot/Core/External.hs +5/−71
• src/Copilot/Core/Interpret/Eval.hs +17/−39
• src/Copilot/Core/Interpret/Render.hs +23/−20
• src/Copilot/Core/Locals.hs +1/−4
• src/Copilot/Core/MakeTags.hs +0/−14
• src/Copilot/Core/Operators.hs +7/−1
• src/Copilot/Core/PrettyDot.hs +1/−15
• src/Copilot/Core/PrettyPrint.hs +1/−10
• src/Copilot/Core/Random.hs +7/−5
• src/Copilot/Core/Spec.hs +3/−10
• src/Copilot/Core/Type.hs +111/−17
• src/Copilot/Core/Type/Array.hs +70/−0
• src/Copilot/Core/Type/Show.hs +4/−0

@@ -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).

@@ -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-  <https://github.com/leepike/copilot-discussion>.+  <https://github.com/Copilot-Language/copilot-discussion>.   .   Examples are available at-  <https://github.com/leepike/Copilot/tree/master/Examples>.+  <https://github.com/Copilot-Language/Copilot/tree/master/Examples>. -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 <dev@dedden.net> 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

@@ -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 <stdint.h>"-  , "#include <stdbool.h>"-  ]------------------------------------------------------------------------------------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----------------------------------------------------------------------------------

@@ -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

@@ -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 }

@@ -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  -------------------------------------------------------------------------------- 

@@ -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 ---------------------------------------------------------------------------------+-------------------------------------------------------------------------------

@@ -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)  -------------------------------------------------------------------------------- 

@@ -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

@@ -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)

@@ -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

@@ -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) )

@@ -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

@@ -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

@@ -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)] }  -------------------------------------------------------------------------------- 

@@ -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  --------------------------------------------------------------------------------

@@ -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

@@ -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"  --------------------------------------------------------------------------------