Cryptol.Eval

Documentation

moduleEnv

Arguments

:: EvalPrims sym

=> sym

-> Module

Module containing declarations to evaluate

-> GenEvalEnv sym

Environment to extend

-> SEval sym (GenEvalEnv sym)

Extend the given evaluation environment with all the declarations contained in the given module.

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

Execute the given evaluation action.

data EvalOpts

Some options for evalutaion

Constructors

EvalOpts

Fields

• evalLogger :: Logger

  Where to print stuff (e.g., for trace)

• evalPPOpts :: PPOpts

  How to pretty print things.

data PPOpts

How to pretty print things when evaluating

Constructors

PPOpts

Fields

• useAscii :: Bool
• useBase :: Int
• useInfLength :: Int
• useFPBase :: Int
• useFPFormat :: PPFloatFormat

Instances

Show PPOpts

Defined in Cryptol.Utils.PP

Methods

showsPrec :: Int -> PPOpts -> ShowS

show :: PPOpts -> String

showList :: [PPOpts] -> ShowS

defaultPPOpts :: PPOpts

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.

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

type EvalEnv = GenEvalEnv Concrete

emptyEnv :: GenEvalEnv sym

Evaluation environment with no bindings

evalExpr

Arguments

:: (?range :: Range, EvalPrims sym)

=> sym

-> GenEvalEnv sym

Evaluation environment

-> Expr

Expression to evaluate

-> SEval sym (GenValue sym)

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

Arguments

:: EvalPrims sym

=> sym

-> [DeclGroup]

Declaration groups to evaluate

-> GenEvalEnv sym

Environment to extend

-> SEval sym (GenEvalEnv sym)

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

evalNewtypeDecls :: EvalPrims sym => sym -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)

evalSel :: Backend sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)

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 sym. Backend sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)

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

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

forceValue :: Backend sym => GenValue sym -> SEval sym ()

Force the evaluation of a value