Copyright | (c) Benjamin Selfridge 2018 Galois Inc. |
---|---|
License | None (yet) |
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
This module exports a type, BVApp
, to aid in building expression languages over
BitVector
s. Let expr :: Nat -> *
be some ADT of expressions that yield
BitVector
s when evaluated. Then, given one or more values of type expr w
(i.e. one or more of these evaluatable expressions), BVApp
provides the various
constructors necessary for creating compound expressions involving pure BitVector
operations. The expr
type can (and often will) include a constructor of type BVApp
expr w -> expr w
in order to create a recursive expression language.
In addition to the BVApp
type, we provide an evaluator which, given a function
mapping values of type expr w
to BitVector
s, will evaluate the compound
BVApp
expressions.
- data BVApp (expr :: Nat -> *) (w :: Nat) where
- LitBVApp :: BitVector w -> BVApp expr w
- AndApp :: !(expr w) -> !(expr w) -> BVApp expr w
- OrApp :: !(expr w) -> !(expr w) -> BVApp expr w
- XorApp :: !(expr w) -> !(expr w) -> BVApp expr w
- NotApp :: !(expr w) -> BVApp expr w
- SllApp :: !(expr w) -> !(expr w) -> BVApp expr w
- SrlApp :: !(expr w) -> !(expr w) -> BVApp expr w
- SraApp :: !(expr w) -> !(expr w) -> BVApp expr w
- AddApp :: !(expr w) -> !(expr w) -> BVApp expr w
- SubApp :: !(expr w) -> !(expr w) -> BVApp expr w
- MulSApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w)
- MulUApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w)
- MulSUApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w)
- DivUApp :: !(expr w) -> !(expr w) -> BVApp expr w
- DivSApp :: !(expr w) -> !(expr w) -> BVApp expr w
- RemUApp :: !(expr w) -> !(expr w) -> BVApp expr w
- RemSApp :: !(expr w) -> !(expr w) -> BVApp expr w
- EqApp :: !(expr w) -> !(expr w) -> BVApp expr 1
- LtuApp :: !(expr w) -> !(expr w) -> BVApp expr 1
- LtsApp :: !(expr w) -> !(expr w) -> BVApp expr 1
- ZExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w'
- SExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w'
- ExtractApp :: NatRepr w' -> Int -> !(expr w) -> BVApp expr w'
- ConcatApp :: !(expr w) -> !(expr w') -> BVApp expr (w + w')
- IteApp :: !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w
- evalBVApp :: (forall w'. expr w' -> BitVector w') -> BVApp expr w -> BitVector w
- evalBVAppM :: Monad m => (forall w'. expr w' -> m (BitVector w')) -> BVApp expr w -> m (BitVector w)
Documentation
data BVApp (expr :: Nat -> *) (w :: Nat) where Source #
Represents the application of a BitVector
operation to one or more
subexpressions.
LitBVApp :: BitVector w -> BVApp expr w | |
AndApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
OrApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
XorApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
NotApp :: !(expr w) -> BVApp expr w | |
SllApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
SrlApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
SraApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
AddApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
SubApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
MulSApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w) | |
MulUApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w) | |
MulSUApp :: !(expr w) -> !(expr w) -> BVApp expr (w + w) | |
DivUApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
DivSApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
RemUApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
RemSApp :: !(expr w) -> !(expr w) -> BVApp expr w | |
EqApp :: !(expr w) -> !(expr w) -> BVApp expr 1 | |
LtuApp :: !(expr w) -> !(expr w) -> BVApp expr 1 | |
LtsApp :: !(expr w) -> !(expr w) -> BVApp expr 1 | |
ZExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w' | |
SExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w' | |
ExtractApp :: NatRepr w' -> Int -> !(expr w) -> BVApp expr w' | |
ConcatApp :: !(expr w) -> !(expr w') -> BVApp expr (w + w') | |
IteApp :: !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w |
Evaluate a BVApp
given a pure evaluation function for the parameterized type expr
.