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.Monad

Description

 
Synopsis

Evaluation monad

data Eval a Source #

The monad for Cryptol evaluation.

Constructors

Ready !a 
Thunk !(EvalOpts -> IO a) 

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

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 

Fields

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

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 #

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.