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.

Execute the given evaluation action.

Lift an IO computation into the Eval monad.

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.

A computation that returns an already-evaluated value.

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.

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

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

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

Get the current call stack

Execute the action with the given call stack

Run the given action with a modify call stack

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.

Add a call frame to the top of a call stack

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

Data type describing errors that can occur during evaluation.

Panic from an Eval context.

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