cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell2010

Cryptol.Eval.Reference

Description

Synopsis

data Value
- = VBit (Either EvalError Bool)
- | VInteger (Either EvalError Integer)
- | VRational (Either EvalError Rational)
- | VFloat (Either EvalError BF)
- | VList Nat' [Value]
- | VTuple [Value]
- | VRecord [(Ident, Value)]
- | VFun (Value -> Value)
- | VPoly (TValue -> Value)
- | VNumPoly (Nat' -> Value)
evaluate :: Expr -> ModuleCmd Value
evalExpr :: Env -> Expr -> Value
evalDeclGroup :: Env -> DeclGroup -> Env
ppValue :: PPOpts -> Value -> Doc

Documentation

data Value Source #

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 Source #

evalExpr Source #

Arguments

:: Env	Evaluation environment
-> Expr	Expression to evaluate
-> Value

evalDeclGroup :: Env -> DeclGroup -> Env Source #

ppValue :: PPOpts -> Value -> Doc Source #