copilot-c99 2.2.1 → 3.0

raw patch · 21 files changed

+571/−1700 lines, 21 filesdep +filepathdep +language-c99dep +language-c99-simpledep −QuickCheckdep −atomdep −bytestringdep ~basedep ~containersdep ~copilot-corenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: filepath, language-c99, language-c99-simple, language-c99-util, mtl

Dependencies removed: QuickCheck, atom, bytestring, csv, process, random, text, vector

Dependency ranges changed: base, containers, copilot-core, directory, pretty

API changes (from Hackage documentation)

Files

• README.md +24/−49
• copilot-c99.cabal +23/−70
• src/Copilot/Compile/C99.hs +1/−78
• src/Copilot/Compile/C99/C2A.hs +0/−232
• src/Copilot/Compile/C99/CodeGen.hs +155/−0
• src/Copilot/Compile/C99/Common.hs +0/−32
• src/Copilot/Compile/C99/Compile.hs +121/−0
• src/Copilot/Compile/C99/External.hs +45/−0
• src/Copilot/Compile/C99/MetaTable.hs +0/−169
• src/Copilot/Compile/C99/Params.hs +0/−20
• src/Copilot/Compile/C99/Phases.hs +0/−246
• src/Copilot/Compile/C99/PrePostCode.hs +0/−55
• src/Copilot/Compile/C99/Queue.hs +0/−56
• src/Copilot/Compile/C99/Test/CheckSpec.hs +0/−134
• src/Copilot/Compile/C99/Test/Driver.hs +0/−263
• src/Copilot/Compile/C99/Test/Iteration.hs +0/−48
• src/Copilot/Compile/C99/Test/ReadCSV.hs +0/−47
• src/Copilot/Compile/C99/Translate.hs +148/−0
• src/Copilot/Compile/C99/Util.hs +54/−0
• src/Copilot/Compile/C99/Witness.hs +0/−143
• test/CopilotC99Test.hs +0/−58

@@ -1,58 +1,33 @@-[![Build Status](https://travis-ci.org/Copilot-Language/copilot-c99.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-c99)+[![Build Status](https://travis-ci.org/Copilot-Language/copilot-c99.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-core) -Overview-========-This package is a Copilot back-end that targets Atom-<http://hackage.haskell.org/package/atom>.  Atom is a Haskell DSL that generates-real-time C code.  +# Copilot: a stream DSL+Copilot-c99 implements a C99 backend for Copilot, producing high quality code+suitable for hard realtime applications. -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. -Examples-=========-Please see the files under the Examples directory in the-[Copilot](http://hackage.haskell.org/package/copilot) for a number of examples-showing the syntax, use of libraries, and use of the interpreter and back-ends.-The examples is the best way to start.+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. -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-c99 -However, we strongly recommend you install Copilot, which installs copilot-c99-and other packages automatically.  Execute+## Installation+Copilot-c99 can be found on+[Hackage](https://hackage.haskell.org/package/copilot-c99). 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). -         cabal install copilot -Dependencies-=============-copilot-c99 depends on the-[Atom](http://hackage.haskell.org/package/copilot-atom) to generate hard-real-time C code.+## Further information+For further information, install instructions and documentation, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io) -Resources-=========-[copilot-c99](http://hackage.haskell.org/package/copilot-c99) 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-c99/master/LICENSE).

@@ -1,100 +1,53 @@ cabal-version             : >= 1.10 name                      : copilot-c99-version                   : 2.2.1+version                   : 3.0 synopsis                  : A compiler for Copilot targeting C99. description               :-  This package is a back-end from Copilot to the Atom DSL.+  This package is a back-end from Copilot to C.   .   Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in   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>.  license                   : BSD3 license-file              : LICENSE-maintainer                : leepike@galois.com+maintainer                : Frank Dedden <dev@dedden.net> stability                 : Experimental category                  : Language, Embedded build-type                : Simple extra-source-files        : README.md -author                    : Lee Pike-                          , Robin Morisset+author                    : Frank Dedden                           , Alwyn Goodloe-                          , Sebastian Niller-                          , Nis Nordby Wegmann  source-repository head     type:       git-    location:   git://github.com/leepike/copilot-c99.git+    location:   git://github.com/Copilot-Language/copilot-c99.git  library   default-language        : Haskell2010   hs-source-dirs          : src   ghc-options             : -Wall -fwarn-tabs-  ghc-prof-options        : -auto-all -caf-all--  build-depends           : atom >= 1.0.13-                          , base >= 4.3 && < 5-                          , bytestring-                          , containers >= 0.4-                          , copilot-core == 2.2.1-                          , csv-                          , directory >= 1.1-                          , process >= 1.0-                          , pretty >= 1.0-                          , random >= 1.0-                          , text >= 0.6-                          , QuickCheck >= 2.4-                          , vector--  exposed-modules         : Copilot.Compile.C99.Test.CheckSpec-                          , Copilot.Compile.C99.Test.Driver-                          , Copilot.Compile.C99.Test.Iteration-                          , Copilot.Compile.C99.Test.ReadCSV-                          , Copilot.Compile.C99-                          , Copilot.Compile.C99.C2A-                          , Copilot.Compile.C99.Common-                          , Copilot.Compile.C99.MetaTable-                          , Copilot.Compile.C99.Params-                          , Copilot.Compile.C99.Phases-                          , Copilot.Compile.C99.PrePostCode-                          , Copilot.Compile.C99.Queue-                          , Copilot.Compile.C99.Witness--executable copilot-c99-qc-  default-language        : Haskell2010-  hs-source-dirs          : test, src-  ghc-options             : -Wall -fwarn-tabs-  main-is                 : CopilotC99Test.hs+  build-depends           : base                >= 4.9 && < 5+                          , containers          >= 0.4 && < 0.7+                          , directory           >= 1.3 && < 1.4+                          , filepath            >= 1.4 && < 1.5+                          , mtl                 >= 2.2 && < 2.3+                          , pretty              >= 1.1 && < 1.2 -  build-depends           : atom >= 1.0.9-                          , base >= 4.3-                          , bytestring-                          , csv-                          , containers >= 0.4-                          , copilot-core == 2.2.1-                          , directory >= 1.1-                          , process >= 1.0-                          , pretty >= 1.0-                          , random >= 1.0-                          , text >= 0.6-                          , QuickCheck >= 2.4-                          , vector+                          , copilot-core        >= 3.0 && < 3.1+                          , language-c99        >= 0.1.1 && < 0.2+                          , language-c99-util   >= 0.1.1 && < 0.2+                          , language-c99-simple >= 0.1.1 && < 0.2 -  other-modules           : Copilot.Compile.C99-                          , Copilot.Compile.C99.C2A-                          , Copilot.Compile.C99.MetaTable-                          , Copilot.Compile.C99.Params-                          , Copilot.Compile.C99.Phases-                          , Copilot.Compile.C99.PrePostCode-                          , Copilot.Compile.C99.Queue-                          , Copilot.Compile.C99.Witness-                          , Copilot.Compile.C99.Test.CheckSpec-                          , Copilot.Compile.C99.Test.Driver-                          , Copilot.Compile.C99.Test.Iteration-                          , Copilot.Compile.C99.Test.ReadCSV+  exposed-modules         : Copilot.Compile.C99+                          , Copilot.Compile.C99.Translate+                          , Copilot.Compile.C99.Util+                          , Copilot.Compile.C99.CodeGen+                          , Copilot.Compile.C99.External+                          , Copilot.Compile.C99.Compile

@@ -1,82 +1,5 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Compile through the Atom backend.- module Copilot.Compile.C99   ( compile-  , c99DirName-  , c99FileRoot-  , module Copilot.Compile.C99.Params   ) where -import qualified Copilot.Core as Core-import Copilot.Compile.Header.C99 (genC99Header)-import Copilot.Compile.C99.MetaTable (allocMetaTable)-import Copilot.Compile.C99.Params-import Copilot.Compile.C99.Phases (schedulePhases)-import Copilot.Compile.C99.PrePostCode (preCode, postCode)---import Language.Atom (Atom)-import qualified Language.Atom as Atom--import Data.Char (toUpper)-import Control.Monad (when, unless)-import System.Directory ( doesDirectoryExist-                        , createDirectory-                        , removeDirectoryRecursive-                        , renameFile-                        , removeFile)------------------------------------------------------------------------------------c99DirName :: String-c99DirName = "copilot-c99-codegen"--c99FileRoot :: String-c99FileRoot = "copilot"------------------------------------------------------------------------------------compile :: Params -> Core.Spec -> IO ()-compile params spec0 = do-  b <- doesDirectoryExist dirName-  when b $ do putStrLn "Directory exists.  Delete? [y/N]:"-              input <- getLine-              if (map toUpper input == "Y") -                then (removeDirectoryRecursive dirName) >> build-                else putStrLn "Ok, nothing done.  Terminating."-  unless b build -  where-  build = do -    createDirectory dirName-    (schedule, _, _, _, _) <- Atom.compile programName atomDefaults atomProgram-    when (verbose params) $ putStrLn (Atom.reportSchedule schedule)-    genC99Header (prefix params) dirName spec-    mv ".c" -- the C file Atom generates-    removeFile (programName ++ ".h")  -- We don't want Atom's .h file, but our own--  mv ext = renameFile p (dirName ++ "/" ++ p)-    where p = programName ++ ext--  dirName = withPrefix (prefix params) c99DirName--  spec :: Core.Spec-  spec = Core.makeTags spec0--  programName :: String-  programName = withPrefix (prefix params) c99FileRoot--  atomDefaults :: Atom.Config-  atomDefaults =-    Atom.defaults-      { Atom.cCode = \ _ _ _ ->-        (preCode params spec, postCode params spec) }--  atomProgram :: Atom ()-  atomProgram =-    do-      meta <- allocMetaTable spec-      schedulePhases params meta spec+import Copilot.Compile.C99.Compile

@@ -1,232 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification, GADTs #-}--module Copilot.Compile.C99.C2A-  ( c2aExpr-  , c2aType-  ) where--import qualified Copilot.Compile.C99.Queue as Q-import qualified Copilot.Compile.C99.Witness as W-import Copilot.Compile.C99.MetaTable-import Copilot.Core (Op1 (..), Op2 (..), Op3 (..))-import Copilot.Core.Error (impossible)-import qualified Copilot.Core as C-import Copilot.Core.Type.Equality ((=~=), coerce, cong)-import Data.Map (Map)-import qualified Data.Map as M-import qualified Language.Atom as A-import qualified Prelude as P-import Prelude hiding (id)------------------------------------------------------------------------------------c2aExpr :: MetaTable -> C.Expr a -> A.E a-c2aExpr meta e = c2aExpr_ e M.empty meta------------------------------------------------------------------------------------c2aType :: C.Type a -> A.Type-c2aType t =-  case t of-    C.Bool   -> A.Bool-    C.Int8   -> A.Int8   ; C.Int16  -> A.Int16-    C.Int32  -> A.Int32  ; C.Int64  -> A.Int64-    C.Word8  -> A.Word8  ; C.Word16 -> A.Word16-    C.Word32 -> A.Word32 ; C.Word64 -> A.Word64-    C.Float  -> A.Float  ; C.Double -> A.Double------------------------------------------------------------------------------------data Local = forall a . Local-  { localAtomExpr :: A.E a-  , localType     :: C.Type a }--type Env = Map C.Name Local------------------------------------------------------------------------------------c2aExpr_ :: C.Expr a -> Env -> MetaTable -> A.E a-c2aExpr_ e0 env meta = case e0 of--  ------------------------------------------------------  C.Const _ x -> A.Const x--  ------------------------------------------------------  C.Drop t i id ->-    let Just strmInfo = M.lookup id (streamInfoMap meta) in-    drop1 t strmInfo--    where-    drop1 :: C.Type a -> StreamInfo -> A.E a-    drop1 t1-      StreamInfo-        { streamInfoQueue = que-        , streamInfoType  = t2-        } =-      let Just p = t2 =~= t1 in-      case W.exprInst t2 of-        W.ExprInst ->-          coerce (cong p) (Q.lookahead (fromIntegral i) que)--  ------------------------------------------------------  C.Local t1 _ name e1 e2 ->-    let e1'  = c2aExpr_ e1 env meta in-    let env' = M.insert name (Local e1' t1) env in-    c2aExpr_ e2 env' meta--  ------------------------------------------------------  C.Var t1 name ->-    let Just local = M.lookup name env in-    case local of-      Local-        { localAtomExpr = e-        , localType     = t2-        } ->-          let Just p = t2 =~= t1 in-          case W.exprInst t2 of-            W.ExprInst ->-              coerce (cong p) e--  ------------------------------------------------------  C.ExternVar t name _ ->-    let Just externInfo = M.lookup name (externInfoMap meta) in-    externVar1 t externInfo--    where-    externVar1 :: C.Type a -> ExternInfo -> A.E a-    externVar1 t1-      ExternInfo-        { externInfoVar  = v-        , externInfoType = t2-        } =-      let Just p = t2 =~= t1 in-      coerce (cong p) (A.value v)--  ------------------------------------------------------  C.ExternFun t name _ _ maybeTag ->-    let tag = case maybeTag of-                Nothing  -> impossible "c2aExpr_ /ExternFun" "copilot-c99"-                Just tg  -> tg-    in-    let Just extFunInfo = M.lookup (name, tag) (externFunInfoMap meta) in-    externFun1 t extFunInfo--    where-    externFun1 t1-      ExternFunInfo-        { externFunInfoVar  = var-        , externFunInfoType = t2-        } =-      let Just p = t2 =~= t1 in-      case W.exprInst t2 of-        W.ExprInst ->-          coerce (cong p) (A.value var)--  ------------------------------------------------------  C.ExternArray _ t name _ _ _ maybeTag -> -    let tag = case maybeTag of-                Nothing  -> impossible "c2aExpr_ /ExternArray" "copilot-c99"-                Just tg  -> tg-    in-    let Just extArrayInfo = M.lookup (name, tag) (externArrayInfoMap meta) in-    externArray1 t extArrayInfo--    where-    externArray1 t1-      ExternArrayInfo-        { externArrayInfoVar      = var-        , externArrayInfoElemType = t2-        } =-      let Just p = t2 =~= t1 in-      case W.exprInst t2 of-        W.ExprInst ->-          coerce (cong p) (A.value var)--  ------------------------------------------------------  C.Op1 op e -> c2aOp1 op (c2aExpr_ e env meta)--    --  ------------------------------------------------------  C.Op2 op e1 e2 ->-    c2aOp2 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta)--  ------------------------------------------------------  C.Op3 op e1 e2 e3 ->-    c2aOp3 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta)-      (c2aExpr_ e3 env meta)--  ------------------------------------------------------c2aOp1 :: C.Op1 a b -> A.E a -> A.E b-c2aOp1 op = case op of-  Not     ->                                                  A.not_-  Abs   t -> case W.numEInst        t of W.NumEInst        -> abs-  Sign  t -> case W.numEInst        t of W.NumEInst        -> signum-  Recip t -> case W.numEInst        t of W.NumEInst        -> recip-  Exp   t -> case W.floatingEInst   t of W.FloatingEInst   -> exp-  Sqrt  t -> case W.floatingEInst   t of W.FloatingEInst   -> sqrt-  Log   t -> case W.floatingEInst   t of W.FloatingEInst   -> log-  Sin   t -> case W.floatingEInst   t of W.FloatingEInst   -> sin-  Tan   t -> case W.floatingEInst   t of W.FloatingEInst   -> tan-  Cos   t -> case W.floatingEInst   t of W.FloatingEInst   -> cos-  Asin  t -> case W.floatingEInst   t of W.FloatingEInst   -> asin-  Atan  t -> case W.floatingEInst   t of W.FloatingEInst   -> atan-  Acos  t -> case W.floatingEInst   t of W.FloatingEInst   -> acos-  Sinh  t -> case W.floatingEInst   t of W.FloatingEInst   -> sinh-  Tanh  t -> case W.floatingEInst   t of W.FloatingEInst   -> tanh-  Cosh  t -> case W.floatingEInst   t of W.FloatingEInst   -> cosh-  Asinh t -> case W.floatingEInst   t of W.FloatingEInst   -> asinh-  Atanh t -> case W.floatingEInst   t of W.FloatingEInst   -> atanh-  Acosh t -> case W.floatingEInst   t of W.FloatingEInst   -> acosh-  BwNot t -> case W.bitsEInst       t of W.BitsEInst       -> (A.complement)-  Cast C.Bool C.Bool ->                                       P.id-  Cast C.Bool t -> case W.numEInst  t of -                     W.NumEInst     -> \e -> A.mux e (A.Const 1) (A.Const 0)-  Cast t0 t1    -> case W.numEInst  t0 of -                     W.NumEInst     -> -                       case W.numEInst t1 of W.NumEInst    -> A.Cast--c2aOp2 :: C.Op2 a b c -> A.E a -> A.E b -> A.E c-c2aOp2 op = case op of-  And     ->                                                  (A.&&.)-  Or      ->                                                  (A.||.)-  Add   t -> case W.numEInst        t of W.NumEInst        -> (+)-  Sub   t -> case W.numEInst        t of W.NumEInst        -> (-)-  Mul   t -> case W.numEInst        t of W.NumEInst        -> (*)-  Div   t -> case W.integralEInst   t of W.IntegralEInst   -> A.div_-  Mod   t -> case W.integralEInst   t of W.IntegralEInst   -> A.mod_-  Fdiv  t -> case W.numEInst        t of W.NumEInst        -> (/)-  Pow   t -> case W.floatingEInst   t of W.FloatingEInst   -> (**)-  Logb  t -> case W.floatingEInst   t of W.FloatingEInst   -> logBase-  Eq    t -> case W.eqEInst         t of W.EqEInst         -> (A.==.)-  Ne    t -> case W.eqEInst         t of W.EqEInst         -> (A./=.)-  Le    t -> case W.ordEInst        t of W.OrdEInst        -> (A.<=.)-  Ge    t -> case W.ordEInst        t of W.OrdEInst        -> (A.>=.)-  Lt    t -> case W.ordEInst        t of W.OrdEInst        -> (A.<.)-  Gt    t -> case W.ordEInst        t of W.OrdEInst        -> (A.>.)-  BwAnd t -> case W.bitsEInst       t of W.BitsEInst       -> (A..&.)-  BwOr  t -> case W.bitsEInst       t of W.BitsEInst       -> (A..|.)-  BwXor t -> case W.bitsEInst       t of W.BitsEInst       -> (A.xor)-  BwShiftL t t' -> case ( W.bitsEInst t, W.integralEInst t' )-                   of ( W.BitsEInst, W.IntegralEInst )      -> (A..<<.)-  BwShiftR t t' -> case ( W.bitsEInst t, W.integralEInst t' )-                   of ( W.BitsEInst, W.IntegralEInst )      -> (A..>>.)--c2aOp3 :: C.Op3 a b c d -> A.E a -> A.E b -> A.E c -> A.E d-c2aOp3 op = case op of-  Mux t   -> case W.exprInst        t of W.ExprInst        -> A.mux

@@ -0,0 +1,155 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Copilot.Compile.C99.CodeGen where++import Control.Monad.State  (runState)+import Data.List            (union)+import Data.Typeable        (Typeable)++import qualified Language.C99.Simple as C++import Copilot.Core+import Copilot.Compile.C99.Util+import Copilot.Compile.C99.External+import Copilot.Compile.C99.Translate++-- | Write a declaration for a generator function.+gendecln :: String -> Type a -> C.Decln+gendecln name ty = C.FunDecln Nothing cty name [] where+  cty = C.decay $ transtype ty++-- | Write a generator function for a stream.+genfun :: String -> Expr a -> Type a -> C.FunDef+genfun name expr ty = C.FunDef cty name [] cvars [C.Return $ Just cexpr] where+  cty = C.decay $ transtype ty+  (cexpr, (cvars, _)) = runState (transexpr expr) mempty++-- | Make a extern declaration of an variable.+mkextdecln :: External -> C.Decln+mkextdecln (External name _ ty) = decln where+  decln = C.VarDecln (Just C.Extern) cty name Nothing+  cty   = transtype ty++-- | Make a declaration for a copy of an external variable.+mkextcpydecln :: External -> C.Decln+mkextcpydecln (External name cpyname ty) = decln where+  cty   = transtype ty+  decln = C.VarDecln (Just C.Static) cty cpyname Nothing++-- | Make a C buffer variable and initialise it with the stream buffer.+mkbuffdecln :: Id -> Type a -> [a] -> C.Decln+mkbuffdecln sid ty xs = C.VarDecln (Just C.Static) cty name initvals where+  name     = streamname sid+  cty      = C.Array (transtype ty) (Just $ C.LitInt $ fromIntegral buffsize)+  buffsize = length xs+  initvals = Just $ C.InitArray $ map (mkinit ty) xs++-- | Make a C index variable and initialise it to 0.+mkindexdecln :: Id -> C.Decln+mkindexdecln sid = C.VarDecln (Just C.Static) cty name initval where+  name    = indexname sid+  cty     = C.TypeSpec $ C.TypedefName "size_t"+  initval = Just $ C.InitExpr $ C.LitInt 0++-- | Make an initial declaration from a single value.+mkinit :: Type a -> a -> C.Init+mkinit (Array ty') xs = C.InitArray $ map (mkinit ty') (arrayelems xs)+mkinit (Struct _)  x  = C.InitArray $ map fieldinit (toValues x) where+  fieldinit (Value ty (Field val)) = mkinit ty val+mkinit ty          x  = C.InitExpr  $ constty ty x++-- | The step function updates all streams,a+mkstep :: [Stream] -> [Trigger] -> [External] -> C.FunDef+mkstep streams triggers exts = C.FunDef void "step" [] declns stmts where+  void = C.TypeSpec C.Void+  declns = []+  stmts  =  map mkexcopy exts+         ++ map mktriggercheck triggers+         ++ map mkupdatebuffer streams+         ++ map mkupdateindex streams++  -- Make code that copies an external variable to its local one.+  mkexcopy :: External -> C.Stmt+  mkexcopy (External name cpyname ty) = C.Expr $ case ty of+    Array _ -> memcpy exvar locvar size where+                 exvar  = C.Ident cpyname+                 locvar = C.Ident name+                 size   = C.LitInt $ fromIntegral $ tysize ty+    _       -> C.Ident cpyname C..= C.Ident name++  -- Make if-statement to check the guard, call the trigger if necessary.+  mktriggercheck :: Trigger -> C.Stmt+  mktriggercheck (Trigger name guard args) = C.If guard' firetrigger where+    guard'      = C.Funcall (C.Ident $ guardname name) []+    firetrigger = [C.Expr $ C.Funcall (C.Ident name) args'] where+      args'        = take (length args) (map argcall (argnames name))+      argcall name = C.Funcall (C.Ident name) []++  -- Code to update the global buffer.+  mkupdatebuffer :: Stream -> C.Stmt+  mkupdatebuffer (Stream sid buff expr ty) = case ty of+    Array _ -> C.Expr $ memcpy dest src size where+      dest = C.Index (C.Ident $ streamname sid) (C.Ident $ indexname sid)+      src  = C.Funcall (C.Ident $ generatorname sid) []+      size = C.LitInt $ fromIntegral $ tysize ty+    _ -> C.Expr $ C.Index var index C..= val where+      var   = C.Ident $ streamname sid+      index = C.Ident $ indexname sid+      val   = C.Funcall (C.Ident $ generatorname sid) []++  -- Code to update the index.+  mkupdateindex :: Stream -> C.Stmt+  mkupdateindex (Stream sid buff expr ty) = C.Expr $ globvar C..= val where+    globvar = C.Ident $ indexname sid+    index   = (C..++) (C.Ident $ indexname sid)+    val     = index C..% (C.LitInt $ fromIntegral len)+    len     = length buff++  -- Write a call to the memcpy function.+  memcpy :: C.Expr -> C.Expr -> C.Expr -> C.Expr+  memcpy dest src size = C.Funcall (C.Ident "memcpy") [dest, src, size]+++-- | Write a struct declaration based on its definition.+mkstructdecln :: Struct a => Type a -> C.Decln+mkstructdecln (Struct x) = C.TypeDecln struct where+  struct = C.TypeSpec $ C.StructDecln (Just $ typename x) fields+  fields = map mkfield (toValues x)++  mkfield :: Value a -> C.FieldDecln+  mkfield (Value ty field) = C.FieldDecln (transtype ty) (fieldname field)++-- | Write a forward struct decralration.+mkstructforwdecln :: Struct a => Type a -> C.Decln+mkstructforwdecln (Struct x) = C.TypeDecln struct where+  struct = C.TypeSpec $ C.Struct (typename x)++-- | List all types of an expression, returns items uniquely.+exprtypes :: Typeable a => Expr a -> [UType]+exprtypes e = case e of+  Const ty _            -> typetypes ty+  Local ty1 ty2 _ e1 e2 -> typetypes ty1 `union` typetypes ty2+                           `union` exprtypes e1 `union` exprtypes e2+  Var ty _              -> typetypes ty+  Drop ty _ _           -> typetypes ty+  ExternVar ty _ _      -> typetypes ty+  Op1 _ e1              -> exprtypes e1+  Op2 _ e1 e2           -> exprtypes e1 `union` exprtypes e2+  Op3 _ e1 e2 e3        -> exprtypes e1 `union` exprtypes e2 `union` exprtypes e3++-- | List all types of an type, returns items uniquely.+typetypes :: Typeable a => Type a -> [UType]+typetypes ty = case ty of+  Array ty' -> [UType ty] `union` typetypes ty'+  Struct x  -> [UType ty] `union` map (\(Value ty' _) -> UType ty') (toValues x)+  _         -> [UType ty]++-- | Collect all expression of a list of streams and triggers and wrap them+-- into an UEXpr.+gatherexprs :: [Stream] -> [Trigger] -> [UExpr]+gatherexprs streams triggers =  map streamexpr streams+                             ++ concatMap triggerexpr triggers where+  streamexpr  (Stream _ _ expr ty)   = UExpr ty expr+  triggerexpr (Trigger _ guard args) = UExpr Bool guard : args+

@@ -1,32 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE GADTs #-}--module Copilot.Compile.C99.Common-  ( mkTmpExtFunVarName-  , typeSpec-  ) where--import qualified Copilot.Core as C------------------------------------------------------------------------------------mkTmpExtFunVarName :: C.Name -> C.Tag -> String-mkTmpExtFunVarName name tag =  "tmp_ext_fun_" ++ name ++ "_" ++ "_" ++ show tag------------------------------------------------------------------------------------typeSpec :: C.Type a -> String-typeSpec C.Bool   = "bool"-typeSpec C.Int8   = "int8_t"-typeSpec C.Int16  = "int16_t"-typeSpec C.Int32  = "int32_t"-typeSpec C.Int64  = "int64_t"-typeSpec C.Word8  = "uint8_t"-typeSpec C.Word16 = "uint16_t"-typeSpec C.Word32 = "uint32_t"-typeSpec C.Word64 = "uint64_t"-typeSpec C.Float  = "float"-typeSpec C.Double = "double"

@@ -0,0 +1,121 @@+module Copilot.Compile.C99.Compile+  ( compile+  ) where++import Text.PrettyPrint     (render)+import Data.List            (nub)+import Data.Maybe           (catMaybes)++import Language.C99.Pretty  (pretty)+import qualified Language.C99.Simple as C++import Copilot.Core+import Copilot.Compile.C99.Util+import Copilot.Compile.C99.External+import Copilot.Compile.C99.Translate+import Copilot.Compile.C99.CodeGen++-- | Compile the specification to a .h and a .c file.+compile :: String -> Spec -> IO ()+compile prefix spec = do+  let cfile = render $ pretty $ C.translate $ compilec spec+      hfile = render $ pretty $ C.translate $ compileh spec++      -- TODO: find a nicer solution using annotated AST's+      cmacros = unlines [ "#include <stdint.h>"+                        , "#include <stdbool.h>"+                        , "#include <string.h>"+                        , ""+                        , "#include \"" ++ prefix ++ ".h\""+                        , ""+                        ]++  writeFile (prefix ++ ".c") $ cmacros ++ cfile+  writeFile (prefix ++ ".h") hfile++-- | Generate the .c file from a spec. It has the following structure:+-- |+-- | * Include .h file+-- | * Declarations of global buffers and indices.+-- | * Generator functions for streams, guards and trigger args.+-- | * Declaration of step() function.+compilec :: Spec -> C.TransUnit+compilec spec = C.TransUnit declns funs where+  streams  = specStreams spec+  triggers = specTriggers spec+  exts     = gatherexts streams triggers+  exprs    = gatherexprs streams triggers++  declns = mkstructdeclns exprs ++ mkexts exts ++ mkglobals streams+  funs   = genfuns streams triggers ++ [mkstep streams triggers exts]++  -- Write struct datatypes+  mkstructdeclns :: [UExpr] -> [C.Decln]+  mkstructdeclns es = catMaybes $ map mkdecln utypes where+    mkdecln (UType ty) = case ty of+      Struct x -> Just $ mkstructdecln ty+      _        -> Nothing++    utypes = nub $ concatMap (\(UExpr _ e) -> exprtypes e) es++  -- Make declarations for copies of external variables.+  mkexts :: [External] -> [C.Decln]+  mkexts exts = map mkextcpydecln exts++  -- Make buffer and index declarations for streams.+  mkglobals :: [Stream] -> [C.Decln]+  mkglobals streams = map buffdecln streams ++ map indexdecln streams where+    buffdecln  (Stream sid buff _ ty) = mkbuffdecln  sid ty buff+    indexdecln (Stream sid _    _ _ ) = mkindexdecln sid++  -- Make generator functions, including trigger arguments.+  genfuns :: [Stream] -> [Trigger] -> [C.FunDef]+  genfuns streams triggers =  map streamgen streams+                           ++ concatMap triggergen triggers where+    streamgen :: Stream -> C.FunDef+    streamgen (Stream sid _ expr ty) = genfun (generatorname sid) expr ty++    triggergen :: Trigger -> [C.FunDef]+    triggergen (Trigger name guard args) = guarddef : argdefs where+      guarddef = genfun (guardname name) guard Bool+      argdefs  = map arggen (zip (argnames name) args)++      arggen :: (String, UExpr) -> C.FunDef+      arggen (argname, UExpr ty expr) = genfun argname expr ty++-- | Generate the .h file from a spec.+compileh :: Spec -> C.TransUnit+compileh spec = C.TransUnit declns [] where+  streams  = specStreams spec+  triggers = specTriggers spec+  exts     = gatherexts streams triggers+  exprs    = gatherexprs streams triggers++  declns =  mkstructforwdeclns exprs+         ++ mkexts exts+         ++ extfundeclns triggers+         ++ [stepdecln]++  mkstructforwdeclns :: [UExpr] -> [C.Decln]+  mkstructforwdeclns es = catMaybes $ map mkdecln utypes where+    mkdecln (UType ty) = case ty of+      Struct x -> Just $ mkstructforwdecln ty+      _        -> Nothing++    utypes = nub $ concatMap (\(UExpr _ e) -> exprtypes e) es++  -- Make declarations for external variables.+  mkexts :: [External] -> [C.Decln]+  mkexts = map mkextdecln++  extfundeclns :: [Trigger] -> [C.Decln]+  extfundeclns triggers = map extfundecln triggers where+    extfundecln :: Trigger -> C.Decln+    extfundecln (Trigger name _ args) = C.FunDecln Nothing cty name params where+        cty    = C.TypeSpec C.Void+        params = map mkparam $ zip (argnames name) args+        mkparam (name, UExpr ty _) = C.Param (transtype ty) name++  -- Declaration for the step function.+  stepdecln :: C.Decln+  stepdecln = C.FunDecln Nothing (C.TypeSpec C.Void) "step" []

@@ -0,0 +1,45 @@+{-# LANGUAGE ExistentialQuantification #-}++module Copilot.Compile.C99.External where++import Data.List  (unionBy)++import Copilot.Core+import Copilot.Compile.C99.Util++-- | Representation of external variables.+data External = forall a. External+  { extname    :: String+  , extcpyname :: String+  , exttype    :: Type a+  }++-- | Union over lists of External, we solely base the equality on the extname's.+extunion :: [External] -> [External] -> [External]+extunion = unionBy (\a b -> extname a == extname b)++-- | Collect all external variables from the streams and triggers.+gatherexts :: [Stream] -> [Trigger] -> [External]+gatherexts streams triggers = streamsexts `extunion` triggersexts where+  streamsexts  = concat $ map streamexts streams+  triggersexts = concat $ map triggerexts triggers++  streamexts :: Stream -> [External]+  streamexts (Stream _ _ expr _) = exprexts expr++  triggerexts :: Trigger -> [External]+  triggerexts (Trigger _ guard args) = guardexts `extunion` argexts where+    guardexts = exprexts guard+    argexts   = concat $ map uexprexts args++  uexprexts :: UExpr -> [External]+  uexprexts (UExpr _ expr) = exprexts expr++  exprexts :: Expr a -> [External]+  exprexts expr = let rec = exprexts in case expr of+    Local _ _ _ e1 e2   -> rec e1 `extunion` rec e2+    ExternVar ty name _ -> [External name (excpyname name) ty]+    Op1 _ e             -> rec e+    Op2 _ e1 e2         -> rec e1 `extunion` rec e2+    Op3 _ e1 e2 e3      -> rec e1 `extunion` rec e2 `extunion` rec e3+    _                   -> []

@@ -1,169 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification #-}--module Copilot.Compile.C99.MetaTable-  ( StreamInfo (..)-  , ExternInfo (..)-  , ExternArrayInfo (..)-  , ExternFunInfo (..)-  , StreamInfoMap-  , ExternInfoMap-  , ExternFunInfoMap-  , MetaTable (..)-  , allocMetaTable-  ) where--import Control.Monad (liftM)-import qualified Copilot.Compile.C99.Queue as Q-import qualified Copilot.Compile.C99.Witness as W-import qualified Copilot.Core as C-import Copilot.Core.Error (impossible)--import Copilot.Core.External-import Data.Map (Map)-import qualified Data.Map as M-import Language.Atom (Atom)-import qualified Language.Atom as A-import Prelude hiding (id)------------------------------------------------------------------------------------data StreamInfo = forall a . StreamInfo-  { streamInfoQueue   :: Q.Queue a-  , streamInfoTempVar :: A.V a-  , streamInfoType    :: C.Type a }--type StreamInfoMap = Map C.Id StreamInfo------------------------------------------------------------------------------------data ExternInfo = forall a . ExternInfo-  { externInfoVar     :: A.V a-  , externInfoType    :: C.Type a }--type ExternInfoMap = Map C.Name ExternInfo------------------------------------------------------------------------------------data ExternArrayInfo = forall a b . Integral a => ExternArrayInfo-  { externArrayInfoVar      :: A.V b-  , externArrayInfoIdxExpr  :: C.Expr a-  , externArrayInfoIdxType  :: C.Type a-  , externArrayInfoElemType :: C.Type b }--type ExternArrayInfoMap = Map (C.Name, C.Tag) ExternArrayInfo------------------------------------------------------------------------------------data ExternFunInfo = forall a . ExternFunInfo-  { externFunInfoArgs  :: [C.UExpr]-  , externFunInfoVar   :: A.V a-  , externFunInfoType  :: C.Type a }--type ExternFunInfoMap = Map (C.Name, C.Tag) ExternFunInfo------------------------------------------------------------------------------------data MetaTable = MetaTable-  { streamInfoMap      :: StreamInfoMap-  , externInfoMap      :: ExternInfoMap-  , externArrayInfoMap :: ExternArrayInfoMap-  , externFunInfoMap   :: ExternFunInfoMap }------------------------------------------------------------------------------------allocMetaTable :: C.Spec -> A.Atom MetaTable-allocMetaTable spec =-  do-    streamInfoMap_ <--      liftM M.fromList $ mapM allocStream (C.specStreams spec)--    externInfoMap_ <--      liftM M.fromList $ mapM allocExternVar (externVars spec)--    externArrayInfoMap_ <--      liftM M.fromList $ mapM allocExternArray (externArrays spec)--    externFunInfoMap_ <--      liftM M.fromList $ mapM allocExternFun (externFuns spec)--    return $-      MetaTable-        streamInfoMap_-        externInfoMap_-        externArrayInfoMap_-        externFunInfoMap_------------------------------------------------------------------------------------allocStream :: C.Stream -> Atom (C.Id, StreamInfo)-allocStream-  C.Stream-    { C.streamId       = id-    , C.streamBuffer   = buf-    , C.streamExprType = t-    } =-  do-    W.ExprInst <- return (W.exprInst t)-    que <- Q.queue (mkQueueName   id) buf-    tmp <- A.var   (mkTempVarName id) (C.uninitialized t)-    let-      strmInfo =-        StreamInfo-          { streamInfoQueue       = que-          , streamInfoTempVar     = tmp-          , streamInfoType        = t }-    return (id, strmInfo)------------------------------------------------------------------------------------allocExternVar :: ExtVar -> Atom (C.Name, ExternInfo)-allocExternVar (ExtVar name ut) =-  case ut of-    C.UType t ->-      do-        W.ExprInst <- return (W.exprInst t)-        v <- A.var (mkExternName name) (C.uninitialized t)-        return (name, ExternInfo v t)------------------------------------------------------------------------------------allocExternArray :: ExtArray -> Atom ((C.Name, C.Tag), ExternArrayInfo)-allocExternArray (ExtArray name elemType idxExpr idxType _ maybeTag) = do-    let tag = case maybeTag of-                Nothing  -> impossible "allocExternArray" "copilot-c99"-                Just tg  -> tg-    W.ExprInst <- return (W.exprInst elemType)-    v <- A.var (mkExternArrayName name tag) (C.uninitialized elemType)-    return ((name, tag), ExternArrayInfo v idxExpr idxType elemType)------------------------------------------------------------------------------------allocExternFun :: ExtFun -> Atom ((C.Name, C.Tag), ExternFunInfo)-allocExternFun (ExtFun name t args maybeTag) = do-    let tag = case maybeTag of-                Nothing  -> impossible "allocExternFun" "copilot-c99"-                Just tg  -> tg-    W.ExprInst <- return (W.exprInst t)-    v <- A.var (mkExternFunName name tag) (C.uninitialized t)-    return ((name, tag), ExternFunInfo args v t)-  -----------------------------------------------------------------------------------mkExternName :: C.Name -> A.Name-mkExternName name = "ext_" ++ name--mkExternArrayName :: C.Name -> C.Tag -> A.Name-mkExternArrayName name tag = "ext_array_" ++ show tag ++ "_" ++ name--mkExternFunName :: C.Name -> C.Tag -> A.Name-mkExternFunName name tag = "ext_fun_" ++ show tag ++ "_" ++ name--mkQueueName :: C.Id -> A.Name-mkQueueName id = "str" ++ show id--mkTempVarName :: C.Id -> A.Name-mkTempVarName id = "tmp" ++ show id

@@ -1,20 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------module Copilot.Compile.C99.Params (Params (..), defaultParams, withPrefix) where--data Params = Params-  { prefix  :: Maybe String -- An string to prefix the output with-  , verbose :: Bool -  }--defaultParams :: Params-defaultParams = Params-  { prefix  = Nothing-  , verbose = True-  }--withPrefix :: Maybe String -> String -> String-withPrefix (Just cs) ds = cs ++ "_" ++ ds-withPrefix _         ds = ds

@@ -1,246 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE GADTs, Rank2Types #-}--module Copilot.Compile.C99.Phases-  ( schedulePhases-  , numberOfPhases-  ) where--import Copilot.Compile.C99.C2A (c2aExpr, c2aType)-import Copilot.Compile.C99.Common (mkTmpExtFunVarName)-import Copilot.Compile.C99.MetaTable-  (MetaTable (..), StreamInfo (..), ExternInfo (..), ExternArrayInfo (..)-  ,ExternFunInfo (..))-import Copilot.Compile.C99.Params-import qualified Copilot.Compile.C99.Queue as Q-import qualified Copilot.Compile.C99.Witness as W-import qualified Copilot.Core as Core-import Copilot.Core.Type.Equality ((=~=), Equal (..))-import Data.List (intersperse)-import qualified Data.Map as M-import Language.Atom (Atom, (<==), atom, cond, exactPhase)-import qualified Language.Atom as A-import Prelude hiding (id)------------------------------------------------------------------------------------data Phase-  = SampleExternVars-  | SampleExternArrays-  | CallExternFuns-  | SampleExternFuns-  | UpdateStates-  | FireTriggers-  | UpdateObservers-  | UpdateBuffers-  deriving (Bounded, Eq, Enum, Ord, Show)--numberOfPhases :: Int-numberOfPhases = succ (fromEnum (maxBound :: Phase))------------------------------------------------------------------------------------schedulePhases :: Params -> MetaTable -> Core.Spec -> Atom ()-schedulePhases params meta spec =-  A.period numberOfPhases $-    sampleExternVars    params meta spec >>-    callExternFuns      params meta spec >>-    sampleExternArrays  params meta spec >>-    sampleExternFuns    params meta spec >>-    fireTriggers        params meta spec >>-    updateObservers     params meta spec >>-    updateStates        params meta spec >>-    updateBuffers       params meta spec------------------------------------------------------------------------------------sampleExternVars :: Params -> MetaTable -> Core.Spec -> Atom ()-sampleExternVars _ meta _ =-  (mapM_ sampleExternVar . M.toList . externInfoMap) meta--  where-  sampleExternVar :: (Core.Name, ExternInfo) -> Atom ()-  sampleExternVar (name, ExternInfo v t) =-    exactPhase (fromEnum SampleExternVars) $-      atom ("sample_var_" ++ name) $ do-        W.AssignInst <- return $ W.assignInst t-        v <== A.value (A.var' name (c2aType t))------------------------------------------------------------------------------------sampleExternArrays :: Params -> MetaTable -> Core.Spec -> Atom ()-sampleExternArrays _ meta _ =-  (mapM_ sampleExternArray . M.toList . externArrayInfoMap) meta--  where-  sampleExternArray :: ((Core.Name, Core.Tag), ExternArrayInfo) -> Atom ()-  sampleExternArray ((name, tag), ExternArrayInfo var idxExpr idxType elemType) =-    exactPhase (fromEnum SampleExternArrays) $-      atom ("sample_array_" ++ name ++ "_" ++ show tag) $ do-        W.IntegralEInst <- return $ W.integralEInst idxType-        W.AssignInst <- return $ W.assignInst elemType-        W.ExprInst <- return $ W.exprInst elemType-        let e   = c2aExpr meta idxExpr-            arr = A.array' name (c2aType elemType)-        var <== A.value (arr A.! e)------------------------------------------------------------------------------------callExternFuns :: Params -> MetaTable -> Core.Spec -> Atom ()-callExternFuns _ meta _ =-  (mapM_ sampleExternFun . M.toList . externFunInfoMap) meta--  where-  c2aUExpr :: Core.UExpr -> A.UE-  c2aUExpr (Core.UExpr t e) =-    case W.exprInst t of-      W.ExprInst -> A.ue (c2aExpr meta e)--  sampleExternFun :: ((Core.Name, Core.Tag), ExternFunInfo) -> Atom ()-  sampleExternFun ((name, tag), ExternFunInfo args _ _) =-    exactPhase (fromEnum CallExternFuns) $-      atom ("call_fun_" ++ name ++ "_" ++ show tag) $ do-        let args' = map c2aUExpr args-        A.action fnCall args'--    where-    fnCall :: [String] -> String-    fnCall xs = mkTmpExtFunVarName name tag ++ " = " ++ name ++ "("-      ++ concat (intersperse "," (reverse xs)) ++ ")"------------------------------------------------------------------------------------sampleExternFuns :: Params -> MetaTable -> Core.Spec -> Atom ()-sampleExternFuns _ meta _ =-  (mapM_ sampleExternFun . M.toList . externFunInfoMap) meta--  where-  sampleExternFun :: ((Core.Name, Core.Tag), ExternFunInfo) -> Atom ()-  sampleExternFun ((name, tag), ExternFunInfo _ var t) =-    exactPhase (fromEnum CallExternFuns) $-      atom ("sample_fun_" ++ name ++ "_" ++ show tag) $ do-        W.AssignInst <- return $ W.assignInst t-        var <== A.value (A.var' (mkTmpExtFunVarName name tag) (c2aType t))------------------------------------------------------------------------------------updateStates :: Params -> MetaTable -> Core.Spec -> Atom ()-updateStates _ meta-  Core.Spec-    { Core.specStreams = streams-    } = mapM_ updateStreamState streams--  where-  updateStreamState :: Core.Stream -> Atom ()-  updateStreamState-    Core.Stream-      { Core.streamId       = id-      , Core.streamExpr     = e-      , Core.streamExprType = t1-      } -    = do-    let e' = c2aExpr meta e-        Just strmInfo = M.lookup id (streamInfoMap meta)-    updateStreamState1 t1 id e' strmInfo--  updateStreamState1-    :: Core.Type a -> Core.Id -> A.E a -> StreamInfo -> Atom ()-  updateStreamState1 t1 id e1-    StreamInfo-      { streamInfoTempVar = tmp-      , streamInfoType    = t2  }-    =-    exactPhase (fromEnum UpdateStates) $-      atom ("update_state_s" ++ show id) $ do-        W.AssignInst <- return (W.assignInst t2)-        Just Refl <- return (t1 =~= t2)-        tmp <== e1 -- coerce (cong p) e1------------------------------------------------------------------------------------fireTriggers :: Params -> MetaTable -> Core.Spec -> Atom ()-fireTriggers params meta-  Core.Spec-    { Core.specTriggers = triggers }-  =-  mapM_ fireTrigger triggers--  where-  fireTrigger :: Core.Trigger -> Atom ()-  fireTrigger-    Core.Trigger-      { Core.triggerName  = name-      , Core.triggerGuard = e0-      , Core.triggerArgs  = args-      } =-    exactPhase (fromEnum FireTriggers) $-      atom ("fire_trigger_" ++ name) $ do-        let args' = map triggerArg2UE (reverse args)-            e0'   = c2aExpr meta e0-        cond e0'-        A.action fnCall args'--      where-      triggerArg2UE :: Core.UExpr -> A.UE-      triggerArg2UE (Core.UExpr t e) =-        case W.exprInst t of-          W.ExprInst -> A.ue (c2aExpr meta e)--      fnCall :: [String] -> String-      fnCall xs = withPrefix (prefix params) name ++-        "(" ++ concat (intersperse "," xs) ++ ")"------------------------------------------------------------------------------------updateObservers :: Params -> MetaTable -> Core.Spec -> Atom ()-updateObservers params meta-  Core.Spec-    { Core.specObservers = observers }-  =-  mapM_ updateObserver observers--  where-  updateObserver :: Core.Observer -> Atom ()-  updateObserver-    Core.Observer-      { Core.observerName     = name-      , Core.observerExpr     = e-      , Core.observerExprType = t-      } =-    exactPhase (fromEnum UpdateObservers) $-      atom ("update_observer_" ++ name) $ do-        let e' = c2aExpr meta e-        W.AssignInst <- return (W.assignInst t)-        (A.var' (withPrefix (prefix params) name) . c2aType) t <== e'------------------------------------------------------------------------------------updateBuffers :: Params -> MetaTable -> Core.Spec -> Atom ()-updateBuffers _ meta-  Core.Spec-    { Core.specStreams = streams }-  =-  mapM_ updateBuffer streams--  where--  updateBuffer :: Core.Stream -> Atom ()-  updateBuffer Core.Stream { Core.streamId = id }-    =-    let Just strmInfo = M.lookup id (streamInfoMap meta) in-    updateBuffer1 id strmInfo--  updateBuffer1 :: Core.Id -> StreamInfo -> Atom ()-  updateBuffer1 id-    StreamInfo-      { streamInfoQueue      = que-      , streamInfoTempVar    = tmp-      , streamInfoType       = t   }-    =-    exactPhase (fromEnum UpdateBuffers) $-      atom ("update_buffer_s" ++ show id) $ do-        W.AssignInst <- return (W.assignInst t)-        Q.dropFirstElemAndSnoc (A.value tmp) que

@@ -1,55 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE GADTs #-}--module Copilot.Compile.C99.PrePostCode-  ( preCode , postCode-  ) where--import Copilot.Core-import Copilot.Compile.C99.Common (typeSpec, mkTmpExtFunVarName)-import Copilot.Compile.C99.Params-import Copilot.Compile.C99.Phases (numberOfPhases)-import Copilot.Compile.Header.C99 (c99HeaderName)------------------------------------------------------------------------------------preCode :: Params -> Spec -> String-preCode params spec = unlines $-  [ "#include \"" ++ c99HeaderName (prefix params) ++ "\"" ] ++-  ( map (observerDecl params) . specObservers ) spec ++-  ( map (tmpExtFunVar params) . externFuns    ) spec------------------------------------------------------------------------------------observerDecl :: Params -> Observer -> String-observerDecl params (Observer cs _ t) = typeSpec t ++ " " ++ name ++ ";"-  where name = withPrefix (prefix params) cs------------------------------------------------------------------------------------tmpExtFunVar :: Params -> ExtFun -> String-tmpExtFunVar _ ExtFun-  { externFunName = name-  , externFunType = t-  , externFunTag  = mtag } =-    case mtag of-      Nothing  -> impossible "tmpExtFunVar" "copilot-c99"-      Just tag -> "static " ++ typeSpec t ++ " " -                    ++ mkTmpExtFunVarName name tag ++ ";"------------------------------------------------------------------------------------postCode :: Params -> Spec -> String-postCode params _ =-  unlines-    [ "void " ++ withPrefix (prefix params) "step" ++ "()"-    , "{"-    , "  " ++ concat (replicate numberOfPhases step)-    , "}"-    ]--  where step = withPrefix (prefix params) "copilot" ++ "();"-  

@@ -1,56 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------module Copilot.Compile.C99.Queue-  ( Queue-  , dropFirstElemAndSnoc-  , lookahead-  , size-  , queue-  ) where--import Data.Word (Word16)-import Language.Atom--type QueueIndexType = Word16--data Queue a = Queue-  { queueRingBuffer :: A a-  , queuePointer    :: V QueueIndexType-  , size            :: QueueIndexType-  }--dropFirstElemAndSnoc :: Assign a => E a -> Queue a -> Atom ()-dropFirstElemAndSnoc x-  Queue-    { queueRingBuffer = buf-    , queuePointer    = p-    , size            = sz-    } =-  do-    (buf ! value p) <== x-    p <== ((value p + 1) `mod_` fromIntegral sz)--lookahead :: Expr a => Int -> Queue a -> E a-lookahead i-  Queue-    { queueRingBuffer = buf-    , queuePointer    = p-    , size            = sz-    } =-  let-    k = (value p + fromIntegral i) `mod_` fromIntegral sz-  in-    buf !. k--queue :: Expr a => String -> [a] -> Atom (Queue a)-queue name xs =-  do-    buf <- array ("queue_buffer_" ++ name) xs-    p   <- var   ("queue_pointer_" ++ name) 0-    return-      Queue-        { queueRingBuffer = buf-        , queuePointer    = p-        , size            = fromIntegral (length xs) }

@@ -1,134 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification #-}--module Copilot.Compile.C99.Test.CheckSpec (checkSpec) where--import Copilot.Core ( Spec (..), Trigger(..))-import Copilot.Core.Expr (Name, UExpr (..))-import Copilot.Core.Type.Eq (UVal (..))-import Copilot.Core.Interpret.Eval (eval)-import Copilot.Compile.C99 (compile, c99DirName, c99FileRoot)-import Copilot.Compile.C99.Params (Params (..), defaultParams)-import Copilot.Compile.C99.Test.Driver (driver)-import Copilot.Compile.C99.Test.Iteration (Iteration(..), execTraceToIterations)-import Copilot.Compile.C99.Test.ReadCSV (iterationsFromCSV)-import Copilot.Core.Type.Show (ShowType(..))-import Copilot.Core.Type.Read (readWithType)--import qualified Data.Map as M-import Data.List (foldl')-import qualified Data.ByteString.Char8 as B-import qualified Data.Text.IO as TIO-import System.Directory (removeDirectoryRecursive)-import System.Process (system, readProcess)-import Control.Monad (when, unless)-import Text.PrettyPrint (text, (<+>), ($$), render, vcat, hang)------------------------------------------------------------------------------------checkSpec :: Int -> Spec -> IO Bool-checkSpec numIterations spec = do-  genCFiles numIterations spec-  compileCFiles-  csv <- execute numIterations-  let is1 = iterationsFromCSV csv-  let is2 = interp numIterations spec-  let eq = typedOutputs spec is1 == typedOutputs spec is2-  unless eq (putStrLn $ showCompare is1 is2)-  when eq cleanUp -- Keep things around if there's a failure-  return eq------------------------------------------------------------------------------------showCompare :: [Iteration] -> [Iteration] -> String-showCompare s1 s2 =-  render $ text "From C:" <+> text "---" <+> text "From Interpreter:" $$ -    (vcat $ map (\(a,b) -> hang a 10 b) zipped)-  where-  zipped  = zip (toDoc s1) (toDoc s2)-  toDoc   = map (text . show) -------------------------------------------------------------------------------------- mapping triggers to arg values-type TypedIteration = M.Map Name [UVal]---- list of output values for comparison-typedOutputs :: Spec -> [Iteration] -> [TypedIteration]-typedOutputs Spec { specTriggers = triggers } = -  map recoverTypes--  where-  recoverTypes :: Iteration -> TypedIteration-  recoverTypes Iteration { iterationOutputs = iterMap } = -    M.mapWithKey recoverType iterMap--  recoverType :: Name -> [String] -> [UVal]-  recoverType trigName outs = -    let types = typedTriggerArgs M.! trigName in-    map typedRead (zip types outs)--  typedRead :: (UExpr, String) -> UVal-  typedRead (UExpr { uExprType = t }, output) = -    UVal { uType = t-         , uVal = readWithType t output }--  typedTriggerArgs :: M.Map Name [UExpr]-  typedTriggerArgs = -    foldl' mkMap M.empty triggers-    where -    mkMap mp trig = M.insert (triggerName trig) (triggerArgs trig) mp------------------------------------------------------------------------------------driverFile :: String-driverFile = "driver.c"--outputFile :: String-outputFile = "_test"------------------------------------------------------------------------------------genCFiles :: Int -> Spec -> IO ()-genCFiles numIterations spec = do-  compile (defaultParams { prefix = Nothing, verbose = False }) spec-  TIO.writeFile (c99DirName ++ "/" ++ driverFile) -                (driver numIterations spec)------------------------------------------------------------------------------------compileCFiles :: IO ()-compileCFiles = do-  _ <- system $ unwords [ "cd " ++ c99DirName ++ ";"-                        , "gcc"-                        , c99FileRoot ++ ".c" -                        , driverFile -                        , "-o"-                        , outputFile ]-  return ()------------------------------------------------------------------------------------execute :: Int -> IO B.ByteString-execute _ =-  fmap B.pack (readProcess ("./" ++ c99DirName ++ "/" ++ outputFile) [] "")------------------------------------------------------------------------------------interp :: Int -> Spec -> [Iteration]-interp numIterations = -  execTraceToIterations . eval C numIterations ------------------------------------------------------------------------------------cleanUp :: IO ()-cleanUp = removeDirectoryRecursive c99DirName-  -- removeFile $ c99FileRoot ++ ".c"-  -- removeFile $ c99FileRoot ++ ".h"-  -- removeFile driverFile-  -- removeFile outputFile----------------------------------------------------------------------------------

@@ -1,263 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE GADTs #-}-{-# LANGUAGE Rank2Types #-}--module Copilot.Compile.C99.Test.Driver-  ( driver---  , ExtVars-  ) where--import Copilot.Core-  ( Spec(..), Trigger(..), UExpr(..), Type(..), UType(..), Name-  , Expr(..), Stream(..)-  )---import Copilot.Core.Error (impossible)-import Copilot.Core.Type (Typed, typeOf)-import Copilot.Core.Type.Dynamic (DynamicF (..), toDynF)-import Copilot.Core.Type.Show (showWithType, ShowType (..))---import Copilot.Core.Interpret.Eval (ExtEnv(..))--import Data.List (intersperse, nubBy)-import Data.Text (Text)-import Data.Text (pack)-import Text.PrettyPrint-  ( Doc, ($$), (<>), (<+>), nest, text, empty, render, vcat-  , hcat, space, equals, semi, lbrack, rbrack, comma-  , punctuate, hsep, lbrace, rbrace)------------------------------------------------------------------------------------driver :: Int -> Spec -> Text-driver numIterations Spec { specTriggers = trigs -                          , specStreams = streams } -  =-  pack . render $-    ppHeader $$-    ppEnvDecls numIterations env $$-    ppMain numIterations env $$-    ppTriggers trigs-  where -  env :: [ExtVars]-  env = nubBy (\(name0,_) (name1,_) -> name0 == name1) -              (concatMap extractExts exprs)-  exprs =    map strmExpr streams-          ++ concatMap triggerArgs trigs -          ++ map uexpr (map triggerGuard trigs)-  strmExpr Stream { streamExpr = expr } = uexpr expr-  uexpr :: Typed a => Expr a -> UExpr-  uexpr e = UExpr { uExprType = typeOf-                  , uExprExpr = e }-------------------------------------------------------------------------------------- XXX will need to be generalized to external arrays and functions at some--- point.-type  ExtVars = (Name, DynamicF [] Type)--extractExts :: UExpr -> [ExtVars]-extractExts UExpr { uExprExpr = expr } -  = go expr--  where-  go :: Expr a -> [ExtVars]-  go e =-    case e of-      Const _ _                    -> []-      Drop _ _ _                   -> []-      Local _ _ _ e0 e1            -> go e0 ++ go e1-      Var _ _                      -> []-      ExternVar t name mvals       -> -        case mvals of-          Nothing   -> impossible "extractExts" "copilot-c99/Test" -          Just vals -> [(name, toDynF t vals)]-      ExternFun _ _ es _ _         -> concatMap extractExts es-      ExternArray _ _ _ _ idx _ _  -> go idx-      Op1 _ e0                     -> go e0-      Op2 _ e0 e1                  -> go e0 ++ go e1-      Op3 _ e0 e1 e2               -> go e0 ++ go e1 ++ go e2------------------------------------------------------------------------------------ppHeader :: Doc-ppHeader =-  vcat $-    [ text "#include <stdint.h>"-    , text "#include <inttypes.h>"-    , text "#include <stdio.h>"-    , text "#include \"copilot.h\""-    ]------------------------------------------------------------------------------------ppEnvDecls :: Int -> [ExtVars] -> Doc-ppEnvDecls numIterations vars = -  vcat $  -    [ space  -    , text "// External variables" -    , vcat $ map ppEnvDecl vars-    , space-    , text "// External values" -    , vcat $ map ppVals vars-    , space-    , space-    ]--  where-  ppEnvDecl :: (Name, DynamicF [] Type) -> Doc-  ppEnvDecl (name, DynamicF _ t) = -    cType <+> text name <> semi-    where-    cType = ppUType UType { uTypeType = t }--  ppVals :: (Name, DynamicF [] Type) -> Doc-  ppVals (name, DynamicF vals t) = -    cType <+> valsName name -      <> lbrack <> (text . show) numIterations <> rbrack -      <+> equals <+> lbrace <+> arrVals <+> rbrace <> semi-    where-    cType = ppUType UType { uTypeType = t }-    arrVals = hsep $ punctuate comma $ map text showVals-    showVals = map (showWithType C t) vals------------------------------------------------------------------------------------valsName :: Name -> Doc-valsName name = text name <> text "_vals" ------------------------------------------------------------------------------------ppMain :: Int -> [ExtVars] -> Doc-ppMain numIterations vars =-  vcat $-    [ text "int main(int argc, char const *argv[]) {"-    , text "  int i;"-    , text "  for (i = 0; i < " <> rnds <> text "; i++) {"-    , space-    , vcat $ map (nest 3) $ map assignVals vars-    , space-    , text "    if (i > 0) printf(\"#\\n\");"-    , text "    " <> text "step();"-    , text "  }"-    , text "  return 0;"-    , text "}"-    , space-    ]--  where-  rnds = text $ show numIterations-  assignVals :: (Name, DynamicF [] Type) -> Doc-  assignVals (name, _) = -    text name <+> equals <+> -      valsName name <> lbrack <> text "i" <> rbrack <> semi------------------------------------------------------------------------------------ppTriggers :: [Trigger] -> Doc-ppTriggers = foldr ($$) empty . map ppTrigger--ppTrigger :: Trigger -> Doc-ppTrigger Trigger { triggerName = name-                  , triggerArgs = args } -  =-  hcat $-    [ text "void" <+> text name <+> -           text "(" <> ppPars args <> text ")"-    , text "{"-    , nest 2 $ ppPrintf name args <> text ";"-    , text "}"-    ]------------------------------------------------------------------------------------ppPrintf :: String -> [UExpr] -> Doc-ppPrintf name args =-  text "printf(\"" <>-  text name <>-  text "," <>-  ppFormats args <>-  text "\"\\n\"," <+>-  ppArgs args <>-  text ")"------------------------------------------------------------------------------------ppFormats :: [UExpr] -> Doc-ppFormats-  = vcat-  . intersperse (text ",")-  . map (text "%\"" <>)-  . map ppFormat------------------------------------------------------------------------------------ppPars :: [UExpr] -> Doc-ppPars-  = vcat-  . intersperse (text ", ")-  . map ppPar-  . zip [0..]--  where--  ppPar :: (Int, UExpr) -> Doc-  ppPar (k, par) = case par of-    UExpr-      { uExprType = t } ->-          ppUType (UType t) <+> text ("t" ++ show k)------------------------------------------------------------------------------------ppArgs :: [UExpr] -> Doc-ppArgs args-  = vcat-  $ intersperse (text ", ")-  $ map ppArg-  $ [0..length args-1]--  where--  ppArg :: Int -> Doc-  ppArg k = text ("t" ++ show k)------------------------------------------------------------------------------------ppUType :: UType -> Doc-ppUType UType { uTypeType = t }-  = text $ 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"------------------------------------------------------------------------------------ppFormat :: UExpr -> Doc-ppFormat-  UExpr { uExprType = t } =-  text $ case t of-    Bool   -> "PRIu8"-    Int8   -> "PRIi8"-    Int16  -> "PRIi16"-    Int32  -> "PRIi32"-    Int64  -> "PRIi64"-    Word8  -> "PRIu8"-    Word16 -> "PRIu16"-    Word32 -> "PRIu32"-    Word64 -> "PRIu64"-    Float  -> "\"f\""-    Double -> "\"lf\""-----------------------------------------------------------------------------------

@@ -1,48 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------module Copilot.Compile.C99.Test.Iteration-  ( Iteration (..)-  , execTraceToIterations-  ) where--import Copilot.Core.Interpret.Eval (ExecTrace (..), Output)-import Data.List (unfoldr)-import Data.Map (Map)-import qualified Data.Map as M-import Data.Maybe (isJust, fromJust)---- An iteration represents the output of all triggers within a single--- iteration.-newtype Iteration =-  Iteration-    { iterationOutputs :: (Map String [Output]) }-  deriving Eq--instance Show Iteration where-  show Iteration { iterationOutputs = io } = show $ M.toList io--execTraceToIterations :: ExecTrace -> [Iteration]-execTraceToIterations = unfoldr step--  where--  step :: ExecTrace -> Maybe (Iteration, ExecTrace)-  step trace@ExecTrace { interpTriggers  = trigs }-    | nullary   = Nothing-    | otherwise = Just (iteration, tails)--    where-    iteration :: Iteration-    iteration = Iteration $-      fmap fromJust-        $ M.filter isJust-        $ fmap head-        $ trigs--    nullary :: Bool-    nullary = any null (M.elems trigs)--    tails :: ExecTrace-    tails = trace { interpTriggers = fmap tail trigs }

@@ -1,47 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------module Copilot.Compile.C99.Test.ReadCSV (iterationsFromCSV) where--import Copilot.Core.Interpret.Eval (Output)-import Copilot.Core.Error (impossible)-import Copilot.Compile.C99.Test.Iteration (Iteration (..))--import Prelude as P-import qualified Data.Vector as V-import qualified Data.ByteString.Char8 as B-import qualified Data.Map as M-import Text.CSV as C--parseError :: a-parseError = impossible "CSV parsing" "copilot-c99"--iterationsFromCSV :: B.ByteString -> [Iteration]-iterationsFromCSV bs =-  case C.parseCSV "csvParseErrors" (B.unpack bs) of-    Left  err -> error (show err)-    Right res -> iterationsFromCSV' res--iterationsFromCSV' :: C.CSV -> [Iteration]-iterationsFromCSV' = map Iteration . go M.empty-  where-  go m []             = [m]-  go m (x:xs)-    | nextIteration x = m : go M.empty xs-    | otherwise =-        let-          m' = M.insert (triggerName x) (triggerOutputs x) m-        in-          go m' xs--nextIteration :: Record -> Bool-nextIteration [x] = x == "#"-nextIteration _   = False--triggerName :: Record -> String-triggerName = head--triggerOutputs :: Record -> [Output]-triggerOutputs = tail-

@@ -0,0 +1,148 @@+{-# LANGUAGE GADTs #-}++module Copilot.Compile.C99.Translate where++import Control.Monad.State++import Copilot.Core+import Copilot.Compile.C99.Util++import qualified Language.C99.Simple as C++-- | Translates a Copilot expression into a C99 expression.+transexpr :: Expr a -> State FunEnv C.Expr+transexpr (Const ty x) = return $ constty ty x++transexpr (Local ty1 _ name e1 e2) = do+  e1' <- transexpr e1+  e2' <- transexpr e2+  let cty1 = transtype ty1+      init = Just $ C.InitExpr e1'+  statetell ([C.VarDecln Nothing cty1 name init], [])+  return $ e2'++transexpr (Var _ n) = return $ C.Ident n++transexpr (Drop _ amount sid) = do+  let var    = streamname sid+      indexvar = indexname sid+      index  = case amount of+        0 -> C.Ident indexvar+        n -> C.Ident indexvar C..+ C.LitInt (fromIntegral n)+  return $ C.Index (C.Ident var) index++transexpr (ExternVar _ name _) = return $ C.Ident (excpyname name)++transexpr (ExternFun _ _ _ _ _) = undefined++transexpr (Label _ _ _) = undefined++transexpr (Op1 op e) = do+  e' <- transexpr e+  return $ transop1 op e'++transexpr (Op2 op e1 e2) = do+  e1' <- transexpr e1+  e2' <- transexpr e2+  return $ transop2 op e1' e2'++transexpr (Op3 op e1 e2 e3) = do+  e1' <- transexpr e1+  e2' <- transexpr e2+  e3' <- transexpr e3+  return $ transop3 op e1' e2' e3'+++-- | Translates a Copilot unary operator and arguments into a C99 expression.+transop1 :: Op1 a b -> C.Expr -> C.Expr+transop1 op e = case op of+  Not             -> (C..!) e+  Abs      _      -> funcall "abs"      [e]+  Sign     _      -> funcall "copysign" [C.LitDouble 1.0, e]+  Recip    _      -> C.LitDouble 1.0 C../ e+  Exp      _      -> funcall "exp"   [e]+  Sqrt     _      -> funcall "sqrt"  [e]+  Log      _      -> funcall "log"   [e]+  Sin      _      -> funcall "sin"   [e]+  Tan      _      -> funcall "tan"   [e]+  Cos      _      -> funcall "cos"   [e]+  Asin     _      -> funcall "asin"  [e]+  Atan     _      -> funcall "atan"  [e]+  Acos     _      -> funcall "acos"  [e]+  Sinh     _      -> funcall "sinh"  [e]+  Tanh     _      -> funcall "tanh"  [e]+  Cosh     _      -> funcall "cosh"  [e]+  Asinh    _      -> funcall "asinh" [e]+  Atanh    _      -> funcall "atanh" [e]+  Acosh    _      -> funcall "acosh" [e]+  BwNot    _      -> (C..~) e+  Cast     _ ty  -> C.Cast (transtypename ty) e+  GetField _  _ n -> C.Dot e n++-- | Translates a Copilot binary operator and arguments into a C99 expression.+transop2 :: Op2 a b c -> C.Expr -> C.Expr -> C.Expr+transop2 op e1 e2 = case op of+  And          -> e1 C..&& e2+  Or           -> e1 C..|| e2+  Add      _   -> e1 C..+  e2+  Sub      _   -> e1 C..-  e2+  Mul      _   -> e1 C..*  e2+  Mod      _   -> e1 C..%  e2+  Div      _   -> e1 C../  e2+  Fdiv     _   -> e1 C../  e2+  Pow      _   -> funcall "pow" [e1, e2]+  Logb     _   -> funcall "log" [e2] C../ funcall "log" [e1]+  Eq       _   -> e1 C..== e2+  Ne       _   -> e1 C..!= e2+  Le       _   -> e1 C..<= e2+  Ge       _   -> e1 C..>= e2+  Lt       _   -> e1 C..<  e2+  Gt       _   -> e1 C..>  e2+  BwAnd    _   -> e1 C..&  e2+  BwOr     _   -> e1 C..|  e2+  BwXor    _   -> e1 C..^  e2+  BwShiftL _ _ -> e1 C..<< e2+  BwShiftR _ _ -> e1 C..>> e2+  Index    _   -> C.Index e1 e2++-- | Translates a Copilot ternaty operator and arguments into a C99 expression.+transop3 :: Op3 a b c d -> C.Expr -> C.Expr -> C.Expr -> C.Expr+transop3 op e1 e2 e3 = case op of+  Mux _ -> C.Cond e1 e2 e3++-- | Give a C99 literal expression based on a value and a type.+constty :: Type a -> a -> C.Expr+constty ty = case ty of+  Bool   -> C.LitBool+  Int8   -> C.LitInt . fromIntegral+  Int16  -> C.LitInt . fromIntegral+  Int32  -> C.LitInt . fromIntegral+  Int64  -> C.LitInt . fromIntegral+  Word8  -> C.LitInt . fromIntegral+  Word16 -> C.LitInt . fromIntegral+  Word32 -> C.LitInt . fromIntegral+  Word64 -> C.LitInt . fromIntegral+  Float  -> C.LitFloat+  Double -> C.LitDouble++-- | Translate a Copilot type to a C99 type.+transtype :: Type a -> C.Type+transtype ty = case ty of+  Bool      -> C.TypeSpec $ C.TypedefName "bool"+  Int8      -> C.TypeSpec $ C.TypedefName "int8_t"+  Int16     -> C.TypeSpec $ C.TypedefName "int16_t"+  Int32     -> C.TypeSpec $ C.TypedefName "int32_t"+  Int64     -> C.TypeSpec $ C.TypedefName "int64_t"+  Word8     -> C.TypeSpec $ C.TypedefName "uint8_t"+  Word16    -> C.TypeSpec $ C.TypedefName "uint16_t"+  Word32    -> C.TypeSpec $ C.TypedefName "uint32_t"+  Word64    -> C.TypeSpec $ C.TypedefName "uint64_t"+  Float     -> C.TypeSpec C.Float+  Double    -> C.TypeSpec C.Double+  Array ty' -> C.Array (transtype ty') size where+    size = Just $ C.LitInt $ fromIntegral $ tysize ty+  Struct s  -> C.TypeSpec $ C.Struct (typename s)++-- | Translate a Copilot type intro a C typename+transtypename :: Type a -> C.TypeName+transtypename ty = C.TypeName $ transtype ty

@@ -0,0 +1,54 @@+module Copilot.Compile.C99.Util where++import Control.Monad.State++import Copilot.Core  (Id)+import qualified Language.C99.Simple.AST as C+++type FunEnv = ([C.Decln], [C.Ident])++-- | `tell` equivalent for `State`.+statetell :: Monoid m => m -> State m ()+statetell m = modify ((flip mappend) m)++-- | Generate fresh variable name based on a given one.+fresh :: String -> [String] -> String+fresh name used = head $ dropWhile (flip elem used) (name:freshnames) where+  freshnames = (name ++).show <$> [0..]++-- | Collect all the names from a list of C99 declarations.+names :: [C.Decln] -> [String]+names ds = map match ds where+  match (C.VarDecln _ _ name _) = name++-- | Turn a stream id into a suitable C variable name.+streamname :: Id -> String+streamname sid = "s" ++ show sid++-- | Turn a stream id into the global varname for indices.+indexname :: Id -> String+indexname sid = streamname sid ++ "_idx"++-- | Add a postfix for copies of external variables the name.+excpyname :: String -> String+excpyname name = name ++ "_cpy"++-- | Turn stream id into name of its generator function.+generatorname :: Id -> String+generatorname sid = streamname sid ++ "_gen"++-- | Turn a the name of a trigger into a guard generator.+guardname :: String -> String+guardname name = name ++ "_guard"++-- | Turn a trigger name into a an trigger argument name.+argname :: String -> Int -> String+argname name n = name ++ "_arg" ++ show n++-- | Enumerate all argument names based on trigger name.+argnames :: String -> [String]+argnames base = [aname | n <- [0..], let aname = argname base n]++funcall :: C.Ident -> [C.Expr] -> C.Expr+funcall name args = C.Funcall (C.Ident name) args

@@ -1,143 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE GADTs #-}--module Copilot.Compile.C99.Witness-  ( ExprInst (..)      , exprInst-  , AssignInst (..)    , assignInst-  , EqEInst (..)       , eqEInst-  , OrdEInst (..)      , ordEInst-  , NumEInst (..)      , numEInst-  , IntegralEInst (..) , integralEInst-  , FloatingEInst (..) , floatingEInst-  , BitsEInst (..)     , bitsEInst-  ) where--import qualified Language.Atom as A-import qualified Copilot.Core as C-import Data.Bits------------------------------------------------------------------------------------badInst :: a-badInst = -  error "Fatal cast in the witnesses of Atom in copilot-sbv.  Are you sure that Atom supports the type you are using?  If you you are, or you don't understand the error, email leepike @ gmail . com (remove spaces) or file a bug report on github.com"------------------------------------------------------------------------------------data ExprInst a = A.Expr a => ExprInst--exprInst :: C.Type a -> ExprInst a-exprInst t =-  case t of-    C.Bool   -> ExprInst-    C.Int8   -> ExprInst ; C.Int16  -> ExprInst-    C.Int32  -> ExprInst ; C.Int64  -> ExprInst-    C.Word8  -> ExprInst ; C.Word16 -> ExprInst-    C.Word32 -> ExprInst ; C.Word64 -> ExprInst-    C.Float  -> ExprInst ; C.Double -> ExprInst------------------------------------------------------------------------------------data AssignInst a = A.Assign a => AssignInst--assignInst :: C.Type a -> AssignInst a-assignInst t =-  case t of-    C.Bool   -> AssignInst-    C.Int8   -> AssignInst ; C.Int16  -> AssignInst-    C.Int32  -> AssignInst ; C.Int64  -> AssignInst-    C.Word8  -> AssignInst ; C.Word16 -> AssignInst-    C.Word32 -> AssignInst ; C.Word64 -> AssignInst-    C.Float  -> AssignInst ; C.Double -> AssignInst------------------------------------------------------------------------------------data EqEInst a = A.EqE a => EqEInst--eqEInst :: Eq a => C.Type a -> EqEInst a-eqEInst t =-  case t of-    C.Bool   -> EqEInst-    C.Int8   -> EqEInst ; C.Int16  -> EqEInst-    C.Int32  -> EqEInst ; C.Int64  -> EqEInst-    C.Word8  -> EqEInst ; C.Word16 -> EqEInst-    C.Word32 -> EqEInst ; C.Word64 -> EqEInst-    C.Float  -> EqEInst ; C.Double -> EqEInst------------------------------------------------------------------------------------data OrdEInst a = A.OrdE a => OrdEInst--ordEInst :: Ord a => C.Type a -> OrdEInst a-ordEInst t =-  case t of-    C.Bool   -> badInst -    C.Int8   -> OrdEInst ; C.Int16  -> OrdEInst-    C.Int32  -> OrdEInst ; C.Int64  -> OrdEInst-    C.Word8  -> OrdEInst ; C.Word16 -> OrdEInst-    C.Word32 -> OrdEInst ; C.Word64 -> OrdEInst-    C.Float  -> OrdEInst ; C.Double -> OrdEInst------------------------------------------------------------------------------------data NumEInst a = A.NumE a => NumEInst--numEInst :: Num a => C.Type a -> NumEInst a-numEInst t =-  case t of-    C.Bool   -> badInst-    C.Int8   -> NumEInst ; C.Int16  -> NumEInst-    C.Int32  -> NumEInst ; C.Int64  -> NumEInst-    C.Word8  -> NumEInst ; C.Word16 -> NumEInst-    C.Word32 -> NumEInst ; C.Word64 -> NumEInst-    C.Float  -> NumEInst ; C.Double -> NumEInst------------------------------------------------------------------------------------data IntegralEInst a = A.IntegralE a => IntegralEInst--integralEInst :: Integral a => C.Type a -> IntegralEInst a-integralEInst t =-  case t of-    C.Bool   -> badInst -    C.Int8   -> IntegralEInst ; C.Int16  -> IntegralEInst-    C.Int32  -> IntegralEInst ; C.Int64  -> IntegralEInst-    C.Word8  -> IntegralEInst ; C.Word16 -> IntegralEInst-    C.Word32 -> IntegralEInst ; C.Word64 -> IntegralEInst-    C.Float  -> badInst-    C.Double -> badInst ------------------------------------------------------------------------------------data FloatingEInst a = A.FloatingE a => FloatingEInst--floatingEInst :: Floating a => C.Type a -> FloatingEInst a-floatingEInst t =-  case t of-    C.Float  -> FloatingEInst-    C.Double -> FloatingEInst-    _          -> badInst------------------------------------------------------------------------------------data BitsEInst a = ( A.Expr a, A.OrdE a, A.EqE a, A.IntegralE a, Bits a ) => BitsEInst--bitsEInst :: Bits a => C.Type a -> BitsEInst a-bitsEInst t =-  case t of-    C.Bool   -> badInst-    C.Int8   -> BitsEInst-    C.Int16  -> BitsEInst-    C.Int32  -> BitsEInst-    C.Int64  -> BitsEInst-    C.Word8  -> BitsEInst-    C.Word16 -> BitsEInst-    C.Word32 -> BitsEInst-    C.Word64 -> BitsEInst-    C.Float  -> badInst-    C.Double -> badInst----------------------------------------------------------------------------------

@@ -1,58 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification #-}--module Main (main) where--import Copilot.Core.PrettyPrint (prettyPrint)-import Copilot.Core.Random (randomSpec)-import Copilot.Core.Random.Weights (Weights (..), simpleWeights)-import Copilot.Compile.C99.Test.CheckSpec (checkSpec)--import Prelude-import System.Random-import Control.Monad (when, unless)--myWeights :: Weights-myWeights =-  simpleWeights-    { maxExprDepth = 2-    , maxBuffSize  = 2-    , maxTriggers  = 1-    , maxTrigArgs  = 1-    , maxObservers = 0-    , numStreams   = 3 -    , floatFreq    = 1-    , doubleFreq   = 1-    , divModFreq   = False-    }---- XXX we'll make this a parameter at some point-numIterations :: Int-numIterations = 10--testRandomSpec :: IO Bool-testRandomSpec = do-  g <- newStdGen-  let spec = randomSpec numIterations myWeights g---  let env = randomExtVals numIterations spec myWeights g-  putStrLn "------------------------------------------"-  putStrLn "Specification to test:"-  putStrLn $ prettyPrint spec-  checkSpec numIterations spec--main :: IO ()-main = do-  putStrLn "Enter the number of random specifications to test:"-  i <- readLn :: IO Int-  go i-  where -  go 0 = putStrLn "No failures found."-  go i = do -    b <- testRandomSpec-    when b   $ putStrLn "" >> go (i-1)-    unless b $ putStrLn "Inconsistency found!" >> return ()-                            -