cryptol-2.7.0: Cryptol: The Language of Cryptography

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

Cryptol.Eval.Monad

Contents

Description

 
Synopsis

Evaluation monad

data Eval a Source #

The monad for Cryptol evaluation.

Constructors

Ready !a 
Thunk !(EvalOpts -> IO a) 
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 #

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

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

Execute the given evaluation action.

data EvalOpts Source #

Some options for evalutaion

Constructors

EvalOpts 

Fields

getEvalOpts :: Eval EvalOpts Source #

Access the evaluation options.

data PPOpts Source #

How to pretty print things when evaluating

Constructors

PPOpts 

io :: IO a -> Eval a Source #

Lift an IO computation into the Eval monad.

delay Source #

Arguments

:: Maybe String

Optional name to print if a loop is detected

-> Eval a

Computation to delay

-> Eval (Eval a) 

Delay the given evaluation computation, returning a thunk which will run the computation when forced. Raise a loop error if the resulting thunk is forced during its own evaluation.

delayFill Source #

Arguments

:: Eval a

Computation to delay

-> Eval a

Backup computation to run if a tight loop is detected

-> Eval (Eval a) 

Delay the given evaluation computation, returning a thunk which will run the computation when forced. Run the retry computation instead if the resulting thunk is forced during its own evaluation.

ready :: a -> Eval a Source #

A computation that returns an already-evaluated value.

blackhole Source #

Arguments

:: String

A name to associate with this thunk.

-> Eval (Eval a, Eval a -> Eval ()) 

Produce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.

Error reporting

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

evalPanic :: HasCallStack => String -> [String] -> a Source #

Panic from an Eval context.

typeCannotBeDemoted :: Type -> a Source #

For things like `(inf) or `(0-1).

divideByZero :: Eval a Source #

For division by 0.

negativeExponent :: Eval a Source #

For exponentiation by a negative integer.

logNegative :: Eval a Source #

For logarithm of a negative integer.

wordTooWide :: Integer -> a Source #

For when we know that a word is too wide and will exceed gmp's limits (though words approaching this size will probably cause the system to crash anyway due to lack of memory).

cryUserError :: String -> Eval a Source #

For the Cryptol error function.

cryLoopError :: String -> Eval a Source #

For cases where we can detect tight loops.

invalidIndex :: Integer -> Eval a Source #

A sequencing operation has gotten an invalid index.