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 Int64
- data Int32
- data Int16
- data Int8
- data Word
- data Word32
- data Word64
- data Word16
- data Word8
- bitReverse16 :: Word16 -> Word16
- bitReverse32 :: Word32 -> Word32
- bitReverse64 :: Word64 -> Word64
- bitReverse8 :: Word8 -> Word8
- byteSwap16 :: Word16 -> Word16
- byteSwap32 :: Word32 -> Word32
- byteSwap64 :: Word64 -> Word64
- type Name = String
- class (Show a, Typeable a) => Typed a
- class (Show a, Typeable a) => Typed a where
- typeOf :: Type a
- simpleType :: Type a -> SimpleType
- data Type a where
- Bool :: Type Bool
- Int8 :: Type Int8
- Int16 :: Type Int16
- Int32 :: Type Int32
- Int64 :: Type Int64
- Word8 :: Type Word8
- Word16 :: Type Word16
- Word32 :: Type Word32
- Word64 :: Type Word64
- Float :: Type Float
- Double :: Type Double
- Array :: forall (n :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t)
- Struct :: forall a. (Typed a, Struct a) => a -> Type a
- class Struct a where
- fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
- data Field (s :: Symbol) t = Field t
- data SimpleType where
- SBool :: SimpleType
- SInt8 :: SimpleType
- SInt16 :: SimpleType
- SInt32 :: SimpleType
- SInt64 :: SimpleType
- SWord8 :: SimpleType
- SWord16 :: SimpleType
- SWord32 :: SimpleType
- SWord64 :: SimpleType
- SFloat :: SimpleType
- SDouble :: SimpleType
- SArray :: forall t. Type t -> SimpleType
- SStruct :: SimpleType
- data UType = Typeable a => UType {}
- data Value a = (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
- accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String
- typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t
- data Array (n :: Nat) t
- arrayElems :: forall (n :: Nat) a. Array n a -> [a]
- arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
- 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 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
Instances
Data Int64 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int64 -> c Int64 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int64 dataTypeOf :: Int64 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int64) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int64) gmapT :: (forall b. Data b => b -> b) -> Int64 -> Int64 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int64 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int64 -> r gmapQ :: (forall d. Data d => d -> u) -> Int64 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Int64 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int64 -> m Int64 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int64 -> m Int64 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int64 -> m Int64 | |
Storable Int64 | |
Defined in Foreign.Storable | |
Bits Int64 | |
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 setBit :: Int64 -> Int -> Int64 clearBit :: Int64 -> Int -> Int64 complementBit :: Int64 -> Int -> Int64 testBit :: Int64 -> Int -> Bool bitSizeMaybe :: Int64 -> Maybe Int shiftL :: Int64 -> Int -> Int64 unsafeShiftL :: Int64 -> Int -> Int64 shiftR :: Int64 -> Int -> Int64 unsafeShiftR :: Int64 -> Int -> Int64 rotateL :: Int64 -> Int -> Int64 | |
FiniteBits Int64 | |
Defined in GHC.Int Methods finiteBitSize :: Int64 -> Int countLeadingZeros :: Int64 -> Int countTrailingZeros :: Int64 -> Int | |
Bounded Int64 | |
Enum Int64 | |
Ix Int64 | |
Num Int64 | |
Read Int64 | |
Integral Int64 | |
Real Int64 | |
Defined in GHC.Int Methods toRational :: Int64 -> Rational # | |
Show Int64 | |
PrintfArg Int64 | |
Defined in Text.Printf | |
Typed Int64 | |
Defined in Copilot.Core.Type | |
NFData Int64 | |
Defined in Control.DeepSeq | |
Eq Int64 | |
Ord Int64 | |
IArray UArray Int64 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Int64 -> (i, i) numElements :: Ix i => UArray i Int64 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Int64)] -> UArray i Int64 unsafeAt :: Ix i => UArray i Int64 -> Int -> Int64 unsafeReplace :: Ix i => UArray i Int64 -> [(Int, Int64)] -> UArray i Int64 unsafeAccum :: Ix i => (Int64 -> e' -> Int64) -> UArray i Int64 -> [(Int, e')] -> UArray i Int64 unsafeAccumArray :: Ix i => (Int64 -> e' -> Int64) -> Int64 -> (i, i) -> [(Int, e')] -> UArray i Int64 | |
Cast Int16 Int64 Source # | Cast number to bigger type. |
Cast Int32 Int64 Source # | Cast number to bigger type. |
Cast Int64 Int64 Source # | Identity casting. |
Cast Int8 Int64 Source # | Cast number to bigger type. |
Cast Word16 Int64 Source # | Cast number to bigger type. |
Cast Word32 Int64 Source # | Cast number to bigger type. |
Cast Word8 Int64 Source # | Cast number to bigger type. |
Cast Bool Int64 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
UnsafeCast Int64 Int16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Int32 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 Int64 Word64 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Double Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Float Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Int64 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
Lift Int64 | |
MArray IOUArray Int64 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Int64 -> IO (i, i) getNumElements :: Ix i => IOUArray i Int64 -> IO Int newArray :: Ix i => (i, i) -> Int64 -> IO (IOUArray i Int64) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int64) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int64) unsafeRead :: Ix i => IOUArray i Int64 -> Int -> IO Int64 unsafeWrite :: Ix i => IOUArray i Int64 -> Int -> Int64 -> IO () | |
MArray (STUArray s) Int64 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Int64 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Int64 -> ST s Int newArray :: Ix i => (i, i) -> Int64 -> ST s (STUArray s i Int64) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int64) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int64) unsafeRead :: Ix i => STUArray s i Int64 -> Int -> ST s Int64 unsafeWrite :: Ix i => STUArray s i Int64 -> Int -> Int64 -> ST s () |
Instances
Data Int32 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int32 -> c Int32 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int32 dataTypeOf :: Int32 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int32) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int32) gmapT :: (forall b. Data b => b -> b) -> Int32 -> Int32 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int32 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int32 -> r gmapQ :: (forall d. Data d => d -> u) -> Int32 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Int32 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int32 -> m Int32 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int32 -> m Int32 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int32 -> m Int32 | |
Storable Int32 | |
Defined in Foreign.Storable | |
Bits Int32 | |
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 setBit :: Int32 -> Int -> Int32 clearBit :: Int32 -> Int -> Int32 complementBit :: Int32 -> Int -> Int32 testBit :: Int32 -> Int -> Bool bitSizeMaybe :: Int32 -> Maybe Int shiftL :: Int32 -> Int -> Int32 unsafeShiftL :: Int32 -> Int -> Int32 shiftR :: Int32 -> Int -> Int32 unsafeShiftR :: Int32 -> Int -> Int32 rotateL :: Int32 -> Int -> Int32 | |
FiniteBits Int32 | |
Defined in GHC.Int Methods finiteBitSize :: Int32 -> Int countLeadingZeros :: Int32 -> Int countTrailingZeros :: Int32 -> Int | |
Bounded Int32 | |
Enum Int32 | |
Ix Int32 | |
Num Int32 | |
Read Int32 | |
Integral Int32 | |
Real Int32 | |
Defined in GHC.Int Methods toRational :: Int32 -> Rational # | |
Show Int32 | |
PrintfArg Int32 | |
Defined in Text.Printf | |
Typed Int32 | |
Defined in Copilot.Core.Type | |
NFData Int32 | |
Defined in Control.DeepSeq | |
Eq Int32 | |
Ord Int32 | |
IArray UArray Int32 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Int32 -> (i, i) numElements :: Ix i => UArray i Int32 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Int32)] -> UArray i Int32 unsafeAt :: Ix i => UArray i Int32 -> Int -> Int32 unsafeReplace :: Ix i => UArray i Int32 -> [(Int, Int32)] -> UArray i Int32 unsafeAccum :: Ix i => (Int32 -> e' -> Int32) -> UArray i Int32 -> [(Int, e')] -> UArray i Int32 unsafeAccumArray :: Ix i => (Int32 -> e' -> Int32) -> Int32 -> (i, i) -> [(Int, e')] -> UArray i Int32 | |
Cast Int16 Int32 Source # | Cast number to bigger type. |
Cast Int32 Int32 Source # | Identity casting. |
Cast Int32 Int64 Source # | Cast number to bigger type. |
Cast Int8 Int32 Source # | Cast number to bigger type. |
Cast Word16 Int32 Source # | Cast number to bigger type. |
Cast Word8 Int32 Source # | Cast number to bigger type. |
Cast Bool Int32 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
UnsafeCast Int32 Int16 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 Int32 Word32 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int32 Double Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int32 Float Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Int32 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word32 Int32 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
Lift Int32 | |
MArray IOUArray Int32 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Int32 -> IO (i, i) getNumElements :: Ix i => IOUArray i Int32 -> IO Int newArray :: Ix i => (i, i) -> Int32 -> IO (IOUArray i Int32) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int32) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int32) unsafeRead :: Ix i => IOUArray i Int32 -> Int -> IO Int32 unsafeWrite :: Ix i => IOUArray i Int32 -> Int -> Int32 -> IO () | |
MArray (STUArray s) Int32 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Int32 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Int32 -> ST s Int newArray :: Ix i => (i, i) -> Int32 -> ST s (STUArray s i Int32) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int32) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int32) unsafeRead :: Ix i => STUArray s i Int32 -> Int -> ST s Int32 unsafeWrite :: Ix i => STUArray s i Int32 -> Int -> Int32 -> ST s () |
Instances
Data Int16 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int16 -> c Int16 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int16 dataTypeOf :: Int16 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int16) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int16) gmapT :: (forall b. Data b => b -> b) -> Int16 -> Int16 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int16 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int16 -> r gmapQ :: (forall d. Data d => d -> u) -> Int16 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Int16 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int16 -> m Int16 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int16 -> m Int16 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int16 -> m Int16 | |
Storable Int16 | |
Defined in Foreign.Storable | |
Bits Int16 | |
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 setBit :: Int16 -> Int -> Int16 clearBit :: Int16 -> Int -> Int16 complementBit :: Int16 -> Int -> Int16 testBit :: Int16 -> Int -> Bool bitSizeMaybe :: Int16 -> Maybe Int shiftL :: Int16 -> Int -> Int16 unsafeShiftL :: Int16 -> Int -> Int16 shiftR :: Int16 -> Int -> Int16 unsafeShiftR :: Int16 -> Int -> Int16 rotateL :: Int16 -> Int -> Int16 | |
FiniteBits Int16 | |
Defined in GHC.Int Methods finiteBitSize :: Int16 -> Int countLeadingZeros :: Int16 -> Int countTrailingZeros :: Int16 -> Int | |
Bounded Int16 | |
Enum Int16 | |
Ix Int16 | |
Num Int16 | |
Read Int16 | |
Integral Int16 | |
Real Int16 | |
Defined in GHC.Int Methods toRational :: Int16 -> Rational # | |
Show Int16 | |
PrintfArg Int16 | |
Defined in Text.Printf | |
Typed Int16 | |
Defined in Copilot.Core.Type | |
NFData Int16 | |
Defined in Control.DeepSeq | |
Eq Int16 | |
Ord Int16 | |
IArray UArray Int16 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Int16 -> (i, i) numElements :: Ix i => UArray i Int16 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Int16)] -> UArray i Int16 unsafeAt :: Ix i => UArray i Int16 -> Int -> Int16 unsafeReplace :: Ix i => UArray i Int16 -> [(Int, Int16)] -> UArray i Int16 unsafeAccum :: Ix i => (Int16 -> e' -> Int16) -> UArray i Int16 -> [(Int, e')] -> UArray i Int16 unsafeAccumArray :: Ix i => (Int16 -> e' -> Int16) -> Int16 -> (i, i) -> [(Int, e')] -> UArray i Int16 | |
Cast Int16 Int16 Source # | Identity casting. |
Cast Int16 Int32 Source # | Cast number to bigger type. |
Cast Int16 Int64 Source # | Cast number to bigger type. |
Cast Int8 Int16 Source # | Cast number to bigger type. |
Cast Word8 Int16 Source # | Cast number to bigger type. |
Cast Bool Int16 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 Int16 Word16 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int16 Double Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int16 Float Source # | Unsafe signed integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int32 Int16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Int64 Int16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Int16 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
Lift Int16 | |
MArray IOUArray Int16 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Int16 -> IO (i, i) getNumElements :: Ix i => IOUArray i Int16 -> IO Int newArray :: Ix i => (i, i) -> Int16 -> IO (IOUArray i Int16) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int16) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int16) unsafeRead :: Ix i => IOUArray i Int16 -> Int -> IO Int16 unsafeWrite :: Ix i => IOUArray i Int16 -> Int -> Int16 -> IO () | |
MArray (STUArray s) Int16 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Int16 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Int16 -> ST s Int newArray :: Ix i => (i, i) -> Int16 -> ST s (STUArray s i Int16) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int16) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int16) unsafeRead :: Ix i => STUArray s i Int16 -> Int -> ST s Int16 unsafeWrite :: Ix i => STUArray s i Int16 -> Int -> Int16 -> ST s () |
Instances
Data Int8 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int8 -> c Int8 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int8 dataTypeOf :: Int8 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int8) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int8) gmapT :: (forall b. Data b => b -> b) -> Int8 -> Int8 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int8 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int8 -> r gmapQ :: (forall d. Data d => d -> u) -> Int8 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Int8 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int8 -> m Int8 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int8 -> m Int8 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int8 -> m Int8 | |
Storable Int8 | |
Defined in Foreign.Storable | |
Bits Int8 | |
Defined in GHC.Int Methods (.&.) :: Int8 -> Int8 -> Int8 # (.|.) :: Int8 -> Int8 -> Int8 # complement :: Int8 -> Int8 # clearBit :: Int8 -> Int -> Int8 complementBit :: Int8 -> Int -> Int8 testBit :: Int8 -> Int -> Bool bitSizeMaybe :: Int8 -> Maybe Int unsafeShiftL :: Int8 -> Int -> Int8 unsafeShiftR :: Int8 -> Int -> Int8 rotateL :: Int8 -> Int -> Int8 | |
FiniteBits Int8 | |
Defined in GHC.Int Methods finiteBitSize :: Int8 -> Int countLeadingZeros :: Int8 -> Int countTrailingZeros :: Int8 -> Int | |
Bounded Int8 | |
Enum Int8 | |
Ix Int8 | |
Num Int8 | |
Read Int8 | |
Integral Int8 | |
Real Int8 | |
Defined in GHC.Int Methods toRational :: Int8 -> Rational # | |
Show Int8 | |
PrintfArg Int8 | |
Defined in Text.Printf | |
Typed Int8 | |
Defined in Copilot.Core.Type | |
NFData Int8 | |
Defined in Control.DeepSeq | |
Eq Int8 | |
Ord Int8 | |
IArray UArray Int8 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Int8 -> (i, i) numElements :: Ix i => UArray i Int8 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Int8)] -> UArray i Int8 unsafeAt :: Ix i => UArray i Int8 -> Int -> Int8 unsafeReplace :: Ix i => UArray i Int8 -> [(Int, Int8)] -> UArray i Int8 unsafeAccum :: Ix i => (Int8 -> e' -> Int8) -> UArray i Int8 -> [(Int, e')] -> UArray i Int8 unsafeAccumArray :: Ix i => (Int8 -> e' -> Int8) -> Int8 -> (i, i) -> [(Int, e')] -> UArray i Int8 | |
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 | |
Lift Int8 | |
MArray IOUArray Int8 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Int8 -> IO (i, i) getNumElements :: Ix i => IOUArray i Int8 -> IO Int newArray :: Ix i => (i, i) -> Int8 -> IO (IOUArray i Int8) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Int8) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Int8) unsafeRead :: Ix i => IOUArray i Int8 -> Int -> IO Int8 unsafeWrite :: Ix i => IOUArray i Int8 -> Int -> Int8 -> IO () | |
MArray (STUArray s) Int8 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Int8 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Int8 -> ST s Int newArray :: Ix i => (i, i) -> Int8 -> ST s (STUArray s i Int8) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int8) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Int8) unsafeRead :: Ix i => STUArray s i Int8 -> Int -> ST s Int8 unsafeWrite :: Ix i => STUArray s i Int8 -> Int -> Int8 -> ST s () |
Instances
Data Word | |||||
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word -> c Word gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word dataTypeOf :: Word -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word) gmapT :: (forall b. Data b => b -> b) -> Word -> Word gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word -> r gmapQ :: (forall d. Data d => d -> u) -> Word -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Word -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word -> m Word gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word -> m Word gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word -> m Word | |||||
Storable Word | |||||
Defined in Foreign.Storable | |||||
Bits Word | |||||
Defined in GHC.Bits Methods (.&.) :: Word -> Word -> Word # (.|.) :: Word -> Word -> Word # complement :: Word -> Word # clearBit :: Word -> Int -> Word complementBit :: Word -> Int -> Word testBit :: Word -> Int -> Bool bitSizeMaybe :: Word -> Maybe Int unsafeShiftL :: Word -> Int -> Word unsafeShiftR :: Word -> Int -> Word rotateL :: Word -> Int -> Word | |||||
FiniteBits Word | |||||
Defined in GHC.Bits Methods finiteBitSize :: Word -> Int countLeadingZeros :: Word -> Int countTrailingZeros :: Word -> Int | |||||
Bounded Word | |||||
Enum Word | |||||
Ix Word | |||||
Num Word | |||||
Read Word | |||||
Integral Word | |||||
Real Word | |||||
Defined in GHC.Real Methods toRational :: Word -> Rational # | |||||
Show Word | |||||
PrintfArg Word | |||||
Defined in Text.Printf | |||||
NFData Word | |||||
Defined in Control.DeepSeq | |||||
Eq Word | |||||
Ord Word | |||||
IArray UArray Word | |||||
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Word -> (i, i) numElements :: Ix i => UArray i Word -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Word)] -> UArray i Word unsafeAt :: Ix i => UArray i Word -> Int -> Word unsafeReplace :: Ix i => UArray i Word -> [(Int, Word)] -> UArray i Word unsafeAccum :: Ix i => (Word -> e' -> Word) -> UArray i Word -> [(Int, e')] -> UArray i Word unsafeAccumArray :: Ix i => (Word -> e' -> Word) -> Word -> (i, i) -> [(Int, e')] -> UArray i Word | |||||
Lift Word | |||||
MArray IOUArray Word IO | |||||
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Word -> IO (i, i) getNumElements :: Ix i => IOUArray i Word -> IO Int newArray :: Ix i => (i, i) -> Word -> IO (IOUArray i Word) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Word) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Word) unsafeRead :: Ix i => IOUArray i Word -> Int -> IO Word unsafeWrite :: Ix i => IOUArray i Word -> Int -> Word -> IO () | |||||
Generic1 (URec Word :: k -> Type) | |||||
Defined in GHC.Generics Associated Types
| |||||
Foldable (UWord :: Type -> Type) | |||||
Defined in Data.Foldable Methods fold :: Monoid m => UWord m -> m foldMap :: Monoid m => (a -> m) -> UWord a -> m # foldMap' :: Monoid m => (a -> m) -> UWord a -> m foldr :: (a -> b -> b) -> b -> UWord a -> b # foldr' :: (a -> b -> b) -> b -> UWord a -> b foldl :: (b -> a -> b) -> b -> UWord a -> b # foldl' :: (b -> a -> b) -> b -> UWord a -> b foldr1 :: (a -> a -> a) -> UWord a -> a # foldl1 :: (a -> a -> a) -> UWord a -> a # toList :: UWord a -> [a] elem :: Eq a => a -> UWord a -> Bool # maximum :: Ord a => UWord a -> a # | |||||
Traversable (UWord :: Type -> Type) | |||||
Defined in Data.Traversable | |||||
MArray (STUArray s) Word (ST s) | |||||
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Word -> ST s (i, i) getNumElements :: Ix i => STUArray s i Word -> ST s Int newArray :: Ix i => (i, i) -> Word -> ST s (STUArray s i Word) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word) unsafeRead :: Ix i => STUArray s i Word -> Int -> ST s Word unsafeWrite :: Ix i => STUArray s i Word -> Int -> Word -> ST s () | |||||
Functor (URec Word :: Type -> Type) | |||||
Generic (URec Word p) | |||||
Defined in GHC.Generics Associated Types
| |||||
Show (URec Word p) | |||||
Eq (URec Word p) | |||||
Ord (URec Word p) | |||||
data URec Word (p :: k) | |||||
Defined in GHC.Generics | |||||
type Rep1 (URec Word :: k -> Type) | |||||
Defined in GHC.Generics | |||||
type Rep (URec Word p) | |||||
Defined in GHC.Generics |
Instances
Data Word32 | |||||
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word32 -> c Word32 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word32 dataTypeOf :: Word32 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word32) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word32) gmapT :: (forall b. Data b => b -> b) -> Word32 -> Word32 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word32 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word32 -> r gmapQ :: (forall d. Data d => d -> u) -> Word32 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Word32 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word32 -> m Word32 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word32 -> m Word32 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word32 -> m Word32 | |||||
Storable Word32 | |||||
Defined in Foreign.Storable | |||||
Bits Word32 | |||||
Defined in GHC.Word Methods (.&.) :: Word32 -> Word32 -> Word32 # (.|.) :: Word32 -> Word32 -> Word32 # xor :: Word32 -> Word32 -> Word32 complement :: Word32 -> Word32 # shift :: Word32 -> Int -> Word32 rotate :: Word32 -> Int -> Word32 setBit :: Word32 -> Int -> Word32 clearBit :: Word32 -> Int -> Word32 complementBit :: Word32 -> Int -> Word32 testBit :: Word32 -> Int -> Bool bitSizeMaybe :: Word32 -> Maybe Int shiftL :: Word32 -> Int -> Word32 unsafeShiftL :: Word32 -> Int -> Word32 shiftR :: Word32 -> Int -> Word32 unsafeShiftR :: Word32 -> Int -> Word32 rotateL :: Word32 -> Int -> Word32 | |||||
FiniteBits Word32 | |||||
Defined in GHC.Word Methods finiteBitSize :: Word32 -> Int countLeadingZeros :: Word32 -> Int countTrailingZeros :: Word32 -> Int | |||||
Bounded Word32 | |||||
Enum Word32 | |||||
Defined in GHC.Word | |||||
Ix Word32 | |||||
Num Word32 | |||||
Read Word32 | |||||
Integral Word32 | |||||
Real Word32 | |||||
Defined in GHC.Word Methods toRational :: Word32 -> Rational # | |||||
Show Word32 | |||||
PrintfArg Word32 | |||||
Defined in Text.Printf | |||||
Typed Word32 | |||||
Defined in Copilot.Core.Type | |||||
NFData Word32 | |||||
Defined in Control.DeepSeq | |||||
Eq Word32 | |||||
Ord Word32 | |||||
IArray UArray Word32 | |||||
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Word32 -> (i, i) numElements :: Ix i => UArray i Word32 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Word32)] -> UArray i Word32 unsafeAt :: Ix i => UArray i Word32 -> Int -> Word32 unsafeReplace :: Ix i => UArray i Word32 -> [(Int, Word32)] -> UArray i Word32 unsafeAccum :: Ix i => (Word32 -> e' -> Word32) -> UArray i Word32 -> [(Int, e')] -> UArray i Word32 unsafeAccumArray :: Ix i => (Word32 -> e' -> Word32) -> Word32 -> (i, i) -> [(Int, e')] -> UArray i Word32 | |||||
Cast Word16 Word32 Source # | Cast number to bigger type. | ||||
Cast Word32 Int64 Source # | Cast number to bigger type. | ||||
Cast Word32 Word32 Source # | Identity casting. | ||||
Cast Word32 Word64 Source # | Cast number to bigger type. | ||||
Cast Word8 Word32 Source # | Cast number to bigger type. | ||||
Cast Bool Word32 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is | ||||
UnsafeCast Int32 Word32 Source # | Signed to unsigned casting. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word32 Int32 Source # | Cast from unsigned numbers to signed numbers. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word32 Word16 Source # | Unsafe downcasting to smaller sizes. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word32 Word8 Source # | Unsafe downcasting to smaller sizes. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word32 Double Source # | Unsafe unsigned integer promotion to floating point values. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word32 Float Source # | Unsafe unsigned integer promotion to floating point values. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
UnsafeCast Word64 Word32 Source # | Unsafe downcasting to smaller sizes. | ||||
Defined in Copilot.Language.Operators.Cast | |||||
Lift Word32 | |||||
MArray IOUArray Word32 IO | |||||
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Word32 -> IO (i, i) getNumElements :: Ix i => IOUArray i Word32 -> IO Int newArray :: Ix i => (i, i) -> Word32 -> IO (IOUArray i Word32) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Word32) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Word32) unsafeRead :: Ix i => IOUArray i Word32 -> Int -> IO Word32 unsafeWrite :: Ix i => IOUArray i Word32 -> Int -> Word32 -> IO () | |||||
MArray (STUArray s) Word32 (ST s) | |||||
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Word32 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Word32 -> ST s Int newArray :: Ix i => (i, i) -> Word32 -> ST s (STUArray s i Word32) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word32) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word32) unsafeRead :: Ix i => STUArray s i Word32 -> Int -> ST s Word32 unsafeWrite :: Ix i => STUArray s i Word32 -> Int -> Word32 -> ST s () | |||||
(KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t Source # | Update a stream of arrays. | ||||
Defined in Copilot.Language.Operators.Array Associated Types
| |||||
data Projection (Array n t) (Stream Word32) t Source # | |||||
Defined in Copilot.Language.Operators.Array |
Instances
Data Word64 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word64 -> c Word64 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word64 dataTypeOf :: Word64 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word64) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word64) gmapT :: (forall b. Data b => b -> b) -> Word64 -> Word64 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word64 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word64 -> r gmapQ :: (forall d. Data d => d -> u) -> Word64 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Word64 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word64 -> m Word64 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word64 -> m Word64 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word64 -> m Word64 | |
Storable Word64 | |
Defined in Foreign.Storable | |
Bits Word64 | |
Defined in GHC.Word Methods (.&.) :: Word64 -> Word64 -> Word64 # (.|.) :: Word64 -> Word64 -> Word64 # xor :: Word64 -> Word64 -> Word64 complement :: Word64 -> Word64 # shift :: Word64 -> Int -> Word64 rotate :: Word64 -> Int -> Word64 setBit :: Word64 -> Int -> Word64 clearBit :: Word64 -> Int -> Word64 complementBit :: Word64 -> Int -> Word64 testBit :: Word64 -> Int -> Bool bitSizeMaybe :: Word64 -> Maybe Int shiftL :: Word64 -> Int -> Word64 unsafeShiftL :: Word64 -> Int -> Word64 shiftR :: Word64 -> Int -> Word64 unsafeShiftR :: Word64 -> Int -> Word64 rotateL :: Word64 -> Int -> Word64 | |
FiniteBits Word64 | |
Defined in GHC.Word Methods finiteBitSize :: Word64 -> Int countLeadingZeros :: Word64 -> Int countTrailingZeros :: Word64 -> Int | |
Bounded Word64 | |
Enum Word64 | |
Defined in GHC.Word | |
Ix Word64 | |
Num Word64 | |
Read Word64 | |
Integral Word64 | |
Real Word64 | |
Defined in GHC.Word Methods toRational :: Word64 -> Rational # | |
Show Word64 | |
PrintfArg Word64 | |
Defined in Text.Printf | |
Typed Word64 | |
Defined in Copilot.Core.Type | |
NFData Word64 | |
Defined in Control.DeepSeq | |
Eq Word64 | |
Ord Word64 | |
IArray UArray Word64 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Word64 -> (i, i) numElements :: Ix i => UArray i Word64 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Word64)] -> UArray i Word64 unsafeAt :: Ix i => UArray i Word64 -> Int -> Word64 unsafeReplace :: Ix i => UArray i Word64 -> [(Int, Word64)] -> UArray i Word64 unsafeAccum :: Ix i => (Word64 -> e' -> Word64) -> UArray i Word64 -> [(Int, e')] -> UArray i Word64 unsafeAccumArray :: Ix i => (Word64 -> e' -> Word64) -> Word64 -> (i, i) -> [(Int, e')] -> UArray i Word64 | |
Cast Word16 Word64 Source # | Cast number to bigger type. |
Cast Word32 Word64 Source # | Cast number to bigger type. |
Cast Word64 Word64 Source # | Identity casting. |
Cast Word8 Word64 Source # | Cast number to bigger type. |
Cast Bool Word64 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
UnsafeCast Int64 Word64 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Int64 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Word16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Word32 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Word8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Double Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Float Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
Lift Word64 | |
MArray IOUArray Word64 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Word64 -> IO (i, i) getNumElements :: Ix i => IOUArray i Word64 -> IO Int newArray :: Ix i => (i, i) -> Word64 -> IO (IOUArray i Word64) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Word64) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Word64) unsafeRead :: Ix i => IOUArray i Word64 -> Int -> IO Word64 unsafeWrite :: Ix i => IOUArray i Word64 -> Int -> Word64 -> IO () | |
MArray (STUArray s) Word64 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Word64 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Word64 -> ST s Int newArray :: Ix i => (i, i) -> Word64 -> ST s (STUArray s i Word64) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word64) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word64) unsafeRead :: Ix i => STUArray s i Word64 -> Int -> ST s Word64 unsafeWrite :: Ix i => STUArray s i Word64 -> Int -> Word64 -> ST s () |
Instances
Data Word16 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word16 -> c Word16 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word16 dataTypeOf :: Word16 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word16) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word16) gmapT :: (forall b. Data b => b -> b) -> Word16 -> Word16 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word16 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word16 -> r gmapQ :: (forall d. Data d => d -> u) -> Word16 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Word16 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word16 -> m Word16 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word16 -> m Word16 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word16 -> m Word16 | |
Storable Word16 | |
Defined in Foreign.Storable | |
Bits Word16 | |
Defined in GHC.Word Methods (.&.) :: Word16 -> Word16 -> Word16 # (.|.) :: Word16 -> Word16 -> Word16 # xor :: Word16 -> Word16 -> Word16 complement :: Word16 -> Word16 # shift :: Word16 -> Int -> Word16 rotate :: Word16 -> Int -> Word16 setBit :: Word16 -> Int -> Word16 clearBit :: Word16 -> Int -> Word16 complementBit :: Word16 -> Int -> Word16 testBit :: Word16 -> Int -> Bool bitSizeMaybe :: Word16 -> Maybe Int shiftL :: Word16 -> Int -> Word16 unsafeShiftL :: Word16 -> Int -> Word16 shiftR :: Word16 -> Int -> Word16 unsafeShiftR :: Word16 -> Int -> Word16 rotateL :: Word16 -> Int -> Word16 | |
FiniteBits Word16 | |
Defined in GHC.Word Methods finiteBitSize :: Word16 -> Int countLeadingZeros :: Word16 -> Int countTrailingZeros :: Word16 -> Int | |
Bounded Word16 | |
Enum Word16 | |
Defined in GHC.Word | |
Ix Word16 | |
Num Word16 | |
Read Word16 | |
Integral Word16 | |
Real Word16 | |
Defined in GHC.Word Methods toRational :: Word16 -> Rational # | |
Show Word16 | |
PrintfArg Word16 | |
Defined in Text.Printf | |
Typed Word16 | |
Defined in Copilot.Core.Type | |
NFData Word16 | |
Defined in Control.DeepSeq | |
Eq Word16 | |
Ord Word16 | |
IArray UArray Word16 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Word16 -> (i, i) numElements :: Ix i => UArray i Word16 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Word16)] -> UArray i Word16 unsafeAt :: Ix i => UArray i Word16 -> Int -> Word16 unsafeReplace :: Ix i => UArray i Word16 -> [(Int, Word16)] -> UArray i Word16 unsafeAccum :: Ix i => (Word16 -> e' -> Word16) -> UArray i Word16 -> [(Int, e')] -> UArray i Word16 unsafeAccumArray :: Ix i => (Word16 -> e' -> Word16) -> Word16 -> (i, i) -> [(Int, e')] -> UArray i Word16 | |
Cast Word16 Int32 Source # | Cast number to bigger type. |
Cast Word16 Int64 Source # | Cast number to bigger type. |
Cast Word16 Word16 Source # | Identity casting. |
Cast Word16 Word32 Source # | Cast number to bigger type. |
Cast Word16 Word64 Source # | Cast number to bigger type. |
Cast Word8 Word16 Source # | Cast number to bigger type. |
Cast Bool Word16 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
UnsafeCast Int16 Word16 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Int16 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Word8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Double Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Float Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word32 Word16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Word16 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
Lift Word16 | |
MArray IOUArray Word16 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Word16 -> IO (i, i) getNumElements :: Ix i => IOUArray i Word16 -> IO Int newArray :: Ix i => (i, i) -> Word16 -> IO (IOUArray i Word16) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Word16) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Word16) unsafeRead :: Ix i => IOUArray i Word16 -> Int -> IO Word16 unsafeWrite :: Ix i => IOUArray i Word16 -> Int -> Word16 -> IO () | |
MArray (STUArray s) Word16 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Word16 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Word16 -> ST s Int newArray :: Ix i => (i, i) -> Word16 -> ST s (STUArray s i Word16) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word16) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word16) unsafeRead :: Ix i => STUArray s i Word16 -> Int -> ST s Word16 unsafeWrite :: Ix i => STUArray s i Word16 -> Int -> Word16 -> ST s () |
Instances
Data Word8 | |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word8 -> c Word8 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word8 dataTypeOf :: Word8 -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word8) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word8) gmapT :: (forall b. Data b => b -> b) -> Word8 -> Word8 gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word8 -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word8 -> r gmapQ :: (forall d. Data d => d -> u) -> Word8 -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Word8 -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word8 -> m Word8 gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word8 -> m Word8 gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word8 -> m Word8 | |
Storable Word8 | |
Defined in Foreign.Storable | |
Bits Word8 | |
Defined in GHC.Word Methods (.&.) :: Word8 -> Word8 -> Word8 # (.|.) :: Word8 -> Word8 -> Word8 # xor :: Word8 -> Word8 -> Word8 complement :: Word8 -> Word8 # shift :: Word8 -> Int -> Word8 rotate :: Word8 -> Int -> Word8 setBit :: Word8 -> Int -> Word8 clearBit :: Word8 -> Int -> Word8 complementBit :: Word8 -> Int -> Word8 testBit :: Word8 -> Int -> Bool bitSizeMaybe :: Word8 -> Maybe Int shiftL :: Word8 -> Int -> Word8 unsafeShiftL :: Word8 -> Int -> Word8 shiftR :: Word8 -> Int -> Word8 unsafeShiftR :: Word8 -> Int -> Word8 rotateL :: Word8 -> Int -> Word8 | |
FiniteBits Word8 | |
Defined in GHC.Word Methods finiteBitSize :: Word8 -> Int countLeadingZeros :: Word8 -> Int countTrailingZeros :: Word8 -> Int | |
Bounded Word8 | |
Enum Word8 | |
Ix Word8 | |
Num Word8 | |
Read Word8 | |
Integral Word8 | |
Real Word8 | |
Defined in GHC.Word Methods toRational :: Word8 -> Rational # | |
Show Word8 | |
PrintfArg Word8 | |
Defined in Text.Printf | |
Typed Word8 | |
Defined in Copilot.Core.Type | |
NFData Word8 | |
Defined in Control.DeepSeq | |
Eq Word8 | |
Ord Word8 | |
IArray UArray Word8 | |
Defined in Data.Array.Base Methods bounds :: Ix i => UArray i Word8 -> (i, i) numElements :: Ix i => UArray i Word8 -> Int unsafeArray :: Ix i => (i, i) -> [(Int, Word8)] -> UArray i Word8 unsafeAt :: Ix i => UArray i Word8 -> Int -> Word8 unsafeReplace :: Ix i => UArray i Word8 -> [(Int, Word8)] -> UArray i Word8 unsafeAccum :: Ix i => (Word8 -> e' -> Word8) -> UArray i Word8 -> [(Int, e')] -> UArray i Word8 unsafeAccumArray :: Ix i => (Word8 -> e' -> Word8) -> Word8 -> (i, i) -> [(Int, e')] -> UArray i Word8 | |
Cast Word8 Int16 Source # | Cast number to bigger type. |
Cast Word8 Int32 Source # | Cast number to bigger type. |
Cast Word8 Int64 Source # | Cast number to bigger type. |
Cast Word8 Word16 Source # | Cast number to bigger type. |
Cast Word8 Word32 Source # | Cast number to bigger type. |
Cast Word8 Word64 Source # | Cast number to bigger type. |
Cast Word8 Word8 Source # | Identity casting. |
Cast Bool Word8 Source # | Cast a boolean stream to a stream of numbers, producing 1 if the
value at a point in time is |
UnsafeCast Int8 Word8 Source # | Signed to unsigned casting. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word16 Word8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word32 Word8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word64 Word8 Source # | Unsafe downcasting to smaller sizes. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word8 Int8 Source # | Cast from unsigned numbers to signed numbers. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word8 Double Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
UnsafeCast Word8 Float Source # | Unsafe unsigned integer promotion to floating point values. |
Defined in Copilot.Language.Operators.Cast | |
Lift Word8 | |
MArray IOUArray Word8 IO | |
Defined in Data.Array.IO.Internals Methods getBounds :: Ix i => IOUArray i Word8 -> IO (i, i) getNumElements :: Ix i => IOUArray i Word8 -> IO Int newArray :: Ix i => (i, i) -> Word8 -> IO (IOUArray i Word8) newArray_ :: Ix i => (i, i) -> IO (IOUArray i Word8) unsafeNewArray_ :: Ix i => (i, i) -> IO (IOUArray i Word8) unsafeRead :: Ix i => IOUArray i Word8 -> Int -> IO Word8 unsafeWrite :: Ix i => IOUArray i Word8 -> Int -> Word8 -> IO () | |
MArray (STUArray s) Word8 (ST s) | |
Defined in Data.Array.Base Methods getBounds :: Ix i => STUArray s i Word8 -> ST s (i, i) getNumElements :: Ix i => STUArray s i Word8 -> ST s Int newArray :: Ix i => (i, i) -> Word8 -> ST s (STUArray s i Word8) newArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word8) unsafeNewArray_ :: Ix i => (i, i) -> ST s (STUArray s i Word8) unsafeRead :: Ix i => STUArray s i Word8 -> Int -> ST s Word8 unsafeWrite :: Ix i => STUArray s i Word8 -> Int -> Word8 -> ST s () |
bitReverse16 :: Word16 -> Word16 #
bitReverse32 :: Word32 -> Word32 #
bitReverse64 :: Word64 -> Word64 #
bitReverse8 :: Word8 -> Word8 #
byteSwap16 :: Word16 -> Word16 #
byteSwap32 :: Word32 -> Word32 #
byteSwap64 :: Word64 -> Word64 #
class (Show a, Typeable a) => Typed a #
Minimal complete definition
Instances
Typed Int16 | |
Defined in Copilot.Core.Type | |
Typed Int32 | |
Defined in Copilot.Core.Type | |
Typed Int64 | |
Defined in Copilot.Core.Type | |
Typed Int8 | |
Defined in Copilot.Core.Type | |
Typed Word16 | |
Defined in Copilot.Core.Type | |
Typed Word32 | |
Defined in Copilot.Core.Type | |
Typed Word64 | |
Defined in Copilot.Core.Type | |
Typed Word8 | |
Defined in Copilot.Core.Type | |
Typed Bool | |
Defined in Copilot.Core.Type | |
Typed Double | |
Defined in Copilot.Core.Type | |
Typed Float | |
Defined in Copilot.Core.Type | |
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |
Defined in Copilot.Core.Type |
class (Show a, Typeable a) => Typed a where #
Minimal complete definition
Instances
Typed Int16 | |
Defined in Copilot.Core.Type | |
Typed Int32 | |
Defined in Copilot.Core.Type | |
Typed Int64 | |
Defined in Copilot.Core.Type | |
Typed Int8 | |
Defined in Copilot.Core.Type | |
Typed Word16 | |
Defined in Copilot.Core.Type | |
Typed Word32 | |
Defined in Copilot.Core.Type | |
Typed Word64 | |
Defined in Copilot.Core.Type | |
Typed Word8 | |
Defined in Copilot.Core.Type | |
Typed Bool | |
Defined in Copilot.Core.Type | |
Typed Double | |
Defined in Copilot.Core.Type | |
Typed Float | |
Defined in Copilot.Core.Type | |
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |
Defined in Copilot.Core.Type |
Constructors
Bool :: Type Bool | |
Int8 :: Type Int8 | |
Int16 :: Type Int16 | |
Int32 :: Type Int32 | |
Int64 :: Type Int64 | |
Word8 :: Type Word8 | |
Word16 :: Type Word16 | |
Word32 :: Type Word32 | |
Word64 :: Type Word64 | |
Float :: Type Float | |
Double :: Type Double | |
Array :: forall (n :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t) | |
Struct :: forall a. (Typed a, Struct a) => a -> Type a |
Instances
TestEquality Type | |
Defined in Copilot.Core.Type Methods testEquality :: Type a -> Type b -> Maybe (a :~: b) |
Constructors
Field t |
Instances
(KnownSymbol f, Typed s, Typed t, Struct s) => Projectable s (s -> Field f t) t Source # | Update a stream of structs. | ||||
Defined in Copilot.Language.Operators.Struct Associated Types
| |||||
(KnownSymbol s, Show t) => Show (Field s t) | |||||
data Projection s (s -> Field f t) t Source # | |||||
Defined in Copilot.Language.Operators.Struct |
data SimpleType where #
Constructors
SBool :: SimpleType | |
SInt8 :: SimpleType | |
SInt16 :: SimpleType | |
SInt32 :: SimpleType | |
SInt64 :: SimpleType | |
SWord8 :: SimpleType | |
SWord16 :: SimpleType | |
SWord32 :: SimpleType | |
SWord64 :: SimpleType | |
SFloat :: SimpleType | |
SDouble :: SimpleType | |
SArray :: forall t. Type t -> SimpleType | |
SStruct :: SimpleType |
Instances
Eq SimpleType | |
Defined in Copilot.Core.Type |
accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String #
typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int #
Instances
Show t => Show (Array n t) | |||||
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) | |||||
Defined in Copilot.Core.Type | |||||
(KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t Source # | Update a stream of arrays. | ||||
Defined in Copilot.Language.Operators.Array Associated Types
| |||||
data Projection (Array n t) (Stream Word32) t Source # | |||||
Defined in Copilot.Language.Operators.Array |
arrayElems :: forall (n :: Nat) a. Array n a -> [a] #
arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a #
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]
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
(Typed a, Bits a) => Bits (Stream a) Source # | Instance of the Only the methods | ||||
Defined in Copilot.Language.Operators.BitWise Methods (.&.) :: Stream a -> Stream a -> Stream a # (.|.) :: Stream a -> Stream a -> Stream a # xor :: Stream a -> Stream a -> Stream a complement :: Stream a -> Stream a # shift :: Stream a -> Int -> Stream a rotate :: Stream a -> Int -> Stream a setBit :: Stream a -> Int -> Stream a clearBit :: Stream a -> Int -> Stream a complementBit :: Stream a -> Int -> Stream a testBit :: Stream a -> Int -> Bool bitSizeMaybe :: Stream a -> Maybe Int shiftL :: Stream a -> Int -> Stream a unsafeShiftL :: Stream a -> Int -> Stream a shiftR :: Stream a -> Int -> Stream a unsafeShiftR :: Stream a -> Int -> Stream a rotateL :: Stream a -> Int -> Stream a | |||||
(Typed a, Eq a, Floating a) => Floating (Stream a) Source # | Streams carrying floating point numbers are instances of | ||||
Defined in Copilot.Language.Stream Methods sqrt :: Stream a -> Stream a # (**) :: Stream a -> Stream a -> Stream a # logBase :: Stream a -> Stream a -> Stream a # asin :: Stream a -> Stream a # acos :: Stream a -> Stream a # atan :: Stream a -> Stream a # sinh :: Stream a -> Stream a # cosh :: Stream a -> Stream a # tanh :: Stream a -> Stream a # asinh :: Stream a -> Stream a # acosh :: Stream a -> Stream a # atanh :: Stream a -> Stream a # | |||||
(Typed a, Eq a, Num a) => Num (Stream a) Source # | Streams carrying numbers are instances of | ||||
(Typed a, Eq a, Fractional a) => Fractional (Stream a) Source # | Streams carrying fractional numbers are instances of | ||||
Show (Stream a) Source # | |||||
Eq (Stream a) Source # | |||||
(KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t Source # | Update a stream of arrays. | ||||
Defined in Copilot.Language.Operators.Array Associated Types
| |||||
data Projection (Array n t) (Stream Word32) t Source # | |||||
Defined in Copilot.Language.Operators.Array |
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.