Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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.
Synopsis
- data Int8
- data Int16
- data Int32
- data Int64
- type Name = String
- class (Show a, Typeable a) => Typed a
- impossible :: String -> String -> a
- badUsage :: String -> a
- csv :: Integer -> Spec -> IO ()
- interpret :: Integer -> Spec -> IO ()
- module Copilot.Language.Operators.Boolean
- module Copilot.Language.Operators.Cast
- module Copilot.Language.Operators.Constant
- module Copilot.Language.Operators.Eq
- module Copilot.Language.Operators.Extern
- module Copilot.Language.Operators.Local
- module Copilot.Language.Operators.Label
- module Copilot.Language.Operators.Integral
- module Copilot.Language.Operators.Mux
- module Copilot.Language.Operators.Ord
- module Copilot.Language.Operators.Temporal
- module Copilot.Language.Operators.BitWise
- module Copilot.Language.Operators.Array
- module Copilot.Language.Operators.Struct
- module Copilot.Language.Prelude
- type Spec = Writer [SpecItem] ()
- data Stream :: * -> *
- observer :: Typed a => String -> Stream a -> Spec
- trigger :: String -> Stream Bool -> [Arg] -> Spec
- arg :: Typed a => Stream a -> Arg
- prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
- theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
- forall :: Stream Bool -> Prop Universal
- exists :: Stream Bool -> Prop Existential
- prettyPrint :: Spec -> IO ()
Documentation
Instances
Bounded Int8 | |
Enum Int8 | |
Eq Int8 | |
Integral Int8 | |
Num Int8 | |
Ord Int8 | |
Read Int8 | |
Real Int8 | |
Defined in GHC.Int toRational :: Int8 -> Rational # | |
Show Int8 | |
Ix Int8 | |
FiniteBits Int8 | |
Defined in GHC.Int | |
Bits Int8 | |
Defined in GHC.Int (.&.) :: Int8 -> Int8 -> Int8 # (.|.) :: Int8 -> Int8 -> Int8 # complement :: Int8 -> Int8 # clearBit :: Int8 -> Int -> Int8 complementBit :: Int8 -> Int -> Int8 testBit :: Int8 -> Int -> Bool bitSizeMaybe :: Int8 -> Maybe Int unsafeShiftL :: Int8 -> Int -> Int8 unsafeShiftR :: Int8 -> Int -> Int8 rotateL :: Int8 -> Int -> Int8 | |
Typed Int8 | |
Defined in Copilot.Core.Type simpleType :: Type Int8 -> SimpleType | |
UnsafeCast Int8 Double Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int8 Float Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int8 Word8 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int16 Int8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int32 Int8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Int8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word8 Int8 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
Cast Bool Int8 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
Cast Int8 Int8 Source # | Identity casting. |
Cast Int8 Int16 Source # | Cast number to bigger type. |
Cast Int8 Int32 Source # | Cast number to bigger type. |
Cast Int8 Int64 Source # | Cast number to bigger type. |
Instances
Instances
Instances
class (Show a, Typeable a) => Typed a #
typeOf
Instances
Typed Bool | |
Defined in Copilot.Core.Type simpleType :: Type Bool -> SimpleType | |
Typed Double | |
Defined in Copilot.Core.Type simpleType :: Type Double -> SimpleType | |
Typed Float | |
Defined in Copilot.Core.Type simpleType :: Type Float -> SimpleType | |
Typed Int8 | |
Defined in Copilot.Core.Type simpleType :: Type Int8 -> SimpleType | |
Typed Int16 | |
Defined in Copilot.Core.Type simpleType :: Type Int16 -> SimpleType | |
Typed Int32 | |
Defined in Copilot.Core.Type simpleType :: Type Int32 -> SimpleType | |
Typed Int64 | |
Defined in Copilot.Core.Type simpleType :: Type Int64 -> SimpleType | |
Typed Word8 | |
Defined in Copilot.Core.Type typeOf :: Type Word8 simpleType :: Type Word8 -> SimpleType | |
Typed Word16 | |
Defined in Copilot.Core.Type typeOf :: Type Word16 simpleType :: Type Word16 -> SimpleType | |
Typed Word32 | |
Defined in Copilot.Core.Type typeOf :: Type Word32 simpleType :: Type Word32 -> SimpleType | |
Typed Word64 | |
Defined in Copilot.Core.Type typeOf :: Type Word64 simpleType :: Type Word64 -> SimpleType | |
(Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) | |
Defined in Copilot.Core.Type typeOf :: Type (Array n t) simpleType :: Type (Array n t) -> SimpleType |
:: String | Name of the function in which the error was detected. |
-> String | Name of the package in which the function is located. |
-> a |
Report an error due to a bug in Copilot.
:: String | Description of the error. |
-> a |
Report an error due to an error detected by Copilot (e.g., user error).
csv :: Integer -> Spec -> IO () Source #
Simulate a number of steps of a given specification, printing the results in a table in comma-separated value (CSV) format.
interpret :: Integer -> Spec -> IO () Source #
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.
module Copilot.Language.Prelude
type Spec = Writer [SpecItem] () Source #
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]
data Stream :: * -> * Source #
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
).
Instances
Eq (Stream a) Source # | |
(Typed a, Eq a, Floating a) => Floating (Stream a) Source # | Streams carrying floating point numbers are instances of |
Defined in Copilot.Language.Stream sqrt :: Stream a -> Stream a # (**) :: Stream a -> Stream a -> Stream a # logBase :: Stream a -> Stream a -> Stream a # asin :: Stream a -> Stream a # acos :: Stream a -> Stream a # atan :: Stream a -> Stream a # sinh :: Stream a -> Stream a # cosh :: Stream a -> Stream a # tanh :: Stream a -> Stream a # asinh :: Stream a -> Stream a # acosh :: Stream a -> Stream a # atanh :: Stream a -> Stream a # | |
(Typed a, Eq a, Fractional a) => Fractional (Stream a) Source # | Streams carrying fractional numbers are instances of |
(Typed a, Eq a, Num a) => Num (Stream a) Source # | Streams carrying numbers are instances of |
Show (Stream a) Source # | |
(Typed a, Bits a) => Bits (Stream a) Source # | Instance of the Only the methods |
Defined in Copilot.Language.Operators.BitWise (.&.) :: Stream a -> Stream a -> Stream a # (.|.) :: Stream a -> Stream a -> Stream a # xor :: Stream a -> Stream a -> Stream a complement :: Stream a -> Stream a # shift :: Stream a -> Int -> Stream a rotate :: Stream a -> Int -> Stream a setBit :: Stream a -> Int -> Stream a clearBit :: Stream a -> Int -> Stream a complementBit :: Stream a -> Int -> Stream a testBit :: Stream a -> Int -> Bool bitSizeMaybe :: Stream a -> Maybe Int shiftL :: Stream a -> Int -> Stream a unsafeShiftL :: Stream a -> Int -> Stream a shiftR :: Stream a -> Int -> Stream a unsafeShiftR :: Stream a -> Int -> Stream a rotateL :: Stream a -> Int -> Stream a |
:: Typed a | |
=> String | Name used to identify the stream monitored in the output produced during interpretation. |
-> Stream a | The stream being monitored. |
-> 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.
:: 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 |
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.
arg :: Typed a => Stream a -> Arg Source #
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.
prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) Source #
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.
theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) Source #
A theorem, or proposition together with a proof.
This function returns, in the monadic context, a reference to the proposition.
forall :: Stream Bool -> Prop Universal Source #
Universal quantification of boolean streams over time.
exists :: Stream Bool -> Prop Existential Source #
Existential quantification of boolean streams over time.
prettyPrint :: Spec -> IO () Source #
Transform a high-level Copilot Language specification into a low-level Copilot Core specification and pretty-print it to stdout.