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

Cryptol.Eval

Description

Synopsis

moduleEnv :: EvalPrims sym => sym -> Module -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
runEval :: CallStack -> Eval a -> IO a
data EvalOpts = EvalOpts {
- evalLogger :: Logger
- evalPPOpts :: PPOpts
}
data PPOpts = PPOpts {
- useAscii :: Bool
- useBase :: Int
- useInfLength :: Int
- useFPBase :: Int
- useFPFormat :: PPFloatFormat
- useFieldOrder :: FieldOrder
}
defaultPPOpts :: PPOpts
data Eval a
type EvalEnv = GenEvalEnv Concrete
emptyEnv :: GenEvalEnv sym
evalExpr :: (?range :: Range, EvalPrims sym) => sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalDecls :: EvalPrims sym => sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNominalDecls :: EvalPrims sym => sym -> Map Name NominalType -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalSel :: Backend sym => sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
evalSetSel :: forall sym. Backend sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
evalEnumCon :: Backend sym => sym -> Ident -> Int -> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
data EvalError
- = InvalidIndex (Maybe Integer)
- | DivideByZero
- | NegativeExponent
- | LogNegative
- | UserError String
- | LoopError String
- | NoPrim Name
- | BadRoundingMode Integer
- | BadValue String
- | NoMatchingPropGuardCase String
- | NoMatchingConstructor (Maybe String)
- | FFINotSupported Name
- | FFITypeNumTooBig Name TParam Integer
data EvalErrorEx = EvalErrorEx CallStack EvalError
data Unsupported = UnsupportedSymbolicOp String
data WordTooWide = WordTooWide Integer
forceValue :: Backend sym => GenValue sym -> SEval sym ()
checkProp :: Prop -> Bool

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 :: CallStack -> 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 useFieldOrder :: FieldOrder

Instances

Instances details

Show PPOpts Source #
Instance details Defined in Cryptol.Utils.PP Methods showsPrec :: Int -> PPOpts -> ShowS # show :: PPOpts -> String # showList :: [PPOpts] -> ShowS #

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

MonadIO Eval Source #
Instance details Defined in Cryptol.Backend.Monad Methods liftIO :: IO a -> 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 #
Functor Eval Source #
Instance details Defined in Cryptol.Backend.Monad Methods fmap :: (a -> b) -> Eval a -> Eval b # (<$) :: a -> Eval b -> Eval a #
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 #

type EvalEnv = GenEvalEnv Concrete Source #

emptyEnv :: GenEvalEnv sym Source #

Evaluation environment with no bindings

evalExpr Source #

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

evalNominalDecls :: EvalPrims sym => sym -> Map Name NominalType -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym) Source #

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

Apply the the given "selector" form to the given value. Note that selectors are expected to apply only to values of the right type, e.g. tuple selectors expect only tuple values. The lifting of tuple an record selectors over functions and sequences has already been resolved earlier in the typechecker.

evalSetSel :: forall sym. Backend sym => sym -> TValue -> GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

evalEnumCon :: Backend sym => sym -> Ident -> Int -> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym) Source #

Make the function for a known constructor

data EvalError Source #

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.
NoMatchingPropGuardCase String	No prop guard holds for the given type variables.
NoMatchingConstructor (Maybe String)	Missing `case` alternative
FFINotSupported Name	Foreign function cannot be called
FFITypeNumTooBig Name TParam Integer	Number passed to foreign function as a type argument is too large

Instances

Instances details

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

data EvalErrorEx Source #

Constructors

EvalErrorEx CallStack EvalError

Instances

Instances details

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

data Unsupported Source #

Constructors

UnsupportedSymbolicOp String

Operation cannot be supported in the symbolic simulator

Instances

Instances details

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

data WordTooWide Source #

Constructors

WordTooWide Integer

Bitvector too large

Instances

Instances details

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

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

Force the evaluation of a value

checkProp :: Prop -> Bool Source #

Checks whether an evaluated Prop holds