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
type Name = String
class (Show a, Typeable a) => Typed a
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
exists :: Stream Bool -> Prop Existential

Documentation

data Int8 #

8-bit signed integer type

Instances

Instances details

Bits Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods (.&.) :: Int8 -> Int8 -> Int8 # (.\|.) :: Int8 -> Int8 -> Int8 # xor :: Int8 -> Int8 -> Int8 # complement :: Int8 -> Int8 # shift :: Int8 -> Int -> Int8 # rotate :: Int8 -> Int -> Int8 # zeroBits :: Int8 # bit :: Int -> Int8 # setBit :: Int8 -> Int -> Int8 # clearBit :: Int8 -> Int -> Int8 # complementBit :: Int8 -> Int -> Int8 # testBit :: Int8 -> Int -> Bool # bitSizeMaybe :: Int8 -> Maybe Int # bitSize :: Int8 -> Int # isSigned :: Int8 -> Bool # shiftL :: Int8 -> Int -> Int8 # unsafeShiftL :: Int8 -> Int -> Int8 # shiftR :: Int8 -> Int -> Int8 # unsafeShiftR :: Int8 -> Int -> Int8 # rotateL :: Int8 -> Int -> Int8 # rotateR :: Int8 -> Int -> Int8 # popCount :: Int8 -> Int #
FiniteBits Int8	Since: base-4.6.0.0
Instance details Defined in GHC.Int Methods finiteBitSize :: Int8 -> Int # countLeadingZeros :: Int8 -> Int # countTrailingZeros :: Int8 -> Int #
Bounded Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods minBound :: Int8 # maxBound :: Int8 #
Enum Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods succ :: Int8 -> Int8 # pred :: Int8 -> Int8 # toEnum :: Int -> Int8 # fromEnum :: Int8 -> Int # enumFrom :: Int8 -> [Int8] # enumFromThen :: Int8 -> Int8 -> [Int8] # enumFromTo :: Int8 -> Int8 -> [Int8] # enumFromThenTo :: Int8 -> Int8 -> Int8 -> [Int8] #
Ix Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods range :: (Int8, Int8) -> [Int8] # index :: (Int8, Int8) -> Int8 -> Int # unsafeIndex :: (Int8, Int8) -> Int8 -> Int # inRange :: (Int8, Int8) -> Int8 -> Bool # rangeSize :: (Int8, Int8) -> Int # unsafeRangeSize :: (Int8, Int8) -> Int #
Num Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods (+) :: Int8 -> Int8 -> Int8 # (-) :: Int8 -> Int8 -> Int8 # (*) :: Int8 -> Int8 -> Int8 # negate :: Int8 -> Int8 # abs :: Int8 -> Int8 # signum :: Int8 -> Int8 # fromInteger :: Integer -> Int8 #
Read Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods readsPrec :: Int -> ReadS Int8 # readList :: ReadS [Int8] # readPrec :: ReadPrec Int8 # readListPrec :: ReadPrec [Int8] #
Integral Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods quot :: Int8 -> Int8 -> Int8 # rem :: Int8 -> Int8 -> Int8 # div :: Int8 -> Int8 -> Int8 # mod :: Int8 -> Int8 -> Int8 # quotRem :: Int8 -> Int8 -> (Int8, Int8) # divMod :: Int8 -> Int8 -> (Int8, Int8) # toInteger :: Int8 -> Integer #
Real Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods toRational :: Int8 -> Rational #
Show Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods showsPrec :: Int -> Int8 -> ShowS # show :: Int8 -> String # showList :: [Int8] -> ShowS #
Typed Int8
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 # simpleType :: Type Int8 -> SimpleType #
NFData Int8
Instance details Defined in Control.DeepSeq Methods rnf :: Int8 -> () #
Eq Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int8 -> Int8 -> Bool # (/=) :: Int8 -> Int8 -> Bool #
Ord Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods compare :: Int8 -> Int8 -> Ordering # (<) :: Int8 -> Int8 -> Bool # (<=) :: Int8 -> Int8 -> Bool # (>) :: Int8 -> Int8 -> Bool # (>=) :: Int8 -> Int8 -> Bool # max :: Int8 -> Int8 -> Int8 # min :: Int8 -> Int8 -> Int8 #
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 # liftTyped :: forall (m :: Type -> Type). Quote m => Int8 -> Code m Int8 #

data Int16 #

16-bit signed integer type

Instances

Instances details

Bits Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods (.&.) :: Int16 -> Int16 -> Int16 # (.\|.) :: Int16 -> Int16 -> Int16 # xor :: Int16 -> Int16 -> Int16 # complement :: Int16 -> Int16 # shift :: Int16 -> Int -> Int16 # rotate :: Int16 -> Int -> Int16 # zeroBits :: Int16 # bit :: Int -> Int16 # setBit :: Int16 -> Int -> Int16 # clearBit :: Int16 -> Int -> Int16 # complementBit :: Int16 -> Int -> Int16 # testBit :: Int16 -> Int -> Bool # bitSizeMaybe :: Int16 -> Maybe Int # bitSize :: Int16 -> Int # isSigned :: Int16 -> Bool # shiftL :: Int16 -> Int -> Int16 # unsafeShiftL :: Int16 -> Int -> Int16 # shiftR :: Int16 -> Int -> Int16 # unsafeShiftR :: Int16 -> Int -> Int16 # rotateL :: Int16 -> Int -> Int16 # rotateR :: Int16 -> Int -> Int16 # popCount :: Int16 -> Int #
FiniteBits Int16	Since: base-4.6.0.0
Instance details Defined in GHC.Int Methods finiteBitSize :: Int16 -> Int # countLeadingZeros :: Int16 -> Int # countTrailingZeros :: Int16 -> Int #
Bounded Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods minBound :: Int16 # maxBound :: Int16 #
Enum Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods succ :: Int16 -> Int16 # pred :: Int16 -> Int16 # toEnum :: Int -> Int16 # fromEnum :: Int16 -> Int # enumFrom :: Int16 -> [Int16] # enumFromThen :: Int16 -> Int16 -> [Int16] # enumFromTo :: Int16 -> Int16 -> [Int16] # enumFromThenTo :: Int16 -> Int16 -> Int16 -> [Int16] #
Ix Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods range :: (Int16, Int16) -> [Int16] # index :: (Int16, Int16) -> Int16 -> Int # unsafeIndex :: (Int16, Int16) -> Int16 -> Int # inRange :: (Int16, Int16) -> Int16 -> Bool # rangeSize :: (Int16, Int16) -> Int # unsafeRangeSize :: (Int16, Int16) -> Int #
Num Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods (+) :: Int16 -> Int16 -> Int16 # (-) :: Int16 -> Int16 -> Int16 # (*) :: Int16 -> Int16 -> Int16 # negate :: Int16 -> Int16 # abs :: Int16 -> Int16 # signum :: Int16 -> Int16 # fromInteger :: Integer -> Int16 #
Read Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods readsPrec :: Int -> ReadS Int16 # readList :: ReadS [Int16] # readPrec :: ReadPrec Int16 # readListPrec :: ReadPrec [Int16] #
Integral Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods quot :: Int16 -> Int16 -> Int16 # rem :: Int16 -> Int16 -> Int16 # div :: Int16 -> Int16 -> Int16 # mod :: Int16 -> Int16 -> Int16 # quotRem :: Int16 -> Int16 -> (Int16, Int16) # divMod :: Int16 -> Int16 -> (Int16, Int16) # toInteger :: Int16 -> Integer #
Real Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods toRational :: Int16 -> Rational #
Show Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods showsPrec :: Int -> Int16 -> ShowS # show :: Int16 -> String # showList :: [Int16] -> ShowS #
Typed Int16
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int16 # simpleType :: Type Int16 -> SimpleType #
NFData Int16
Instance details Defined in Control.DeepSeq Methods rnf :: Int16 -> () #
Eq Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int16 -> Int16 -> Bool # (/=) :: Int16 -> Int16 -> Bool #
Ord Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods compare :: Int16 -> Int16 -> Ordering # (<) :: Int16 -> Int16 -> Bool # (<=) :: Int16 -> Int16 -> Bool # (>) :: Int16 -> Int16 -> Bool # (>=) :: Int16 -> Int16 -> Bool # max :: Int16 -> Int16 -> Int16 # min :: Int16 -> Int16 -> Int16 #
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 # liftTyped :: forall (m :: Type -> Type). Quote m => Int16 -> Code m Int16 #

data Int32 #

32-bit signed integer type

Instances

Instances details

Bits Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods (.&.) :: Int32 -> Int32 -> Int32 # (.\|.) :: Int32 -> Int32 -> Int32 # xor :: Int32 -> Int32 -> Int32 # complement :: Int32 -> Int32 # shift :: Int32 -> Int -> Int32 # rotate :: Int32 -> Int -> Int32 # zeroBits :: Int32 # bit :: Int -> Int32 # setBit :: Int32 -> Int -> Int32 # clearBit :: Int32 -> Int -> Int32 # complementBit :: Int32 -> Int -> Int32 # testBit :: Int32 -> Int -> Bool # bitSizeMaybe :: Int32 -> Maybe Int # bitSize :: Int32 -> Int # isSigned :: Int32 -> Bool # shiftL :: Int32 -> Int -> Int32 # unsafeShiftL :: Int32 -> Int -> Int32 # shiftR :: Int32 -> Int -> Int32 # unsafeShiftR :: Int32 -> Int -> Int32 # rotateL :: Int32 -> Int -> Int32 # rotateR :: Int32 -> Int -> Int32 # popCount :: Int32 -> Int #
FiniteBits Int32	Since: base-4.6.0.0
Instance details Defined in GHC.Int Methods finiteBitSize :: Int32 -> Int # countLeadingZeros :: Int32 -> Int # countTrailingZeros :: Int32 -> Int #
Bounded Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods minBound :: Int32 # maxBound :: Int32 #
Enum Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods succ :: Int32 -> Int32 # pred :: Int32 -> Int32 # toEnum :: Int -> Int32 # fromEnum :: Int32 -> Int # enumFrom :: Int32 -> [Int32] # enumFromThen :: Int32 -> Int32 -> [Int32] # enumFromTo :: Int32 -> Int32 -> [Int32] # enumFromThenTo :: Int32 -> Int32 -> Int32 -> [Int32] #
Ix Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods range :: (Int32, Int32) -> [Int32] # index :: (Int32, Int32) -> Int32 -> Int # unsafeIndex :: (Int32, Int32) -> Int32 -> Int # inRange :: (Int32, Int32) -> Int32 -> Bool # rangeSize :: (Int32, Int32) -> Int # unsafeRangeSize :: (Int32, Int32) -> Int #
Num Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods (+) :: Int32 -> Int32 -> Int32 # (-) :: Int32 -> Int32 -> Int32 # (*) :: Int32 -> Int32 -> Int32 # negate :: Int32 -> Int32 # abs :: Int32 -> Int32 # signum :: Int32 -> Int32 # fromInteger :: Integer -> Int32 #
Read Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods readsPrec :: Int -> ReadS Int32 # readList :: ReadS [Int32] # readPrec :: ReadPrec Int32 # readListPrec :: ReadPrec [Int32] #
Integral Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods quot :: Int32 -> Int32 -> Int32 # rem :: Int32 -> Int32 -> Int32 # div :: Int32 -> Int32 -> Int32 # mod :: Int32 -> Int32 -> Int32 # quotRem :: Int32 -> Int32 -> (Int32, Int32) # divMod :: Int32 -> Int32 -> (Int32, Int32) # toInteger :: Int32 -> Integer #
Real Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods toRational :: Int32 -> Rational #
Show Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods showsPrec :: Int -> Int32 -> ShowS # show :: Int32 -> String # showList :: [Int32] -> ShowS #
Typed Int32
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int32 # simpleType :: Type Int32 -> SimpleType #
NFData Int32
Instance details Defined in Control.DeepSeq Methods rnf :: Int32 -> () #
Eq Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int32 -> Int32 -> Bool # (/=) :: Int32 -> Int32 -> Bool #
Ord Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods compare :: Int32 -> Int32 -> Ordering # (<) :: Int32 -> Int32 -> Bool # (<=) :: Int32 -> Int32 -> Bool # (>) :: Int32 -> Int32 -> Bool # (>=) :: Int32 -> Int32 -> Bool # max :: Int32 -> Int32 -> Int32 # min :: Int32 -> Int32 -> Int32 #
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 # liftTyped :: forall (m :: Type -> Type). Quote m => Int32 -> Code m Int32 #

data Int64 #

64-bit signed integer type

Instances

Instances details

Bits Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods (.&.) :: Int64 -> Int64 -> Int64 # (.\|.) :: Int64 -> Int64 -> Int64 # xor :: Int64 -> Int64 -> Int64 # complement :: Int64 -> Int64 # shift :: Int64 -> Int -> Int64 # rotate :: Int64 -> Int -> Int64 # zeroBits :: Int64 # bit :: Int -> Int64 # setBit :: Int64 -> Int -> Int64 # clearBit :: Int64 -> Int -> Int64 # complementBit :: Int64 -> Int -> Int64 # testBit :: Int64 -> Int -> Bool # bitSizeMaybe :: Int64 -> Maybe Int # bitSize :: Int64 -> Int # isSigned :: Int64 -> Bool # shiftL :: Int64 -> Int -> Int64 # unsafeShiftL :: Int64 -> Int -> Int64 # shiftR :: Int64 -> Int -> Int64 # unsafeShiftR :: Int64 -> Int -> Int64 # rotateL :: Int64 -> Int -> Int64 # rotateR :: Int64 -> Int -> Int64 # popCount :: Int64 -> Int #
FiniteBits Int64	Since: base-4.6.0.0
Instance details Defined in GHC.Int Methods finiteBitSize :: Int64 -> Int # countLeadingZeros :: Int64 -> Int # countTrailingZeros :: Int64 -> Int #
Bounded Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods minBound :: Int64 # maxBound :: Int64 #
Enum Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods succ :: Int64 -> Int64 # pred :: Int64 -> Int64 # toEnum :: Int -> Int64 # fromEnum :: Int64 -> Int # enumFrom :: Int64 -> [Int64] # enumFromThen :: Int64 -> Int64 -> [Int64] # enumFromTo :: Int64 -> Int64 -> [Int64] # enumFromThenTo :: Int64 -> Int64 -> Int64 -> [Int64] #
Ix Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods range :: (Int64, Int64) -> [Int64] # index :: (Int64, Int64) -> Int64 -> Int # unsafeIndex :: (Int64, Int64) -> Int64 -> Int # inRange :: (Int64, Int64) -> Int64 -> Bool # rangeSize :: (Int64, Int64) -> Int # unsafeRangeSize :: (Int64, Int64) -> Int #
Num Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods (+) :: Int64 -> Int64 -> Int64 # (-) :: Int64 -> Int64 -> Int64 # (*) :: Int64 -> Int64 -> Int64 # negate :: Int64 -> Int64 # abs :: Int64 -> Int64 # signum :: Int64 -> Int64 # fromInteger :: Integer -> Int64 #
Read Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods readsPrec :: Int -> ReadS Int64 # readList :: ReadS [Int64] # readPrec :: ReadPrec Int64 # readListPrec :: ReadPrec [Int64] #
Integral Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods quot :: Int64 -> Int64 -> Int64 # rem :: Int64 -> Int64 -> Int64 # div :: Int64 -> Int64 -> Int64 # mod :: Int64 -> Int64 -> Int64 # quotRem :: Int64 -> Int64 -> (Int64, Int64) # divMod :: Int64 -> Int64 -> (Int64, Int64) # toInteger :: Int64 -> Integer #
Real Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods toRational :: Int64 -> Rational #
Show Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods showsPrec :: Int -> Int64 -> ShowS # show :: Int64 -> String # showList :: [Int64] -> ShowS #
Typed Int64
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int64 # simpleType :: Type Int64 -> SimpleType #
NFData Int64
Instance details Defined in Control.DeepSeq Methods rnf :: Int64 -> () #
Eq Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int64 -> Int64 -> Bool # (/=) :: Int64 -> Int64 -> Bool #
Ord Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods compare :: Int64 -> Int64 -> Ordering # (<) :: Int64 -> Int64 -> Bool # (<=) :: Int64 -> Int64 -> Bool # (>) :: Int64 -> Int64 -> Bool # (>=) :: Int64 -> Int64 -> Bool # max :: Int64 -> Int64 -> Int64 # min :: Int64 -> Int64 -> Int64 #
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 # liftTyped :: forall (m :: Type -> Type). Quote m => Int64 -> Code m Int64 #

module Data.Word

type Name = String #

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

class (Show a, Typeable a) => Typed a #

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

module Copilot.Core.Type

module Copilot.Core.Type.Array

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.

badUsage Source #

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.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 :: * -> * 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 # (.\|.) :: 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 # zeroBits :: Stream a # bit :: 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 # bitSize :: Stream a -> Int # isSigned :: Stream a -> Bool # 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 # rotateR :: Stream a -> Int -> Stream a # popCount :: Stream a -> Int #
(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 # exp :: Stream a -> Stream a # log :: Stream a -> Stream a # sqrt :: Stream a -> Stream a # (**) :: Stream a -> Stream a -> Stream a # logBase :: Stream a -> Stream a -> Stream a # sin :: Stream a -> Stream a # cos :: Stream a -> Stream a # tan :: 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 # log1p :: Stream a -> Stream a # expm1 :: Stream a -> Stream a # log1pexp :: Stream a -> Stream a # log1mexp :: Stream a -> Stream a #
(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 # (-) :: Stream a -> Stream a -> Stream a # (*) :: Stream a -> Stream a -> Stream a # negate :: Stream a -> Stream a # abs :: Stream a -> Stream a # signum :: Stream a -> Stream a # fromInteger :: Integer -> Stream a #
(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 # recip :: Stream a -> Stream a # fromRational :: Rational -> Stream a #
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 # show :: Stream a -> String # showList :: [Stream a] -> ShowS #
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 # (/=) :: Stream a -> Stream a -> Bool #
(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 Source # 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.

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.