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
- module Copilot.Core.Type
- module Copilot.Core.Type.Array
- 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
- forall :: Stream Bool -> Prop Universal
- exists :: Stream Bool -> Prop Existential
Documentation
8-bit signed integer type
Instances
Bits Int8 | Since: base-2.1 |
Defined in GHC.Int Methods (.&.) :: Int8 -> Int8 -> Int8 Source # (.|.) :: Int8 -> Int8 -> Int8 Source # xor :: Int8 -> Int8 -> Int8 Source # complement :: Int8 -> Int8 Source # shift :: Int8 -> Int -> Int8 Source # rotate :: Int8 -> Int -> Int8 Source # setBit :: Int8 -> Int -> Int8 Source # clearBit :: Int8 -> Int -> Int8 Source # complementBit :: Int8 -> Int -> Int8 Source # testBit :: Int8 -> Int -> Bool Source # bitSizeMaybe :: Int8 -> Maybe Int Source # bitSize :: Int8 -> Int Source # isSigned :: Int8 -> Bool Source # shiftL :: Int8 -> Int -> Int8 Source # unsafeShiftL :: Int8 -> Int -> Int8 Source # shiftR :: Int8 -> Int -> Int8 Source # unsafeShiftR :: Int8 -> Int -> Int8 Source # rotateL :: Int8 -> Int -> Int8 Source # | |
FiniteBits Int8 | Since: base-4.6.0.0 |
Bounded Int8 | Since: base-2.1 |
Enum Int8 | Since: base-2.1 |
Ix Int8 | Since: base-2.1 |
Num Int8 | Since: base-2.1 |
Read Int8 | Since: base-2.1 |
Integral Int8 | Since: base-2.1 |
Defined in GHC.Int | |
Real Int8 | Since: base-2.1 |
Show Int8 | Since: base-2.1 |
Typed Int8 | |
Defined in Copilot.Core.Type | |
Eq Int8 | Since: base-2.1 |
Ord Int8 | Since: base-2.1 |
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. |
Cast Int8 Int8 Source # | Identity casting. |
Cast Bool Int8 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
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 Int8 Word8 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
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 Word8 Int8 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast |
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 Source #
A typed expression, from which we can obtain the two type representations
used by Copilot: Type
and SimpleType
.
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 |
module Copilot.Core.Type
module Copilot.Core.Type.Array
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
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.
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.