sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Brian Huffman
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Misc.Word4

Description

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

Synopsis

- newtype Word4 = Word4 Word8
- word4 :: Word8 -> Word4
- type SWord4 = SBV Word4

# Documentation

newtype Word4 Source

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

Constructors

Word4 Word8 |

Instances

Bounded Word4 Source | Bounded instance; from 0 to 255
Enum Word4 Source | Enum instance, trivial definitions.
Eq Word4 Source |
Integral Word4 Source | 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.
Data Word4 Source |
Num Word4 Source | Num instance, merely lifts underlying 8-bit operation and casts back
Ord Word4 Source |
Read Word4 Source | Read instance. We read as an 8-bit word, and coerce
Real Word4 Source | Real instance simply uses the Word8 instance
Show Word4 Source | Show instance
Bits Word4 Source | Bits instance
Random Word4 Source | Random instance, used in quick-check
HasKind Word4 Source | HasKind instance; simply returning the underlying kind for the type
SymWord Word4 Source | SymWord instance, allowing this type to be used in proofs/sat etc.
SatModel Word4 Source | SatModel instance, merely uses the generic parsing method.
SDivisible SWord4 Source | SDvisible instance, using default methods
SDivisible Word4 Source | SDvisible instance, using 0-extension
SIntegral Word4 Source | SIntegral instance, using default methods
FromBits SWord4 Source | Conversion from bits
Splittable Word8 Word4 Source | Joiningsplitting tofrom Word8

word4 :: Word8 -> Word4 Source

Smart constructor; simplifies conversion from Word8

type SWord4 = SBV Word4 Source

SWord4 type synonym