cryptol-2.8.0: Cryptol: The Language of Cryptography

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
  }
- io :: IO a -> Eval a
- delay :: Maybe String -> Eval a -> Eval (Eval a)
- delayFill :: Eval a -> Eval a -> Eval (Eval a)
- ready :: a -> Eval a
- blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
- data EvalError
  - = InvalidIndex Integer
  - | TypeCannotBeDemoted Type
  - | DivideByZero
  - | NegativeExponent
  - | LogNegative
  - | WordTooWide Integer
  - | UserError String
  - | LoopError String
  - | NoPrim Name
- evalPanic :: HasCallStack => String -> [String] -> a
- typeCannotBeDemoted :: Type -> a
- divideByZero :: Eval a
- negativeExponent :: Eval a
- logNegative :: Eval a
- wordTooWide :: Integer -> a
- cryUserError :: String -> Eval a
- cryLoopError :: String -> Eval a
- cryNoPrimError :: Name -> Eval a
- invalidIndex :: Integer -> Eval a

# Evaluation monad

data Eval a Source #

The monad for Cryptol evaluation.

Constructors

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

#### Instances

Instances details

Monad Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods (>>=) :: Eval a -> (a -> Eval b) -> Eval b Source # (>>) :: Eval a -> Eval b -> Eval b Source # return :: a -> Eval a Source #
Functor Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods fmap :: (a -> b) -> Eval a -> Eval b Source # (<$) :: a -> Eval b -> Eval a Source #
MonadFix Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods mfix :: (a -> Eval a) -> Eval a Source #
MonadFail Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods fail :: String -> Eval a Source #
Applicative Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods pure :: a -> Eval a Source # (<*>) :: Eval (a -> b) -> Eval a -> Eval b Source # liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c Source # (*>) :: Eval a -> Eval b -> Eval b Source # (<*) :: Eval a -> Eval b -> Eval a Source #
MonadIO Eval Source # |
Instance details Defined in Cryptol.Eval.Monad Methods liftIO :: IO a -> Eval a Source #
NFData a => NFData (Eval a) Source # |
Instance details Defined in Cryptol.Eval.Monad Methods rnf :: Eval a -> () Source #

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

io :: IO a -> Eval a Source #

Lift an `IO` computation into the `Eval` monad.

delay Source #

Arguments

:: Maybe String | Optional name to print if a loop is detected
-> Eval a | Computation to delay
-> Eval (Eval a) |

Delay the given evaluation computation, returning a thunk which will run the computation when forced. Raise a loop error if the resulting thunk is forced during its own evaluation.

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.

# Error reporting

data EvalError Source #

Data type describing errors that can occur during evaluation.

Constructors

InvalidIndex 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

#### Instances

Instances details

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

typeCannotBeDemoted :: Type -> a Source #

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

divideByZero :: Eval a Source #

For division by 0.

negativeExponent :: Eval a Source #

For exponentiation by a negative integer.

logNegative :: Eval a Source #

For logarithm of a negative integer.

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

cryUserError :: String -> Eval a Source #

For the Cryptol `error` function.

cryLoopError :: String -> Eval a Source #

For cases where we can detect tight loops.

cryNoPrimError :: Name -> Eval a Source #

invalidIndex :: Integer -> Eval a Source #

A sequencing operation has gotten an invalid index.