Data.BitVector.Sized.App

This module exports a type, BVApp, to aid in building expression languages over BitVectors. Let expr :: Nat -> * be some ADT of expressions that yield BitVectors 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 BitVectors, will evaluate the compound BVApp expressions.

Documentation

data BVApp (expr :: Nat -> *) (w :: Nat) where

Represents the application of a BitVector operation to one or more subexpressions.

Constructors

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

Arguments

:: (forall w'. expr w' -> BitVector w')

expression evaluator

-> BVApp expr w

application

-> BitVector w

Evaluate a BVApp given a pure evaluation function for the parameterized type expr.

evalBVAppM

Arguments

:: Monad m

=> (forall w'. expr w' -> m (BitVector w'))

expression evaluator

-> BVApp expr w

application

-> m (BitVector w)

Evaluate a BVApp given a monadic evaluation function for the parameterized type expr.