packages feed

copilot-core (empty) → 0.2

raw patch · 26 files changed

+2368/−0 lines, 26 filesdep +basedep +containersdep +dlistsetup-changed

Dependencies added: base, containers, dlist, mtl, pretty, pretty-ncols, random

Files

+ LICENSE view
@@ -0,0 +1,29 @@+2009+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,59 @@+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 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.++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++However, we strongly recommend you install Copilot, which installs copilot-c99+and other packages automatically.  Execute++         cabal install copilot++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.+++ 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-core.cabal view
@@ -0,0 +1,68 @@+cabal-version:       >=1.10+name:                copilot-core+version:             0.2+synopsis:            An intermediate representation for Copilot.+description:         Intermediate representation for Copilot.+                     Strictly follows Haskell 2010 except for universal+                     and existential quantification.+author:              Lee Pike, Robin Morisset, Alwyn Goodloe,+                     Sebastian Niller, Nis Nordby Wegmann+license:             BSD3+license-file:        LICENSE+maintainer:          leepike@gmail.com+stability:           Experimental+category:            Language, Embedded+build-type:          Simple+extra-source-files:  README.md++source-repository head+    type:       git+    location:   git://github.com/niswegmann/copilot-core.git++library++  default-language:  Haskell2010++  hs-source-dirs:    src++  ghc-options:+    -Wall+    -fwarn-tabs+    -auto-all+    -caf-all+    -fno-warn-orphans+    --enable-library-profiling++  build-depends:+    containers >= 0.4 && < 1,+    base >= 4.0 && < 5,+    pretty >= 1.0,+    random > 1.0,+    pretty-ncols >= 0.1,+    mtl >= 2.0,+    dlist++  exposed-modules:++    Copilot.Compile.Header.C99+    Copilot.Core+    Copilot.Core.Error+    Copilot.Core.Expr+    Copilot.Core.External+    Copilot.Core.Interpret+    Copilot.Core.Interpret.Eval+    Copilot.Core.Interpret.Render+    Copilot.Core.MakeTags+    Copilot.Core.Operators+    Copilot.Core.Spec+    Copilot.Core.Spec.Locals+    Copilot.Core.Random+    Copilot.Core.Random.Gen+    Copilot.Core.Random.Weights+    Copilot.Core.Type+    Copilot.Core.Type.Dynamic+    Copilot.Core.Type.Equality+    Copilot.Core.Type.Show+    Copilot.Core.Type.Uninitialized+    Copilot.Core.PrettyPrint+    Copilot.Core.Version
+ src/Copilot/Compile/Header/C99.hs view
@@ -0,0 +1,198 @@+--------------------------------------------------------------------------------+-- 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 GADTs #-}++module Copilot.Compile.Header.C99+  ( genC99Header+  , c99HeaderName+  ) where++import Copilot.Core+import Copilot.Core.Version+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 v." <+> text version <+> 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 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 = vcat . 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 } =+        text "extern" <+> text (typeSpec (UType t)) <+> text "*" <+>+        text name <> 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))++--------------------------------------------------------------------------------++typeSpec :: UType -> String+typeSpec UType { uTypeType = t } = typeSpec' t++  where++  typeSpec' Bool = "bool"+  typeSpec' Int8   = "int8_t"+  typeSpec' Int16  = "int16_t"+  typeSpec' Int32  = "int32_t"+  typeSpec' Int64  = "int64_t"+  typeSpec' Word8  = "uint8_t"+  typeSpec' Word16 = "uint16_t"+  typeSpec' Word32 = "uint32_t"+  typeSpec' Word64 = "uint64_t"+  typeSpec' Float  = "float"+  typeSpec' Double = "double"++--------------------------------------------------------------------------------++ppStep :: String -> Doc+ppStep prefix = text "void" <+> text (prefix ++ "step") <> text "();"++--------------------------------------------------------------------------------++unlines :: [String] -> Doc+unlines = vcat . map text
+ src/Copilot/Core.hs view
@@ -0,0 +1,47 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Intermediate representation for Copilot specifications.+-- The form of the representation is based on this paper:+--+-- * 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.+--+-- The following article might also be useful:+--+-- * Guillemette, Louis-Julien and Monnier, Stefan,+-- \"/Type-Safe Code Transformations in Haskell/\",+-- Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007.+--+-- For examples of how to traverse a Copilot specification see+-- the source code of the interpreter+-- ("Copilot.Core.Interpret")+-- and the pretty-printer+-- ("Copilot.Core.PrettyPrint").++module Copilot.Core+  ( module Copilot.Core.Error+  , module Copilot.Core.Expr+  , module Copilot.Core.External+  , module Copilot.Core.MakeTags+  , module Copilot.Core.Operators+  , module Copilot.Core.Spec+  , module Copilot.Core.Type+  , module Copilot.Core.Type.Uninitialized+  , module Data.Int+  , module Data.Word+  ) where++import Copilot.Core.Error+import Copilot.Core.Expr+import Copilot.Core.External+import Copilot.Core.MakeTags+import Copilot.Core.Operators+import Copilot.Core.Spec+import Copilot.Core.Type+import Copilot.Core.Type.Uninitialized+import Data.Int+import Data.Word
+ src/Copilot/Core/Error.hs view
@@ -0,0 +1,16 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++module Copilot.Core.Error +  ( impossible+  , badUsage ) where++impossible :: String -> String -> a+impossible function package = +  error $ "Impossible error in function " ++ function ++ ", in package " ++ +    package ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " +++    "(remove spaces) or file a bug report on github.com."++badUsage :: String -> a+badUsage msg = error $ "Copilot error: " ++ msg ++ "."
+ src/Copilot/Core/Expr.hs view
@@ -0,0 +1,102 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs, ExistentialQuantification #-}++module Copilot.Core.Expr+  ( Id+  , Name+  , Expr (..)+  , UExpr (..)+  , DropIdx+  , Tag+  ) where++import Copilot.Core.Operators (Op1, Op2, Op3)+import Copilot.Core.Type (Type)+import Data.Word (Word16)++--------------------------------------------------------------------------------++-- | A stream identifier.+type Id = Int++--------------------------------------------------------------------------------++-- | A name of a trigger, an external variable, or an external function.+type Name = String++--------------------------------------------------------------------------------++-- | An index for the drop operator.+type DropIdx = Word16++--------------------------------------------------------------------------------++-- | A unique tag for external arrays/function calls.+type Tag = Int++--------------------------------------------------------------------------------++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+    -> Expr a+  ExternFun+    :: Type a+    -> Name+    -> [UExpr]+    -> Maybe Tag+    -> Expr a+  ExternArray+    :: Integral a+    => Type a+    -> Type b+    -> Name+    -> Expr a+    -> Maybe Tag+    -> 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++--------------------------------------------------------------------------------++-- | A untyped expression (no phantom type).+data UExpr = forall a . UExpr+  { uExprType :: Type a+  , uExprExpr :: Expr a }
+ src/Copilot/Core/External.hs view
@@ -0,0 +1,133 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE Rank2Types #-}++module Copilot.Core.External+  ( ExtVar (..), ExtArray (..), ExtFun (..)+  , externVars, externArrays, externFuns+  ) where++import Copilot.Core.Expr+import Copilot.Core.Type+import Copilot.Core.Spec+import Data.DList (DList, empty, singleton, append, concat, toList)+import Data.List (nubBy)+import Prelude hiding (all, concat, foldr)++--------------------------------------------------------------------------------++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+  , externArrayTag      :: Maybe Tag }++data ExtFun = forall a . ExtFun+  { externFunName      :: Name+  , externFunType      :: Type a+  , externFunArgs      :: [UExpr]+  , externFunTag       :: Maybe Tag }++--------------------------------------------------------------------------------++externVars :: Spec -> [ExtVar]+externVars = nubBy eqExt . toList . all externVarsExpr++  where++  eqExt :: ExtVar -> ExtVar -> Bool+  eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } =+    name1 == name2++externVarsExpr :: Expr a -> DList ExtVar+externVarsExpr e0 = case e0 of+  Const  _ _            -> empty+  Drop   _ _ _          -> empty+  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)+  Op1 _ e               -> externVarsExpr e+  Op2 _ e1 e2           -> externVarsExpr e1 `append` externVarsExpr e2+  Op3 _ e1 e2 e3        -> externVarsExpr e1 `append`+                           externVarsExpr e2 `append`+                           externVarsExpr e3++externVarsUExpr :: UExpr -> DList ExtVar+externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e++--------------------------------------------------------------------------------++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 idx tag -> singleton (ExtArray name t2 idx t1 tag)+  ExternFun _ _ ues _             -> concat (map externArraysUExpr ues)+  Op1 _ e                         -> externArraysExpr e+  Op2 _ e1 e2                     -> externArraysExpr e1 `append` externArraysExpr e2+  Op3 _ e1 e2 e3                  -> externArraysExpr e1 `append`+                                     externArraysExpr e2 `append`+                                     externArraysExpr e3++externArraysUExpr :: UExpr -> DList ExtArray+externArraysUExpr UExpr { uExprExpr = e } = externArraysExpr e++--------------------------------------------------------------------------------++externFuns :: Spec -> [ExtFun]+externFuns = toList . all externFunsExpr++externFunsExpr :: Expr a -> DList ExtFun+externFunsExpr e0 = case e0 of+  Const  _ _                  -> empty+  Drop   _ _ _                -> empty+  Local _ _ _ e1 e2           -> externFunsExpr e1 `append` externFunsExpr e2+  Var _ _                     -> empty+  ExternVar _ _               -> empty+  ExternArray _ _ _ idx _     -> externFunsExpr idx+  ExternFun t name ues tag    -> singleton (ExtFun name t ues tag)+  Op1 _ e                     -> externFunsExpr e+  Op2 _ e1 e2                 -> externFunsExpr e1 `append` externFunsExpr e2+  Op3 _ e1 e2 e3              -> externFunsExpr e1 `append`+                                 externFunsExpr e2 `append`+                                 externFunsExpr e3++--------------------------------------------------------------------------------++all :: (forall a . Expr a -> DList b) -> Spec -> DList b+all f spec =+  concat (fmap (allStream) (specStreams   spec)) `append`+  concat (fmap allTrigger  (specTriggers  spec)) `append`+  concat (fmap allObserver (specObservers spec))++  where+  +  allStream+    Stream { streamExpr = e } = f e++  allTrigger+    Trigger+      { triggerGuard = e+      , triggerArgs = args } = f e `append` concat (fmap allUExpr args)++  allUExpr+    (UExpr _ e1) = f e1++  allObserver+    Observer { observerExpr = e } = f e
+ src/Copilot/Core/Interpret.hs view
@@ -0,0 +1,27 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | An interpreter for Copilot specifications.++module Copilot.Core.Interpret+  ( ExtEnv (..)+  , Format (..)+  , interpret+  ) where++import Copilot.Core+import Copilot.Core.Interpret.Eval+import Copilot.Core.Interpret.Render+import Copilot.Core.Type.Show (ShowType(..))++data Format = Table | CSV++-- | Interprets a Copilot specification.+interpret :: Format -> Int -> ExtEnv -> Spec -> String+interpret format k exts spec =+  case format of+    Table -> renderAsTable e+    CSV   -> renderAsCSV e++  where e = eval Haskell k exts spec
+ src/Copilot/Core/Interpret/Eval.hs view
@@ -0,0 +1,310 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | A tagless interpreter for Copilot specifications.++{-# LANGUAGE GADTs, BangPatterns #-}++module Copilot.Core.Interpret.Eval+  ( ExtEnv (..)+  , Output+  , ExecTrace (..)+  , eval+  ) where++import Copilot.Core+import Copilot.Core.Type.Dynamic+import Copilot.Core.Type.Show (showWithType, ShowType)++import Data.List (transpose)+import qualified Data.Map as M+import Data.Map (Map)+import Data.Maybe (fromJust, catMaybes)+import Data.Bits++import Prelude hiding (id)+import qualified Prelude as P++--------------------------------------------------------------------------------++type Env nm = [(nm, DynamicF [] Type)]++-- | External arrays environment.+type ArrEnv = [(Name, [DynamicF [] Type])] ++-- | Environment for simulation.+data ExtEnv = ExtEnv { varEnv  :: Env Name+                     , arrEnv  :: ArrEnv +                     , funcEnv :: [(Name, Spec)] +                     }++--------------------------------------------------------------------------------++type Output = String++data ExecTrace = ExecTrace+    -- map from trigger names to their maybe output, which is a list of strings+    -- representing their valus.  (Nothing output if the guard for the trigger+    -- is false).+  { interpTriggers  :: Map String [Maybe [Output]]+    -- map from observer names to their outputs.  We also show observer outputs.+  , interpObservers :: Map String [Output] }+  deriving Show++--------------------------------------------------------------------------------++{-+eval :: Int -> Env Name -> Spec -> ExecTrace+eval k exts spec =+  let+    strms = fmap (evalStream     exts strms) (specStreams   spec)+    trigs = fmap (evalTrigger  k exts strms) (specTriggers  spec)+    obsvs = fmap (evalObserver k exts strms) (specObservers spec)+  in+    ExecTrace+      { interpTriggers  = M.fromList $+          zip (fmap triggerName  (specTriggers  spec)) trigs+      , interpObservers = M.fromList $+          zip (fmap observerName (specObservers spec)) obsvs+      }+-}++-- We could write this in a beautiful lazy style like above, but that creates a+-- space leak in the interpreter that is hard to fix while maintaining laziness.+-- We take a more brute-force appraoch below.+eval :: ShowType -> Int -> ExtEnv -> Spec -> ExecTrace+eval showType k exts spec =+--  let exts  = take k $ reverse exts'                          in++  let initStrms = map initStrm (specStreams spec)             in++  let strms = evalStreams k exts (specStreams spec) initStrms in++  let trigs = map (evalTrigger showType k exts strms) +                  (specTriggers spec)                         in++  let obsvs = map (evalObserver showType k exts strms) +                  (specObservers spec)                        in ++  strms `seq` ExecTrace+                { interpTriggers  = M.fromList $+                    zip (map triggerName  (specTriggers  spec)) trigs+                , interpObservers = M.fromList $+                    zip (map observerName (specObservers spec)) obsvs+                }++--------------------------------------------------------------------------------++type LocalEnv = [(Name, Dynamic Type)]++evalExpr_ :: Int -> Expr a -> ExtEnv -> LocalEnv -> Env Id -> a+evalExpr_ k e0 exts 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)+  Local t1 _ name e1 e2 -> +    let x     = evalExpr_ k e1 exts locs strms in+    let locs' = (name, toDyn t1 x) : locs  in+    x `seq` locs' `seq` evalExpr_ k e2 exts locs' strms+  Var t name                 -> fromJust $ lookup name locs >>= fromDyn t+  ExternVar t name           -> evalExtern k t name (varEnv exts)+  ExternFun t name _ _       -> evalFunc k t name exts+  ExternArray _ t name idx _ -> evalArray k t name evalIdx (arrEnv exts)+    where evalIdx = evalExpr_ k idx exts locs strms+  Op1 op e1              -> +    let ev1 = evalExpr_ k e1 exts locs strms in +    let op1 = evalOp1 op                     in+    ev1 `seq` op1 `seq` op1 ev1               +  Op2 op e1 e2           -> +    let ev1 = evalExpr_ k e1 exts locs strms in +    let ev2 = evalExpr_ k e2 exts locs strms in +    let op2 = evalOp2 op                     in+    ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2+  Op3 op e1 e2 e3        -> +    let ev1 = evalExpr_ k e1 exts locs strms in +    let ev2 = evalExpr_ k e2 exts locs strms in +    let ev3 = evalExpr_ k e3 exts locs strms in +    let op3 = evalOp3 op                     in+    ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3++--------------------------------------------------------------------------------++evalExtern :: Int -> Type a -> Name -> Env Name -> a+evalExtern k t name exts = +  case lookup name exts of+    Nothing -> badUsage $ "you need to supply a list of values for interpreting variable " ++ name+    Just dyn ->+      case fromDynF t dyn of+        Nothing -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."+        Just xs -> xs !! k++--------------------------------------------------------------------------------++evalFunc :: Int -> Type a -> Name -> ExtEnv -> a+evalFunc k t name exts  = +  case lookup name (funcEnv exts) of+    Nothing -> +      badUsage $ "to simulate a spec containing the external function "+                   ++ name ++ ", you need to include a stream to simulate it"++    -- We created this spec in Interpreter.hs, copilot-language, so it should+    -- contain no triggers and exactly one observer.+    Just Spec { specStreams   = specStrms+              , specObservers = obsLs }  -> +     let initStrms = map initStrm specStrms             in+     let strms = evalStreams k exts specStrms initStrms in+     case obsLs of+       [Observer { observerExpr     = expr_+                 , observerExprType = t1 }] -> +         let dyn = toDynF t1 expr_ in+           case fromDynF t dyn of+             Nothing    -> impossible "evalFunc" "copilot-core"+             Just expr  -> evalExpr_ k expr exts [] strms+       _ -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."++--------------------------------------------------------------------------------++evalArray :: Integral b => Int -> Type a -> Name -> b -> ArrEnv -> a+evalArray k t name idx exts =+  case lookup name exts of+    Nothing -> badUsage $ "you need to supply a list of finite lists " ++ +                 "for interpreting array " ++ name+    Just dyn ->+      case catMaybes $ map (fromDynF t) dyn of+        [] -> badUsage $ "you probably gave the wrong type for external variable " ++ name ++ ".  Recheck your types and re-evaluate."+        xs -> let arr = (xs !! k) in+              if length arr > fromIntegral idx+                then arr !! fromIntegral idx+                else badUsage $ "in the environment for array " ++ name ++ +                          ", you tried to index out of bounds"+  +--------------------------------------------------------------------------------++evalOp1 :: Op1 a b -> (a -> b)+evalOp1 op = case op of+  Not        -> P.not+  Abs _      -> P.abs+  Sign _     -> P.signum+  Recip _    -> P.recip+  Exp _      -> P.exp+  Sqrt _     -> P.sqrt+  Log _      -> P.log+  Sin _      -> P.sin+  Tan _      -> P.tan+  Cos _      -> P.cos+  Asin _     -> P.asin+  Atan _     -> P.atan+  Acos _     -> P.acos+  Sinh _     -> P.sinh+  Tanh _     -> P.tanh+  Cosh _     -> P.cosh+  Asinh _    -> P.asinh+  Atanh _    -> P.atanh+  Acosh _    -> P.acosh+  BwNot _    -> complement+  Cast _ _   -> P.fromIntegral ++--------------------------------------------------------------------------------++evalOp2 :: Op2 a b c -> (a -> b -> c)+evalOp2 op = case op of+  And          -> (&&)+  Or           -> (||)+  Add _        -> (+)+  Sub _        -> (-)+  Mul _        -> (*)+  Mod _        -> (catchZero P.mod)+  Div _        -> (catchZero P.div)+  Fdiv _       -> (P./)+  Pow _        -> (P.**)+  Logb _       -> P.logBase+  Eq _         -> (==)+  Ne _         -> (/=)+  Le _         -> (<=)+  Ge _         -> (>=)+  Lt _         -> (<)+  Gt _         -> (>)+  BwAnd _      -> (.&.)+  BwOr  _      -> (.|.)+  BwXor _      -> (xor)+  BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )+  BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )++catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)+catchZero _ _ 0 = badUsage "divide by zero"+catchZero f x y = f x y++--------------------------------------------------------------------------------++evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)+evalOp3 (Mux _) = \ !v !x !y -> if v then x else y++--------------------------------------------------------------------------------++initStrm :: Stream -> (Id, DynamicF [] Type)+initStrm Stream { streamId       = id+                , streamBuffer   = buffer+                , streamExprType = t } =+  (id, toDynF t (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]+evalStreams :: Int -> ExtEnv -> [Stream] -> Env Id -> Env Id+evalStreams top exts specStrms initStrms = +  evalStreams_ 0 initStrms +  where +  evalStreams_ :: Int -> Env Id -> Env Id+  evalStreams_ k strms | k == top  = strms+  evalStreams_ k strms | otherwise = +    evalStreams_ (k+1) $! strms_ +    where +    strms_ = map evalStream specStrms+    evalStream Stream { streamId       = id+                      , streamExpr     = e+                      , streamExprType = t } =+      let xs = fromJust $ lookup id strms >>= fromDynF t       in+      let x  = evalExpr_ k e exts [] strms                     in+      let ls = x `seq` (x:xs)                                  in+      (id, toDynF t ls)++--------------------------------------------------------------------------------++evalTrigger :: +  ShowType -> Int -> ExtEnv -> Env Id -> Trigger -> [Maybe [Output]]+evalTrigger showType k exts strms+  Trigger+    { triggerGuard = e+    , triggerArgs  = args+    } = take k $ map tag (zip bs vs) ++ repeat Nothing -- there might be 0 args!++  where+  tag :: (Bool, a) -> Maybe a+  tag (True,  x) = Just x+  tag (False, _) = Nothing++  bs :: [Bool]+  bs = evalExprs_ k e exts strms++  vs :: [[Output]]+  vs = transpose $ map evalUExpr args ++  evalUExpr :: UExpr -> [Output]+  evalUExpr (UExpr t e1) =+    map (showWithType showType t) (evalExprs_ k e1 exts strms)++--------------------------------------------------------------------------------+evalObserver :: ShowType -> Int -> ExtEnv -> Env Id -> Observer -> [Output]+evalObserver showType k exts strms+  Observer+    { observerExpr     = e+    , observerExprType = t }+  = map (showWithType showType t) (evalExprs_ k e exts strms)++--------------------------------------------------------------------------------++evalExprs_ :: Int -> Expr a -> ExtEnv -> Env Id -> [a]+evalExprs_ k e exts strms = +  map (\i -> evalExpr_ i e exts [] strms) [0..(k-1)]+
+ src/Copilot/Core/Interpret/Render.hs view
@@ -0,0 +1,95 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | An tagless interpreter for Copilot specifications.++module Copilot.Core.Interpret.Render+  ( renderAsTable+  , renderAsCSV+  ) where++import Data.List (intersperse, transpose, foldl')+import Data.Maybe (catMaybes)+import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))+import qualified Data.Map as M+import Text.PrettyPrint.NCol (asColumns)+import Text.PrettyPrint (Doc, ($$), (<>), text, render, empty)++--------------------------------------------------------------------------------++renderAsTable :: ExecTrace -> String+renderAsTable+  ExecTrace+    { interpTriggers  = trigs+    , interpObservers = obsvs } =+  ( render+  . asColumns+  . transpose+  . (:) (ppTriggerNames ++ ppObserverNames)+  . transpose+  ) (ppTriggerOutputs ++ ppObserverOutputs)++  where++  ppTriggerNames :: [Doc]+  ppTriggerNames  = map (text . (++ ":")) (M.keys trigs)++  ppObserverNames :: [Doc]+  ppObserverNames = map (text . (++ ":")) (M.keys obsvs)++  ppTriggerOutputs :: [[Doc]]+  ppTriggerOutputs = map (map ppTriggerOutput) (M.elems trigs)++  ppTriggerOutput :: Maybe [Output] -> Doc+  ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"+  ppTriggerOutput Nothing   = text "--"++  ppObserverOutputs :: [[Doc]]+  ppObserverOutputs = map (map text) (M.elems obsvs)++--------------------------------------------------------------------------------++renderAsCSV :: ExecTrace -> String+renderAsCSV = render . unfold++unfold :: ExecTrace -> Doc+unfold r =+  case step r of+    (cs, Nothing) -> cs+    (cs, Just r') -> cs $$ unfold r'++step :: ExecTrace -> (Doc, Maybe ExecTrace)+step ExecTrace+       { interpTriggers  = trigs+       } = +  if M.null trigs then (empty, Nothing)+    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)++  where++  ppTriggerOutputs :: [Doc]+  ppTriggerOutputs =+      catMaybes +    . fmap ppTriggerOutput +    . M.assocs +    . fmap head +    $ trigs++  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc+  ppTriggerOutput (_,  Nothing) = Nothing+  ppTriggerOutput (cs, Just xs) = Just $+    text cs <> text "," <>+      (foldr (<>) empty . map text . intersperse ",") xs++  tails :: Maybe ExecTrace+  tails =+    if any null (M.elems (fmap tail trigs))+      then Nothing+      else Just+        ExecTrace+          { interpTriggers  = fmap tail trigs+          , interpObservers = M.empty+          }++--------------------------------------------------------------------------------
+ src/Copilot/Core/MakeTags.hs view
@@ -0,0 +1,112 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Sets a unique tags for each external array/function call.++module Copilot.Core.MakeTags (makeTags) where++import Copilot.Core.Expr+import Copilot.Core.Spec+import Control.Monad.State+import Prelude hiding (id)++next :: State Int Int+next =+  do+    k <- get+    put (succ k)+    return k++makeTags :: Spec -> Spec+makeTags spec = evalState (mkTagsSpec spec) 0++mkTagsSpec :: Spec -> State Int Spec+mkTagsSpec+  Spec+    { specStreams   = strms+    , specObservers = obsvs+    , specTriggers  = trigs+    } =+  liftM3 Spec+    (mkTagsStrms strms)+    (mkTagsObsvs obsvs)+    (mkTagsTrigs trigs)++mkTagsStrms :: [Stream] -> State Int [Stream]+mkTagsStrms = mapM mkTagsStrm++  where++    mkTagsStrm Stream+      { streamId         = id+      , streamBuffer     = xs+      , streamGuard      = g+      , streamExpr       = e+      , streamExprType   = t } =+        do+          e' <- mkTagsExpr e+          return $ Stream+            { streamId         = id+            , streamBuffer     = xs+            , streamGuard      = g+            , streamExpr       = e'+            , streamExprType   = t }++mkTagsObsvs :: [Observer] -> State Int [Observer]+mkTagsObsvs = mapM mkTagsObsv++  where++    mkTagsObsv Observer+      { observerName     = name+      , observerExpr     = e+      , observerExprType = t } =+        do+          e' <- mkTagsExpr e+          return $ Observer+            { observerName     = name+            , observerExpr     = e'+            , observerExprType = t }++mkTagsTrigs :: [Trigger] -> State Int [Trigger]+mkTagsTrigs = mapM mkTagsTrig++ where++   mkTagsTrig Trigger+     { triggerName      = name+     , triggerGuard     = g+     , triggerArgs      = args } =+       do+         g' <- mkTagsExpr g+         args' <- mapM mkTagsUExpr args+         return $ Trigger+           { triggerName      = name+           , triggerGuard     = g'+           , triggerArgs      = args' }++mkTagsUExpr :: UExpr -> State Int UExpr+mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } =+  do+    e' <- mkTagsExpr e+    return $ UExpr { uExprExpr = e', uExprType = t }++mkTagsExpr :: Expr a -> State Int (Expr a)+mkTagsExpr e0 = case e0 of+  Const t x                     -> return $ Const t x+  Drop t k id                   -> return $ Drop t k id+  Local t1 t2 name e1 e2        -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)+  Var t name                    -> return $ Var t name+  ExternVar t name              -> return $ ExternVar t name+  ExternFun t name args _       -> do+                                     args' <- mapM mkTagsUExpr args+                                     k <- next+                                     return $ ExternFun t name args' (Just k)+  ExternArray t1 t2 name idx _  -> do+                                     idx' <- mkTagsExpr idx+                                     k <- next+                                     return $ ExternArray t1 t2 name idx' (Just k)+  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)
+ src/Copilot/Core/Operators.hs view
@@ -0,0 +1,83 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs, Rank2Types #-}++module Copilot.Core.Operators+  ( Op1 (..)+  , Op2 (..)+  , Op3 (..)+  ) where++import Copilot.Core.Type (Type)+import Data.Bits++--------------------------------------------------------------------------------++-- Unary operators.+data Op1 a b where+  -- Boolean operators.+  Not      :: Op1 Bool Bool+  -- Numeric operators.+  Abs      :: Num a => Type a -> Op1 a a+  Sign     :: Num a => Type a -> Op1 a a+  -- Fractional operators.+  Recip    :: Fractional a => Type a -> Op1 a a+  -- Floating operators.+  Exp      :: Floating a => Type a -> Op1 a a+  Sqrt     :: Floating a => Type a -> Op1 a a+  Log      :: Floating a => Type a -> Op1 a a+  Sin      :: Floating a => Type a -> Op1 a a+  Tan      :: Floating a => Type a -> Op1 a a+  Cos      :: Floating a => Type a -> Op1 a a+  Asin     :: Floating a => Type a -> Op1 a a+  Atan     :: Floating a => Type a -> Op1 a a+  Acos     :: Floating a => Type a -> Op1 a a+  Sinh     :: Floating a => Type a -> Op1 a a+  Tanh     :: Floating a => Type a -> Op1 a a+  Cosh     :: Floating a => Type a -> Op1 a a+  Asinh    :: Floating a => Type a -> Op1 a a+  Atanh    :: Floating a => Type a -> Op1 a a+  Acosh    :: Floating a => Type a -> Op1 a a+  -- Bitwise operators.+  BwNot    :: Bits     a => Type a -> Op1 a a+  -- Casting operaators.+  Cast     :: (Integral a, Num b) => Type a -> Type b -> Op1 a b++-- | Binary operators.+data Op2 a b c where+  -- Boolean operators.+  And      :: Op2 Bool Bool Bool+  Or       :: Op2 Bool Bool Bool+  -- Numeric operators.+  Add      :: Num a => Type a -> Op2 a a a+  Sub      :: Num a => Type a -> Op2 a a a+  Mul      :: Num a => Type a -> Op2 a a a+  -- Integral operators.+  Mod      :: Integral a => Type a -> Op2 a a a+  Div      :: Integral a => Type a -> Op2 a a a+  -- Fractional operators.+  Fdiv     :: Fractional a => Type a -> Op2 a a a+  -- Floating operators.+  Pow      :: Floating a => Type a -> Op2 a a a+  Logb     :: Floating a => Type a -> Op2 a a a+  -- Equality operators.+  Eq       :: Eq a => Type a -> Op2 a a Bool+  Ne       :: Eq a => Type a -> Op2 a a Bool+  -- Relational operators.+  Le       :: Ord a => Type a -> Op2 a a Bool+  Ge       :: Ord a => Type a -> Op2 a a Bool+  Lt       :: Ord a => Type a -> Op2 a a Bool+  Gt       :: Ord a => Type a -> Op2 a a Bool+  -- Bitwise operators.+  BwAnd    :: Bits a => Type a -> Op2 a a a+  BwOr     :: Bits a => Type a -> Op2 a a a+  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++-- | Ternary operators.+data Op3 a b c d where+  -- Conditional operator:+  Mux   :: Type a -> Op3 Bool a a a
+ src/Copilot/Core/PrettyPrint.hs view
@@ -0,0 +1,174 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | A pretty printer for Copilot specifications.++{-# LANGUAGE GADTs #-}++module Copilot.Core.PrettyPrint+  ( prettyPrint+  ) where++import Copilot.Core+import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)+import Prelude hiding (id)+import Text.PrettyPrint.HughesPJ+import Data.List (intersperse)++--------------------------------------------------------------------------------++strmName :: Int -> Doc+strmName id = text "s" <> int id++--------------------------------------------------------------------------------++ppExpr :: Expr a -> Doc+ppExpr e0 = case e0 of+  Const t x                  -> text (showWithType Haskell t x)+  Drop _ 0 id                -> strmName id+  Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id+  ExternVar _ name           -> text "extern" <+> doubleQuotes (text name)+  ExternFun _ name args _    -> +    text "extern" <+> doubleQuotes +      (text name <> lparen <> +         hcat (punctuate (comma <> space) (map ppUExpr args))+       <> rparen)+  ExternArray _ _ name idx _ -> text "extern" <+> doubleQuotes (text name <> lbrack +                                  <> ppExpr idx <> rbrack)+  Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals+                                          <+> ppExpr e1 $$ text "in" <+> ppExpr e2+  Var _ name                 -> text "var" <+> doubleQuotes (text name)+  Op1 op e                   -> ppOp1 op (ppExpr e)+  Op2 op e1 e2               -> ppOp2 op (ppExpr e1) (ppExpr e2)+  Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)++ppUExpr :: UExpr -> Doc+ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0++ppOp1 :: Op1 a b -> Doc -> Doc+ppOp1 op = case op of+  Not      -> ppPrefix "not"+  Abs _    -> ppPrefix "abs"+  Sign _   -> ppPrefix "signum"+  Recip _  -> ppPrefix "recip"+  Exp _    -> ppPrefix "exp"+  Sqrt _   -> ppPrefix "sqrt"+  Log _    -> ppPrefix "log"+  Sin _    -> ppPrefix "sin"+  Tan _    -> ppPrefix "tan"+  Cos _    -> ppPrefix "cos"+  Asin _   -> ppPrefix "asin"+  Atan _   -> ppPrefix "atan"+  Acos _   -> ppPrefix "acos"+  Sinh _   -> ppPrefix "sinh"+  Tanh _   -> ppPrefix "tanh"+  Cosh _   -> ppPrefix "cosh"+  Asinh _  -> ppPrefix "asinh"+  Atanh _  -> ppPrefix "atanh"+  Acosh _  -> ppPrefix "acosh"+  BwNot _  -> ppPrefix "~"+  Cast _ _ -> ppPrefix "(cast)"++ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc+ppOp2 op = case op of+  And          -> ppInfix "&&"+  Or           -> ppInfix "||"+  Add      _   -> ppInfix "+"+  Sub      _   -> ppInfix "-"+  Mul      _   -> ppInfix "*"+  Div      _   -> ppInfix "div"+  Mod      _   -> ppInfix "mod"+  Fdiv     _   -> ppInfix "/"+  Pow      _   -> ppInfix "**"+  Logb     _   -> ppInfix "logBase"+  Eq       _   -> ppInfix "=="+  Ne       _   -> ppInfix "/="+  Le       _   -> ppInfix "<="+  Ge       _   -> ppInfix ">="+  Lt       _   -> ppInfix "<"+  Gt       _   -> ppInfix ">"+  BwAnd    _   -> ppInfix "&"+  BwOr     _   -> ppInfix "|"+  BwXor    _   -> ppInfix "^"+  BwShiftL _ _ -> ppInfix "<<"+  BwShiftR _ _ -> ppInfix ">>"++ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc+ppOp3 op = case op of+  Mux _    -> \ doc1 doc2 doc3 ->+    text "(if"   <+> doc1 <+>+    text "then" <+> doc2 <+>+    text "else" <+> doc3 <> text ")"++--------------------------------------------------------------------------------+  +ppInfix :: String -> Doc -> Doc -> Doc+ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2++ppPrefix :: String -> Doc -> Doc+ppPrefix cs = (text cs <+>)++--------------------------------------------------------------------------------++ppStream :: Stream -> Doc+ppStream+  Stream+    { streamId       = id+    , streamBuffer   = buffer+    , streamExpr     = e+    , streamExprType = t+    }+      = (parens . text . showType) t+          <+> strmName id +    <+> text "="+    <+> text ("["+              ++ ( concat $ intersperse "," +                              $ map (showWithType Haskell t) buffer )+              ++ "]")+    <+> text "++"+    <+> ppExpr e++--------------------------------------------------------------------------------++ppTrigger :: Trigger -> Doc+ppTrigger+  Trigger+    { triggerName  = name+    , triggerGuard = e+    , triggerArgs  = args }+  =   text "trigger" <+> text "\"" <> text name <> text "\""+  <+> text "="+  <+> ppExpr e+  <+> lbrack+  $$  (nest 2 $ vcat (punctuate comma $ +                          map (\a -> text "arg" <+> ppUExpr a) args))+  $$  nest 2 rbrack++--------------------------------------------------------------------------------++ppObserver :: Observer -> Doc+ppObserver+  Observer+    { observerName     = name+    , observerExpr     = e }+  =   text "observer \"" <> text name <> text "\""+  <+> text "="+  <+> ppExpr e++--------------------------------------------------------------------------------++ppSpec :: Spec -> Doc+ppSpec spec = cs $$ ds $$ es+  where+    cs = foldr (($$) . ppStream)   empty (specStreams   spec)+    ds = foldr (($$) . ppTrigger)  empty (specTriggers  spec)+    es = foldr (($$) . ppObserver) empty (specObservers spec)++--------------------------------------------------------------------------------++-- | Pretty-prints a Copilot specification.+prettyPrint :: Spec -> String+prettyPrint = render . ppSpec++--------------------------------------------------------------------------------
+ src/Copilot/Core/Random.hs view
@@ -0,0 +1,311 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs, ExistentialQuantification #-}++module Copilot.Core.Random+  ( randomSpec+  ) where++import Control.Monad+import Copilot.Core (UExpr (..))+import qualified Copilot.Core as E+import Copilot.Core.Spec+import Copilot.Core.Random.Gen+import Copilot.Core.Random.Weights+import Copilot.Core.Type+import Copilot.Core.Type.Equality+import Data.Int+import Data.Word+import Prelude hiding (id)+import System.Random (StdGen)++--------------------------------------------------------------------------------++randomSpec :: Weights -> StdGen -> Spec+randomSpec = runGen genSpec 0++--------------------------------------------------------------------------------++genSpec :: Gen Spec+genSpec =+  do+    ws <- weights+    numTriggers <- choose (1, maxTriggers ws)+    ss <- genStreamInfo's+    streams  <- mapM (genStream ss) ss+    triggers <- mapM (genTrigger ss) (map mkTriggerName [0..numTriggers-1])+    return+      Spec+        { specStreams   = streams+        , specObservers = []+        , specTriggers  = triggers }++  where++  mkTriggerName :: Int -> E.Name+  mkTriggerName k = "f" ++ show k++--------------------------------------------------------------------------------++data StreamInfo = forall a . (Eq a, Ord a) => StreamInfo+  { streamInfoId         :: E.Id+  , streamInfoType       :: Type a+  , streamInfoBufferSize :: Int }++--------------------------------------------------------------------------------++data WrapType = forall a . (Eq a, Ord a) => WrapType (Type a)++genType :: Weights -> Gen WrapType+genType ws = freq+  [ (boolFreq   ws, return $ WrapType (typeOf :: Type Bool  ))+  , (int8Freq   ws, return $ WrapType (typeOf :: Type Int8  ))+  , (int16Freq  ws, return $ WrapType (typeOf :: Type Int16 ))+  , (int32Freq  ws, return $ WrapType (typeOf :: Type Int32 ))+  , (int64Freq  ws, return $ WrapType (typeOf :: Type Int64 ))+  , (word8Freq  ws, return $ WrapType (typeOf :: Type Word8 ))+  , (word16Freq ws, return $ WrapType (typeOf :: Type Word16))+  , (word32Freq ws, return $ WrapType (typeOf :: Type Word32))+  , (word64Freq ws, return $ WrapType (typeOf :: Type Word64))+  , (floatFreq  ws, return $ WrapType (typeOf :: Type Float ))+  , (floatFreq  ws, return $ WrapType (typeOf :: Type Double)) ]++genTypeFromStreamInfo's :: [StreamInfo] -> Gen WrapType+genTypeFromStreamInfo's = elements . map (\ (StreamInfo _ t _) -> WrapType t)++--------------------------------------------------------------------------------++genStreamInfo's :: Gen [StreamInfo]+genStreamInfo's =+  do+    let+      s0 = StreamInfo 0 (typeOf :: Type Bool) 1+    ws <- weights+    ss <- mapM genStreamInfo [1 .. numStreams ws - 1]+    return (s0 : ss)++  where+  genStreamInfo :: Int -> Gen StreamInfo+  genStreamInfo id =+    do+      ws <- weights+      k  <- choose (1, maxBuffSize ws)+      WrapType t <- genType ws+      return+        StreamInfo+          { streamInfoId         = id+          , streamInfoType       = t+          , streamInfoBufferSize = k }++--------------------------------------------------------------------------------++genStream :: [StreamInfo] -> StreamInfo -> Gen Stream+genStream ss+  StreamInfo+    { streamInfoId         = id+    , streamInfoType       = t+    , streamInfoBufferSize = k } =+  do+    xs <- replicateM k (randomFromType t)+    w  <- genExpr ss t+    return+      Stream+        { streamId       = id+        , streamBuffer   = xs+        , streamGuard    = E.Const (typeOf :: Type Bool) True+        , streamExpr     = w+        , streamExprType = t }++--------------------------------------------------------------------------------++genTrigger :: [StreamInfo] -> E.Name -> Gen Trigger+genTrigger ss name =+  do+    w  <- genExpr ss (typeOf :: Type Bool)+    ws <- weights+    i  <- choose (1, maxTrigArgs ws)+    args <- replicateM i genArg+    return+      Trigger+        { triggerName  = name+        , triggerGuard = w+        , triggerArgs  = args }++  where++  genArg :: Gen UExpr+  genArg =+    do+      WrapType t <- genTypeFromStreamInfo's ss+      w <- genExpr ss t+      return+        UExpr+          { uExprExpr = w+          , uExprType = t }++--------------------------------------------------------------------------------++genExpr :: [StreamInfo] -> Type a -> Gen (E.Expr a)+genExpr ss t =+  do+    dp <- depth+    ws <- weights+    if dp >= maxExprDepth ws+      then freq+        [ (constFreq ws, genConst)+        , (dropFreq  ws, genDrop) ]+      else freq+        [ (constFreq ws, genConst)+        , (dropFreq  ws, genDrop)+        , (op1Freq   ws, genOp1)+        , (op2Freq   ws, genOp2)+        , (op3Freq   ws, genOp3) ]++  where+  genConst =+    do+      x <- randomFromType t+      return $ E.Const t x+  genDrop =+    do+      s <- findStreamInfoWithMatchingType+      k <- choose (0, streamInfoBufferSize s - 1)+      return $ E.Drop t (fromIntegral k) (streamInfoId s)++    where+    findStreamInfoWithMatchingType =+      let+        p (StreamInfo _ t1 _) =+          case t =~= t1 of+            Just _ -> True+            _      -> False+      in+        elements (filter p ss)++  genOp1 = incDepth $ case t of+    Bool   -> genOp1Bool ss+    Int8   -> genOp1Num  ss t+    Int16  -> genOp1Num  ss t+    Int32  -> genOp1Num  ss t+    Int64  -> genOp1Num  ss t+    Word8  -> genOp1Num  ss t+    Word16 -> genOp1Num  ss t+    Word32 -> genOp1Num  ss t+    Word64 -> genOp1Num  ss t+    Float  -> genOp1Num  ss t+    Double -> genOp1Num  ss t++  genOp2 = incDepth $ case t of+-- XXX +--    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss, genOp2Ord ss]+    Bool    -> oneOf [genOp2Bool ss, genOp2Eq ss]+    Int8    -> intOrWord NumWit IntegralWit+    Int16   -> intOrWord NumWit IntegralWit+    Int32   -> intOrWord NumWit IntegralWit+    Int64   -> intOrWord NumWit IntegralWit+    Word8   -> intOrWord NumWit IntegralWit+    Word16  -> intOrWord NumWit IntegralWit+    Word32  -> intOrWord NumWit IntegralWit+    Word64  -> intOrWord NumWit IntegralWit+    Float   -> floatOrDouble NumWit+    Double  -> floatOrDouble NumWit++    where++      intOrWord numWit integralWit = do +        ws <- weights +        if divModFreq ws +          then oneOf $ num ++ [genOp2Integral ss t integralWit ]+          else oneOf num+        where num = [ genOp2Num ss t numWit ]++      floatOrDouble numWit = oneOf+        [ genOp2Num ss t numWit ]++  genOp3 = incDepth (genOp3Mux ss t)++--------------------------------------------------------------------------------++genOp1Bool :: [StreamInfo] -> Gen (E.Expr Bool)+genOp1Bool ss =+  do+    ew <- genExpr ss (typeOf :: Type Bool)+    return $ E.Op1 E.Not ew++genOp1Num :: Num a => [StreamInfo] -> Type a -> Gen (E.Expr a)+genOp1Num ss t =+  do+    ew  <- genExpr ss t+    opw <- elements [E.Abs t, E.Sign t]+    return $ E.Op1 opw ew++genOp2Bool :: [StreamInfo] -> Gen (E.Expr Bool)+genOp2Bool ss =+  do+    ew1 <- genExpr ss (typeOf :: Type Bool)+    ew2 <- genExpr ss (typeOf :: Type Bool)+    opw <- elements [E.And, E.Or]+    return $ E.Op2 opw ew1 ew2++genOp2Eq :: [StreamInfo] -> Gen (E.Expr Bool)+genOp2Eq ss =+  do+    WrapType t <- genTypeFromStreamInfo's ss+    ew1 <- genExpr ss t+    ew2 <- genExpr ss t+    opw <- elements [E.Eq t, E.Ne t]+    return $ E.Op2 opw ew1 ew2++-- XXX+-- Figure out how to ensure t comes from a Numeric Class+-- genOp2Ord :: [StreamInfo] -> Gen (E.Expr Bool)+-- genOp2Ord ss =+--   do+--     WrapType t <- genTypeFromStreamInfo's ss+--     ew1 <- genExpr ss t+--     ew2 <- genExpr ss t+--     opw <- elements+--       [ (E.Lt t)+--       , (E.Gt t)+--       , (E.Le t)+--       , (E.Ge t) ]+--     return $ E.Op2 opw ew1 ew2++genOp2Num :: [StreamInfo] -> Type a -> NumWit a -> Gen (E.Expr a)+genOp2Num ss t NumWit =+  do+    ew1 <- genExpr ss t+    ew2 <- genExpr ss t+    opw <-+      elements+        [ (E.Add t)+        , (E.Sub t)+        , (E.Mul t) ]+    return+      $ E.Op2 opw ew1 ew2++genOp2Integral :: [StreamInfo] -> Type a -> IntegralWit a -> Gen (E.Expr a)+genOp2Integral ss t IntegralWit =+  do+    ew1 <- genExpr ss t+    ew2 <- genExpr ss t+    opw <-+      elements+        [ (E.Div t)+        , (E.Mod t) ]+    return+      $ E.Op2 opw ew1 ew2++genOp3Mux :: [StreamInfo] -> Type a -> Gen (E.Expr a)+genOp3Mux ss t =+  do+    ew1 <- genExpr ss (typeOf :: Type Bool)+    ew2 <- genExpr ss t+    ew3 <- genExpr ss t+    return $ E.Op3 (E.Mux t) ew1 ew2 ew3++data NumWit a = Num a => NumWit++data IntegralWit a = Integral a => IntegralWit
+ src/Copilot/Core/Random/Gen.hs view
@@ -0,0 +1,127 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs, ExistentialQuantification #-}++module Copilot.Core.Random.Gen+  ( Gen+  , runGen+  , randomFromType+  , oneOf+  , freq+  , choose+  , elements+  , depth+  , weights+  , incDepth+  ) where++import Copilot.Core.Random.Weights+import Copilot.Core.Error+import Copilot.Core.Type+import System.Random (StdGen, Random, random, randomR, split)++--------------------------------------------------------------------------------++-- | @runGen@ takes a @Gen a@, a max depth of the expression, the weights, and+-- the standard random generator.+newtype Gen a = MkGen { runGen :: Depth -> Weights -> StdGen -> a }++--------------------------------------------------------------------------------++instance Functor Gen where+  fmap f (MkGen h) = MkGen (\ d ws r -> f (h d ws r))++instance Monad Gen where+  return x = MkGen (\ _ _ _ -> x)++  MkGen m >>= k = MkGen $ \ d ws r ->+    let (r1, r2) = split r       in+    let MkGen m' = k (m d ws r1) in+    m' d ws r2++--------------------------------------------------------------------------------++stdGen :: Gen StdGen+stdGen = MkGen $ \ _ _ g -> g++depth :: Gen Depth+depth = MkGen $ \ d _ _ -> d++weights :: Gen Weights+weights = MkGen $ \ _ ws _ -> ws++incDepth :: Gen a -> Gen a+incDepth gen = MkGen $ \ d ws g -> runGen gen (succ d) ws g++--------------------------------------------------------------------------------++randomFromType :: Type a -> Gen a+randomFromType t =+  case t of+    Bool   -> genBool+    Int8   -> genBoundedIntegral+    Int16  -> genBoundedIntegral+    Int32  -> genBoundedIntegral+    Int64  -> genBoundedIntegral+    Word8  -> genBoundedIntegral+    Word16 -> genBoundedIntegral+    Word32 -> genBoundedIntegral+    Word64 -> genBoundedIntegral+    Float  -> genFractional+    Double -> genFractional++  where++  genBool :: Gen Bool+  genBool =+    do+      g <- stdGen+      return $ fst (random g)++  genBoundedIntegral :: (Bounded a, Integral a) => Gen a+  genBoundedIntegral =+    do let mn = minBound+           mx = maxBound `asTypeOf` mn+       n <- choose (toInteger mn, toInteger mx)+       return (fromInteger n `asTypeOf` mn)++  genFractional :: (Random a, Fractional a) => Gen a+  genFractional =+    do+      g <- stdGen+      return $ fst (random g)++--------------------------------------------------------------------------------++choose :: Random a => (a, a) -> Gen a+choose rng =+  do+    g <- stdGen+    return $ fst (randomR rng g)++oneOf :: [Gen a] -> Gen a+oneOf [] = impossible "oneof" "copilot-core" +oneOf gs = choose (0,length gs - 1) >>= (gs !!)++-- | Takes a list of pairs (weight, Gen), and choose the Gen based on the+-- weights.  To get the frequency of choosing a Gen, sum up all the weights, and+-- choose c between 1 and the total.  Now recurse down the list, choosing an+-- item only when c <= weight.  If not, subtract the current weight from c.+freq :: [(Int, Gen a)] -> Gen a+freq [] = impossible "feq" "copilot-core" +freq xs0 = choose (1, tot) >>= (`pick` xs0)++ where+  tot = sum (map fst xs0)+  pick n ((k,x):xs)+    | n <= k    = x+    | otherwise = pick (n-k) xs+  pick _ _  = impossible "pick" "copilot-core" ++elements :: [a] -> Gen a+elements [] = impossible "elements" "copilot-core" +elements xs = (xs !!) `fmap` choose (0, length xs - 1)++--------------------------------------------------------------------------------
+ src/Copilot/Core/Random/Weights.hs view
@@ -0,0 +1,69 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++module Copilot.Core.Random.Weights+  ( Depth+  , Weights (..)+  , simpleWeights ) where++type Depth = Int++data Weights = Weights+  { maxExprDepth :: Int+  , maxBuffSize  :: Int+  , maxTriggers  :: Int+  , maxTrigArgs  :: Int+  , maxObservers :: Int+  , numStreams   :: Int+  -- Expression frequencies:+  , constFreq    :: Int+  , drop0Freq    :: Int+  , dropFreq     :: Int+  , externFreq   :: Int+  , op1Freq      :: Int+  , op2Freq      :: Int+  , op3Freq      :: Int+  -- Type frequencies:+  , boolFreq     :: Int+  , int8Freq     :: Int+  , int16Freq    :: Int+  , int32Freq    :: Int+  , int64Freq    :: Int+  , word8Freq    :: Int+  , word16Freq   :: Int+  , word32Freq   :: Int+  , word64Freq   :: Int+  , floatFreq    :: Int+  , doubleFreq   :: Int +  , divModFreq   :: Bool }++simpleWeights :: Weights+simpleWeights = Weights +  { maxExprDepth = 10+  , maxBuffSize  = 8+  , maxTriggers  = 5+  , maxTrigArgs  = 5+  , maxObservers = 8+  , numStreams   = 10+  -- Expression frequencies:+  , constFreq    = 1+  , drop0Freq    = 1+  , dropFreq     = 1+  , externFreq   = 1+  , op1Freq      = 1+  , op2Freq      = 1+  , op3Freq      = 1+  -- Type frequencies:+  , boolFreq     = 1+  , int8Freq     = 1+  , int16Freq    = 1+  , int32Freq    = 1+  , int64Freq    = 1+  , word8Freq    = 1+  , word16Freq   = 1+  , word32Freq   = 1+  , word64Freq   = 1+  , floatFreq    = 1+  , doubleFreq   = 1 +  , divModFreq   = True }
+ src/Copilot/Core/Spec.hs view
@@ -0,0 +1,53 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification, GADTs #-}++module Copilot.Core.Spec+  ( Stream (..)+  , Observer (..)+  , Trigger (..)+  , Spec (..)+  ) where++import Copilot.Core.Expr (Name, Id, Expr, UExpr)+import Copilot.Core.Type (Type)++--------------------------------------------------------------------------------++-- | A stream.+data Stream = forall a  . Stream+  { streamId         :: Id+  , streamBuffer     :: [a]+  , streamGuard      :: Expr Bool+  , streamExpr       :: Expr a+  , streamExprType   :: Type a }++--------------------------------------------------------------------------------++-- | An observer.+data Observer = forall a . Observer+  { observerName     :: Name+  , observerExpr     :: Expr a+  , observerExprType :: Type a }++--------------------------------------------------------------------------------++-- | A trigger.+data Trigger = Trigger+  { triggerName      :: Name+  , triggerGuard     :: Expr Bool+  , triggerArgs      :: [UExpr] }++--------------------------------------------------------------------------------++-- | A Copilot specification consists of a list of variables bound to anonymous+-- streams, a lost of anomymous streams, a list of observers, and a list of+-- triggers.+data Spec = Spec+  { specStreams      :: [Stream]+  , specObservers    :: [Observer]+  , specTriggers     :: [Trigger] }++--------------------------------------------------------------------------------
+ src/Copilot/Core/Spec/Locals.hs view
@@ -0,0 +1,86 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification #-}++-- |++module Copilot.Core.Spec.Locals+  ( Loc (..)+  , locals+  ) where++import Copilot.Core+import Data.DList (DList, empty, singleton, append, concat, toList)+import Data.List (nubBy)+import Prelude hiding (concat, foldr)++--------------------------------------------------------------------------------++data Loc = forall a . Loc+  { localName :: Name+  , localType :: Type a }++instance Show Loc where+  show Loc { localName = name } = name++--------------------------------------------------------------------------------++locals :: Spec -> [Loc]+locals+  Spec+    { specStreams   = streams+    , specTriggers  = triggers+    , specObservers = observers+    } = nubBy eqLoc . toList $+          concat (fmap locsStream   streams)  `append`+          concat (fmap locsTrigger  triggers) `append`+          concat (fmap locsObserver observers)++  where++  eqLoc :: Loc -> Loc -> Bool+  eqLoc Loc { localName = name1 } Loc { localName = name2 } =+    name1 == name2++--------------------------------------------------------------------------------++locsStream :: Stream -> DList Loc+locsStream Stream { streamExpr = e } = locsExpr e++--------------------------------------------------------------------------------++locsTrigger :: Trigger -> DList Loc+locsTrigger Trigger { triggerGuard = e, triggerArgs = args } =+  locsExpr e `append` concat (fmap locsUExpr args)++  where++  locsUExpr :: UExpr -> DList Loc+  locsUExpr (UExpr _ e1) = locsExpr e1++--------------------------------------------------------------------------------++locsObserver :: Observer -> DList Loc+locsObserver Observer { observerExpr = e } = locsExpr e++--------------------------------------------------------------------------------++locsExpr :: Expr a -> DList Loc+locsExpr e0 = case e0 of+  Const  _ _             -> empty+  Drop   _ _ _           -> empty+  Local t _ name e1 e2   -> singleton (Loc name t)+                                        `append` locsExpr e1+                                        `append` locsExpr e2+  Var _ _                -> empty+  ExternVar _ _          -> empty+  ExternFun _ _ _ _      -> empty+  ExternArray _ _ _ _ _  -> empty+  Op1 _ e                -> locsExpr e+  Op2 _ e1 e2            -> locsExpr e1 `append` locsExpr e2+  Op3 _ e1 e2 e3         -> locsExpr e1 `append` locsExpr e2+                                        `append` locsExpr e3++--------------------------------------------------------------------------------
+ src/Copilot/Core/Type.hs view
@@ -0,0 +1,64 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | ++{-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-}++module Copilot.Core.Type+  ( Type (..)+  , Typed (..)+  , UType (..)+  ) where++import Data.Int+import Data.Word+import Copilot.Core.Type.Equality++data Type :: * -> * where+  Bool    :: Type Bool+  Int8    :: Type Int8+  Int16   :: Type Int16+  Int32   :: Type Int32+  Int64   :: Type Int64+  Word8   :: Type Word8+  Word16  :: Type Word16+  Word32  :: Type Word32+  Word64  :: Type Word64+  Float   :: Type Float+  Double  :: Type Double++instance EqualType Type where+  (=~=) Bool   Bool   = Just Refl+  (=~=) Int8   Int8   = Just Refl+  (=~=) Int16  Int16  = Just Refl+  (=~=) Int32  Int32  = Just Refl+  (=~=) Int64  Int64  = Just Refl+  (=~=) Word8  Word8  = Just Refl+  (=~=) Word16 Word16 = Just Refl+  (=~=) Word32 Word32 = Just Refl+  (=~=) Word64 Word64 = Just Refl+  (=~=) Float  Float  = Just Refl+  (=~=) Double Double = Just Refl+  (=~=) _ _ = Nothing++class Typed a where+  typeOf :: Type a++instance Typed Bool   where typeOf = Bool+instance Typed Int8   where typeOf = Int8+instance Typed Int16  where typeOf = Int16+instance Typed Int32  where typeOf = Int32+instance Typed Int64  where typeOf = Int64+instance Typed Word8  where typeOf = Word8+instance Typed Word16 where typeOf = Word16+instance Typed Word32 where typeOf = Word32+instance Typed Word64 where typeOf = Word64+instance Typed Float  where typeOf = Float+instance Typed Double where typeOf = Double++--------------------------------------------------------------------------------++-- | A untyped type (no phantom type).+data UType = forall a . UType { uTypeType :: Type a }
+ src/Copilot/Core/Type/Dynamic.hs view
@@ -0,0 +1,52 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE Rank2Types #-}++-- | An implementation of dynamic types using "Copilot.Core.Type.Equality".+-- The theory behind this technique is described the following paper:+--+-- * Baars, Arthur I. and Swierstra, S. Doaitse,+-- \"/Typing dynamic typing/\",+-- ACM SIGPLAN Notices vol. 37, p. 157-166, 2002++{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-}++module Copilot.Core.Type.Dynamic+  ( Dynamic+  , DynamicF+  , toDyn+  , fromDyn+  , toDynF+  , fromDynF+  ) where++import Copilot.Core.Type.Equality++--------------------------------------------------------------------------------++data Dynamic :: (* -> *) -> * where+  Dynamic :: a -> t a -> Dynamic t++data DynamicF :: (* -> *) -> (* -> *) -> * where+  DynamicF :: f a -> t a -> DynamicF f t++toDyn :: EqualType t => t a -> a -> Dynamic t+toDyn t x = Dynamic x t++fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a+fromDyn t1 (Dynamic x t2) =+  case t1 =~= t2 of+    Just Refl -> return x+    Nothing   -> Nothing++toDynF :: EqualType t => t a -> f a -> DynamicF f t+toDynF t fx = DynamicF fx t++fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)+fromDynF t1 (DynamicF fx t2) =+  case t1 =~= t2 of+    Just Refl -> return fx+    Nothing   -> Nothing
+ src/Copilot/Core/Type/Equality.hs view
@@ -0,0 +1,36 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE GADTs, KindSignatures #-}++module Copilot.Core.Type.Equality+  ( Equal (..)+  , EqualType (..)+  , coerce+  , refl+  , trans+  , symm+  , cong+  ) where++data Equal :: * -> * -> * where+  Refl :: Equal a a++class EqualType t where+  (=~=) :: t a -> t b -> Maybe (Equal a b)++coerce :: Equal a b -> a -> b+coerce Refl x = x++refl :: Equal a a+refl = Refl++symm :: Equal a b -> Equal b a+symm Refl = Refl++trans :: Equal a b -> Equal b c -> Equal a c+trans Refl Refl = Refl++cong :: Equal a b -> Equal (f a) (f b)+cong Refl = Refl
+ src/Copilot/Core/Type/Show.hs view
@@ -0,0 +1,76 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++{-# LANGUAGE ExistentialQuantification, GADTs #-}++module Copilot.Core.Type.Show+  ( ShowWit (..)+  , showWit+  , showWithType+  , ShowType(..)+  , showType+  ) where++import Copilot.Core.Type++--------------------------------------------------------------------------------++data ShowWit a = Show a => ShowWit++--------------------------------------------------------------------------------++showWit :: Type a -> ShowWit a+showWit t =+  case t of+    Bool   -> ShowWit+    Int8   -> ShowWit+    Int16  -> ShowWit+    Int32  -> ShowWit+    Int64  -> ShowWit+    Word8  -> ShowWit+    Word16 -> ShowWit+    Word32 -> ShowWit+    Word64 -> ShowWit+    Float  -> ShowWit+    Double -> ShowWit++--------------------------------------------------------------------------------++showType :: Type a -> String+showType t =+  case t of+    Bool   -> "Bool"+    Int8   -> "Int8"+    Int16  -> "Int16"+    Int32  -> "Int32"+    Int64  -> "Int64"+    Word8  -> "Word8"+    Word16 -> "Word16"+    Word32 -> "Word32"+    Word64 -> "Word64"+    Float  -> "Float"+    Double -> "Double"++--------------------------------------------------------------------------------++-- Are we proving equivalence with a C backend, in which case we want to show+-- Booleans as '0' and '1'.+data ShowType = C | Haskell++--------------------------------------------------------------------------------++showWithType :: ShowType -> Type a -> a -> String+showWithType showT t x =+  case showT of+    C         -> case t of+                   Bool -> if x then "1" else "0"+                   _    -> sw+    Haskell   -> case t of+                   Bool -> if x then "true" else "false"+                   _    -> sw                   +  where+  sw = case showWit t of+         ShowWit -> show x++--------------------------------------------------------------------------------
+ src/Copilot/Core/Type/Uninitialized.hs view
@@ -0,0 +1,30 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | ++{-# LANGUAGE GADTs #-}++module Copilot.Core.Type.Uninitialized+  ( uninitialized+  ) where++import Copilot.Core.Type++--------------------------------------------------------------------------------++uninitialized :: Type a -> a+uninitialized t =+  case t of+    Bool   -> False+    Int8   -> 0+    Int16  -> 0+    Int32  -> 0+    Int64  -> 0+    Word8  -> 0+    Word16 -> 0+    Word32 -> 0+    Word64 -> 0+    Float  -> 0+    Double -> 0
+ src/Copilot/Core/Version.hs view
@@ -0,0 +1,9 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++module Copilot.Core.Version (version) where++-- | The current version of Copilot Core.+version :: String+version = "0.1"