copilot-language 3.2 → 3.2.1

raw patch · 25 files changed

+584/−79 lines, 25 filesdep ~copilot-coredep ~copilot-theoremPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: copilot-core, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• copilot-language.cabal +3/−3
• src/Copilot.hs +0/−2
• src/Copilot/Language.hs +6/−0
• src/Copilot/Language/Analyze.hs +42/−5
• src/Copilot/Language/Error.hs +8/−2
• src/Copilot/Language/Interpret.hs +16/−2
• src/Copilot/Language/Operators/Array.hs +7/−0
• src/Copilot/Language/Operators/BitWise.hs +13/−6
• src/Copilot/Language/Operators/Boolean.hs +9/−2
• src/Copilot/Language/Operators/Cast.hs +139/−14
• src/Copilot/Language/Operators/Constant.hs +46/−12
• src/Copilot/Language/Operators/Eq.hs +9/−2
• src/Copilot/Language/Operators/Extern.hs +82/−17
• src/Copilot/Language/Operators/Integral.hs +7/−1
• src/Copilot/Language/Operators/Label.hs +8/−1
• src/Copilot/Language/Operators/Local.hs +16/−0
• src/Copilot/Language/Operators/Mux.hs +9/−2
• src/Copilot/Language/Operators/Ord.hs +21/−2
• src/Copilot/Language/Operators/Propositional.hs +7/−0
• src/Copilot/Language/Operators/Struct.hs +8/−0
• src/Copilot/Language/Operators/Temporal.hs +15/−1
• src/Copilot/Language/Reify.hs +13/−1
• src/Copilot/Language/Spec.hs +80/−4
• src/Copilot/Language/Stream.hs +16/−0

@@ -1,3 +1,7 @@+2021-03-07+        * Version bump (3.2.1). (#20)+        * Completed the documentation. (#14)+ 2020-05-07         * Version bump (3.2).         * Fixed the reverse order of triggers (#11).

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             3.2+version:             3.2.1 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:@@ -40,8 +40,8 @@                , mtl             >= 2.0 && < 3                , ghc-prim        >= 0.3 && < 0.7 -               , copilot-core    >= 3.2 && < 3.3-               , copilot-theorem >= 3.2 && < 3.3+               , copilot-core    >= 3.2.1 && < 3.3+               , copilot-theorem >= 3.2.1 && < 3.3    exposed-modules: Copilot                  , Copilot.Language

@@ -2,8 +2,6 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Main import module for the front-end lanugage.- {-# LANGUAGE Safe #-}  module Copilot

@@ -3,6 +3,10 @@ --------------------------------------------------------------------------------  -- | Main Copilot language export file.+--+-- This is mainly a meta-module that re-exports most definitions in this+-- library. It also provides a default pretty printer that prints a+-- specification to stdout.  {-# LANGUAGE Safe #-} @@ -69,6 +73,8 @@  -------------------------------------------------------------------------------- +-- | 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 

@@ -31,6 +31,8 @@  -------------------------------------------------------------------------------- +-- | Exceptions or kinds of errors in Copilot specifications that the analysis+-- implemented is able to detect. data AnalyzeException   = DropAppliedToNonAppend   | DropIndexOverflow@@ -45,6 +47,7 @@   | BadFunctionArgType String   deriving Typeable +-- | Show instance that prints a detailed message for each kind of exception. instance Show AnalyzeException where   show DropAppliedToNonAppend = badUsage $  "Drop applied to non-append operation!"   show DropIndexOverflow      = badUsage $  "Drop index overflow!"@@ -66,17 +69,24 @@   show (BadFunctionArgType name) = badUsage $     "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types." +-- | 'Exception' instance so we can throw and catch 'AnalyzeExcetion's. instance Exception AnalyzeException +-- | Max level of recursion supported. Any level above this constant+-- will result in a 'TooMuchRecursion' exception. 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'. analyze :: Spec' a -> IO () analyze spec = do   refStreams <- newIORef M.empty@@ -88,6 +98,9 @@  -------------------------------------------------------------------------------- +-- | Analyze a Copilot trigger and report any errors detected.+--+-- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeTrigger :: IORef Env -> Trigger -> IO () analyzeTrigger refStreams (Trigger _ e0 args) =   analyzeExpr refStreams e0 >> mapM_ analyzeTriggerArg args@@ -98,11 +111,17 @@  -------------------------------------------------------------------------------- +-- | 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 @@ -115,6 +134,9 @@  -------------------------------------------------------------------------------- +-- | Analyze a Copilot stream and report any errors detected.+--+-- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeExpr :: IORef Env -> Stream a -> IO () analyzeExpr refStreams s = do   b <- mapCheck refStreams@@ -145,6 +167,10 @@  -------------------------------------------------------------------------------- +-- | Detect whether the given stream name has already been visited.+--+-- This function throws a 'ReferentialCycle' exception if the second argument+-- represents a name that has already been visited. assertNotVisited :: Stream a -> DynStableName -> Env -> IO () assertNotVisited (Append _ _ _) _    _     = return () assertNotVisited _              dstn nodes =@@ -154,6 +180,7 @@  -------------------------------------------------------------------------------- +-- | Check that the level of recursion is not above the max recursion allowed. mapCheck :: IORef Env -> IO Bool mapCheck refStreams = do   ref <- readIORef refStreams@@ -161,6 +188,7 @@  -------------------------------------------------------------------------------- +-- | Analyze a Copilot stream append and report any errors detected. analyzeAppend ::      IORef Env -> DynStableName -> Stream a -> b   -> (IORef Env -> Stream a -> IO b) -> IO b@@ -174,6 +202,11 @@  -------------------------------------------------------------------------------- +-- | 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+-- append, or if the length of the drop is larger than that of the subsequent+-- append. analyzeDrop :: Int -> Stream a -> IO () analyzeDrop k (Append xs _ _)   | k >= length xs                         = throw DropIndexOverflow@@ -188,9 +221,9 @@ -- 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 external to--- have two different types.+-- | 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+-- external to have two different types. data ExternEnv = ExternEnv   { externVarEnv  :: [(String, C.SimpleType)]   , externArrEnv  :: [(String, C.SimpleType)]@@ -200,8 +233,8 @@  -------------------------------------------------------------------------------- --- Make sure external variables, functions, arrays, and structs are correctly typed.-+-- | Make sure external variables, functions, arrays, and structs are correctly+-- typed. analyzeExts :: ExternEnv -> IO () analyzeExts ExternEnv { externVarEnv  = vars                       , externArrEnv  = arrs@@ -271,6 +304,7 @@  -------------------------------------------------------------------------------- +-- | Obtain all the externs in a specification. specExts :: IORef Env -> Spec' a -> IO ExternEnv specExts refStreams spec = do   env <- foldM triggerExts@@ -288,6 +322,7 @@     foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')           env' args +-- | Obtain all the externs in a stream. collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv collectExts refStreams stream_ env_ = do   b <- mapCheck refStreams@@ -321,6 +356,8 @@  -------------------------------------------------------------------------------- +-- | 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) 

@@ -4,15 +4,21 @@  {-# LANGUAGE Safe #-} +-- | Custom functions to report error messages to users. module Copilot.Language.Error   ( impossible   , badUsage ) where -impossible :: String -> String -> a+-- | Report an error due to a bug in Copilot.+impossible :: String -- ^ Name of the function in which the error was detected.+           -> String -- ^ Name of the package in which the function is located.+           -> a impossible function package =   error $ "Impossible error in function " ++ function ++ ", in package " ++     package ++ ".  Please email Lee Pike at <lee pike @ gmail . com> " ++     "(remove spaces) or file a bug report on github.com." -badUsage :: String -> a+-- | Report an error due to an error detected by Copilot (e.g., user error).+badUsage :: String -- ^ Description of the error.+         -> a badUsage msg = error $ "Copilot error: " ++ msg

@@ -1,6 +1,12 @@ {- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc. -} --- | The interpreter.+-- | This module implements two interpreters, which may be used to simulated or+-- executed Copilot specifications on a computer to understand their behavior+-- to debug possible errors.+--+-- The interpreters included vary in how the present the results to the user.+-- 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 #-}@@ -45,6 +51,8 @@  -------------------------------------------------------------------------------- +-- | 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 () csv i spec = do   putStrLn "Note: CSV format does not output observers."@@ -52,10 +60,16 @@  -------------------------------------------------------------------------------- --- | Much slower, but pretty-printed interpreter output.+-- | Simulate a number of steps of a given specification, printing the results+-- in a table in readable format.+--+-- Compared to 'csv', this function is slower but the output may be more+-- readable. interpret :: Integer -> Spec -> IO () interpret = interpret' I.Table +-- | Simulate a number of steps of a given specification, printing the results+-- in the format specified. interpret' :: I.Format -> Integer -> Spec -> IO () interpret' format i spec = do   coreSpec <- reify spec

@@ -2,6 +2,7 @@  {-# LANGUAGE TypeFamilies #-} +-- | Combinators to deal with streams carrying arrays. module Copilot.Language.Operators.Array   ( (.!!)   ) where@@ -19,6 +20,12 @@  -------------------------------------------------------------------------------- +-- | 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+-- position, over time. For example, if @s@ is a stream of type @Stream (Array+-- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd+-- element (starting from zero) of the arrays in @s@ at any point in time. (.!!) :: ( KnownNat n          , t' ~ InnerType t          , Flatten t t'

@@ -2,12 +2,11 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Bitwise operators.- {-# LANGUAGE Safe #-}  {-# OPTIONS_GHC -fno-warn-orphans #-} +-- | Bitwise operators applied on streams, pointwise. module Copilot.Language.Operators.BitWise   ( Bits ((.&.), complement, (.|.))   , (.^.)@@ -21,6 +20,9 @@ import qualified Prelude as P import Data.Bits +-- | Instance of the 'Bits' class for 'Stream's.+--+-- Only the methods '.&.', 'complement', '.|.' and 'xor' are defined. instance (Typed a, Bits a) => Bits (Stream a) where   (.&.)        = Op2 (Core.BwAnd typeOf)   complement   = Op1 (Core.BwNot typeOf)@@ -36,11 +38,16 @@   bit          = P.error "tbd: bit"   popCount     = P.error "tbd: popCount" --- Avoid redefinition of the Operators.Boolean xor+-- | See 'xor'. (.^.) :: Bits a => a -> a -> a-(.^.) = xor+(.^.) = xor -- Avoid redefinition of the Operators.Boolean xor -(.<<.), (.>>.) :: (Bits a, Typed a, Typed b, P.Integral b)-               => Stream a -> Stream b -> Stream a+-- | Shifting values of a stream to the left.+(.<<.) :: (Bits a, Typed a, Typed b, P.Integral b)+       => Stream a -> Stream b -> Stream a (.<<.) = Op2 (Core.BwShiftL typeOf typeOf)++-- | Shifting values of a stream to the right.+(.>>.) :: (Bits a, Typed a, Typed b, P.Integral b)+       => Stream a -> Stream b -> Stream a (.>>.) = Op2 (Core.BwShiftR typeOf typeOf)

@@ -2,10 +2,9 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Boolean operators.- {-# LANGUAGE Safe #-} +-- | Boolean operators applied point-wise to streams. module Copilot.Language.Operators.Boolean   ( (&&)   , (||)@@ -24,14 +23,17 @@  -------------------------------------------------------------------------------- +-- | A stream that contains the constant value 'True'. true :: Stream Bool true = constant True +-- | A stream that contains the constant value 'False'. false :: Stream Bool false = constant False  infixr 4 && +-- | Apply the and ('&&') operator to two boolean streams, point-wise. (&&) :: Stream Bool -> Stream Bool -> Stream Bool (Const False) && _ = false _ && (Const False) = false@@ -41,6 +43,7 @@  infixr 4 || +-- | Apply the or ('||') operator to two boolean streams, point-wise. (||) :: Stream Bool -> Stream Bool -> Stream Bool (Const True) || _  = true _ || (Const True)  = true@@ -48,13 +51,17 @@ x || (Const False) = x x || y             = Op2 Core.Or x y +-- | Negate all the values in a boolean stream. not :: Stream Bool -> Stream Bool not (Const c) = (Const $ P.not c) not x         = Op1 Core.Not x +-- | Apply the exclusive-or ('xor') operator to two boolean streams,+-- point-wise. xor :: Stream Bool -> Stream Bool -> Stream Bool xor x y = ( not x && y ) || ( x && not y ) +-- | Apply the implication ('==>') operator to two boolean streams, point-wise. (==>) :: Stream Bool -> Stream Bool -> Stream Bool x ==> y = not x || y 

@@ -2,11 +2,10 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Type-safe casting operators.- {-# LANGUAGE Safe #-} {-# LANGUAGE MultiParamTypeClasses #-} +-- | Type-safe casting operators. module Copilot.Language.Operators.Cast   ( cast, unsafeCast, Cast, UnsafeCast ) where @@ -19,213 +18,339 @@  -------------------------------------------------------------------------------- +-- | Class to capture casting between types for which it can be performed+-- safely. class Cast a b where+  -- | Perform a safe cast from @Stream a@ to @Stream b@.   cast :: (Typed a, Typed b) => Stream a -> Stream b +-- | Class to capture casting between types for which casting may be unsafe+-- and/or result in a loss of precision or information. class UnsafeCast a b where+  -- | 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++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Word8 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Word16 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Word32 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Word64 where   cast = castBool +-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Int8 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Int16 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. instance Cast Bool Int32 where   cast = castBool++-- | Cast a boolean stream to a stream of numbers, producing 1 if the+-- value at a point in time is 'True', and 0 otherwise. 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++-- | Cast number to bigger type. instance Cast Word8 Word16 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word8 Word32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word8 Word64 where   cast = castIntegral +-- | Cast number to bigger type. instance Cast Word8 Int16 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word8 Int32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word8 Int64 where   cast = castIntegral  -------------------------------------------------------------------------------- +-- | Identity casting. instance Cast Word16 Word16 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word16 Word32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word16 Word64 where   cast = castIntegral +-- | Cast number to bigger type. instance Cast Word16 Int32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word16 Int64 where   cast = castIntegral  -------------------------------------------------------------------------------- +-- | Identity casting. instance Cast Word32 Word32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Word32 Word64 where   cast = castIntegral +-- | Cast number to bigger type. 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++-- | Cast number to bigger type. instance Cast Int8 Int16 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Int8 Int32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Int8 Int64 where   cast = castIntegral  -------------------------------------------------------------------------------- +-- | Identity casting. instance Cast Int16 Int16 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Int16 Int32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Int16 Int64 where   cast = castIntegral  -------------------------------------------------------------------------------- +-- | Identity casting. instance Cast Int32 Int32 where   cast = castIntegral++-- | Cast number to bigger type. instance Cast Int32 Int64 where   cast = castIntegral  -------------------------------------------------------------------------------- +-- | Identity casting. instance Cast Int64 Int64 where   cast = castIntegral ------------------------------------------------------------------------------------ | Unsafe downcasting to smaller sizes----------------------------------------------------------------------------------+-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word64 Word32 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word64 Word16 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word64 Word8 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word32 Word16 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word32 Word8 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Word16 Word8 where   unsafeCast = castIntegral +-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int64 Int32 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int64 Int16 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int64 Int8 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int32 Int16 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int32 Int8 where   unsafeCast = castIntegral++-- | Unsafe downcasting to smaller sizes. instance UnsafeCast Int16 Int8 where   unsafeCast = castIntegral ------------------------------------------------------------------------------------ | Unsafe unsigned and signed promotion to floating point values----------------------------------------------------------------------------------+-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int64 Float where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int32 Float where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int16 Float where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int8 Float where   unsafeCast = castIntegral +-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int64 Double where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int32 Double where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int16 Double where   unsafeCast = castIntegral++-- | Unsafe signed integer promotion to floating point values. instance UnsafeCast Int8 Double where   unsafeCast = castIntegral +-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word64 Float where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word32 Float where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word16 Float where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word8 Float where   unsafeCast = castIntegral +-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word64 Double where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word32 Double where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word16 Double where   unsafeCast = castIntegral++-- | Unsafe unsigned integer promotion to floating point values. instance UnsafeCast Word8 Double where   unsafeCast = castIntegral ------------------------------------------------------------------------------------ | Signed to unsigned and vice versa----------------------------------------------------------------------------------+-- | Cast from unsigned numbers to signed numbers. instance UnsafeCast Word64 Int64 where   unsafeCast = castIntegral++-- | Cast from unsigned numbers to signed numbers. instance UnsafeCast Word32 Int32 where   unsafeCast = castIntegral++-- | Cast from unsigned numbers to signed numbers. instance UnsafeCast Word16 Int16 where   unsafeCast = castIntegral++-- | Cast from unsigned numbers to signed numbers. instance UnsafeCast Word8 Int8 where   unsafeCast = castIntegral +-- | Signed to unsigned casting. instance UnsafeCast Int64 Word64 where   unsafeCast = castIntegral++-- | Signed to unsigned casting. instance UnsafeCast Int32 Word32 where   unsafeCast = castIntegral++-- | Signed to unsigned casting. instance UnsafeCast Int16 Word16 where   unsafeCast = castIntegral++-- | Signed to unsigned casting. instance UnsafeCast Int8 Word8 where   unsafeCast = castIntegral

@@ -2,10 +2,10 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Constants.- {-# LANGUAGE Safe #-} ++-- | Primitives to build constant streams. module Copilot.Language.Operators.Constant   ( constant   , constB@@ -29,30 +29,64 @@  -------------------------------------------------------------------------------- +-- | Create a constant stream that is equal to the given argument, at any+-- point in time. constant :: Typed a => a -> Stream a constant = Const  -------------------------------------------------------------------------------- -constB   :: Bool -> Stream Bool-constB   = constant-constW8  :: Word8 -> Stream Word8-constW8  = constant+-- | Create a constant stream carrying values of type 'Bool' that is equal to+-- the given argument, at any point in time.+constB :: Bool -> Stream Bool+constB = constant++-- | Create a constant stream carrying values of type 'Word8' that is equal to+-- the given argument, at any point in time.+constW8 :: Word8 -> Stream Word8+constW8 = constant++-- | Create a constant stream carrying values of type 'Word16' that is equal to+-- the given argument, at any point in time. constW16 :: Word16 -> Stream Word16 constW16 = constant++-- | Create a constant stream carrying values of type 'Word32' that is equal to+-- the given argument, at any point in time. constW32 :: Word32 -> Stream Word32 constW32 = constant++-- | Create a constant stream carrying values of type 'Word64' that is equal to+-- the given argument, at any point in time. constW64 :: Word64 -> Stream Word64 constW64 = constant-constI8  :: Int8 -> Stream Int8-constI8  = constant++-- | Create a constant stream carrying values of type 'Int8' that is equal to+-- the given argument, at any point in time.+constI8 :: Int8 -> Stream Int8+constI8 = constant++-- | Create a constant stream carrying values of type 'Int16' that is equal to+-- the given argument, at any point in time. constI16 :: Int16 -> Stream Int16 constI16 = constant++-- | Create a constant stream carrying values of type 'Int32' that is equal to+-- the given argument, at any point in time. constI32 :: Int32 -> Stream Int32 constI32 = constant++-- | Create a constant stream carrying values of type 'Int64' that is equal to+-- the given argument, at any point in time. constI64 :: Int64 -> Stream Int64 constI64 = constant-constF   :: Float -> Stream Float-constF   = constant-constD   :: Double -> Stream Double-constD   = constant++-- | Create a constant stream carrying values of type 'Float' that is equal to+-- the given argument, at any point in time.+constF :: Float -> Stream Float+constF = constant++-- | Create a constant stream carrying values of type 'Double' that is equal to+-- the given argument, at any point in time.+constD :: Double -> Stream Double+constD = constant

@@ -2,10 +2,9 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Equality operator.- {-# LANGUAGE Safe #-} +-- | Equality applied point-wise on streams. module Copilot.Language.Operators.Eq   ( (==)   , (/=)@@ -19,10 +18,18 @@  -------------------------------------------------------------------------------- +-- | Compare two streams point-wise for equality.+--+-- The output stream contains the value True at a point in time if both+-- argument streams contain the same value at that point in time. (==) :: (P.Eq a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) == (Const y) = Const (x P.== y) x == y = Op2 (Core.Eq typeOf) x y +-- | Compare two streams point-wise for inequality.+--+-- The output stream contains the value True at a point in time if both+-- argument streams contain different values at that point in time. (/=) :: (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

@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | External variables, arrays, and functions.+-- | Primitives to build streams connected to external variables.  {-# LANGUAGE Safe #-} @@ -18,7 +18,7 @@   , externI32   , externI64   , externD-  , funArg -- * Deprecated.+  , funArg   ) where  import Copilot.Core (Typed)@@ -30,7 +30,18 @@  -------------------------------------------------------------------------------- -extern :: Typed a => String -> Maybe [a] -> Stream a+-- | Create a stream populated by an external global variable.+--+-- The Copilot compiler does not check that the type is correct. If the list+-- given as second argument does not constrain the type of the values carried+-- by the stream, this primitive stream building function will match any stream+-- of any type, which is potentially dangerous if the global variable mentioned+-- has a different type. We rely on the compiler used with the generated code+-- to detect type errors of this kind.+extern :: Typed a+       => String    -- ^ Name of the global variable to make accessible.+       -> Maybe [a] -- ^ Values to be used exclusively for testing/simulation.+       -> Stream a extern = Extern  -- | Deprecated.@@ -39,23 +50,77 @@  -------------------------------------------------------------------------------- -externB   :: String -> Maybe [Bool] -> Stream Bool-externB   = extern-externW8  :: String -> Maybe [Word8] -> Stream Word8-externW8  = extern-externW16 :: String -> Maybe [Word16] -> Stream Word16+-- | Create a stream carrying values of type Bool, populated by an external+-- global variable.+externB :: String       -- ^ Name of the global variable to make accessible.+        -> Maybe [Bool] -- ^ Values to be used exclusively for+                        -- testing/simulation.+        -> Stream Bool+externB = extern++-- | Create a stream carrying values of type Word8, populated by an external+-- global variable.+externW8 :: String         -- ^ Name of the global variable to make accessible.+         -> Maybe [Word8]  -- ^ Values to be used exclusively for+                           --   testing/simulation.+         -> Stream Word8+externW8 = extern++-- | Create a stream carrying values of type Word16, populated by an external+-- global variable.+externW16 :: String          -- ^ Name of the global variable to make accessible.+          -> Maybe [Word16]  -- ^ Values to be used exclusively for+                             -- testing/simulation.+          -> Stream Word16 externW16 = extern-externW32 :: String -> Maybe [Word32] -> Stream Word32++-- | Create a stream carrying values of type Word32, populated by an external+-- global variable.+externW32 :: String          -- ^ Name of the global variable to make accessible.+          -> Maybe [Word32]  -- ^ Values to be used exclusively for+                             -- testing/simulation.+          -> Stream Word32 externW32 = extern-externW64 :: String -> Maybe [Word64] -> Stream Word64++-- | Create a stream carrying values of type Word64, populated by an external+-- global variable.+externW64 :: String          -- ^ Name of the global variable to make accessible.+          -> Maybe [Word64]  -- ^ Values to be used exclusively for+                             -- testing/simulation.+          -> Stream Word64 externW64 = extern-externI8  :: String -> Maybe [Int8] -> Stream Int8-externI8  = extern-externI16 :: String -> Maybe [Int16] -> Stream Int16++-- | Create a stream carrying values of type Int8, populated by an external+-- global variable.+externI8 :: String    -- ^ Name of the global variable to make accessible.+         -> Maybe [Int8] -- ^ Values to be used exclusively for testing/simulation.+         -> Stream Int8+externI8 = extern++-- | Create a stream carrying values of type Int16, populated by an external+-- global variable.+externI16 :: String    -- ^ Name of the global variable to make accessible.+          -> Maybe [Int16] -- ^ Values to be used exclusively for testing/simulation.+          -> Stream Int16 externI16 = extern-externI32 :: String -> Maybe [Int32] -> Stream Int32++-- | Create a stream carrying values of type Int32, populated by an external+-- global variable.+externI32 :: String    -- ^ Name of the global variable to make accessible.+          -> Maybe [Int32] -- ^ Values to be used exclusively for testing/simulation.+          -> Stream Int32 externI32 = extern-externI64 :: String -> Maybe [Int64] -> Stream Int64++-- | Create a stream carrying values of type Int64, populated by an external+-- global variable.+externI64 :: String    -- ^ Name of the global variable to make accessible.+          -> Maybe [Int64] -- ^ Values to be used exclusively for testing/simulation.+          -> Stream Int64 externI64 = extern-externD   :: String -> Maybe [Double] -> Stream Double-externD   = extern++-- | Create a stream carrying values of type Double, populated by an external+-- global variable.+externD :: String    -- ^ Name of the global variable to make accessible.+        -> Maybe [Double] -- ^ Values to be used exclusively for testing/simulation.+        -> Stream Double+externD = extern

@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Integral class operators.+-- | Integral class operators applied point-wise on streams.  {-# LANGUAGE Safe #-} @@ -23,18 +23,24 @@  -------------------------------------------------------------------------------- +-- | 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 _ `div` (Const 0) = Core.badUsage "in div: division by zero." x `div` (Const 1) = x x `div` y = Op2 (Core.Div typeOf) x y +-- | Apply the 'Prelude.mod' operation to two streams, point-wise. mod :: (Typed a, P.Integral a) => Stream a -> Stream a -> Stream a _         `mod` (Const 0) = Core.badUsage "in mod: division by zero." (Const 0) `mod` _         = (Const 0) (Const x) `mod` (Const y) = Const (x `P.mod` y) x `mod` y = Op2 (Core.Mod typeOf) x y +-- | Apply a limited form of exponentiation (@^@) to two streams, point-wise.+--+-- Either the first stream must be the constant 2, or the second must be a+-- constant stream. (^) :: (Typed a, Typed b, P.Num a, B.Bits a, P.Integral b)     => Stream a -> Stream b -> Stream a (Const 0) ^ (Const 0)  = Const 1

@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Let expressions.+-- | Label a stream with additional information.  {-# LANGUAGE Safe #-} @@ -15,6 +15,13 @@  -------------------------------------------------------------------------------- +-- | 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).+--+-- Semantically, a labelled stream is just the stream inside it. The use of+-- label should not affect the observable behavior of the monitor, and how it+-- is used in the code generated is a decision specific to each backend. label :: (Typed a) => String -> Stream a -> Stream a label = Label 

@@ -3,6 +3,11 @@ --------------------------------------------------------------------------------  -- | Let expressions.+--+-- Although Copilot is a DSL embedded in Haskell and Haskell does support let+-- expressions, we want Copilot to be able to implement sharing, to detect when+-- the same stream is being used in multiple places in a specification and+-- avoid recomputing it unnecessarily.  {-# LANGUAGE Safe #-} @@ -15,6 +20,17 @@  -------------------------------------------------------------------------------- +-- | Let expressions.+--+--   Create a stream that results from applying a stream to a function on+--   streams. Standard usage would be similar to Haskell's let. See the+--   following example, where @stream1@, @stream2@ and @s@ are all streams+--   carrying values of some numeric type:+--+--   @+--   expression = local (stream1 + stream2) $ \\s ->+--                (s >= 0 && s <= 10)+--   @ local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b local = Local 

@@ -2,10 +2,10 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | if-then-else.- {-# LANGUAGE Safe #-} +-- | Pick values from one of two streams, depending whether a condition is true+-- or false. module Copilot.Language.Operators.Mux   ( mux   , ifThenElse@@ -19,6 +19,7 @@  -------------------------------------------------------------------------------- +-- | 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@@ -26,6 +27,12 @@  -------------------------------------------------------------------------------- +-- | If-then-else applied point-wise to three streams (a condition stream, a+-- then-branch stream, and an else-branch stream).+--+-- Produce a stream that, at any point in time, if the value of the first+-- stream at that point is true, contains the value in the second stream at+-- that time, otherwise it contains the value in the third stream. ifThenElse :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a ifThenElse = mux 

@@ -2,10 +2,9 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Comparison operators.- {-# LANGUAGE Safe #-} +-- | Comparison operators applied point-wise on streams. module Copilot.Language.Operators.Ord   ( (<=)   , (>=)@@ -21,18 +20,38 @@  -------------------------------------------------------------------------------- +-- | Compare two streams point-wise for order.+--+-- The output stream contains the value True at a point in time if the+-- element in the first stream is smaller or equal than the element in+-- the second stream at that point in time, and False otherwise. (<=) :: (P.Ord a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) <= (Const y) = Const (x P.<= y) x <= y                 = Op2 (Core.Le typeOf) x y +-- | Compare two streams point-wise for order.+--+-- The output stream contains the value True at a point in time if the+-- element in the first stream is greater or equal than the element in+-- the second stream at that point in time, and False otherwise. (>=) :: (P.Ord a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) >= (Const y) = Const (x P.>= y) x >= y                 = Op2 (Core.Ge typeOf) x y +-- | Compare two streams point-wise for order.+--+-- The output stream contains the value True at a point in time if the+-- element in the first stream is smaller than the element in the second stream+-- at that point in time, and False otherwise. (<) :: (P.Ord a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) < (Const y) = Const (x P.< y) x < y                 = Op2 (Core.Lt typeOf) x y +-- | Compare two streams point-wise for order.+--+-- The output stream contains the value True at a point in time if the element+-- in the first stream is greater than the element in the second stream at that+-- point in time, and False otherwise. (>) :: (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

@@ -4,6 +4,9 @@  {-# LANGUAGE Safe, FlexibleInstances, GADTs, MultiParamTypeClasses #-} +-- | Implement negation over quantified extensions of boolean streams.+--+-- For details, see 'Prop'. module Copilot.Language.Operators.Propositional (not) where  import Prelude (($))@@ -15,12 +18,16 @@  -------------------------------------------------------------------------------- +-- | A proposition that can be negated. class Negatable a b where+  -- | Negate a proposition.   not :: a -> b +-- | Negation of an existentially quantified proposition. instance Negatable (Prop Existential) (Prop Universal) where   not (Exists p)  = Forall $ B.not p +-- | Negation of a universally quantified proposition. instance Negatable (Prop Universal) (Prop Existential) where   not (Forall p)  = Exists $ B.not p 

@@ -1,5 +1,6 @@ {-# LANGUAGE Safe #-} +-- | Combinators to deal with streams carrying structs. module Copilot.Language.Operators.Struct   ( (#)   ) where@@ -12,6 +13,13 @@  -------------------------------------------------------------------------------- +-- | 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+-- example, if a struct of type @T@ has two fields, @t1@ of type @Int@ and @t2@+-- of type @Word8@, and @s@ is a stream of type @Stream T@, then @s # t2@ has+-- type @Stream Word8@ and contains the values of the @t2@ field of the structs+-- in @s@ at any point in time. (#) :: (KnownSymbol s, Typed t, Typed a, Struct a)       => Stream a -> (a -> Field s t) -> Stream t (#) s f = Op1 (GetField typeOf typeOf f) s

@@ -2,10 +2,10 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Stream construction.  {-# LANGUAGE Safe #-} +-- | Temporal stream transformations. module Copilot.Language.Operators.Temporal   ( (++)   , drop@@ -20,9 +20,23 @@  infixr 1 ++ +-- | Prepend a fixed number of samples to a stream.+--+-- The elements to be appended at the beginning of the stream must be limited,+-- that is, the list must have finite length.+--+-- Prepending elements to a stream may increase the memory requirements of the+-- generated programs (which now must hold the same number of elements in+-- memory for future processing). (++) :: Typed a => [a] -> Stream a -> Stream a (++) = (`Append` Nothing) +-- | Drop a number of samples from a stream.+--+-- The elements must be realizable at the present time to be able to drop+-- elements. For most kinds of streams, you cannot drop elements without+-- prepending an equal or greater number of elements to them first, as it+-- could result in undefined samples. drop :: Typed a => Int -> Stream a -> Stream a drop 0 s             = s drop _ ( Const j )   = Const j

@@ -2,7 +2,7 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Transforms a Copilot Language specification into a Copilot Core+-- | Transform a Copilot Language specification into a Copilot Core -- specification.  {-# LANGUAGE Safe #-}@@ -30,6 +30,8 @@ import Control.Monad (liftM, unless) -------------------------------------------------------------------------------- +-- | Transform a Copilot Language specification into a Copilot Core+-- specification. reify :: Spec' a -> IO Core.Spec reify spec = do   analyze spec@@ -61,6 +63,8 @@  -------------------------------------------------------------------------------- +-- | Transform a Copilot observer specification into a Copilot Core+-- observer specification. {-# INLINE mkObserver #-} mkObserver   :: IORef Int@@ -77,6 +81,8 @@  -------------------------------------------------------------------------------- +-- | Transform a Copilot trigger specification into a Copilot Core+-- trigger specification. {-# INLINE mkTrigger #-} mkTrigger   :: IORef Int@@ -101,6 +107,8 @@  -------------------------------------------------------------------------------- +-- | Transform a Copilot property specification into a Copilot Core+-- property specification. {-# INLINE mkProperty #-} mkProperty   :: IORef Int@@ -140,6 +148,7 @@ --------------------------------------------------------------------------------  +-- | Transform a Copilot stream expression into a Copilot Core expression. {-# INLINE mkExpr #-} mkExpr   :: Typed a@@ -257,6 +266,8 @@  -------------------------------------------------------------------------------- +-- | Transform a Copilot stream expression into a Copilot Core stream+-- expression. {-# INLINE mkStream #-} mkStream   :: Typed a@@ -302,5 +313,6 @@  -------------------------------------------------------------------------------- +-- | Create a fresh, unused 'Id'. mkId :: IORef Int -> IO Id mkId refMkId = atomicModifyIORef refMkId $ \ n -> (succ n, n)

@@ -2,13 +2,19 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Copilot specifications.- {-# LANGUAGE Safe #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} +-- | Copilot specifications consistute the main declaration of Copilot modules.+--+-- A specification normally contains the association between streams to monitor+-- and their handling functions, or streams to observe, or a theorem that must+-- be proved.+--+-- In order to be executed, 'Spec's must be turned into Copilot Core (see+-- 'Reify') and either simulated or converted into C99 code to be executed. module Copilot.Language.Spec   ( Spec, Spec'   , runSpec@@ -41,16 +47,42 @@  -------------------------------------------------------------------------------- +-- | A specification is a list of declarations of triggers, observers,+-- properties and theorems.+--+-- Specifications are normally declared in monadic style, for example:+--+-- @+-- monitor1 :: Stream Bool+-- monitor1 = [False] ++ not monitor1+--+-- counter :: Stream Int32+-- counter = [0] ++ not counter+--+-- spec :: Spec+-- spec = do+--   trigger "handler_1" monitor1 []+--   trigger "handler_2" (counter > 10) [arg counter]+-- @ type Spec = Writer [SpecItem] ()++-- | An action in a specification (e.g., a declaration) that returns a value that+-- 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+-- specifications or monitors, and is merely related to the monad defined by a+-- 'Spec' runSpec :: Spec' a -> [SpecItem] runSpec = execWriter  -------------------------------------------------------------------------------- +-- | Filter a list of spec items to keep only the observers. observers :: [SpecItem] -> [Observer] observers =   foldr lets' []@@ -60,6 +92,7 @@       ObserverItem l -> l : ls       _              -> ls +-- | Filter a list of spec items to keep only the triggers. triggers :: [SpecItem] -> [Trigger] triggers =   foldr triggers' []@@ -69,6 +102,7 @@       TriggerItem t -> t : ls       _             -> ls +-- | Filter a list of spec items to keep only the properties. properties :: [SpecItem] -> [Property] properties =   foldr properties' []@@ -78,6 +112,7 @@       PropertyItem p -> p : ls       _              -> ls +-- | Filter a list of spec items to keep only the theorems. theorems :: [SpecItem] -> [(Property, UProof)] theorems =   foldr theorems' []@@ -89,6 +124,7 @@  -------------------------------------------------------------------------------- +-- | An item of a Copilot specification. data SpecItem   = ObserverItem Observer   | TriggerItem  Trigger@@ -97,59 +133,99 @@  -------------------------------------------------------------------------------- +-- | An observer, representing a stream that we observe during execution at+-- every sample. data Observer where   Observer :: Typed a => String -> Stream a -> Observer  -------------------------------------------------------------------------------- -observer :: Typed a => String -> Stream a -> Spec+-- | 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.+observer :: Typed a+         => String    -- ^ Name used to identify the stream monitored in the+                      -- output produced during interpretation.+         -> Stream a  -- ^ The stream being monitored.+         -> 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  -------------------------------------------------------------------------------- -trigger :: String -> Stream Bool -> [Arg] -> Spec+-- | 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.+trigger :: String       -- ^ Name of the handler to be called.+        -> Stream Bool  -- ^ The stream used as the guard for the trigger.+        -> [Arg]        -- ^ List of arguments to the handler.+        -> 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   Forall :: Stream Bool -> Prop Universal   Exists :: Stream Bool -> Prop Existential +-- | Universal quantification of boolean streams over time. forall :: Stream Bool -> Prop Universal forall = Forall +-- | Existential quantification of boolean streams over time. exists :: Stream Bool -> Prop Existential exists = Exists +-- | Extract the underlying stream from a quantified proposition. extractProp :: Prop a -> Stream Bool 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.+--+-- This function returns, in the monadic context, a reference to the+-- proposition. prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) 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+-- proposition. theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) 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+-- provide additional information to monitor handlers in order to address+-- property violations. At any given point (e.g., when the trigger must be+-- called due to a violation), the arguments passed using 'arg' will contain+-- the current samples of the given streams. arg :: Typed a => Stream a -> Arg arg = Arg 

@@ -23,6 +23,13 @@  -------------------------------------------------------------------------------- +-- | 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+-- step-wise (e.g., 'Op1') or temporal transformations (e.g., 'Append', 'Drop')+-- to streams, or by combining existing streams to form new streams (e.g.,+-- 'Op2', 'Op3').+ data Stream :: * -> * where   Append      :: Typed a               => [a] -> Maybe (Stream Bool) -> Stream a -> Stream a@@ -45,6 +52,7 @@  -------------------------------------------------------------------------------- +-- | Wrapper to use 'Stream's as arguments to triggers. data Arg where   Arg :: Typed a => Stream a -> Arg @@ -65,6 +73,8 @@  -------------------------------------------------------------------------------- +-- | 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   (Const x) + (Const y)   = Const (x + y)   (Const 0) + y           = y@@ -92,6 +102,9 @@  -------------------------------------------------------------------------------- +-- | Streams carrying fractional numbers are instances of 'Fractional', and you can+-- apply to them the 'Fractional' functions, point-wise.+ -- XXX we may not want to precompute these if they're constants if someone is -- relying on certain floating-point behavior. instance (Typed a, P.Eq a, Fractional a) => Fractional (Stream a) where@@ -103,6 +116,9 @@   fromRational            = Const . fromRational  --------------------------------------------------------------------------------++-- | Streams carrying floating point numbers are instances of 'Floating', and+-- you can apply to them the 'Floating' functions, point-wise.  -- XXX we may not want to precompute these if they're constants if someone is -- relying on certain floating-point behavior.