diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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). diff --git a/copilot-language.cabal b/copilot-language.cabal --- a/copilot-language.cabal +++ b/copilot-language.cabal @@ -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 diff --git a/src/Copilot.hs b/src/Copilot.hs --- a/src/Copilot.hs +++ b/src/Copilot.hs @@ -2,8 +2,6 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Main import module for the front-end lanugage. - {-# LANGUAGE Safe #-} module Copilot diff --git a/src/Copilot/Language.hs b/src/Copilot/Language.hs --- a/src/Copilot/Language.hs +++ b/src/Copilot/Language.hs @@ -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 diff --git a/src/Copilot/Language/Analyze.hs b/src/Copilot/Language/Analyze.hs --- a/src/Copilot/Language/Analyze.hs +++ b/src/Copilot/Language/Analyze.hs @@ -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) diff --git a/src/Copilot/Language/Error.hs b/src/Copilot/Language/Error.hs --- a/src/Copilot/Language/Error.hs +++ b/src/Copilot/Language/Error.hs @@ -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 " ++ "(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 diff --git a/src/Copilot/Language/Interpret.hs b/src/Copilot/Language/Interpret.hs --- a/src/Copilot/Language/Interpret.hs +++ b/src/Copilot/Language/Interpret.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Array.hs b/src/Copilot/Language/Operators/Array.hs --- a/src/Copilot/Language/Operators/Array.hs +++ b/src/Copilot/Language/Operators/Array.hs @@ -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' diff --git a/src/Copilot/Language/Operators/BitWise.hs b/src/Copilot/Language/Operators/BitWise.hs --- a/src/Copilot/Language/Operators/BitWise.hs +++ b/src/Copilot/Language/Operators/BitWise.hs @@ -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) diff --git a/src/Copilot/Language/Operators/Boolean.hs b/src/Copilot/Language/Operators/Boolean.hs --- a/src/Copilot/Language/Operators/Boolean.hs +++ b/src/Copilot/Language/Operators/Boolean.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Cast.hs b/src/Copilot/Language/Operators/Cast.hs --- a/src/Copilot/Language/Operators/Cast.hs +++ b/src/Copilot/Language/Operators/Cast.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Constant.hs b/src/Copilot/Language/Operators/Constant.hs --- a/src/Copilot/Language/Operators/Constant.hs +++ b/src/Copilot/Language/Operators/Constant.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Eq.hs b/src/Copilot/Language/Operators/Eq.hs --- a/src/Copilot/Language/Operators/Eq.hs +++ b/src/Copilot/Language/Operators/Eq.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Extern.hs b/src/Copilot/Language/Operators/Extern.hs --- a/src/Copilot/Language/Operators/Extern.hs +++ b/src/Copilot/Language/Operators/Extern.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Integral.hs b/src/Copilot/Language/Operators/Integral.hs --- a/src/Copilot/Language/Operators/Integral.hs +++ b/src/Copilot/Language/Operators/Integral.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Label.hs b/src/Copilot/Language/Operators/Label.hs --- a/src/Copilot/Language/Operators/Label.hs +++ b/src/Copilot/Language/Operators/Label.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Local.hs b/src/Copilot/Language/Operators/Local.hs --- a/src/Copilot/Language/Operators/Local.hs +++ b/src/Copilot/Language/Operators/Local.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Mux.hs b/src/Copilot/Language/Operators/Mux.hs --- a/src/Copilot/Language/Operators/Mux.hs +++ b/src/Copilot/Language/Operators/Mux.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Ord.hs b/src/Copilot/Language/Operators/Ord.hs --- a/src/Copilot/Language/Operators/Ord.hs +++ b/src/Copilot/Language/Operators/Ord.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Propositional.hs b/src/Copilot/Language/Operators/Propositional.hs --- a/src/Copilot/Language/Operators/Propositional.hs +++ b/src/Copilot/Language/Operators/Propositional.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Struct.hs b/src/Copilot/Language/Operators/Struct.hs --- a/src/Copilot/Language/Operators/Struct.hs +++ b/src/Copilot/Language/Operators/Struct.hs @@ -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 diff --git a/src/Copilot/Language/Operators/Temporal.hs b/src/Copilot/Language/Operators/Temporal.hs --- a/src/Copilot/Language/Operators/Temporal.hs +++ b/src/Copilot/Language/Operators/Temporal.hs @@ -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 diff --git a/src/Copilot/Language/Reify.hs b/src/Copilot/Language/Reify.hs --- a/src/Copilot/Language/Reify.hs +++ b/src/Copilot/Language/Reify.hs @@ -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) diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs --- a/src/Copilot/Language/Spec.hs +++ b/src/Copilot/Language/Spec.hs @@ -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 diff --git a/src/Copilot/Language/Stream.hs b/src/Copilot/Language/Stream.hs --- a/src/Copilot/Language/Stream.hs +++ b/src/Copilot/Language/Stream.hs @@ -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.