Cryptol.Eval.Reference

Documentation

data Value

Value type for the reference evaluator.

Constructors

VBit (Either EvalError Bool)

Bit booleans

VInteger (Either EvalError Integer)

Integer or Z n integers

VRational (Either EvalError Rational)

Rational rationals

VFloat (Either EvalError BF)

Floating point numbers

VList Nat' [Value]

[n]a finite or infinite lists

VTuple [Value]

( .. ) tuples

VRecord [(Ident, Value)]

{ .. } records

VFun (Value -> Value)

functions

VPoly (TValue -> Value)

polymorphic values (kind *)

VNumPoly (Nat' -> Value)

polymorphic values (kind #)

evaluate :: Expr -> ModuleCmd Value

evalExpr

Arguments

:: Env

Evaluation environment

-> Expr

Expression to evaluate

-> Value

evalDeclGroup :: Env -> DeclGroup -> Env

ppValue :: PPOpts -> Value -> Doc