cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Eval.Reference

Description

Synopsis

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

# Documentation

data Value Source #

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

Computation monad for the reference evaluator.

Constructors

Value !a |
Err EvalError |

#### Instances

Instances details

Applicative E Source # |
Instance details Defined in Cryptol.Eval.Reference Methods pure :: a -> E a Source # (<*>) :: E (a -> b) -> E a -> E b Source # liftA2 :: (a -> b -> c) -> E a -> E b -> E c Source # (*>) :: E a -> E b -> E b Source # (<*) :: E a -> E b -> E a Source #
Functor E Source # |
Instance details Defined in Cryptol.Eval.Reference Methods fmap :: (a -> b) -> E a -> E b Source # (<$) :: a -> E b -> E a Source #
Monad E Source # |
Instance details Defined in Cryptol.Eval.Reference Methods (>>=) :: E a -> (a -> E b) -> E b Source # (>>) :: E a -> E b -> E b Source # return :: a -> E a Source #

evaluate :: Expr -> ModuleCmd (E Value) Source #

evalExpr Source #

Arguments

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

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

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

ppEValue :: PPOpts -> E Value -> Doc Source #