Cryptol.Eval

Documentation

moduleEnv

Arguments

:: EvalPrims b w

=> Module

Module containing declarations to evaluate

-> GenEvalEnv b w

Environment to extend

-> Eval (GenEvalEnv b w)

Extend the given evaluation environment with all the declarations contained in the given module.

runEval :: Eval a -> IO a

Execute the given evaluation action.

data Eval a

The monad for Cryptol evaluation.

Instances

Monad Eval

Methods

(>>=) :: Eval a -> (a -> Eval b) -> Eval b

(>>) :: Eval a -> Eval b -> Eval b

return :: a -> Eval a

fail :: String -> Eval a

Functor Eval

Methods

fmap :: (a -> b) -> Eval a -> Eval b

(<$) :: a -> Eval b -> Eval a

MonadFix Eval

Methods

mfix :: (a -> Eval a) -> Eval a

Applicative Eval

Methods

pure :: a -> Eval a

(<*>) :: Eval (a -> b) -> Eval a -> Eval b

(*>) :: Eval a -> Eval b -> Eval b

(<*) :: Eval a -> Eval b -> Eval a

MonadIO Eval

Methods

liftIO :: IO a -> Eval a

NFData a => NFData (Eval a)

Methods

rnf :: Eval a -> ()

type EvalEnv = GenEvalEnv Bool BV

emptyEnv :: GenEvalEnv b w

Evaluation environment with no bindings

evalExpr

Arguments

:: EvalPrims b w

=> GenEvalEnv b w

Evaluation environment

-> Expr

Expression to evaluate

-> Eval (GenValue b w)

Evaluate a Cryptol expression to a value. This evaluator is parameterized by the EvalPrims class, which defines the behavior of bits and words, in addition to providing implementations for all the primitives.

evalDecls

Arguments

:: EvalPrims b w

=> [DeclGroup]

Declaration groups to evaluate

-> GenEvalEnv b w

Environment to extend

-> Eval (GenEvalEnv b w)

Extend the given evaluation environment with the result of evaluating the given collection of declaration groups.

data EvalError

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex Integer

Out-of-bounds index

TypeCannotBeDemoted Type

Non-numeric type passed to demote function

DivideByZero

Division or modulus by 0

WordTooWide Integer

Bitvector too large

UserError String

Call to the Cryptol error primitive

LoopError String

Detectable nontermination

Instances

Show EvalError

Methods

showsPrec :: Int -> EvalError -> ShowS

show :: EvalError -> String

showList :: [EvalError] -> ShowS

Exception EvalError

Methods

toException :: EvalError -> SomeException

fromException :: SomeException -> Maybe EvalError

displayException :: EvalError -> String

PP EvalError

Methods

ppPrec :: Int -> EvalError -> Doc

forceValue :: GenValue b w -> Eval ()

Force the evaluation of a value