Data.SBV.Examples.Misc.Word4

Demonstrates how new sizes of word/int types can be defined and used with SBV.

Documentation

newtype Word4

Word4 as a newtype. Invariant: Word4 x should satisfy x < 16.

Constructors

Word4 Word8

Instances

Bounded Word4

Bounded instance; from 0 to 255

Methods

minBound :: Word4

maxBound :: Word4

Enum Word4

Enum instance, trivial definitions.

Methods

succ :: Word4 -> Word4

pred :: Word4 -> Word4

toEnum :: Int -> Word4

fromEnum :: Word4 -> Int

enumFrom :: Word4 -> [Word4]

enumFromThen :: Word4 -> Word4 -> [Word4]

enumFromTo :: Word4 -> Word4 -> [Word4]

enumFromThenTo :: Word4 -> Word4 -> Word4 -> [Word4]

Eq Word4

Methods

(==) :: Word4 -> Word4 -> Bool

(/=) :: Word4 -> Word4 -> Bool

Integral Word4

Integral instance, again using Word8 instance and casting. NB. we do not need to use the smart constructor here as neither the quotient nor the remainder can overflow a Word4.

Methods

quot :: Word4 -> Word4 -> Word4

rem :: Word4 -> Word4 -> Word4

div :: Word4 -> Word4 -> Word4

mod :: Word4 -> Word4 -> Word4

quotRem :: Word4 -> Word4 -> (Word4, Word4)

divMod :: Word4 -> Word4 -> (Word4, Word4)

toInteger :: Word4 -> Integer

Data Word4

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word4 -> c Word4

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word4

toConstr :: Word4 -> Constr

dataTypeOf :: Word4 -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Word4)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word4)

gmapT :: (forall b. Data b => b -> b) -> Word4 -> Word4

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word4 -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word4 -> r

gmapQ :: (forall d. Data d => d -> u) -> Word4 -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Word4 -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word4 -> m Word4

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word4 -> m Word4

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word4 -> m Word4

Num Word4

Num instance, merely lifts underlying 8-bit operation and casts back

Methods

(+) :: Word4 -> Word4 -> Word4

(-) :: Word4 -> Word4 -> Word4

(*) :: Word4 -> Word4 -> Word4

negate :: Word4 -> Word4

abs :: Word4 -> Word4

signum :: Word4 -> Word4

fromInteger :: Integer -> Word4

Ord Word4

Methods

compare :: Word4 -> Word4 -> Ordering

(<) :: Word4 -> Word4 -> Bool

(<=) :: Word4 -> Word4 -> Bool

(>) :: Word4 -> Word4 -> Bool

(>=) :: Word4 -> Word4 -> Bool

max :: Word4 -> Word4 -> Word4

min :: Word4 -> Word4 -> Word4

Read Word4

Read instance. We read as an 8-bit word, and coerce

Methods

readsPrec :: Int -> ReadS Word4

readList :: ReadS [Word4]

readPrec :: ReadPrec Word4

readListPrec :: ReadPrec [Word4]

Real Word4

Real instance simply uses the Word8 instance

Methods

toRational :: Word4 -> Rational

Show Word4

Show instance

Methods

showsPrec :: Int -> Word4 -> ShowS

show :: Word4 -> String

showList :: [Word4] -> ShowS

Bits Word4

Bits instance

Methods

(.&.) :: Word4 -> Word4 -> Word4

(.|.) :: Word4 -> Word4 -> Word4

xor :: Word4 -> Word4 -> Word4

complement :: Word4 -> Word4

shift :: Word4 -> Int -> Word4

rotate :: Word4 -> Int -> Word4

zeroBits :: Word4

bit :: Int -> Word4

setBit :: Word4 -> Int -> Word4

clearBit :: Word4 -> Int -> Word4

complementBit :: Word4 -> Int -> Word4

testBit :: Word4 -> Int -> Bool

bitSizeMaybe :: Word4 -> Maybe Int

bitSize :: Word4 -> Int

isSigned :: Word4 -> Bool

shiftL :: Word4 -> Int -> Word4

unsafeShiftL :: Word4 -> Int -> Word4

shiftR :: Word4 -> Int -> Word4

unsafeShiftR :: Word4 -> Int -> Word4

rotateL :: Word4 -> Int -> Word4

rotateR :: Word4 -> Int -> Word4

popCount :: Word4 -> Int

Random Word4

Random instance, used in quick-check

Methods

randomR :: RandomGen g => (Word4, Word4) -> g -> (Word4, g)

random :: RandomGen g => g -> (Word4, g)

randomRs :: RandomGen g => (Word4, Word4) -> g -> [Word4]

randoms :: RandomGen g => g -> [Word4]

randomRIO :: (Word4, Word4) -> IO Word4

randomIO :: IO Word4

HasKind Word4

HasKind instance; simply returning the underlying kind for the type

Methods

kindOf :: Word4 -> Kind

hasSign :: Word4 -> Bool

intSizeOf :: Word4 -> Int

isBoolean :: Word4 -> Bool

isBounded :: Word4 -> Bool

isReal :: Word4 -> Bool

isFloat :: Word4 -> Bool

isDouble :: Word4 -> Bool

isInteger :: Word4 -> Bool

isUninterpreted :: Word4 -> Bool

showType :: Word4 -> String

SymWord Word4

SymWord instance, allowing this type to be used in proofs/sat etc.

Methods

forall :: String -> Symbolic (SBV Word4)

forall_ :: Symbolic (SBV Word4)

mkForallVars :: Int -> Symbolic [SBV Word4]

exists :: String -> Symbolic (SBV Word4)

exists_ :: Symbolic (SBV Word4)

mkExistVars :: Int -> Symbolic [SBV Word4]

free :: String -> Symbolic (SBV Word4)

free_ :: Symbolic (SBV Word4)

mkFreeVars :: Int -> Symbolic [SBV Word4]

symbolic :: String -> Symbolic (SBV Word4)

symbolics :: [String] -> Symbolic [SBV Word4]

literal :: Word4 -> SBV Word4

unliteral :: SBV Word4 -> Maybe Word4

fromCW :: CW -> Word4

isConcrete :: SBV Word4 -> Bool

isSymbolic :: SBV Word4 -> Bool

isConcretely :: SBV Word4 -> (Word4 -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Word4)

SatModel Word4

SatModel instance, merely uses the generic parsing method.

Methods

parseCWs :: [CW] -> Maybe (Word4, [CW])

cvtModel :: (Word4 -> Maybe b) -> Maybe (Word4, [CW]) -> Maybe (b, [CW])

SDivisible SWord4

SDvisible instance, using default methods

Methods

sQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4)

sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4)

sQuot :: SWord4 -> SWord4 -> SWord4

sRem :: SWord4 -> SWord4 -> SWord4

sDiv :: SWord4 -> SWord4 -> SWord4

sMod :: SWord4 -> SWord4 -> SWord4

SDivisible Word4

SDvisible instance, using 0-extension

Methods

sQuotRem :: Word4 -> Word4 -> (Word4, Word4)

sDivMod :: Word4 -> Word4 -> (Word4, Word4)

sQuot :: Word4 -> Word4 -> Word4

sRem :: Word4 -> Word4 -> Word4

sDiv :: Word4 -> Word4 -> Word4

sMod :: Word4 -> Word4 -> Word4

SIntegral Word4

SIntegral instance, using default methods

FromBits SWord4

Conversion from bits

Methods

fromBitsLE :: [SBool] -> SWord4

fromBitsBE :: [SBool] -> SWord4

Splittable Word8 Word4

Joiningsplitting tofrom Word8

Methods

split :: Word8 -> (Word4, Word4)

(#) :: Word4 -> Word4 -> Word8

extend :: Word4 -> Word8

word4 :: Word8 -> Word4

Smart constructor; simplifies conversion from Word8

type SWord4 = SBV Word4

SWord4 type synonym