cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Eval

Description

 
Synopsis

Documentation

moduleEnv Source #

Arguments

:: EvalPrims sym 
=> sym 
-> Module

Module containing declarations to evaluate

-> GenEvalEnv sym

Environment to extend

-> SEval sym (GenEvalEnv sym) 

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

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

Execute the given evaluation action.

data EvalOpts Source #

Some options for evalutaion

Constructors

EvalOpts 

Fields

data PPOpts Source #

How to pretty print things when evaluating

data Eval a Source #

The monad for Cryptol evaluation.

Instances
Monad Eval Source # 
Instance details

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

Defined in Cryptol.Eval.Monad

Methods

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

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

MonadFix Eval Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

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

MonadFail Eval Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

fail :: String -> Eval a #

Applicative Eval Source # 
Instance details

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

Defined in Cryptol.Eval.Monad

Methods

liftIO :: IO a -> Eval a #

NFData a => NFData (Eval a) Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

rnf :: Eval a -> () #

emptyEnv :: GenEvalEnv sym Source #

Evaluation environment with no bindings

evalExpr Source #

Arguments

:: EvalPrims sym 
=> sym 
-> GenEvalEnv sym

Evaluation environment

-> Expr

Expression to evaluate

-> SEval sym (GenValue sym) 

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

Arguments

:: EvalPrims sym 
=> sym 
-> [DeclGroup]

Declaration groups to evaluate

-> GenEvalEnv sym

Environment to extend

-> SEval sym (GenEvalEnv sym) 

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

evalSel :: EvalPrims sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym) Source #

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 sym. EvalPrims sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

data EvalError Source #

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex (Maybe 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

NoPrim Name

Primitive with no implementation

BadRoundingMode Integer

Invalid rounding mode

BadValue String

Value outside the domain of a partial function.

data Unsupported Source #

Constructors

UnsupportedSymbolicOp String

Operation cannot be supported in the symbolic simulator

forceValue :: Backend sym => GenValue sym -> SEval sym () Source #

Force the evaluation of a value