Cryptol.Backend.Monad

Evaluation monad

data Eval a

The monad for Cryptol evaluation. A computation is either "ready", which means it represents only trivial computation, or is an "eval" action which must be computed to get the answer, or it is a "thunk", which represents a delayed, shared computation.

Constructors

Ready !a

Eval !(CallStack -> IO a)

Thunk !(TVar (ThunkState a))

Instances

Monad Eval

Defined in Cryptol.Backend.Monad

Methods

(>>=) :: Eval a -> (a -> Eval b) -> Eval b

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

return :: a -> Eval a

Functor Eval

Defined in Cryptol.Backend.Monad

Methods

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

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

Applicative Eval

Defined in Cryptol.Backend.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

Defined in Cryptol.Backend.Monad

Methods

liftIO :: IO a -> Eval a

runEval :: CallStack -> Eval a -> IO a

Execute the given evaluation action.

io :: IO a -> Eval a

Lift an IO computation into the Eval monad.

delayFill

Arguments

:: Eval a

Computation to delay

-> Maybe (Eval a)

Optional backup computation to run if a tight loop is detected

-> String

message for the exception 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

A computation that returns an already-evaluated value.

blackhole

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.

evalSpark :: Eval a -> Eval (Eval a)

Begin executing the given operation in a separate thread, returning a thunk which will await the completion of the computation when forced.

maybeReady :: Eval a -> Eval (Maybe a)

Test if a value is "ready", which means that it requires no computation to return.

Call stacks

type CallStack = Seq (Name, Range)

The type of dynamic call stacks for the interpreter. New frames are pushed onto the right side of the sequence.

getCallStack :: Eval CallStack

Get the current call stack

withCallStack :: CallStack -> Eval a -> Eval a

Execute the action with the given call stack

modifyCallStack :: (CallStack -> CallStack) -> Eval a -> Eval a

Run the given action with a modify call stack

combineCallStacks

Arguments

:: CallStack

call stack of the application context

-> CallStack

call stack of the function being applied

-> CallStack

Combine the call stack of a function value with the call stack of the current calling context. This algorithm is the same one GHC uses to compute profiling calling contexts.

The algorithm is as follows.

ccs ++> ccsfn = ccs ++ dropCommonPrefix ccs ccsfn

where

dropCommonPrefix A B -- returns the suffix of B after removing any prefix common -- to both A and B.

pushCallFrame :: Name -> Range -> CallStack -> CallStack

Add a call frame to the top of a call stack

displayCallStack :: CallStack -> Doc

Pretty print a call stack with each call frame on a separate line, with most recent call frames at the top.

Error reporting

data Unsupported

Constructors

UnsupportedSymbolicOp String

Operation cannot be supported in the symbolic simulator

Instances

Show Unsupported

Defined in Cryptol.Backend.Monad

Methods

showsPrec :: Int -> Unsupported -> ShowS

show :: Unsupported -> String

showList :: [Unsupported] -> ShowS

Exception Unsupported

Defined in Cryptol.Backend.Monad

Methods

toException :: Unsupported -> SomeException

fromException :: SomeException -> Maybe Unsupported

displayException :: Unsupported -> String

PP Unsupported

Defined in Cryptol.Backend.Monad

Methods

ppPrec :: Int -> Unsupported -> Doc

data EvalError

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex (Maybe Integer)

Out-of-bounds index

DivideByZero

Division or modulus by 0

NegativeExponent

Exponentiation by negative integer

LogNegative

Logarithm of a negative integer

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.

Instances

Show EvalError

Defined in Cryptol.Backend.Monad

Methods

showsPrec :: Int -> EvalError -> ShowS

show :: EvalError -> String

showList :: [EvalError] -> ShowS

PP EvalError

Defined in Cryptol.Backend.Monad

Methods

ppPrec :: Int -> EvalError -> Doc

data EvalErrorEx

Constructors

EvalErrorEx CallStack EvalError

Instances

Show EvalErrorEx

Defined in Cryptol.Backend.Monad

Methods

showsPrec :: Int -> EvalErrorEx -> ShowS

show :: EvalErrorEx -> String

showList :: [EvalErrorEx] -> ShowS

Exception EvalErrorEx

Defined in Cryptol.Backend.Monad

Methods

toException :: EvalErrorEx -> SomeException

fromException :: SomeException -> Maybe EvalErrorEx

displayException :: EvalErrorEx -> String

PP EvalErrorEx

Defined in Cryptol.Backend.Monad

Methods

ppPrec :: Int -> EvalErrorEx -> Doc

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

Panic from an Eval context.

wordTooWide :: Integer -> a

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

data WordTooWide

Constructors

WordTooWide Integer

Bitvector too large

Instances

Show WordTooWide

Defined in Cryptol.Backend.Monad

Methods

showsPrec :: Int -> WordTooWide -> ShowS

show :: WordTooWide -> String

showList :: [WordTooWide] -> ShowS

Exception WordTooWide

Defined in Cryptol.Backend.Monad

Methods

toException :: WordTooWide -> SomeException

fromException :: SomeException -> Maybe WordTooWide

displayException :: WordTooWide -> String

PP WordTooWide

Defined in Cryptol.Backend.Monad

Methods

ppPrec :: Int -> WordTooWide -> Doc