Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell2010

Cryptol.Eval

Description

Synopsis

moduleEnv :: EvalPrims sym => sym -> Module -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
runEval :: Eval a -> IO a
data EvalOpts = EvalOpts {
- evalLogger :: Logger
- evalPPOpts :: PPOpts
}
data PPOpts = PPOpts {
- useAscii :: Bool
- useBase :: Int
- useInfLength :: Int
- useFPBase :: Int
- useFPFormat :: PPFloatFormat
}
defaultPPOpts :: PPOpts
data Eval a
type EvalEnv = GenEvalEnv Concrete
emptyEnv :: GenEvalEnv sym
evalExpr :: EvalPrims sym => sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalDecls :: EvalPrims sym => sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalSel :: EvalPrims sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
evalSetSel :: forall sym. EvalPrims sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
data EvalError
- = InvalidIndex (Maybe Integer)
- | TypeCannotBeDemoted Type
- | DivideByZero
- | NegativeExponent
- | LogNegative
- | WordTooWide Integer
- | UserError String
- | LoopError String
- | NoPrim Name
- | BadRoundingMode Integer
- | BadValue String
data Unsupported = UnsupportedSymbolicOp String
forceValue :: Backend sym => GenValue sym -> SEval sym ()

Documentation

moduleEnv Source #

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 :: Eval a -> IO a Source #

Execute the given evaluation action.

data EvalOpts Source #

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

How to pretty print things when evaluating

Constructors

PPOpts
Fields useAscii :: Bool useBase :: Int useInfLength :: Int useFPBase :: Int useFPFormat :: PPFloatFormat

defaultPPOpts :: PPOpts Source #

data Eval a Source #

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

Instances details

Monad Eval Source #
Instance details 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 Source #
Instance details Defined in Cryptol.Backend.Monad Methods fmap :: (a -> b) -> Eval a -> Eval b # (<$) :: a -> Eval b -> Eval a #
MonadFix Eval Source #
Instance details Defined in Cryptol.Backend.Monad Methods mfix :: (a -> Eval a) -> Eval a #
MonadFail Eval Source #
Instance details Defined in Cryptol.Backend.Monad Methods fail :: String -> Eval a #
Applicative Eval Source #
Instance details 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 Source #
Instance details Defined in Cryptol.Backend.Monad Methods liftIO :: IO a -> Eval a #

type EvalEnv = GenEvalEnv Concrete Source #

emptyEnv :: GenEvalEnv sym Source #

Evaluation environment with no bindings

evalExpr Source #

Arguments

:: 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 Source #

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.

evalSel :: EvalPrims sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym) Source #

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

data EvalError Source #

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex (Maybe 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
BadRoundingMode Integer	Invalid rounding mode
BadValue String	Value outside the domain of a partial function.

Instances

Instances details

Show EvalError Source #
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> EvalError -> ShowS # show :: EvalError -> String # showList :: [EvalError] -> ShowS #
Exception EvalError Source #
Instance details Defined in Cryptol.Backend.Monad Methods toException :: EvalError -> SomeException # fromException :: SomeException -> Maybe EvalError # displayException :: EvalError -> String #
PP EvalError Source #
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> EvalError -> Doc Source #

data Unsupported Source #

Constructors

UnsupportedSymbolicOp String

Operation cannot be supported in the symbolic simulator

Instances

Instances details

Show Unsupported Source #
Instance details Defined in Cryptol.Backend.Monad Methods showsPrec :: Int -> Unsupported -> ShowS # show :: Unsupported -> String # showList :: [Unsupported] -> ShowS #
Exception Unsupported Source #
Instance details Defined in Cryptol.Backend.Monad Methods toException :: Unsupported -> SomeException # fromException :: SomeException -> Maybe Unsupported # displayException :: Unsupported -> String #
PP Unsupported Source #
Instance details Defined in Cryptol.Backend.Monad Methods ppPrec :: Int -> Unsupported -> Doc Source #

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

Force the evaluation of a value