packages feed

copilot-language 3.8 → 3.9

raw patch · 28 files changed

+30/−252 lines, 28 filesdep ~copilot-coredep ~copilot-theoremPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core, copilot-theorem

API changes (from Hackage documentation)

Files

CHANGELOG view
@@ -1,3 +1,7 @@+2022-05-06+        * Version bump (3.9). (#320)+        * Compliance with style guide (partial). (#316)+ 2022-03-07         * Version bump (3.8). (#298)         * Introduce testing infrastructure. (#271)
copilot-language.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             3.8+version:             3.9 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:@@ -42,8 +42,8 @@                , data-reify      >= 0.6 && < 0.7                , mtl             >= 2.0 && < 3 -               , copilot-core    >= 3.8 && < 3.9-               , copilot-theorem >= 3.8 && < 3.9+               , copilot-core    >= 3.9 && < 3.10+               , copilot-theorem >= 3.9 && < 3.10    exposed-modules: Copilot.Language                  , Copilot.Language.Operators.BitWise
src/Copilot/Language.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Main Copilot language export file. --@@ -71,11 +69,7 @@ import Copilot.Language.Spec import Copilot.Language.Stream (Stream) ---------------------------------------------------------------------------------- -- | Transform a high-level Copilot Language specification into a low-level -- Copilot Core specification and pretty-print it to stdout. prettyPrint :: Spec -> IO () prettyPrint e = fmap PP.prettyPrint (reify e) >>= putStr----------------------------------------------------------------------------------
src/Copilot/Language/Analyze.hs view
@@ -1,10 +1,8 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE Safe                #-} {-# LANGUAGE ScopedTypeVariables #-}  -- | Copilot specification sanity check.@@ -29,8 +27,6 @@ import Control.Monad (when, foldM_, foldM) import Control.Exception (Exception, throw) ---------------------------------------------------------------------------------- -- | Exceptions or kinds of errors in Copilot specifications that the analysis -- implemented is able to detect. data AnalyzeException@@ -57,7 +53,7 @@   show NestedArray            = badUsage $     "An external function cannot take another external function or external array as an argument.  Try defining a stream, and using the stream values in the other definition."   show TooMuchRecursion       = badUsage $-    "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition.  Likely, you have accidently defined a circular stream, such as 'x = x'.  Another possibility is you have defined a a polymorphic function with type constraints that references other streams.  For example,\n\n  nats :: (Typed a, Num a) => Stream a\n  nats = [0] ++ nats + 1\n\nis not allowed.  Make the definition monomorphic, or add a level of indirection, like \n\n  nats :: (Typed a, Num a) => Stream a\n  nats = n\n    where n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression.  You can try shrinking the expression by using local variables.  It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."+    "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition.  Likely, you have accidently defined a circular stream, such as 'x = x'.  Another possibility is you have defined a a polymorphic function with type constraints that references other streams.  For example,\n\n  nats :: (Typed a, Num a) => Stream a\n  nats = [0] ++ nats + 1\n\nis not allowed.  Make the definition monomorphic, or add a level of indirection, like \n\n  nats :: (Typed a, Num a) => Stream a\n  nats = n\n    where\n      n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression.  You can try shrinking the expression by using local variables.  It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."   show InvalidField           = badUsage $     "A struct can only take external variables, arrays, or other structs as fields."   show (DifferentTypes name) = badUsage $@@ -77,13 +73,9 @@ maxRecursion :: Int maxRecursion = 100000 ---------------------------------------------------------------------------------- -- | An environment that contains the nodes visited. type Env = Map () ---------------------------------------------------------------------------------- -- | Analyze a Copilot specification and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -96,8 +88,6 @@   mapM_ (analyzeProperty refStreams) (map fst $ theorems $ runSpec spec)   specExts refStreams spec >>= analyzeExts ---------------------------------------------------------------------------------- -- | Analyze a Copilot trigger and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -109,31 +99,23 @@   analyzeTriggerArg :: Arg -> IO ()   analyzeTriggerArg (Arg e) = analyzeExpr refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot observer and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeObserver :: IORef Env -> Observer -> IO () analyzeObserver refStreams (Observer _ e) = analyzeExpr refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot property and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeProperty :: IORef Env -> Property -> IO () analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e ---------------------------------------------------------------------------------- data SeenExtern = NoExtern                 | SeenFun                 | SeenArr                 | SeenStruct ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -165,8 +147,6 @@                              go seenExt nodes' e3       Label _ e           -> go seenExt nodes' e ---------------------------------------------------------------------------------- -- | Detect whether the given stream name has already been visited. -- -- This function throws a 'ReferentialCycle' exception if the second argument@@ -178,16 +158,12 @@     Just () -> throw ReferentialCycle     Nothing -> return () ---------------------------------------------------------------------------------- -- | Check that the level of recursion is not above the max recursion allowed. mapCheck :: IORef Env -> IO Bool mapCheck refStreams = do   ref <- readIORef refStreams   return $ getSize ref > maxRecursion ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream append and report any errors detected. analyzeAppend ::      IORef Env -> DynStableName -> Stream a -> b@@ -200,8 +176,6 @@       modifyIORef refStreams $ M.insert dstn ()       f refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream drop and report any errors detected. -- -- This function can fail if the drop is exercised over a stream that is not an@@ -214,12 +188,9 @@   | otherwise                              = return () analyzeDrop _ _                            = throw DropAppliedToNonAppend ---------------------------------------------------------------------------------- -- Analyzing external variables.  We check that every reference to an external -- variable has the same type, and for external functions, they have the same -- typed arguments.---------------------------------------------------------------------------------  -- | An environment to store external variables, arrays, functions and structs, -- so that we can check types in the expression---e.g., if we declare the same@@ -231,8 +202,6 @@   , externStructArgs :: [(String, [C.SimpleType])]   } ---------------------------------------------------------------------------------- -- | Make sure external variables, functions, arrays, and structs are correctly -- typed. analyzeExts :: ExternEnv -> IO ()@@ -296,8 +265,6 @@            (head grp) -- should be typesafe, since this is from groupBy            grp ---------------------------------------------------------------------------------- -- | Obtain all the externs in a specification. specExts :: IORef Env -> Spec' a -> IO ExternEnv specExts refStreams spec = do@@ -348,11 +315,7 @@                                    go nodes env'' e3       Label _ e              -> go nodes env e ---------------------------------------------------------------------------------- -- | Return the simple C type representation of the type of the values carried -- by a stream. getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)----------------------------------------------------------------------------------
src/Copilot/Language/Error.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-}
src/Copilot/Language/Interpret.hs view
@@ -1,4 +1,4 @@-{- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc. -}+-- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc.  -- | This module implements two interpreters, which may be used to simulated or -- executed Copilot specifications on a computer to understand their behavior@@ -8,8 +8,9 @@ -- One of them uses a format (csv) that may be more machine-readable, while the -- other uses a format that may be easier for humans to read. -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs, FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE Safe              #-}  module Copilot.Language.Interpret   ( csv@@ -21,8 +22,6 @@ import Copilot.Language.Spec (Spec) import Copilot.Language.Reify ---------------------------------------------------------------------------------- -- | Simulate a number of steps of a given specification, printing the results -- in a table in comma-separated value (CSV) format. csv :: Integer -> Spec -> IO ()@@ -30,8 +29,6 @@   putStrLn "Note: CSV format does not output observers."   interpret' I.CSV i spec ---------------------------------------------------------------------------------- -- | Simulate a number of steps of a given specification, printing the results -- in a table in readable format. --@@ -46,5 +43,3 @@ interpret' format i spec = do   coreSpec <- reify spec   putStrLn $ I.interpret format (fromIntegral i) coreSpec----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Array.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe         #-}  {-# LANGUAGE TypeFamilies #-} @@ -18,8 +18,6 @@ import Data.Word                (Word32) import GHC.TypeLits             (KnownNat) ---------------------------------------------------------------------------------- -- | Create a stream that carries an element of an array in another stream. -- -- This function implements a projection of the element of an array at a given@@ -33,5 +31,3 @@          , Typed t'          ) => Stream (Array n t) -> Stream Word32 -> Stream t arr .!! n = Op2 (Index typeOf) arr n----------------------------------------------------------------------------------
src/Copilot/Language/Operators/BitWise.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-}
src/Copilot/Language/Operators/Boolean.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-} @@ -21,8 +19,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | A stream that contains the constant value 'True'. true :: Stream Bool true = constant True@@ -64,5 +60,3 @@ -- | Apply the implication ('==>') operator to two boolean streams, point-wise. (==>) :: Stream Bool -> Stream Bool -> Stream Bool x ==> y = not x || y----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Cast.hs view
@@ -1,9 +1,7 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe                  #-}  -- | Type-safe casting operators. module Copilot.Language.Operators.Cast@@ -16,8 +14,6 @@ import Data.Int import Data.Word ---------------------------------------------------------------------------------- -- | Class to capture casting between types for which it can be performed -- safely. class Cast a b where@@ -30,16 +26,12 @@   -- | Perform an unsafe cast from @Stream a@ to @Stream b@.   unsafeCast :: (Typed a, Typed b) => Stream a -> Stream b ---------------------------------------------------------------------------------- -- | Cast a boolean stream to a stream of numbers, producing 1 if the -- value at a point in time is 'True', and 0 otherwise. castBool :: (Eq a, Num a, Typed a) => Stream Bool -> Stream a castBool (Const bool) = Const $ if bool then 1 else 0 castBool x            = Op3 (C.Mux typeOf) x 1 0 ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Bool Bool where   cast = id@@ -84,15 +76,11 @@ instance Cast Bool Int64 where   cast = castBool ---------------------------------------------------------------------------------- -- | Cast a stream carrying numbers to an integral using 'fromIntegral'. castIntegral :: (Integral a, Typed a, Num b, Typed b) => Stream a -> Stream b castIntegral (Const x) = Const (fromIntegral x) castIntegral x         = Op1 (C.Cast typeOf typeOf) x ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word8 Word8 where   cast = castIntegral@@ -121,8 +109,6 @@ instance Cast Word8 Int64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word16 Word16 where   cast = castIntegral@@ -143,8 +129,6 @@ instance Cast Word16 Int64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word32 Word32 where   cast = castIntegral@@ -157,14 +141,10 @@ instance Cast Word32 Int64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word64 Word64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int8 Int8 where   cast = castIntegral@@ -181,8 +161,6 @@ instance Cast Int8 Int64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int16 Int16 where   cast = castIntegral@@ -195,8 +173,6 @@ instance Cast Int16 Int64 where   cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int32 Int32 where   cast = castIntegral@@ -204,8 +180,6 @@ -- | Cast number to bigger type. instance Cast Int32 Int64 where   cast = castIntegral----------------------------------------------------------------------------------  -- | Identity casting. instance Cast Int64 Int64 where
src/Copilot/Language/Operators/Constant.hs view
@@ -1,10 +1,7 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-} - -- | Primitives to build constant streams. module Copilot.Language.Operators.Constant   ( constant@@ -27,14 +24,10 @@ import Data.Word import Data.Int ---------------------------------------------------------------------------------- -- | Create a constant stream that is equal to the given argument, at any -- point in time. constant :: Typed a => a -> Stream a constant = Const----------------------------------------------------------------------------------  -- | Create a constant stream carrying values of type 'Bool' that is equal to -- the given argument, at any point in time.
src/Copilot/Language/Operators/Eq.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-} @@ -16,8 +14,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | Compare two streams point-wise for equality. -- -- The output stream contains the value True at a point in time if both@@ -33,5 +29,3 @@ (/=) :: (P.Eq a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) /= (Const y) = Const (x P./= y) x /= y = Op2 (Core.Ne typeOf) x y----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Extern.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Primitives to build streams connected to external variables. @@ -26,8 +24,6 @@ import Data.Word import Data.Int ---------------------------------------------------------------------------------- -- | Create a stream populated by an external global variable. -- -- The Copilot compiler does not check that the type is correct. If the list@@ -41,8 +37,6 @@        -> Maybe [a] -- ^ Values to be used exclusively for testing/simulation.        -> Stream a extern = Extern----------------------------------------------------------------------------------  -- | Create a stream carrying values of type Bool, populated by an external -- global variable.
src/Copilot/Language/Operators/Integral.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Integral class operators applied point-wise on streams. @@ -22,8 +20,6 @@ import qualified Prelude as P import Data.List (foldl', replicate) ---------------------------------------------------------------------------------- -- | Apply the 'Prelude.div' operation to two streams, point-wise. div :: (Typed a, P.Integral a) => Stream a -> Stream a -> Stream a (Const 0) `div` _ = Const 0@@ -51,5 +47,3 @@ (Const 2) ^ y          = (Const 1) .<<. y x ^ (Const y)          = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x) _ ^ _                  = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Label.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Label a stream with additional information. @@ -13,8 +11,6 @@ import Copilot.Core (Typed) import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------- -- | This function allows you to label a stream with a tag, which can be used -- by different backends to provide additional information either in error -- messages or in the generated code (e.g., for traceability purposes).@@ -24,5 +20,3 @@ -- is used in the code generated is a decision specific to each backend. label :: (Typed a) => String -> Stream a -> Stream a label = Label----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Local.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Let expressions. --@@ -18,8 +16,6 @@ import Copilot.Core (Typed) import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------- -- | Let expressions. -- --   Create a stream that results from applying a stream to a function on@@ -33,5 +29,3 @@ --   @ local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b local = Local----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Mux.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-} @@ -17,16 +15,12 @@ import Copilot.Language.Stream import Prelude () ---------------------------------------------------------------------------------- -- | Convenient synonym for 'ifThenElse'. mux :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a mux (Const True) t _  = t mux (Const False) _ f = f mux b t f             = Op3 (Core.Mux typeOf) b t f ---------------------------------------------------------------------------------- -- | If-then-else applied point-wise to three streams (a condition stream, a -- then-branch stream, and an else-branch stream). --@@ -35,5 +29,3 @@ -- that time, otherwise it contains the value in the third stream. ifThenElse :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a ifThenElse = mux----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Ord.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-} @@ -18,8 +16,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | Compare two streams point-wise for order. -- -- The output stream contains the value True at a point in time if the@@ -55,5 +51,3 @@ (>) :: (P.Ord a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) > (Const y) = Const (x P.> y) x > y                 = Op2 (Core.Gt typeOf) x y----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Propositional.hs view
@@ -1,8 +1,9 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe, FlexibleInstances, GADTs, MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe                  #-}  -- | Implement negation over quantified extensions of boolean streams. --@@ -16,8 +17,6 @@  import Copilot.Theorem ---------------------------------------------------------------------------------- -- | A proposition that can be negated. class Negatable a b where   -- | Negate a proposition.@@ -30,5 +29,3 @@ -- | Negation of a universally quantified proposition. instance Negatable (Prop Universal) (Prop Existential) where   not (Forall p)  = Exists $ B.not p----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Struct.hs view
@@ -11,8 +11,6 @@  import GHC.TypeLits             (KnownSymbol) ---------------------------------------------------------------------------------- -- | Create a stream that carries a field of a struct in another stream. -- -- This function implements a projection of a field of a struct over time. For@@ -23,5 +21,3 @@ (#) :: (KnownSymbol s, Typed t, Typed a, Struct a)       => Stream a -> (a -> Field s t) -> Stream t (#) s f = Op1 (GetField typeOf typeOf f) s----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Temporal.hs view
@@ -1,8 +1,5 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- - {-# LANGUAGE Safe #-}  -- | Temporal stream transformations.@@ -15,8 +12,6 @@ import Copilot.Language.Prelude import Copilot.Language.Stream import Prelude ()----------------------------------------------------------------------------------  infixr 1 ++
src/Copilot/Language/Prelude.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Reexports 'Prelude' from package "base" hiding identifiers redefined by -- Copilot.@@ -31,5 +29,3 @@   , cycle   , take   )----------------------------------------------------------------------------------
src/Copilot/Language/Reify.hs view
@@ -1,12 +1,11 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Transform a Copilot Language specification into a Copilot Core -- specification. -{-# LANGUAGE Safe #-}-{-# LANGUAGE ExistentialQuantification, Rank2Types #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE Rank2Types                #-}+{-# LANGUAGE Safe                      #-}  module Copilot.Language.Reify   ( reify@@ -28,7 +27,6 @@ import System.Mem.StableName.Map (Map) import qualified System.Mem.StableName.Map as M import Control.Monad (liftM, unless)---------------------------------------------------------------------------------  -- | Transform a Copilot Language specification into a Copilot Core -- specification.@@ -58,8 +56,6 @@    return cspec ---------------------------------------------------------------------------------- -- | Transform a Copilot observer specification into a Copilot Core -- observer specification. {-# INLINE mkObserver #-}@@ -76,8 +72,6 @@     , Core.observerExpr     = w     , Core.observerExprType = typeOf } ---------------------------------------------------------------------------------- -- | Transform a Copilot trigger specification into a Copilot Core -- trigger specification. {-# INLINE mkTrigger #-}@@ -102,8 +96,6 @@     w <- mkExpr refMkId refStreams refMap e     return $ Core.UExpr typeOf w ---------------------------------------------------------------------------------- -- | Transform a Copilot property specification into a Copilot Core -- property specification. {-# INLINE mkProperty #-}@@ -119,8 +111,6 @@     { Core.propertyName  = name     , Core.propertyExpr  = w1 } ---------------------------------------------------------------------------------- -- | Transform a Copilot stream expression into a Copilot Core expression. {-# INLINE mkExpr #-} mkExpr@@ -210,8 +200,6 @@     w <- mkExpr refMkId refStreams refMap e     return $ (name, Core.UExpr typeOf w) ---------------------------------------------------------------------------------- -- | Transform a Copilot stream expression into a Copilot Core stream -- expression. {-# INLINE mkStream #-}@@ -256,8 +244,6 @@         , Core.streamExpr       = w         , Core.streamExprType   = typeOf }     return id----------------------------------------------------------------------------------  -- | Create a fresh, unused 'Id'. mkId :: IORef Int -> IO Id
src/Copilot/Language/Spec.hs view
@@ -1,11 +1,9 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE GADTs          #-} {-# LANGUAGE KindSignatures #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RankNTypes     #-}+{-# LANGUAGE Safe           #-}  -- | Copilot specifications consistute the main declaration of Copilot modules. --@@ -43,8 +41,6 @@  import Copilot.Theorem.Prove ---------------------------------------------------------------------------------- -- | A specification is a list of declarations of triggers, observers, -- properties and theorems. --@@ -68,8 +64,6 @@ -- can be used in subsequent actions. type Spec' a = Writer [SpecItem] a ---------------------------------------------------------------------------------- -- | Return the complete list of declarations inside a 'Spec' or 'Spec''. -- -- The word run in this function is unrelated to running the underlying@@ -78,8 +72,6 @@ runSpec :: Spec' a -> [SpecItem] runSpec = execWriter ---------------------------------------------------------------------------------- -- | Filter a list of spec items to keep only the observers. observers :: [SpecItem] -> [Observer] observers =@@ -120,8 +112,6 @@       TheoremItem p -> p : ls       _              -> ls ---------------------------------------------------------------------------------- -- | An item of a Copilot specification. data SpecItem   = ObserverItem Observer@@ -129,15 +119,11 @@   | PropertyItem Property   | TheoremItem (Property, UProof) ---------------------------------------------------------------------------------- -- | An observer, representing a stream that we observe during execution at -- every sample. data Observer where   Observer :: Typed a => String -> Stream a -> Observer ---------------------------------------------------------------------------------- -- | Define a new observer as part of a specification. This allows someone to -- print the value at every iteration during interpretation. Observers do not -- have any functionality outside the interpreter.@@ -148,15 +134,11 @@          -> Spec observer name e = tell [ObserverItem $ Observer name e] ---------------------------------------------------------------------------------- -- | A trigger, representing a function we execute when a boolean stream becomes -- true at a sample. data Trigger where   Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger ---------------------------------------------------------------------------------- -- | Define a new trigger as part of a specification. A trigger declares which -- external function, or handler, will be called when a guard defined by a -- boolean stream becomes true.@@ -166,15 +148,11 @@         -> Spec trigger name e args = tell [TriggerItem $ Trigger name e args] ---------------------------------------------------------------------------------- -- | A property, representing a boolean stream that is existentially or -- universally quantified over time. data Property where   Property :: String -> Stream Bool -> Property ---------------------------------------------------------------------------------- -- | A proposition, representing the quantification of a boolean streams over -- time. data Prop a where@@ -194,8 +172,6 @@ extractProp (Forall p) = p extractProp (Exists p) = p ---------------------------------------------------------------------------------- -- | A proposition, representing a boolean stream that is existentially or -- universally quantified over time, as part of a specification. --@@ -205,8 +181,6 @@ prop name e = tell [PropertyItem $ Property name (extractProp e)]   >> return (PropRef name) ---------------------------------------------------------------------------------- -- | A theorem, or proposition together with a proof. -- -- This function returns, in the monadic context, a reference to the@@ -215,8 +189,6 @@ theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]   >> return (PropRef name) ---------------------------------------------------------------------------------- -- | Construct a function argument from a stream. -- -- 'Arg's can be used to pass arguments to handlers or trigger functions, to@@ -226,5 +198,3 @@ -- the current samples of the given streams. arg :: Typed a => Stream a -> Arg arg = Arg----------------------------------------------------------------------------------
src/Copilot/Language/Stream.hs view
@@ -1,13 +1,11 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  -- | Abstract syntax for streams and operators. -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE GADTs          #-} {-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types     #-}+{-# LANGUAGE Safe           #-}  module Copilot.Language.Stream   ( Stream (..)@@ -23,8 +21,6 @@ import Copilot.Language.Prelude import qualified Prelude as P ---------------------------------------------------------------------------------- -- | A stream in Copilot is an infinite succession of values of the same type. -- -- Streams can be built using simple primities (e.g., 'Const'), by applying@@ -52,27 +48,19 @@               => Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d   Label       :: Typed a => String -> Stream a -> Stream a ---------------------------------------------------------------------------------- -- | Wrapper to use 'Stream's as arguments to triggers. data Arg where   Arg :: Typed a => Stream a -> Arg ---------------------------------------------------------------------------------- -- | Dummy instance in order to make 'Stream' an instance of 'Num'. instance Show (Stream a) where   show _      = "Stream" ---------------------------------------------------------------------------------- -- | Dummy instance in order to make 'Stream' an instance of 'Num'. instance P.Eq (Stream a) where   (==)        = badUsage "'Prelude.(==)' isn't implemented for streams!"   (/=)        = badUsage "'Prelude.(/=)' isn't implemented for streams!" ---------------------------------------------------------------------------------- -- | Streams carrying numbers are instances of 'Num', and you can apply to them -- the 'Num' functions, point-wise. instance (Typed a, P.Eq a, Num a) => Num (Stream a) where@@ -100,8 +88,6 @@    fromInteger             = Const . fromInteger ---------------------------------------------------------------------------------- -- | Streams carrying fractional numbers are instances of 'Fractional', and you can -- apply to them the 'Fractional' functions, point-wise. @@ -115,8 +101,6 @@    fromRational            = Const . fromRational ---------------------------------------------------------------------------------- -- | Streams carrying floating point numbers are instances of 'Floating', and -- you can apply to them the 'Floating' functions, point-wise. @@ -142,8 +126,6 @@   atanh        = Op1 (Core.Atanh typeOf)   acosh        = Op1 (Core.Acosh typeOf) ---------------------------------------------------------------------------------- -- | Point-wise application of @ceiling@ to a stream. -- -- Unlike the Haskell variant of this function, this variant takes and returns@@ -175,9 +157,6 @@ -- qualified to use this function. floor :: (Typed a, RealFrac a) => Stream a -> Stream a floor = Op1 (Core.Floor typeOf)-----------------------------------------------------------------------------------  -- | Point-wise application of @atan2@ to the values of two streams. --
src/System/Mem/StableName/Dynamic.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.---------------------------------------------------------------------------------  {-# LANGUAGE Trustworthy #-}
src/System/Mem/StableName/Map.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Most of this code is taken from 'http://github.com/ekmett/stable-maps'.---------------------------------------------------------------------------------  {-# LANGUAGE Safe #-}
tests/Test/Copilot/Language/Reify.hs view
@@ -116,9 +116,7 @@   , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word64))   ] - -- ** Random Stream generators-  -- | An arbitrary constant expression of any type, paired with its expected -- meaning.