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

Cryptol.Eval.Monad

Contents

Evaluation monad
Error reporting

Description

Synopsis

data Eval a
- = Ready !a
- | Thunk !(EvalOpts -> IO a)
runEval :: EvalOpts -> Eval a -> IO a
data EvalOpts = EvalOpts {
- evalLogger :: Logger
- evalPPOpts :: PPOpts
}
getEvalOpts :: Eval EvalOpts
data PPOpts = PPOpts {
- useAscii :: Bool
- useBase :: Int
- useInfLength :: Int
- useFPBase :: Int
- useFPFormat :: PPFloatFormat
}
data PPFloatFormat
- = FloatFixed Int PPFloatExp
- | FloatFrac Int
- | FloatFree PPFloatExp
data PPFloatExp
- = ForceExponent
- | AutoExponent
defaultPPOpts :: PPOpts
io :: IO a -> Eval a
delayFill :: Eval a -> Eval a -> Eval (Eval a)
ready :: a -> Eval a
blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
evalSpark :: Eval a -> Eval (Eval a)
data Unsupported = UnsupportedSymbolicOp String
data EvalError
- = InvalidIndex (Maybe Integer)
- | TypeCannotBeDemoted Type
- | DivideByZero
- | NegativeExponent
- | LogNegative
- | WordTooWide Integer
- | UserError String
- | LoopError String
- | NoPrim Name
- | BadRoundingMode Integer
- | BadValue String
evalPanic :: HasCallStack => String -> [String] -> a
wordTooWide :: Integer -> a
typeCannotBeDemoted :: Type -> a

Evaluation monad

data Eval a Source #

The monad for Cryptol evaluation.

Constructors

Ready !a
Thunk !(EvalOpts -> IO a)

Instances

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

runEval :: EvalOpts -> 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.

getEvalOpts :: Eval EvalOpts Source #

Access the evaluation options.

data PPOpts Source #

How to pretty print things when evaluating

Constructors

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

data PPFloatFormat Source #

Constructors

FloatFixed Int PPFloatExp	Use this many significant digis
FloatFrac Int	Show this many digits after floating point
FloatFree PPFloatExp	Use the correct number of digits

data PPFloatExp Source #

Constructors

ForceExponent	Always show an exponent
AutoExponent	Only show exponent when needed

defaultPPOpts :: PPOpts Source #

io :: IO a -> Eval a Source #

Lift an IO computation into the Eval monad.

delayFill Source #

Arguments

:: Eval a	Computation to delay
-> Eval a	Backup computation to run 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 Source #

A computation that returns an already-evaluated value.

blackhole Source #

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

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

Error reporting

data Unsupported Source #

Constructors

UnsupportedSymbolicOp String

Operation cannot be supported in the symbolic simulator

Instances

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

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

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

Panic from an Eval context.

wordTooWide :: Integer -> a Source #

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

typeCannotBeDemoted :: Type -> a Source #

For things like `(inf) or `(0-1).