| 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.
Synopsis
- data Int8
- data Int16
- data Int32
- data Int64
- module Data.Word
- class (Show a, Typeable a) => Typed a
- type Name = String
- data Type a where
- Bool :: Type Bool
- Int8 :: Type Int8
- Int16 :: Type Int16
- Int32 :: Type Int32
- Int64 :: Type Int64
- Word8 :: Type Word8
- Word16 :: Type Word16
- Word32 :: Type Word32
- Word64 :: Type Word64
- Float :: Type Float
- Double :: Type Double
- Array :: forall (n :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t)
- Struct :: forall a. (Typed a, Struct a) => a -> Type a
- class (Show a, Typeable a) => Typed a where
- typeOf :: Type a
- simpleType :: Type a -> SimpleType
- data UType = Typeable a => UType (Type a)
- data SimpleType where
- SBool :: SimpleType
- SInt8 :: SimpleType
- SInt16 :: SimpleType
- SInt32 :: SimpleType
- SInt64 :: SimpleType
- SWord8 :: SimpleType
- SWord16 :: SimpleType
- SWord32 :: SimpleType
- SWord64 :: SimpleType
- SFloat :: SimpleType
- SDouble :: SimpleType
- SArray :: forall t. Type t -> SimpleType
- SStruct :: SimpleType
- class Struct a where
- data Field (s :: Symbol) t = Field t
- data Value a = (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
- fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
- accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String
- typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String
- toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a]
- updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a
- typeOfDefault :: (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a
- array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t
- data Array (n :: Nat) t
- arrayElems :: forall (n :: Nat) a. Array n a -> [a]
- arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
- badUsage :: String -> a
- impossible :: String -> String -> a
- interpret :: Integer -> Spec -> IO ()
- csv :: 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 a
- 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
Documentation
8-bit signed integer type
Instances
16-bit signed integer type
Instances
32-bit signed integer type
Instances
64-bit signed integer type
Instances
module Data.Word
class (Show a, Typeable a) => Typed a #
Minimal complete definition
Instances
| Typed Int16 | |
Defined in Copilot.Core.Type | |
| Typed Int32 | |
Defined in Copilot.Core.Type | |
| Typed Int64 | |
Defined in Copilot.Core.Type | |
| Typed Int8 | |
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 | |
| Typed Word8 | |
Defined in Copilot.Core.Type | |
| Typed Bool | |
Defined in Copilot.Core.Type | |
| Typed Double | |
Defined in Copilot.Core.Type | |
| Typed Float | |
Defined in Copilot.Core.Type | |
| (Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |
Defined in Copilot.Core.Type | |
Constructors
| Bool :: Type Bool | |
| Int8 :: Type Int8 | |
| Int16 :: Type Int16 | |
| Int32 :: Type Int32 | |
| Int64 :: Type Int64 | |
| Word8 :: Type Word8 | |
| Word16 :: Type Word16 | |
| Word32 :: Type Word32 | |
| Word64 :: Type Word64 | |
| Float :: Type Float | |
| Double :: Type Double | |
| Array :: forall (n :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t) | |
| Struct :: forall a. (Typed a, Struct a) => a -> Type a |
class (Show a, Typeable a) => Typed a where #
Minimal complete definition
Instances
| Typed Int16 | |
Defined in Copilot.Core.Type | |
| Typed Int32 | |
Defined in Copilot.Core.Type | |
| Typed Int64 | |
Defined in Copilot.Core.Type | |
| Typed Int8 | |
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 | |
| Typed Word8 | |
Defined in Copilot.Core.Type | |
| Typed Bool | |
Defined in Copilot.Core.Type | |
| Typed Double | |
Defined in Copilot.Core.Type | |
| Typed Float | |
Defined in Copilot.Core.Type | |
| (Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |
Defined in Copilot.Core.Type | |
data SimpleType where #
Constructors
| SBool :: SimpleType | |
| SInt8 :: SimpleType | |
| SInt16 :: SimpleType | |
| SInt32 :: SimpleType | |
| SInt64 :: SimpleType | |
| SWord8 :: SimpleType | |
| SWord16 :: SimpleType | |
| SWord32 :: SimpleType | |
| SWord64 :: SimpleType | |
| SFloat :: SimpleType | |
| SDouble :: SimpleType | |
| SArray :: forall t. Type t -> SimpleType | |
| SStruct :: SimpleType |
Instances
| Eq SimpleType | |
Defined in Copilot.Core.Type Methods (==) :: SimpleType -> SimpleType -> Bool Source # (/=) :: SimpleType -> SimpleType -> Bool Source # | |
Constructors
| Field t |
Instances
| (KnownSymbol f, Typed s, Typed t, Struct s) => Projectable s (s -> Field f t) t Source # | Update a stream of structs. | ||||
Defined in Copilot.Language.Operators.Struct Associated Types
| |||||
| (KnownSymbol s, Show t) => Show (Field s t) | |||||
| data Projection s (s -> Field f t) t Source # | |||||
Defined in Copilot.Language.Operators.Struct | |||||
accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String #
typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String #
toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a] #
updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a #
Instances
| (Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |||||
Defined in Copilot.Core.Type | |||||
| Show t => Show (Array n t) | |||||
| (KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t Source # | Update a stream of arrays. | ||||
Defined in Copilot.Language.Operators.Array Associated Types
| |||||
| data Projection (Array n t) (Stream Word32) t Source # | |||||
Defined in Copilot.Language.Operators.Array | |||||
arrayElems :: forall (n :: Nat) a. Array n a -> [a] #
Arguments
| :: String | Description of the error. |
| -> a |
Report an error due to an error detected by Copilot (e.g., user error).
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.
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.
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.
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]
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
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.