Safe Haskell	Safe
Language	Haskell2010

Copilot.Language

Description

Main Copilot language export file.

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
prettyPrint :: Spec -> IO ()

Documentation

data Int8 #

8-bit signed integer type

Instances

Instances details

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] #
Eq Int8	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int8 -> Int8 -> Bool # (/=) :: Int8 -> Int8 -> Bool #
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 #
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 #
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 #
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] #
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 #
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 #
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 #
Typed Int8
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 # simpleType :: Type Int8 -> SimpleType #
UnsafeCast Int8 Double Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Double Source #
UnsafeCast Int8 Float Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Float Source #
UnsafeCast Int8 Word8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int8 -> Stream Word8 Source #
UnsafeCast Int16 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Int8 Source #
UnsafeCast Int32 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int8 Source #
UnsafeCast Int64 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int8 Source #
UnsafeCast Word8 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word8 -> Stream Int8 Source #
Cast Bool Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int8 Source #
Cast Int8 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int8 Source #
Cast Int8 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int16 Source #
Cast Int8 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int32 Source #
Cast Int8 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int64 Source #

data Int16 #

16-bit signed integer type

Instances

Instances details

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] #
Eq Int16	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int16 -> Int16 -> Bool # (/=) :: Int16 -> Int16 -> Bool #
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 #
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 #
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 #
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] #
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 #
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 #
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 #
Typed Int16
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int16 # simpleType :: Type Int16 -> SimpleType #
UnsafeCast Int16 Double Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Double Source #
UnsafeCast Int16 Float Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Float Source #
UnsafeCast Int16 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Int8 Source #
UnsafeCast Int16 Word16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int16 -> Stream Word16 Source #
UnsafeCast Int32 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int16 Source #
UnsafeCast Int64 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int16 Source #
UnsafeCast Word16 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word16 -> Stream Int16 Source #
Cast Bool Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int16 Source #
Cast Int8 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int16 Source #
Cast Int16 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int16 Source #
Cast Int16 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int32 Source #
Cast Int16 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int64 Source #
Cast Word8 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int16 Source #

data Int32 #

32-bit signed integer type

Instances

Instances details

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] #
Eq Int32	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int32 -> Int32 -> Bool # (/=) :: Int32 -> Int32 -> Bool #
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 #
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 #
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 #
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] #
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 #
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 #
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 #
Typed Int32
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int32 # simpleType :: Type Int32 -> SimpleType #
UnsafeCast Int32 Double Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Double Source #
UnsafeCast Int32 Float Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Float Source #
UnsafeCast Int32 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int8 Source #
UnsafeCast Int32 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Int16 Source #
UnsafeCast Int32 Word32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int32 -> Stream Word32 Source #
UnsafeCast Int64 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int32 Source #
UnsafeCast Word32 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word32 -> Stream Int32 Source #
Cast Bool Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int32 Source #
Cast Int8 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int32 Source #
Cast Int16 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int32 Source #
Cast Int32 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int32 Source #
Cast Int32 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int64 Source #
Cast Word8 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int32 Source #
Cast Word16 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word16 -> Stream Int32 Source #

data Int64 #

64-bit signed integer type

Instances

Instances details

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] #
Eq Int64	Since: base-2.1
Instance details Defined in GHC.Int Methods (==) :: Int64 -> Int64 -> Bool # (/=) :: Int64 -> Int64 -> Bool #
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 #
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 #
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 #
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] #
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 #
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 #
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 #
Typed Int64
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int64 # simpleType :: Type Int64 -> SimpleType #
UnsafeCast Int64 Double Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Double Source #
UnsafeCast Int64 Float Source #	Unsafe unsigned and signed promotion to floating point values
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Float Source #
UnsafeCast Int64 Int8 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int8 Source #
UnsafeCast Int64 Int16 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int16 Source #
UnsafeCast Int64 Int32 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Int32 Source #
UnsafeCast Int64 Word64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Int64 -> Stream Word64 Source #
UnsafeCast Word64 Int64 Source #	Signed to unsigned and vice versa
Instance details Defined in Copilot.Language.Operators.Cast Methods unsafeCast :: Stream Word64 -> Stream Int64 Source #
Cast Bool Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Bool -> Stream Int64 Source #
Cast Int8 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int8 -> Stream Int64 Source #
Cast Int16 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int16 -> Stream Int64 Source #
Cast Int32 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int32 -> Stream Int64 Source #
Cast Int64 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Int64 -> Stream Int64 Source #
Cast Word8 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word8 -> Stream Int64 Source #
Cast Word16 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word16 -> Stream Int64 Source #
Cast Word32 Int64 Source #
Instance details Defined in Copilot.Language.Operators.Cast Methods cast :: Stream Word32 -> Stream Int64 Source #

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 #

Minimal complete definition

typeOf

Instances

Instances details

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 #
Typed Int8
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 # simpleType :: Type Int8 -> SimpleType #
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 Word8
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word8 # simpleType :: Type Word8 -> 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 #
(Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => 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 :: String -> String -> a Source #

badUsage :: String -> a Source #

csv :: Integer -> Spec -> IO () Source #

interpret :: Integer -> Spec -> IO () Source #

Much slower, but pretty-printed interpreter output.

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 #

data Stream :: * -> * Source #

Instances

Instances details

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 #
(Typed a, Eq a, Floating a) => Floating (Stream a) Source #
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, Fractional a) => Fractional (Stream a) Source #
Instance details Defined in Copilot.Language.Stream Methods (/) :: Stream a -> Stream a -> Stream a # recip :: Stream a -> Stream a # fromRational :: Rational -> Stream a #
(Typed a, Eq a, Num a) => Num (Stream a) Source #
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 #
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 #
(Typed a, Bits a) => Bits (Stream a) Source #
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 #

observer :: Typed a => String -> Stream a -> Spec Source #

trigger :: String -> Stream Bool -> [Arg] -> Spec Source #

arg :: Typed a => Stream a -> Arg Source #

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) Source #

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) Source #

forall :: Stream Bool -> Prop Universal Source #

exists :: Stream Bool -> Prop Existential Source #

prettyPrint :: Spec -> IO () Source #