Cryptol.Eval.Reference

Documentation

data Value

Value type for the reference evaluator.

Constructors

VBit !Bool

Bit booleans

VInteger !Integer

Integer or Z n integers

VRational !Rational

Rational rationals

VFloat !BF

Floating point numbers

VList Nat' [E Value]

[n]a finite or infinite lists

VTuple [E Value]

( .. ) tuples

VRecord [(Ident, E Value)]

{ .. } records

VFun (E Value -> E Value)

functions

VPoly (TValue -> E Value)

polymorphic values (kind *)

VNumPoly (Nat' -> E Value)

polymorphic values (kind #)

data E a

Computation monad for the reference evaluator.

Constructors

Value !a

Err EvalError

Instances

Monad E

Defined in Cryptol.Eval.Reference

Methods

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

(>>) :: E a -> E b -> E b

return :: a -> E a

Functor E

Defined in Cryptol.Eval.Reference

Methods

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

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

Applicative E

Defined in Cryptol.Eval.Reference

Methods

pure :: a -> E a

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

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

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

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

evaluate :: Expr -> ModuleCmd (E Value)

evalExpr

Arguments

:: Env

Evaluation environment

-> Expr

Expression to evaluate

-> E Value

evalDeclGroup :: Env -> DeclGroup -> Env

ppValue :: PPOpts -> Value -> Doc

ppEValue :: PPOpts -> E Value -> Doc