copilot-language-4.7.1: A Haskell-embedded DSL for monitoring hard real-time distributed systems.

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
- 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

data Int8 Source #

8-bit signed integer type

#### Instances

Instances details

PrintfArg Int8 | Since: base-2.1
Instance details Defined in Text.Printf Methods formatArg :: Int8 -> FieldFormatter Source # parseFormat :: Int8 -> ModifierParser Source #
Typed Int8 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 Source # simpleType :: Type Int8 -> SimpleType Source #
NFData Int8 |
Instance details Defined in Control.DeepSeq Methods rnf :: Int8 -> () Source #
Bits Int8 | Since: base-2.1

Instance details

Defined in GHC.Internal.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 #

zeroBits :: Int8 Source #

bit :: 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 #

rotateR :: Int8 -> Int -> Int8 Source #

popCount :: Int8 -> Int Source #

FiniteBits Int8 | Since: base-4.6.0.0
Instance details Defined in GHC.Internal.Int Methods finiteBitSize :: Int8 -> Int Source # countLeadingZeros :: Int8 -> Int Source # countTrailingZeros :: Int8 -> Int Source #
Bounded Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods minBound :: Int8 Source # maxBound :: Int8 Source #
Enum Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods succ :: Int8 -> Int8 Source # pred :: Int8 -> Int8 Source # toEnum :: Int -> Int8 Source # fromEnum :: Int8 -> Int Source # enumFrom :: Int8 -> [Int8] Source # enumFromThen :: Int8 -> Int8 -> [Int8] Source # enumFromTo :: Int8 -> Int8 -> [Int8] Source # enumFromThenTo :: Int8 -> Int8 -> Int8 -> [Int8] Source #
Ix Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods range :: (Int8, Int8) -> [Int8] Source # index :: (Int8, Int8) -> Int8 -> Int Source # unsafeIndex :: (Int8, Int8) -> Int8 -> Int Source # inRange :: (Int8, Int8) -> Int8 -> Bool Source # rangeSize :: (Int8, Int8) -> Int Source # unsafeRangeSize :: (Int8, Int8) -> Int Source #
Num Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (+) :: Int8 -> Int8 -> Int8 Source # (-) :: Int8 -> Int8 -> Int8 Source # (*) :: Int8 -> Int8 -> Int8 Source # negate :: Int8 -> Int8 Source # abs :: Int8 -> Int8 Source # signum :: Int8 -> Int8 Source # fromInteger :: Integer -> Int8 Source #
Read Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods readsPrec :: Int -> ReadS Int8 Source # readList :: ReadS [Int8] Source # readPrec :: ReadPrec Int8 Source # readListPrec :: ReadPrec [Int8] Source #
Integral Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods quot :: Int8 -> Int8 -> Int8 Source # rem :: Int8 -> Int8 -> Int8 Source # div :: Int8 -> Int8 -> Int8 Source # mod :: Int8 -> Int8 -> Int8 Source # quotRem :: Int8 -> Int8 -> (Int8, Int8) Source # divMod :: Int8 -> Int8 -> (Int8, Int8) Source # toInteger :: Int8 -> Integer Source #
Real Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods toRational :: Int8 -> Rational Source #
Show Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods showsPrec :: Int -> Int8 -> ShowS Source # show :: Int8 -> String Source # showList :: [Int8] -> ShowS Source #
Eq Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (==) :: Int8 -> Int8 -> Bool Source # (/=) :: Int8 -> Int8 -> Bool Source #
Ord Int8 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods compare :: Int8 -> Int8 -> Ordering Source # (<) :: Int8 -> Int8 -> Bool Source # (<=) :: Int8 -> Int8 -> Bool Source # (>) :: Int8 -> Int8 -> Bool Source # (>=) :: Int8 -> Int8 -> Bool Source # max :: Int8 -> Int8 -> Int8 Source # min :: Int8 -> Int8 -> Int8 Source #
IArray UArray Int8 |

Instance details

Defined in Data.Array.Base

Methods

bounds :: Ix i => UArray i Int8 -> (i, i) Source #

numElements :: Ix i => UArray i Int8 -> Int Source #

unsafeArray :: Ix i => (i, i) -> [(Int, Int8)] -> UArray i Int8 Source #

unsafeAt :: Ix i => UArray i Int8 -> Int -> Int8 Source #

unsafeReplace :: Ix i => UArray i Int8 -> [(Int, Int8)] -> UArray i Int8 Source #

unsafeAccum :: Ix i => (Int8 -> e' -> Int8) -> UArray i Int8 -> [(Int, e')] -> UArray i Int8 Source #

unsafeAccumArray :: Ix i => (Int8 -> e' -> Int8) -> Int8 -> (i, i) -> [(Int, e')] -> UArray i Int8 Source #

Cast Int8 Int16 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int16 Source #
Cast Int8 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int32 Source #
Cast Int8 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int64 Source #
Cast Int8 Int8 Source # | Identity casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int8 Source #
Cast Bool Int8 Source # | 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 details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int8 Source #
UnsafeCast Int16 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Int8 Source #
UnsafeCast Int32 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int8 Source #
UnsafeCast Int64 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int8 Source #
UnsafeCast Int8 Word8 Source # | Signed to unsigned casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Word8 Source #
UnsafeCast Int8 Double Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Double Source #
UnsafeCast Int8 Float Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Float Source #
UnsafeCast Word8 Int8 Source # | Cast from unsigned numbers to signed numbers.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word8 -> Stream Int8 Source #
Lift Int8 |
Instance details Defined in Language.Haskell.TH.Syntax Methods lift :: Quote m => Int8 -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Int8 -> Code m Int8 Source #
MArray IOUArray Int8 IO |

Instance details

Defined in Data.Array.IO.Internals

Methods

getBounds :: Ix i => IOUArray i Int8 -> IO (i, i) Source #

getNumElements :: Ix i => IOUArray i Int8 -> IO Int Source #

newArray :: Ix i => (i, i) -> Int8 -> IO (IOUArray i Int8) Source #

newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int8) Source #

unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int8) Source #

unsafeRead :: Ix i => IOUArray i Int8 -> Int -> IO Int8 Source #

unsafeWrite :: Ix i => IOUArray i Int8 -> Int -> Int8 -> IO () Source #

MArray (STUArray s) Int8 (ST s) |

Instance details

Defined in Data.Array.Base

Methods

getBounds :: Ix i => STUArray s i Int8 -> ST s (i, i) Source #

getNumElements :: Ix i => STUArray s i Int8 -> ST s Int Source #

newArray :: Ix i => (i, i) -> Int8 -> ST s (STUArray s i Int8) Source #

newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int8) Source #

unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int8) Source #

unsafeRead :: Ix i => STUArray s i Int8 -> Int -> ST s Int8 Source #

unsafeWrite :: Ix i => STUArray s i Int8 -> Int -> Int8 -> ST s () Source #

data Int16 Source #

16-bit signed integer type

#### Instances

Instances details

PrintfArg Int16 | Since: base-2.1
Instance details Defined in Text.Printf Methods formatArg :: Int16 -> FieldFormatter Source # parseFormat :: Int16 -> ModifierParser Source #
Typed Int16 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int16 Source # simpleType :: Type Int16 -> SimpleType Source #
NFData Int16 |
Instance details Defined in Control.DeepSeq Methods rnf :: Int16 -> () Source #
Bits Int16 | Since: base-2.1

Instance details

Defined in GHC.Internal.Int

Methods

(.&.) :: Int16 -> Int16 -> Int16 Source #

(.|.) :: Int16 -> Int16 -> Int16 Source #

xor :: Int16 -> Int16 -> Int16 Source #

complement :: Int16 -> Int16 Source #

shift :: Int16 -> Int -> Int16 Source #

rotate :: Int16 -> Int -> Int16 Source #

zeroBits :: Int16 Source #

bit :: Int -> Int16 Source #

setBit :: Int16 -> Int -> Int16 Source #

clearBit :: Int16 -> Int -> Int16 Source #

complementBit :: Int16 -> Int -> Int16 Source #

testBit :: Int16 -> Int -> Bool Source #

bitSizeMaybe :: Int16 -> Maybe Int Source #

bitSize :: Int16 -> Int Source #

isSigned :: Int16 -> Bool Source #

shiftL :: Int16 -> Int -> Int16 Source #

unsafeShiftL :: Int16 -> Int -> Int16 Source #

shiftR :: Int16 -> Int -> Int16 Source #

unsafeShiftR :: Int16 -> Int -> Int16 Source #

rotateL :: Int16 -> Int -> Int16 Source #

rotateR :: Int16 -> Int -> Int16 Source #

popCount :: Int16 -> Int Source #

FiniteBits Int16 | Since: base-4.6.0.0
Instance details Defined in GHC.Internal.Int Methods finiteBitSize :: Int16 -> Int Source # countLeadingZeros :: Int16 -> Int Source # countTrailingZeros :: Int16 -> Int Source #
Bounded Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods minBound :: Int16 Source # maxBound :: Int16 Source #
Enum Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods succ :: Int16 -> Int16 Source # pred :: Int16 -> Int16 Source # toEnum :: Int -> Int16 Source # fromEnum :: Int16 -> Int Source # enumFrom :: Int16 -> [Int16] Source # enumFromThen :: Int16 -> Int16 -> [Int16] Source # enumFromTo :: Int16 -> Int16 -> [Int16] Source # enumFromThenTo :: Int16 -> Int16 -> Int16 -> [Int16] Source #
Ix Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods range :: (Int16, Int16) -> [Int16] Source # index :: (Int16, Int16) -> Int16 -> Int Source # unsafeIndex :: (Int16, Int16) -> Int16 -> Int Source # inRange :: (Int16, Int16) -> Int16 -> Bool Source # rangeSize :: (Int16, Int16) -> Int Source # unsafeRangeSize :: (Int16, Int16) -> Int Source #
Num Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (+) :: Int16 -> Int16 -> Int16 Source # (-) :: Int16 -> Int16 -> Int16 Source # (*) :: Int16 -> Int16 -> Int16 Source # negate :: Int16 -> Int16 Source # abs :: Int16 -> Int16 Source # signum :: Int16 -> Int16 Source # fromInteger :: Integer -> Int16 Source #
Read Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods readsPrec :: Int -> ReadS Int16 Source # readList :: ReadS [Int16] Source # readPrec :: ReadPrec Int16 Source # readListPrec :: ReadPrec [Int16] Source #
Integral Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods quot :: Int16 -> Int16 -> Int16 Source # rem :: Int16 -> Int16 -> Int16 Source # div :: Int16 -> Int16 -> Int16 Source # mod :: Int16 -> Int16 -> Int16 Source # quotRem :: Int16 -> Int16 -> (Int16, Int16) Source # divMod :: Int16 -> Int16 -> (Int16, Int16) Source # toInteger :: Int16 -> Integer Source #
Real Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods toRational :: Int16 -> Rational Source #
Show Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods showsPrec :: Int -> Int16 -> ShowS Source # show :: Int16 -> String Source # showList :: [Int16] -> ShowS Source #
Eq Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (==) :: Int16 -> Int16 -> Bool Source # (/=) :: Int16 -> Int16 -> Bool Source #
Ord Int16 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods compare :: Int16 -> Int16 -> Ordering Source # (<) :: Int16 -> Int16 -> Bool Source # (<=) :: Int16 -> Int16 -> Bool Source # (>) :: Int16 -> Int16 -> Bool Source # (>=) :: Int16 -> Int16 -> Bool Source # max :: Int16 -> Int16 -> Int16 Source # min :: Int16 -> Int16 -> Int16 Source #
IArray UArray Int16 |

Instance details

Defined in Data.Array.Base

Methods

bounds :: Ix i => UArray i Int16 -> (i, i) Source #

numElements :: Ix i => UArray i Int16 -> Int Source #

unsafeArray :: Ix i => (i, i) -> [(Int, Int16)] -> UArray i Int16 Source #

unsafeAt :: Ix i => UArray i Int16 -> Int -> Int16 Source #

unsafeReplace :: Ix i => UArray i Int16 -> [(Int, Int16)] -> UArray i Int16 Source #

unsafeAccum :: Ix i => (Int16 -> e' -> Int16) -> UArray i Int16 -> [(Int, e')] -> UArray i Int16 Source #

unsafeAccumArray :: Ix i => (Int16 -> e' -> Int16) -> Int16 -> (i, i) -> [(Int, e')] -> UArray i Int16 Source #

Cast Int16 Int16 Source # | Identity casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int16 Source #
Cast Int16 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int32 Source #
Cast Int16 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int64 Source #
Cast Int8 Int16 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int16 Source #
Cast Word8 Int16 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int16 Source #
Cast Bool Int16 Source # | 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 details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int16 Source #
UnsafeCast Int16 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Int8 Source #
UnsafeCast Int16 Word16 Source # | Signed to unsigned casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Word16 Source #
UnsafeCast Int16 Double Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Double Source #
UnsafeCast Int16 Float Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Float Source #
UnsafeCast Int32 Int16 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int16 Source #
UnsafeCast Int64 Int16 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int16 Source #
UnsafeCast Word16 Int16 Source # | Cast from unsigned numbers to signed numbers.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word16 -> Stream Int16 Source #
Lift Int16 |
Instance details Defined in Language.Haskell.TH.Syntax Methods lift :: Quote m => Int16 -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Int16 -> Code m Int16 Source #
MArray IOUArray Int16 IO |

Instance details

Defined in Data.Array.IO.Internals

Methods

getBounds :: Ix i => IOUArray i Int16 -> IO (i, i) Source #

getNumElements :: Ix i => IOUArray i Int16 -> IO Int Source #

newArray :: Ix i => (i, i) -> Int16 -> IO (IOUArray i Int16) Source #

newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int16) Source #

unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int16) Source #

unsafeRead :: Ix i => IOUArray i Int16 -> Int -> IO Int16 Source #

unsafeWrite :: Ix i => IOUArray i Int16 -> Int -> Int16 -> IO () Source #

MArray (STUArray s) Int16 (ST s) |

Instance details

Defined in Data.Array.Base

Methods

getBounds :: Ix i => STUArray s i Int16 -> ST s (i, i) Source #

getNumElements :: Ix i => STUArray s i Int16 -> ST s Int Source #

newArray :: Ix i => (i, i) -> Int16 -> ST s (STUArray s i Int16) Source #

newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int16) Source #

unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int16) Source #

unsafeRead :: Ix i => STUArray s i Int16 -> Int -> ST s Int16 Source #

unsafeWrite :: Ix i => STUArray s i Int16 -> Int -> Int16 -> ST s () Source #

data Int32 Source #

32-bit signed integer type

#### Instances

Instances details

PrintfArg Int32 | Since: base-2.1
Instance details Defined in Text.Printf Methods formatArg :: Int32 -> FieldFormatter Source # parseFormat :: Int32 -> ModifierParser Source #
Typed Int32 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int32 Source # simpleType :: Type Int32 -> SimpleType Source #
NFData Int32 |
Instance details Defined in Control.DeepSeq Methods rnf :: Int32 -> () Source #
Bits Int32 | Since: base-2.1

Instance details

Defined in GHC.Internal.Int

Methods

(.&.) :: Int32 -> Int32 -> Int32 Source #

(.|.) :: Int32 -> Int32 -> Int32 Source #

xor :: Int32 -> Int32 -> Int32 Source #

complement :: Int32 -> Int32 Source #

shift :: Int32 -> Int -> Int32 Source #

rotate :: Int32 -> Int -> Int32 Source #

zeroBits :: Int32 Source #

bit :: Int -> Int32 Source #

setBit :: Int32 -> Int -> Int32 Source #

clearBit :: Int32 -> Int -> Int32 Source #

complementBit :: Int32 -> Int -> Int32 Source #

testBit :: Int32 -> Int -> Bool Source #

bitSizeMaybe :: Int32 -> Maybe Int Source #

bitSize :: Int32 -> Int Source #

isSigned :: Int32 -> Bool Source #

shiftL :: Int32 -> Int -> Int32 Source #

unsafeShiftL :: Int32 -> Int -> Int32 Source #

shiftR :: Int32 -> Int -> Int32 Source #

unsafeShiftR :: Int32 -> Int -> Int32 Source #

rotateL :: Int32 -> Int -> Int32 Source #

rotateR :: Int32 -> Int -> Int32 Source #

popCount :: Int32 -> Int Source #

FiniteBits Int32 | Since: base-4.6.0.0
Instance details Defined in GHC.Internal.Int Methods finiteBitSize :: Int32 -> Int Source # countLeadingZeros :: Int32 -> Int Source # countTrailingZeros :: Int32 -> Int Source #
Bounded Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods minBound :: Int32 Source # maxBound :: Int32 Source #
Enum Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods succ :: Int32 -> Int32 Source # pred :: Int32 -> Int32 Source # toEnum :: Int -> Int32 Source # fromEnum :: Int32 -> Int Source # enumFrom :: Int32 -> [Int32] Source # enumFromThen :: Int32 -> Int32 -> [Int32] Source # enumFromTo :: Int32 -> Int32 -> [Int32] Source # enumFromThenTo :: Int32 -> Int32 -> Int32 -> [Int32] Source #
Ix Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods range :: (Int32, Int32) -> [Int32] Source # index :: (Int32, Int32) -> Int32 -> Int Source # unsafeIndex :: (Int32, Int32) -> Int32 -> Int Source # inRange :: (Int32, Int32) -> Int32 -> Bool Source # rangeSize :: (Int32, Int32) -> Int Source # unsafeRangeSize :: (Int32, Int32) -> Int Source #
Num Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (+) :: Int32 -> Int32 -> Int32 Source # (-) :: Int32 -> Int32 -> Int32 Source # (*) :: Int32 -> Int32 -> Int32 Source # negate :: Int32 -> Int32 Source # abs :: Int32 -> Int32 Source # signum :: Int32 -> Int32 Source # fromInteger :: Integer -> Int32 Source #
Read Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods readsPrec :: Int -> ReadS Int32 Source # readList :: ReadS [Int32] Source # readPrec :: ReadPrec Int32 Source # readListPrec :: ReadPrec [Int32] Source #
Integral Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods quot :: Int32 -> Int32 -> Int32 Source # rem :: Int32 -> Int32 -> Int32 Source # div :: Int32 -> Int32 -> Int32 Source # mod :: Int32 -> Int32 -> Int32 Source # quotRem :: Int32 -> Int32 -> (Int32, Int32) Source # divMod :: Int32 -> Int32 -> (Int32, Int32) Source # toInteger :: Int32 -> Integer Source #
Real Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods toRational :: Int32 -> Rational Source #
Show Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods showsPrec :: Int -> Int32 -> ShowS Source # show :: Int32 -> String Source # showList :: [Int32] -> ShowS Source #
Eq Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (==) :: Int32 -> Int32 -> Bool Source # (/=) :: Int32 -> Int32 -> Bool Source #
Ord Int32 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods compare :: Int32 -> Int32 -> Ordering Source # (<) :: Int32 -> Int32 -> Bool Source # (<=) :: Int32 -> Int32 -> Bool Source # (>) :: Int32 -> Int32 -> Bool Source # (>=) :: Int32 -> Int32 -> Bool Source # max :: Int32 -> Int32 -> Int32 Source # min :: Int32 -> Int32 -> Int32 Source #
IArray UArray Int32 |

Instance details

Defined in Data.Array.Base

Methods

bounds :: Ix i => UArray i Int32 -> (i, i) Source #

numElements :: Ix i => UArray i Int32 -> Int Source #

unsafeArray :: Ix i => (i, i) -> [(Int, Int32)] -> UArray i Int32 Source #

unsafeAt :: Ix i => UArray i Int32 -> Int -> Int32 Source #

unsafeReplace :: Ix i => UArray i Int32 -> [(Int, Int32)] -> UArray i Int32 Source #

unsafeAccum :: Ix i => (Int32 -> e' -> Int32) -> UArray i Int32 -> [(Int, e')] -> UArray i Int32 Source #

unsafeAccumArray :: Ix i => (Int32 -> e' -> Int32) -> Int32 -> (i, i) -> [(Int, e')] -> UArray i Int32 Source #

Cast Int16 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int32 Source #
Cast Int32 Int32 Source # | Identity casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int32 Source #
Cast Int32 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int64 Source #
Cast Int8 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int32 Source #
Cast Word16 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word16 -> Stream Int32 Source #
Cast Word8 Int32 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int32 Source #
Cast Bool Int32 Source # | 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 details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int32 Source #
UnsafeCast Int32 Int16 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int16 Source #
UnsafeCast Int32 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int8 Source #
UnsafeCast Int32 Word32 Source # | Signed to unsigned casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Word32 Source #
UnsafeCast Int32 Double Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Double Source #
UnsafeCast Int32 Float Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Float Source #
UnsafeCast Int64 Int32 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int32 Source #
UnsafeCast Word32 Int32 Source # | Cast from unsigned numbers to signed numbers.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word32 -> Stream Int32 Source #
Lift Int32 |
Instance details Defined in Language.Haskell.TH.Syntax Methods lift :: Quote m => Int32 -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Int32 -> Code m Int32 Source #
MArray IOUArray Int32 IO |

Instance details

Defined in Data.Array.IO.Internals

Methods

getBounds :: Ix i => IOUArray i Int32 -> IO (i, i) Source #

getNumElements :: Ix i => IOUArray i Int32 -> IO Int Source #

newArray :: Ix i => (i, i) -> Int32 -> IO (IOUArray i Int32) Source #

newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int32) Source #

unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int32) Source #

unsafeRead :: Ix i => IOUArray i Int32 -> Int -> IO Int32 Source #

unsafeWrite :: Ix i => IOUArray i Int32 -> Int -> Int32 -> IO () Source #

MArray (STUArray s) Int32 (ST s) |

Instance details

Defined in Data.Array.Base

Methods

getBounds :: Ix i => STUArray s i Int32 -> ST s (i, i) Source #

getNumElements :: Ix i => STUArray s i Int32 -> ST s Int Source #

newArray :: Ix i => (i, i) -> Int32 -> ST s (STUArray s i Int32) Source #

newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int32) Source #

unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int32) Source #

unsafeRead :: Ix i => STUArray s i Int32 -> Int -> ST s Int32 Source #

unsafeWrite :: Ix i => STUArray s i Int32 -> Int -> Int32 -> ST s () Source #

data Int64 Source #

64-bit signed integer type

#### Instances

Instances details

PrintfArg Int64 | Since: base-2.1
Instance details Defined in Text.Printf Methods formatArg :: Int64 -> FieldFormatter Source # parseFormat :: Int64 -> ModifierParser Source #
Typed Int64 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int64 Source # simpleType :: Type Int64 -> SimpleType Source #
NFData Int64 |
Instance details Defined in Control.DeepSeq Methods rnf :: Int64 -> () Source #
Bits Int64 | Since: base-2.1

Instance details

Defined in GHC.Internal.Int

Methods

(.&.) :: Int64 -> Int64 -> Int64 Source #

(.|.) :: Int64 -> Int64 -> Int64 Source #

xor :: Int64 -> Int64 -> Int64 Source #

complement :: Int64 -> Int64 Source #

shift :: Int64 -> Int -> Int64 Source #

rotate :: Int64 -> Int -> Int64 Source #

zeroBits :: Int64 Source #

bit :: Int -> Int64 Source #

setBit :: Int64 -> Int -> Int64 Source #

clearBit :: Int64 -> Int -> Int64 Source #

complementBit :: Int64 -> Int -> Int64 Source #

testBit :: Int64 -> Int -> Bool Source #

bitSizeMaybe :: Int64 -> Maybe Int Source #

bitSize :: Int64 -> Int Source #

isSigned :: Int64 -> Bool Source #

shiftL :: Int64 -> Int -> Int64 Source #

unsafeShiftL :: Int64 -> Int -> Int64 Source #

shiftR :: Int64 -> Int -> Int64 Source #

unsafeShiftR :: Int64 -> Int -> Int64 Source #

rotateL :: Int64 -> Int -> Int64 Source #

rotateR :: Int64 -> Int -> Int64 Source #

popCount :: Int64 -> Int Source #

FiniteBits Int64 | Since: base-4.6.0.0
Instance details Defined in GHC.Internal.Int Methods finiteBitSize :: Int64 -> Int Source # countLeadingZeros :: Int64 -> Int Source # countTrailingZeros :: Int64 -> Int Source #
Bounded Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods minBound :: Int64 Source # maxBound :: Int64 Source #
Enum Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods succ :: Int64 -> Int64 Source # pred :: Int64 -> Int64 Source # toEnum :: Int -> Int64 Source # fromEnum :: Int64 -> Int Source # enumFrom :: Int64 -> [Int64] Source # enumFromThen :: Int64 -> Int64 -> [Int64] Source # enumFromTo :: Int64 -> Int64 -> [Int64] Source # enumFromThenTo :: Int64 -> Int64 -> Int64 -> [Int64] Source #
Ix Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods range :: (Int64, Int64) -> [Int64] Source # index :: (Int64, Int64) -> Int64 -> Int Source # unsafeIndex :: (Int64, Int64) -> Int64 -> Int Source # inRange :: (Int64, Int64) -> Int64 -> Bool Source # rangeSize :: (Int64, Int64) -> Int Source # unsafeRangeSize :: (Int64, Int64) -> Int Source #
Num Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (+) :: Int64 -> Int64 -> Int64 Source # (-) :: Int64 -> Int64 -> Int64 Source # (*) :: Int64 -> Int64 -> Int64 Source # negate :: Int64 -> Int64 Source # abs :: Int64 -> Int64 Source # signum :: Int64 -> Int64 Source # fromInteger :: Integer -> Int64 Source #
Read Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods readsPrec :: Int -> ReadS Int64 Source # readList :: ReadS [Int64] Source # readPrec :: ReadPrec Int64 Source # readListPrec :: ReadPrec [Int64] Source #
Integral Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods quot :: Int64 -> Int64 -> Int64 Source # rem :: Int64 -> Int64 -> Int64 Source # div :: Int64 -> Int64 -> Int64 Source # mod :: Int64 -> Int64 -> Int64 Source # quotRem :: Int64 -> Int64 -> (Int64, Int64) Source # divMod :: Int64 -> Int64 -> (Int64, Int64) Source # toInteger :: Int64 -> Integer Source #
Real Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods toRational :: Int64 -> Rational Source #
Show Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods showsPrec :: Int -> Int64 -> ShowS Source # show :: Int64 -> String Source # showList :: [Int64] -> ShowS Source #
Eq Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods (==) :: Int64 -> Int64 -> Bool Source # (/=) :: Int64 -> Int64 -> Bool Source #
Ord Int64 | Since: base-2.1
Instance details Defined in GHC.Internal.Int Methods compare :: Int64 -> Int64 -> Ordering Source # (<) :: Int64 -> Int64 -> Bool Source # (<=) :: Int64 -> Int64 -> Bool Source # (>) :: Int64 -> Int64 -> Bool Source # (>=) :: Int64 -> Int64 -> Bool Source # max :: Int64 -> Int64 -> Int64 Source # min :: Int64 -> Int64 -> Int64 Source #
IArray UArray Int64 |

Instance details

Defined in Data.Array.Base

Methods

bounds :: Ix i => UArray i Int64 -> (i, i) Source #

numElements :: Ix i => UArray i Int64 -> Int Source #

unsafeArray :: Ix i => (i, i) -> [(Int, Int64)] -> UArray i Int64 Source #

unsafeAt :: Ix i => UArray i Int64 -> Int -> Int64 Source #

unsafeReplace :: Ix i => UArray i Int64 -> [(Int, Int64)] -> UArray i Int64 Source #

unsafeAccum :: Ix i => (Int64 -> e' -> Int64) -> UArray i Int64 -> [(Int, e')] -> UArray i Int64 Source #

unsafeAccumArray :: Ix i => (Int64 -> e' -> Int64) -> Int64 -> (i, i) -> [(Int, e')] -> UArray i Int64 Source #

Cast Int16 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int64 Source #
Cast Int32 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int64 Source #
Cast Int64 Int64 Source # | Identity casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int64 -> Stream Int64 Source #
Cast Int8 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int64 Source #
Cast Word16 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word16 -> Stream Int64 Source #
Cast Word32 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word32 -> Stream Int64 Source #
Cast Word8 Int64 Source # | Cast number to bigger type.
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int64 Source #
Cast Bool Int64 Source # | 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 details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int64 Source #
UnsafeCast Int64 Int16 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int16 Source #
UnsafeCast Int64 Int32 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int32 Source #
UnsafeCast Int64 Int8 Source # | Unsafe downcasting to smaller sizes.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int8 Source #
UnsafeCast Int64 Word64 Source # | Signed to unsigned casting.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Word64 Source #
UnsafeCast Int64 Double Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Double Source #
UnsafeCast Int64 Float Source # | Unsafe signed integer promotion to floating point values.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Float Source #
UnsafeCast Word64 Int64 Source # | Cast from unsigned numbers to signed numbers.
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word64 -> Stream Int64 Source #
Lift Int64 |
Instance details Defined in Language.Haskell.TH.Syntax Methods lift :: Quote m => Int64 -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Int64 -> Code m Int64 Source #
MArray IOUArray Int64 IO |

Instance details

Defined in Data.Array.IO.Internals

Methods

getBounds :: Ix i => IOUArray i Int64 -> IO (i, i) Source #

getNumElements :: Ix i => IOUArray i Int64 -> IO Int Source #

newArray :: Ix i => (i, i) -> Int64 -> IO (IOUArray i Int64) Source #

newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int64) Source #

unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int64) Source #

unsafeRead :: Ix i => IOUArray i Int64 -> Int -> IO Int64 Source #

unsafeWrite :: Ix i => IOUArray i Int64 -> Int -> Int64 -> IO () Source #

MArray (STUArray s) Int64 (ST s) |

Instance details

Defined in Data.Array.Base

Methods

getBounds :: Ix i => STUArray s i Int64 -> ST s (i, i) Source #

getNumElements :: Ix i => STUArray s i Int64 -> ST s Int Source #

newArray :: Ix i => (i, i) -> Int64 -> ST s (STUArray s i Int64) Source #

newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int64) Source #

unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int64) Source #

unsafeRead :: Ix i => STUArray s i Int64 -> Int -> ST s Int64 Source #

unsafeWrite :: Ix i => STUArray s i Int64 -> Int -> Int64 -> ST s () Source #

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

typeOf

#### Instances

Instances details

Typed Int16 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int16 Source # simpleType :: Type Int16 -> SimpleType Source #
Typed Int32 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int32 Source # simpleType :: Type Int32 -> SimpleType Source #
Typed Int64 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int64 Source # simpleType :: Type Int64 -> SimpleType Source #
Typed Int8 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 Source # simpleType :: Type Int8 -> SimpleType Source #
Typed Word16 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word16 Source # simpleType :: Type Word16 -> SimpleType Source #
Typed Word32 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word32 Source # simpleType :: Type Word32 -> SimpleType Source #
Typed Word64 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word64 Source # simpleType :: Type Word64 -> SimpleType Source #
Typed Word8 |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word8 Source # simpleType :: Type Word8 -> SimpleType Source #
Typed Bool |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Bool Source # simpleType :: Type Bool -> SimpleType Source #
Typed Double |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Double Source # simpleType :: Type Double -> SimpleType Source #
Typed Float |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Float Source # simpleType :: Type Float -> SimpleType Source #
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type (Array n t) Source # simpleType :: Type (Array n t) -> SimpleType Source #

type Name = String Source #

A name of a trigger, an external variable, or an external function.

module Copilot.Core.Type

module Copilot.Core.Type.Array

badUsage Source #

Arguments

:: String | Description of the error.
-> a |

Report an error due to an error detected by Copilot (e.g., user error).

impossible Source #

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.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] () 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 a 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

Instances details

(Typed a, Bits a) => Bits (Stream a) Source # | Instance of the `Bits` class for `Stream`s. Only the methods `.&.`, `complement`, `.|.` and `xor` are defined.

Instance details

Defined in Copilot.Language.Operators.BitWise

Methods

(.&.) :: Stream a -> Stream a -> Stream a Source #

(.|.) :: Stream a -> Stream a -> Stream a Source #

xor :: Stream a -> Stream a -> Stream a Source #

complement :: Stream a -> Stream a Source #

shift :: Stream a -> Int -> Stream a Source #

rotate :: Stream a -> Int -> Stream a Source #

zeroBits :: Stream a Source #

bit :: Int -> Stream a Source #

setBit :: Stream a -> Int -> Stream a Source #

clearBit :: Stream a -> Int -> Stream a Source #

complementBit :: Stream a -> Int -> Stream a Source #

testBit :: Stream a -> Int -> Bool Source #

bitSizeMaybe :: Stream a -> Maybe Int Source #

bitSize :: Stream a -> Int Source #

isSigned :: Stream a -> Bool Source #

shiftL :: Stream a -> Int -> Stream a Source #

unsafeShiftL :: Stream a -> Int -> Stream a Source #

shiftR :: Stream a -> Int -> Stream a Source #

unsafeShiftR :: Stream a -> Int -> Stream a Source #

rotateL :: Stream a -> Int -> Stream a Source #

rotateR :: Stream a -> Int -> Stream a Source #

popCount :: Stream a -> Int Source #

(Typed a, Eq a, Floating a) => Floating (Stream a) Source # | Streams carrying floating point numbers are instances of `Floating`, and you can apply to them the `Floating` functions, point-wise.

Instance details

Defined in Copilot.Language.Stream

Methods

pi :: Stream a Source #

exp :: Stream a -> Stream a Source #

log :: Stream a -> Stream a Source #

sqrt :: Stream a -> Stream a Source #

(**) :: Stream a -> Stream a -> Stream a Source #

logBase :: Stream a -> Stream a -> Stream a Source #

sin :: Stream a -> Stream a Source #

cos :: Stream a -> Stream a Source #

tan :: Stream a -> Stream a Source #

asin :: Stream a -> Stream a Source #

acos :: Stream a -> Stream a Source #

atan :: Stream a -> Stream a Source #

sinh :: Stream a -> Stream a Source #

cosh :: Stream a -> Stream a Source #

tanh :: Stream a -> Stream a Source #

asinh :: Stream a -> Stream a Source #

acosh :: Stream a -> Stream a Source #

atanh :: Stream a -> Stream a Source #

log1p :: Stream a -> Stream a Source #

expm1 :: Stream a -> Stream a Source #

log1pexp :: Stream a -> Stream a Source #

log1mexp :: Stream a -> Stream a Source #

(Typed a, Eq a, Num a) => Num (Stream a) Source # | Streams carrying numbers are instances of `Num`, and you can apply to them the `Num` functions, point-wise.
Instance details Defined in Copilot.Language.Stream Methods (+) :: Stream a -> Stream a -> Stream a Source # (-) :: Stream a -> Stream a -> Stream a Source # (*) :: Stream a -> Stream a -> Stream a Source # negate :: Stream a -> Stream a Source # abs :: Stream a -> Stream a Source # signum :: Stream a -> Stream a Source # fromInteger :: Integer -> Stream a Source #
(Typed a, Eq a, Fractional a) => Fractional (Stream a) Source # | Streams carrying fractional numbers are instances of `Fractional`, and you can apply to them the `Fractional` functions, point-wise.
Instance details Defined in Copilot.Language.Stream Methods (/) :: Stream a -> Stream a -> Stream a Source # recip :: Stream a -> Stream a Source # fromRational :: Rational -> Stream a Source #
Show (Stream a) Source # | Dummy instance in order to make `Stream` an instance of `Num`.
Instance details Defined in Copilot.Language.Stream Methods showsPrec :: Int -> Stream a -> ShowS Source # show :: Stream a -> String Source # showList :: [Stream a] -> ShowS Source #
Eq (Stream a) Source # | Dummy instance in order to make `Stream` an instance of `Num`.
Instance details Defined in Copilot.Language.Stream Methods (==) :: Stream a -> Stream a -> Bool Source # (/=) :: Stream a -> Stream a -> Bool Source #
(KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t Source # | Update a stream of arrays.

Instance details

Defined in Copilot.Language.Operators.Array

Associated Types

data Projection (Array n t) (Stream Word32) t |
Instance details Defined in Copilot.Language.Operators.Array data Projection (Array n t) (Stream Word32) t = ProjectionA (Stream (Array n t)) (Stream Word32)

Methods

(=:) :: Projection (Array n t) (Stream Word32) t -> Stream t -> Stream (Array n t) Source #

(=$) :: Projection (Array n t) (Stream Word32) t -> (Stream t -> Stream t) -> Stream (Array n t) Source #

data Projection (Array n t) (Stream Word32) t Source # |
Instance details Defined in Copilot.Language.Operators.Array data Projection (Array n t) (Stream Word32) t = ProjectionA (Stream (Array n t)) (Stream Word32)

observer Source #

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.

trigger Source #

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.

exists :: Stream Bool -> Prop Existential Source #

Existential quantification of boolean streams over time.