cryptol-2.8.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 b w i 
=> Module

Module containing declarations to evaluate

-> GenEvalEnv b w i

Environment to extend

-> Eval (GenEvalEnv b w i) 

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

Constructors

PPOpts 

Fields

data Eval a Source #

The monad for Cryptol evaluation.

Instances

Instances details
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 #

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 -> ()

type EvalEnv = GenEvalEnv Bool BV Integer Source #

emptyEnv :: GenEvalEnv b w i Source #

Evaluation environment with no bindings

evalExpr Source #

Arguments

:: EvalPrims b w i 
=> GenEvalEnv b w i

Evaluation environment

-> Expr

Expression to evaluate

-> Eval (GenValue b w i) 

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 b w i 
=> [DeclGroup]

Declaration groups to evaluate

-> GenEvalEnv b w i

Environment to extend

-> Eval (GenEvalEnv b w i) 

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

evalSel :: forall b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i) 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 b w i. EvalPrims b w i => GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i) Source #

data EvalError Source #

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex 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

Instances

Instances details
Show EvalError Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

showsPrec :: Int -> EvalError -> ShowS

show :: EvalError -> String

showList :: [EvalError] -> ShowS

Exception EvalError Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

toException :: EvalError -> SomeException

fromException :: SomeException -> Maybe EvalError

displayException :: EvalError -> String

PP EvalError Source # 
Instance details

Defined in Cryptol.Eval.Monad

Methods

ppPrec :: Int -> EvalError -> Doc Source #

forceValue :: GenValue b w i -> Eval () Source #

Force the evaluation of a value