diff --git a/copilot-core.cabal b/copilot-core.cabal --- a/copilot-core.cabal +++ b/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 2.1.1 +version: 2.1.2 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. @@ -15,7 +15,7 @@ . author: Lee Pike, Robin Morisset, Alwyn Goodloe, - Sebastian Niller, Nis Nordby Wegmann + Sebastian Niller, Nis Nordbyop Wegmann license: BSD3 license-file: LICENSE maintainer: leepike@gmail.com @@ -43,15 +43,17 @@ --enable-library-profiling - -fpackage-trust - -- Trusted packages - -trust base - -trust random - -trust array + -- -fpackage-trust + -- -- Trusted packages + -- -trust base + -- -trust random + -- -trust array + -- -trust dlist + -- -trust containers build-depends: - base >= 4.0 && <= 5.0, containers >= 0.4, + base >= 4.0 && < 5, pretty >= 1.0, random > 1.0, pretty-ncols >= 0.1, diff --git a/src/Copilot/Compile/Header/C99.hs b/src/Copilot/Compile/Header/C99.hs --- a/src/Copilot/Compile/Header/C99.hs +++ b/src/Copilot/Compile/Header/C99.hs @@ -7,6 +7,7 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE Rank2Types #-} module Copilot.Compile.Header.C99 ( genC99Header @@ -168,20 +169,19 @@ -------------------------------------------------------------------------------- typeSpec :: UType -> String -typeSpec UType { uTypeType = t } = typeSpec' t - - where - typeSpec' Bool = "bool" - typeSpec' Int8 = "int8_t" - typeSpec' Int16 = "int16_t" - typeSpec' Int32 = "int32_t" - typeSpec' Int64 = "int64_t" - typeSpec' Word8 = "uint8_t" - typeSpec' Word16 = "uint16_t" - typeSpec' Word32 = "uint32_t" - typeSpec' Word64 = "uint64_t" - typeSpec' Float = "float" - typeSpec' Double = "double" +typeSpec UType { uTypeType = t } + = case t of + Bool -> "bool" + Int8 -> "int8_t" + Int16 -> "int16_t" + Int32 -> "int32_t" + Int64 -> "int64_t" + Word8 -> "uint8_t" + Word16 -> "uint16_t" + Word32 -> "uint32_t" + Word64 -> "uint64_t" + Float -> "float" + Double -> "double" -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs --- a/src/Copilot/Core.hs +++ b/src/Copilot/Core.hs @@ -22,7 +22,7 @@ -- and the pretty-printer -- ("Copilot.Core.PrettyPrint"). -{-# LANGUAGE Safe #-} +{-# LANGUAGE Trustworthy #-} module Copilot.Core ( module Copilot.Core.Error diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs --- a/src/Copilot/Core/External.hs +++ b/src/Copilot/Core/External.hs @@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE Rank2Types #-} diff --git a/src/Copilot/Core/Locals.hs b/src/Copilot/Core/Locals.hs --- a/src/Copilot/Core/Locals.hs +++ b/src/Copilot/Core/Locals.hs @@ -4,7 +4,7 @@ -- | Let expressions. -{-# LANGUAGE Safe #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE ExistentialQuantification #-} module Copilot.Core.Locals diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs --- a/src/Copilot/Core/MakeTags.hs +++ b/src/Copilot/Core/MakeTags.hs @@ -25,14 +25,16 @@ mkTagsSpec :: Spec -> State Int Spec mkTagsSpec Spec - { specStreams = strms - , specObservers = obsvs - , specTriggers = trigs + { specStreams = strms + , specObservers = obsvs + , specTriggers = trigs + , specProperties = props } = - liftM3 Spec + liftM4 Spec (mkTagsStrms strms) (mkTagsObsvs obsvs) (mkTagsTrigs trigs) + (mkTagsProps props) mkTagsStrms :: [Stream] -> State Int [Stream] mkTagsStrms = mapM mkTagsStrm @@ -81,6 +83,13 @@ { triggerName = name , triggerGuard = g' , triggerArgs = args' } + +mkTagsProps :: [Property] -> State Int [Property] +mkTagsProps = mapM mkTagsProp + + where mkTagsProp p = do + e' <- mkTagsExpr (propertyExpr p) + return $ p { propertyExpr = e' } mkTagsUExpr :: UExpr -> State Int UExpr mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } = diff --git a/src/Copilot/Core/Random.hs b/src/Copilot/Core/Random.hs --- a/src/Copilot/Core/Random.hs +++ b/src/Copilot/Core/Random.hs @@ -41,9 +41,10 @@ triggers <- runReaderT (mapM (genTrigger ss) (map mkTriggerName [0..numTriggers-1])) extVars - return Spec { specStreams = streams - , specObservers = [] - , specTriggers = triggers } + return Spec { specStreams = streams + , specObservers = [] + , specTriggers = triggers + , specProperties = [] } where mkTriggerName :: Int -> Name mkTriggerName k = "f" ++ show k diff --git a/src/Copilot/Core/Spec.hs b/src/Copilot/Core/Spec.hs --- a/src/Copilot/Core/Spec.hs +++ b/src/Copilot/Core/Spec.hs @@ -10,6 +10,7 @@ , Observer (..) , Trigger (..) , Spec (..) + , Property (..) ) where import Copilot.Core.Expr (Name, Id, Expr, UExpr) @@ -42,12 +43,20 @@ -------------------------------------------------------------------------------- +-- | A property. +data Property = Property + { propertyName :: Name + , propertyExpr :: Expr Bool } + +-------------------------------------------------------------------------------- + -- | A Copilot specification consists of a list of variables bound to anonymous -- streams, a lost of anomymous streams, a list of observers, and a list of -- triggers. data Spec = Spec { specStreams :: [Stream] , specObservers :: [Observer] - , specTriggers :: [Trigger] } + , specTriggers :: [Trigger] + , specProperties :: [Property] } -------------------------------------------------------------------------------- diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs --- a/src/Copilot/Core/Type/Dynamic.hs +++ b/src/Copilot/Core/Type/Dynamic.hs @@ -16,7 +16,7 @@ {-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-} module Copilot.Core.Type.Dynamic - ( Dynamic + ( Dynamic (..) , DynamicF (..) , toDyn , fromDyn