copilot-core 0.2.3 → 0.2.4

raw patch · 25 files changed

+140/−105 lines, 25 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• copilot-core.cabal +21/−5
• src/Copilot/Compile/Header/C99.hs +3/−6
• src/Copilot/Core.hs +2/−0
• src/Copilot/Core/Error.hs +2/−0
• src/Copilot/Core/Expr.hs +1/−0
• src/Copilot/Core/External.hs +1/−2
• src/Copilot/Core/Interpret.hs +2/−0
• src/Copilot/Core/Interpret/Eval.hs +1/−0
• src/Copilot/Core/Interpret/Render.hs +2/−0
• src/Copilot/Core/Locals.hs +87/−0
• src/Copilot/Core/MakeTags.hs +2/−2
• src/Copilot/Core/Operators.hs +1/−0
• src/Copilot/Core/PrettyPrint.hs +1/−0
• src/Copilot/Core/Random.hs +1/−1
• src/Copilot/Core/Random/Gen.hs +1/−0
• src/Copilot/Core/Random/Weights.hs +2/−0
• src/Copilot/Core/Spec.hs +1/−1
• src/Copilot/Core/Spec/Locals.hs +0/−86
• src/Copilot/Core/Type.hs +2/−1
• src/Copilot/Core/Type/Dynamic.hs +1/−0
• src/Copilot/Core/Type/Eq.hs +1/−0
• src/Copilot/Core/Type/Equality.hs +1/−0
• src/Copilot/Core/Type/Read.hs +1/−0
• src/Copilot/Core/Type/Show.hs +1/−0
• src/Copilot/Core/Type/Uninitialized.hs +2/−1

@@ -1,10 +1,19 @@ cabal-version:       >=1.10 name:                copilot-core-version:             0.2.3+version:             0.2.4 synopsis:            An intermediate representation for Copilot.-description:         Intermediate representation for Copilot.-                     Strictly follows Haskell 2010 except for universal-                     and existential quantification.+description:         +  Intermediate representation for Copilot. +  . +  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/niswegmann/copilot-discussion>.  +  .  +  Examples are available at+  <https://github.com/leepike/Copilot/tree/master/Examples>.+ author:              Lee Pike, Robin Morisset, Alwyn Goodloe,                      Sebastian Niller, Nis Nordby Wegmann license:             BSD3@@ -31,8 +40,15 @@     -auto-all     -caf-all     -fno-warn-orphans+     --enable-library-profiling +    -fpackage-trust    +    -- Trusted packages+    -trust base+    -trust random+    -trust array+   build-depends:     containers >= 0.4 && < 1,     base >= 4.0 && < 5,@@ -55,7 +71,7 @@     Copilot.Core.MakeTags     Copilot.Core.Operators     Copilot.Core.Spec-    Copilot.Core.Spec.Locals+    Copilot.Core.Locals     Copilot.Core.Random     Copilot.Core.Random.Gen     Copilot.Core.Random.Weights

@@ -5,6 +5,7 @@ -- | Generates a C99 header from a copilot-specification. The functionality -- provided by the header must be implemented by back-ends targetting C99. +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-}  module Copilot.Compile.Header.C99@@ -125,9 +126,7 @@  ppExternalArrays :: [ExtArray] -> Doc ppExternalArrays = vcat . map ppExternalArray . nubBy eq-   where-   eq ExtArray { externArrayName = name1 } ExtArray { externArrayName = name2 } =     name1 == name2 @@ -146,9 +145,7 @@  ppExternalFunctions :: [ExtFun] -> Doc ppExternalFunctions = vcat . map ppExternalFunction . nubBy eq-   where-   eq ExtFun { externFunName = name1 } ExtFun { externFunName = name2 } =     name1 == name2 @@ -162,7 +159,6 @@         text "(" <> ppArgs args <> text ");"    where-   ppArgs :: [UExpr] -> Doc   ppArgs = hcat . intersperse (text ",") . map ppArg @@ -175,7 +171,6 @@ typeSpec UType { uTypeType = t } = typeSpec' t    where-   typeSpec' Bool = "bool"   typeSpec' Int8   = "int8_t"   typeSpec' Int16  = "int16_t"@@ -197,3 +192,5 @@  unlines :: [String] -> Doc unlines = vcat . map text++--------------------------------------------------------------------------------

@@ -22,6 +22,8 @@ -- and the pretty-printer -- ("Copilot.Core.PrettyPrint"). +{-# LANGUAGE Safe #-}+ module Copilot.Core   ( module Copilot.Core.Error   , module Copilot.Core.Expr

@@ -2,6 +2,8 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Core.Error    ( impossible   , badUsage ) where

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, ExistentialQuantification #-}  module Copilot.Core.Expr

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE Rank2Types #-} @@ -41,9 +42,7 @@  externVars :: Spec -> [ExtVar] externVars = nubBy eqExt . toList . all externVarsExpr-   where-   eqExt :: ExtVar -> ExtVar -> Bool   eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } =     name1 == name2

@@ -4,6 +4,8 @@  -- | An interpreter for Copilot specifications. +{-# LANGUAGE Safe #-}+ module Copilot.Core.Interpret   ( --ExtEnv (..)     Format (..)

@@ -4,6 +4,7 @@  -- | A tagless interpreter for Copilot specifications. +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, BangPatterns, DeriveDataTypeable #-}  module Copilot.Core.Interpret.Eval

@@ -4,6 +4,8 @@  -- | An tagless interpreter for Copilot specifications. +{-# LANGUAGE Safe #-}+ module Copilot.Core.Interpret.Render   ( renderAsTable   , renderAsCSV

@@ -0,0 +1,87 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Let expressions.++{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}++module Copilot.Core.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++--------------------------------------------------------------------------------

@@ -4,6 +4,8 @@  -- | Sets a unique tags for each external array/function call. +{-# LANGUAGE Safe #-}+ module Copilot.Core.MakeTags (makeTags) where  import Copilot.Core.Expr@@ -39,7 +41,6 @@     mkTagsStrm Stream       { streamId         = id       , streamBuffer     = xs-      , streamGuard      = g       , streamExpr       = e       , streamExprType   = t } =         do@@ -47,7 +48,6 @@           return $ Stream             { streamId         = id             , streamBuffer     = xs-            , streamGuard      = g             , streamExpr       = e'             , streamExprType   = t } 

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, Rank2Types #-}  module Copilot.Core.Operators

@@ -4,6 +4,7 @@  -- | A pretty printer for Copilot specifications. +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-}  module Copilot.Core.PrettyPrint

@@ -4,6 +4,7 @@  -- | Random spec generator. +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, ExistentialQuantification #-}  module Copilot.Core.Random@@ -135,7 +136,6 @@       Stream         { streamId       = id         , streamBuffer   = xs-        , streamGuard    = Const (typeOf :: Type Bool) True         , streamExpr     = w         , streamExprType = t } 

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, ExistentialQuantification #-}  module Copilot.Core.Random.Gen

@@ -2,6 +2,8 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Core.Random.Weights   ( Depth   , Weights (..)

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-}  module Copilot.Core.Spec@@ -20,7 +21,6 @@ data Stream = forall a. Typed a => Stream   { streamId         :: Id   , streamBuffer     :: [a]-  , streamGuard      :: Expr Bool   , streamExpr       :: Expr a   , streamExprType   :: Type a } 

@@ -1,86 +0,0 @@------------------------------------------------------------------------------------ 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----------------------------------------------------------------------------------

@@ -2,8 +2,9 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | +-- | Typing for Core. +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs, KindSignatures #-}  module Copilot.Core.Type

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE Rank2Types #-} 

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-}  module Copilot.Core.Type.Eq

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs, KindSignatures #-}  module Copilot.Core.Type.Equality

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-}  module Copilot.Core.Type.Read

@@ -2,6 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-} {-# LANGUAGE ExistentialQuantification, GADTs #-}  module Copilot.Core.Type.Show

@@ -2,8 +2,9 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | +-- | Initial values for give types. +{-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-}  module Copilot.Core.Type.Uninitialized