| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Copilot.Language
Description
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
Instances
Instances
Instances
class (Show a, Typeable a) => Typed a #
Minimal complete definition
typeOf
Instances
| Typed Bool | |
Defined in Copilot.Core.Type | |
| Typed Double | |
Defined in Copilot.Core.Type | |
| Typed Float | |
Defined in Copilot.Core.Type | |
| Typed Int8 | |
Defined in Copilot.Core.Type | |
| Typed Int16 | |
Defined in Copilot.Core.Type | |
| Typed Int32 | |
Defined in Copilot.Core.Type | |
| Typed Int64 | |
Defined in Copilot.Core.Type | |
| Typed Word8 | |
Defined in Copilot.Core.Type | |
| Typed Word16 | |
Defined in Copilot.Core.Type | |
| Typed Word32 | |
Defined in Copilot.Core.Type | |
| Typed Word64 | |
Defined in Copilot.Core.Type | |
| (Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) | |
Defined in Copilot.Core.Type | |
Arguments
| :: 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.
Arguments
| :: 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 Methods 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 Methods (.&.) :: 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 | |
Arguments
| :: 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.
Arguments
| :: 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.
Args 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.