Cryptol.Eval

Documentation

moduleEnv

Arguments

:: EvalPrims b w i

=> Module

Module containing declarations to evaluate

-> GenEvalEnv b w i

Environment to extend

-> Eval (GenEvalEnv b w i)

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

runEval :: EvalOpts -> Eval a -> IO a

Execute the given evaluation action.

data EvalOpts

Some options for evalutaion

Constructors

EvalOpts

Fields

• evalLogger :: Logger

  Where to print stuff (e.g., for trace)

• evalPPOpts :: PPOpts

  How to pretty print things.

data PPOpts

How to pretty print things when evaluating

Constructors

PPOpts

Fields

• useAscii :: Bool
• useBase :: Int
• useInfLength :: Int

defaultPPOpts :: PPOpts

data Eval a

The monad for Cryptol evaluation.

Instances

Monad Eval

Defined in Cryptol.Eval.Monad

Methods

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

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

return :: a -> Eval a

fail :: String -> Eval a

Functor Eval

Defined in Cryptol.Eval.Monad

Methods

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

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

MonadFix Eval

Defined in Cryptol.Eval.Monad

Methods

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

Applicative Eval

Defined in Cryptol.Eval.Monad

Methods

pure :: a -> Eval a

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

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

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

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

MonadIO Eval

Defined in Cryptol.Eval.Monad

Methods

liftIO :: IO a -> Eval a

NFData a => NFData (Eval a)

Defined in Cryptol.Eval.Monad

Methods

rnf :: Eval a -> ()

type EvalEnv = GenEvalEnv Bool BV Integer

emptyEnv :: GenEvalEnv b w i

Evaluation environment with no bindings

evalExpr

Arguments

:: EvalPrims b w i

=> GenEvalEnv b w i

Evaluation environment

-> Expr

Expression to evaluate

-> Eval (GenValue b w i)

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 i

=> [DeclGroup]

Declaration groups to evaluate

-> GenEvalEnv b w i

Environment to extend

-> Eval (GenEvalEnv b w i)

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

evalSel :: forall b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i)

Apply the the given "selector" form to the given value. This function pushes tuple and record selections pointwise down into other value constructs (e.g., streams and functions).

evalSetSel :: forall b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)

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 number function

DivideByZero

Division or modulus by 0

NegativeExponent

Exponentiation by negative integer

LogNegative

Logarithm of a negative integer

WordTooWide Integer

Bitvector too large

UserError String

Call to the Cryptol error primitive

LoopError String

Detectable nontermination

Instances

Show EvalError

Defined in Cryptol.Eval.Monad

Methods

showsPrec :: Int -> EvalError -> ShowS

show :: EvalError -> String

showList :: [EvalError] -> ShowS

Exception EvalError

Defined in Cryptol.Eval.Monad

Methods

toException :: EvalError -> SomeException

fromException :: SomeException -> Maybe EvalError

displayException :: EvalError -> String

PP EvalError

Defined in Cryptol.Eval.Monad

Methods

ppPrec :: Int -> EvalError -> Doc

forceValue :: GenValue b w i -> Eval ()

Force the evaluation of a value