    > -- |
    > -- Module      :  Cryptol.Eval.Reference
    > -- Description :  The reference implementation of the Cryptol evaluation semantics.
    > -- Copyright   :  (c) 2013-2020 Galois, Inc.
    > -- License     :  BSD3
    > -- Maintainer  :  cryptol@galois.com
    > -- Stability   :  provisional
    > -- Portability :  portable
    >
    > {-# LANGUAGE BlockArguments #-}
    > {-# LANGUAGE PatternGuards #-}
    > {-# LANGUAGE LambdaCase #-}
    > {-# LANGUAGE NamedFieldPuns #-}
    > {-# LANGUAGE ViewPatterns #-}
    >
    > module Cryptol.Eval.Reference
    >   ( Value(..)
    >   , E(..)
    >   , evaluate
    >   , evalExpr
    >   , evalDeclGroup
    >   , ppValue
    >   , ppEValue
    >   ) where
    >
    > import Data.Bits
    > import Data.Ratio((%))
    > import Data.List
    >   (genericIndex, genericLength, genericReplicate, genericTake, sortBy)
    > import Data.Ord (comparing)
    > import Data.Map (Map)
    > import qualified Data.Map as Map
    > import qualified Data.Text as T (pack)
    > import LibBF (BigFloat)
    > import qualified LibBF as FP
    > import qualified GHC.Num.Compat as Integer
    > import qualified Data.List as List
    >
    > import Cryptol.ModuleSystem.Name (asPrim)
    > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
    > import Cryptol.TypeCheck.AST
    > import Cryptol.Backend.FloatHelpers (BF(..))
    > import qualified Cryptol.Backend.FloatHelpers as FP
    > import Cryptol.Backend.Monad (EvalError(..))
    > import Cryptol.Eval.Type
    >   (TValue(..), isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)
    > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
    > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
    > import Cryptol.Utils.Panic (panic)
    > import Cryptol.Utils.PP
    > import Cryptol.Utils.RecordMap
    > import Cryptol.Eval (checkProp)
    > import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy)
    >
    > import qualified Cryptol.ModuleSystem as M
    > import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)

    Overview
    ========

    This file describes the semantics of the explicitly-typed Cryptol
    language (i.e., terms after type checking). Issues related to type
    inference, type functions, and type constraints are beyond the scope
    of this document.

    Cryptol Types
    -------------

    Cryptol types come in two kinds: numeric types (kind `#`) and value
    types (kind `*`). While value types are inhabited by well-typed
    Cryptol expressions, numeric types are only used as parameters to
    other types; they have no inhabitants. In this implementation we
    represent numeric types as values of the Haskell type `Nat'` of
    natural numbers with infinity; value types are represented as values
    of type `TValue`.

    The value types of Cryptol, along with their Haskell representations,
    are as follows:

    | Cryptol type      | Description       | `TValue` representation     |
    |:------------------|:------------------|:----------------------------|
    | `Bit`             | booleans          | `TVBit`                     |
    | `Integer`         | integers          | `TVInteger`                 |
    | `Z n`             | integers modulo n | `TVIntMod n`                |
    | `Rational`        | rationals         | `TVRational`                |
    | `Float e p`       | floating point    | `TVFloat`                   |
    | `Array`           | arrays            | `TVArray`                   |
    | `[n]a`            | finite lists      | `TVSeq n a`                 |
    | `[inf]a`          | infinite lists    | `TVStream a`                |
    | `(a, b, c)`       | tuples            | `TVTuple [a,b,c]`           |
    | `{x:a, y:b, z:c}` | records           | `TVRec [(x,a),(y,b),(z,c)]` |
    | `a -> b`          | functions         | `TVFun a b`                 |

    We model each (closed) Cryptol value type `t` as a complete partial order (cpo)
    *M*(`t`). The values of *M*(`t`) represent the _values_ present in the
    type `t`; we distinguish these from the _computations_ at type `t`.
    Operationally, the difference is that computations may raise errors or cause
    nontermination when evaluated; however, values are already evaluated, and will
    not cause errors or nontermination.  Denotationally, we represent this
    difference via a monad (in the style of Moggi) called *E*.  As an
    operation on CPOs, *E* adds a new bottom element representing
    nontermination, and a collection of erroneous values representing
    various runtime error conditions.

    To each Cryptol expression `e : t` we assign a meaning
    *M*(`e`) in *E*(*M*(`t`)); in particular, recursive Cryptol programs of
    type `t` are modeled as least fixed points in *E*(*M*(`t`)). In other words,
    this is a domain-theoretic denotational semantics.  Note, we do not requre
    CPOs defined via *M*(`t`) to have bottom elements, which is why we must take
    fixpoints in *E*. We cannot directly represent values without bottom in Haskell,
    so instead we are careful in this document only to write clearly-terminating
    functions, unless they represent computations under *E*.

    *M*(`Bit`) is a discrete cpo with values for `True`, `False`, which
    we simply represent in Haskell as `Bool`.
    Similarly, *M*(`Integer`) is a discrete cpo with values for integers,
    which we model as Haskell's `Integer`.  Likewise with the other
    base types.

    The value cpos for lists, tuples, and records are cartesian products
    of _computations_.  For example *M*(`(a,b)`) = *E*(*M*(`a`)) × *E*(*M*(`b`)).
    The cpo ordering is pointwise.  The trivial types `[0]t`,
    `()` and `{}` denote single-element cpos.  *M*(`a -> b`) is the
    continuous function space *E*(*M*(`a`)) $\to$ *E*(*M*(`b`)).

    Type schemas of the form `{a1 ... an} (p1 ... pk) => t` classify
    polymorphic values in Cryptol. These are represented with the Haskell
    type `Schema`. The meaning of a schema is cpo whose elements are
    functions: For each valid instantiation `t1 ... tn` of the type
    parameters `a1 ... an` that satisfies the constraints `p1 ... pk`, the
    function returns a value in *E*(*M*(`t[t1/a1 ... tn/an]`)).

    Computation Monad
    ------------------

    This monad represents either an evaluated thing of type `a`
    or an evaluation error. In the reference interpreter, only
    things under this monad should potentially result in errors
    or fail to terminate.

    > -- | Computation monad for the reference evaluator.
    > data E a = Value !a | Err EvalError
    >
    > instance Functor E where
    >   fmap :: forall a b. (a -> b) -> E a -> E b
    fmap a -> b
    f (Value a
    x) = b -> E b
    forall a. a -> E a
    Value (a -> b
    f a
    x)
    >   fmap a -> b
    _ (Err EvalError
    e)   = EvalError -> E b
    forall a. EvalError -> E a
    Err EvalError
    e

    > instance Applicative E where
    >   pure :: forall a. a -> E a
    pure a
    x = a -> E a
    forall a. a -> E a
    Value a
    x
    >   Err EvalError
    e   <*> :: forall a b. E (a -> b) -> E a -> E b
    <*> E a
    _       = EvalError -> E b
    forall a. EvalError -> E a
    Err EvalError
    e
    >   Value a -> b
    _ <*> Err EvalError
    e   = EvalError -> E b
    forall a. EvalError -> E a
    Err EvalError
    e
    >   Value a -> b
    f <*> Value a
    x = b -> E b
    forall a. a -> E a
    Value (a -> b
    f a
    x)

    > instance Monad E where
    >   E a
    m >>= :: forall a b. E a -> (a -> E b) -> E b
    >>= a -> E b
    f =
    >     case E a
    m of
    >       Value a
    x -> a -> E b
    f a
    x
    >       Err EvalError
    r   -> EvalError -> E b
    forall a. EvalError -> E a
    Err EvalError
    r
    >
    > eitherToE :: Either EvalError a -> E a
    > eitherToE :: forall a. Either EvalError a -> E a
    eitherToE (Left EvalError
    e)  = EvalError -> E a
    forall a. EvalError -> E a
    Err EvalError
    e
    > eitherToE (Right a
    x) = a -> E a
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x

    Values
    ------

    The Haskell code in this module defines the semantics of typed Cryptol
    terms by providing an evaluator to an appropriate `Value` type.

    > -- | Value type for the reference evaluator.
    > data Value
    >   = VBit !Bool                 -- ^ @ Bit    @ booleans
    >   | VInteger !Integer          -- ^ @ Integer @  or @Z n@ integers
    >   | VRational !Rational        -- ^ @ Rational @ rationals
    >   | VFloat !BF                 -- ^ Floating point numbers
    >   | VList Nat' [E Value]       -- ^ @ [n]a   @ finite or infinite lists
    >   | VTuple [E Value]           -- ^ @ ( .. ) @ tuples
    >   | VRecord [(Ident, E Value)] -- ^ @ { .. } @ records
    >   | VFun (E Value -> E Value)  -- ^ functions
    >   | VPoly (TValue -> E Value)  -- ^ polymorphic values (kind *)
    >   | VNumPoly (Nat' -> E Value) -- ^ polymorphic values (kind #)

    Operations on Values
    --------------------

    > -- | Destructor for @VBit@.
    > fromVBit :: Value -> Bool
    > fromVBit :: Value -> Bool
    fromVBit (VBit Bool
    b) = Bool
    b
    > fromVBit Value
    _        = String -> [String] -> Bool
    forall a. String -> [String] -> a
    evalPanic String
    "fromVBit" [String
    "Expected a bit"]
    >
    > -- | Destructor for @VInteger@.
    > fromVInteger :: Value -> Integer
    > fromVInteger :: Value -> Integer
    fromVInteger (VInteger Integer
    i) = Integer
    i
    > fromVInteger Value
    _            = String -> [String] -> Integer
    forall a. String -> [String] -> a
    evalPanic String
    "fromVInteger" [String
    "Expected an integer"]
    >
    > -- | Destructor for @VRational@.
    > fromVRational :: Value -> Rational
    > fromVRational :: Value -> Rational
    fromVRational (VRational Rational
    i) = Rational
    i
    > fromVRational Value
    _             = String -> [String] -> Rational
    forall a. String -> [String] -> a
    evalPanic String
    "fromVRational" [String
    "Expected a rational"]
    >
    > fromVFloat :: Value -> BigFloat
    > fromVFloat :: Value -> BigFloat
    fromVFloat = BF -> BigFloat
    bfValue (BF -> BigFloat) -> (Value -> BF) -> Value -> BigFloat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> BF
    fromVFloat'
    >
    > fromVFloat' :: Value -> BF
    > fromVFloat' :: Value -> BF
    fromVFloat' Value
    v =
    >   case Value
    v of
    >     VFloat BF
    f -> BF
    f
    >     Value
    _ -> String -> [String] -> BF
    forall a. String -> [String] -> a
    evalPanic String
    "fromVFloat" [ String
    "Expected a floating point value." ]
    >
    > -- | Destructor for @VList@.
    > fromVList :: Value -> [E Value]
    > fromVList :: Value -> [E Value]
    fromVList (VList Nat'
    _ [E Value]
    vs) = [E Value]
    vs
    > fromVList Value
    _            = String -> [String] -> [E Value]
    forall a. String -> [String] -> a
    evalPanic String
    "fromVList" [String
    "Expected a list"]
    >
    > -- | Destructor for @VTuple@.
    > fromVTuple :: Value -> [E Value]
    > fromVTuple :: Value -> [E Value]
    fromVTuple (VTuple [E Value]
    vs) = [E Value]
    vs
    > fromVTuple Value
    _           = String -> [String] -> [E Value]
    forall a. String -> [String] -> a
    evalPanic String
    "fromVTuple" [String
    "Expected a tuple"]
    >
    > -- | Destructor for @VRecord@.
    > fromVRecord :: Value -> [(Ident, E Value)]
    > fromVRecord :: Value -> [(Ident, E Value)]
    fromVRecord (VRecord [(Ident, E Value)]
    fs) = [(Ident, E Value)]
    fs
    > fromVRecord Value
    _            = String -> [String] -> [(Ident, E Value)]
    forall a. String -> [String] -> a
    evalPanic String
    "fromVRecord" [String
    "Expected a record"]
    >
    > -- | Destructor for @VFun@.
    > fromVFun :: Value -> (E Value -> E Value)
    > fromVFun :: Value -> E Value -> E Value
    fromVFun (VFun E Value -> E Value
    f) = E Value -> E Value
    f
    > fromVFun Value
    _        = String -> [String] -> E Value -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "fromVFun" [String
    "Expected a function"]
    >
    > -- | Look up a field in a record.
    > lookupRecord :: Ident -> Value -> E Value
    > lookupRecord :: Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    v =
    >   case Ident -> [(Ident, E Value)] -> Maybe (E Value)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Ident
    f (Value -> [(Ident, E Value)]
    fromVRecord Value
    v) of
    >     Just E Value
    val -> E Value
    val
    >     Maybe (E Value)
    Nothing  -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "lookupRecord" [String
    "Malformed record"]
    >
    > -- | Polymorphic function values that expect a finite numeric type.
    > vFinPoly :: (Integer -> E Value) -> Value
    > vFinPoly :: (Integer -> E Value) -> Value
    vFinPoly Integer -> E Value
    f = (Nat' -> E Value) -> Value
    VNumPoly Nat' -> E Value
    g
    >   where
    >     g :: Nat' -> E Value
    g (Nat Integer
    n) = Integer -> E Value
    f Integer
    n
    >     g Nat'
    Inf     = String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "vFinPoly" [String
    "Expected finite numeric type"]

    Environments
    ------------

    An evaluation environment keeps track of the values of term variables
    and type variables that are in scope at any point.

    > data Env = Env
    >   { Env -> Map Name (E Value)
    envVars       :: !(Map Name (E Value))
    >   , Env -> TypeEnv
    envTypes      :: !TypeEnv
    >   }
    >
    > instance Semigroup Env where
    >   Env
    l <> :: Env -> Env -> Env
    <> Env
    r = Env
    >     { envVars :: Map Name (E Value)
    envVars  = Env -> Map Name (E Value)
    envVars  Env
    l Map Name (E Value) -> Map Name (E Value) -> Map Name (E Value)
    forall a. Semigroup a => a -> a -> a
    <> Env -> Map Name (E Value)
    envVars  Env
    r
    >     , envTypes :: TypeEnv
    envTypes = Env -> TypeEnv
    envTypes Env
    l TypeEnv -> TypeEnv -> TypeEnv
    forall a. Semigroup a => a -> a -> a
    <> Env -> TypeEnv
    envTypes Env
    r
    >     }
    >
    > instance Monoid Env where
    >   mempty :: Env
    mempty = Env
    >     { envVars :: Map Name (E Value)
    envVars  = Map Name (E Value)
    forall a. Monoid a => a
    mempty
    >     , envTypes :: TypeEnv
    envTypes = TypeEnv
    forall a. Monoid a => a
    mempty
    >     }
    >   mappend :: Env -> Env -> Env
    mappend = Env -> Env -> Env
    forall a. Semigroup a => a -> a -> a
    (<>)
    >
    > -- | Bind a variable in the evaluation environment.
    > bindVar :: (Name, E Value) -> Env -> Env
    > bindVar :: (Name, E Value) -> Env -> Env
    bindVar (Name
    n, E Value
    val) Env
    env = Env
    env { envVars :: Map Name (E Value)
    envVars = Name -> E Value -> Map Name (E Value) -> Map Name (E Value)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n E Value
    val (Env -> Map Name (E Value)
    envVars Env
    env) }
    >
    > -- | Bind a type variable of kind # or *.
    > bindType :: TVar -> Either Nat' TValue -> Env -> Env
    > bindType :: TVar -> Either Nat' TValue -> Env -> Env
    bindType TVar
    p Either Nat' TValue
    ty Env
    env = Env
    env { envTypes :: TypeEnv
    envTypes = TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
    bindTypeVar TVar
    p Either Nat' TValue
    ty (Env -> TypeEnv
    envTypes Env
    env) }

    Evaluation
    ==========

    The meaning *M*(`expr`) of a Cryptol expression `expr` is defined by
    recursion over its structure. For an expression that contains free
    variables, the meaning also depends on the environment `env`, which
    assigns values to those variables.

    > evalExpr :: Env     -- ^ Evaluation environment
    >          -> Expr    -- ^ Expression to evaluate
    >          -> E Value
    > evalExpr :: Env -> Expr -> E Value
    evalExpr Env
    env Expr
    expr =
    >   case Expr
    expr of
    >
    >     ELocated Range
    _ Expr
    e -> Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e
    >
    >     EList [Expr]
    es Prop
    _ty  ->
    >       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat ([Expr] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Expr]
    es)) [ Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e | Expr
    e <- [Expr]
    es ]
    >
    >     ETuple [Expr]
    es     ->
    >       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [E Value] -> Value
    VTuple [ Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e | Expr
    e <- [Expr]
    es ]
    >
    >     ERec RecordMap Ident Expr
    fields   ->
    >       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord [ (Ident
    f, Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e) | (Ident
    f, Expr
    e) <- RecordMap Ident Expr -> [(Ident, Expr)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident Expr
    fields ]
    >
    >     ESel Expr
    e Selector
    sel    ->
    >       Selector -> Value -> E Value
    evalSel Selector
    sel (Value -> E Value) -> E Value -> E Value
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e
    >
    >     ESet Prop
    ty Expr
    e Selector
    sel Expr
    v ->
    >       TValue -> E Value -> Selector -> E Value -> E Value
    evalSet (TypeEnv -> Prop -> TValue
    evalValType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty)
    >               (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e) Selector
    sel (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    v)
    >
    >     EIf Expr
    c Expr
    t Expr
    f ->
    >       E Bool -> E Value -> E Value -> E Value
    condValue (Value -> Bool
    fromVBit (Value -> Bool) -> E Value -> E Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Env -> Expr -> E Value
    evalExpr Env
    env Expr
    c) (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    t) (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    f)
    >
    >     EComp Prop
    _n Prop
    _ty Expr
    e [[Match]]
    branches -> Env -> Expr -> [[Match]] -> E Value
    evalComp Env
    env Expr
    e [[Match]]
    branches
    >
    >     EVar Name
    n ->
    >       case Name -> Map Name (E Value) -> Maybe (E Value)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n (Env -> Map Name (E Value)
    envVars Env
    env) of
    >         Just E Value
    val -> E Value
    val
    >         Maybe (E Value)
    Nothing  ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalExpr" [String
    "var `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "` is not defined" ]
    >
    >     ETAbs TParam
    tv Expr
    b ->
    >       case TParam -> Kind
    tpKind TParam
    tv of
    >         Kind
    KType -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty ->
    >                    Env -> Expr -> E Value
    evalExpr (TVar -> Either Nat' TValue -> Env -> Env
    bindType (TParam -> TVar
    tpVar TParam
    tv) (TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right TValue
    ty) Env
    env) Expr
    b
    >         Kind
    KNum  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n ->
    >                    Env -> Expr -> E Value
    evalExpr (TVar -> Either Nat' TValue -> Env -> Env
    bindType (TParam -> TVar
    tpVar TParam
    tv) (Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left Nat'
    n) Env
    env) Expr
    b
    >         Kind
    k     -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalExpr" [String
    "Invalid kind on type abstraction", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]
    >
    >     ETApp Expr
    e Prop
    ty ->
    >       Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e E Value -> (Value -> E Value) -> E Value
    forall a b. E a -> (a -> E b) -> E b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
    >         VPoly TValue -> E Value
    f     -> TValue -> E Value
    f (TValue -> E Value) -> TValue -> E Value
    forall a b. (a -> b) -> a -> b
    $! (TypeEnv -> Prop -> TValue
    evalValType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty)
    >         VNumPoly Nat' -> E Value
    f  -> Nat' -> E Value
    f (Nat' -> E Value) -> Nat' -> E Value
    forall a b. (a -> b) -> a -> b
    $! (TypeEnv -> Prop -> Nat'
    evalNumType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty)
    >         Value
    _           -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalExpr" [String
    "Expected a polymorphic value"]
    >
    >     EApp Expr
    e1 Expr
    e2     -> E Value -> E Value -> E Value
    appFun (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e1) (Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e2)
    >     EAbs Name
    n Prop
    _ty Expr
    b   -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun (\E Value
    v -> Env -> Expr -> E Value
    evalExpr ((Name, E Value) -> Env -> Env
    bindVar (Name
    n, E Value
    v) Env
    env) Expr
    b)
    >     EProofAbs Prop
    _ Expr
    e  -> Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e
    >     EProofApp Expr
    e    -> Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e
    >     EWhere Expr
    e [DeclGroup]
    dgs   -> Env -> Expr -> E Value
    evalExpr ((Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Env -> DeclGroup -> Env
    evalDeclGroup Env
    env [DeclGroup]
    dgs) Expr
    e
    >
    >     EPropGuards [([Prop], Expr)]
    guards Prop
    _ty ->
    >       case (([Prop], Expr) -> Bool)
    -> [([Prop], Expr)] -> Maybe ([Prop], Expr)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Prop -> Bool) -> [Prop] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Prop -> Bool
    checkProp (Prop -> Bool) -> (Prop -> Prop) -> Prop -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env -> Prop -> Prop
    evalProp Env
    env) ([Prop] -> Bool)
    -> (([Prop], Expr) -> [Prop]) -> ([Prop], Expr) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Prop], Expr) -> [Prop]
    forall a b. (a, b) -> a
    fst) [([Prop], Expr)]
    guards of
    >         Just ([Prop]
    _, Expr
    e) -> Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e
    >         Maybe ([Prop], Expr)
    Nothing -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "fromVBit" [String
    "No guard constraint was satisfied"]

    > appFun :: E Value -> E Value -> E Value
    > appFun :: E Value -> E Value -> E Value
    appFun E Value
    f E Value
    v = E Value
    f E Value -> (Value -> E Value) -> E Value
    forall a b. E a -> (a -> E b) -> E b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Value
    f' -> Value -> E Value -> E Value
    fromVFun Value
    f' E Value
    v

    > -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables
    > -- according to `envTypes` and expanding all type synonyms via `tNoUser`.
    > evalProp :: Env -> Prop -> Prop
    > evalProp :: Env -> Prop -> Prop
    evalProp env :: Env
    env@Env { TypeEnv
    envTypes :: Env -> TypeEnv
    envTypes :: TypeEnv
    envTypes } = \case
    >   TCon TCon
    tc [Prop]
    tys -> TCon -> [Prop] -> Prop
    TCon TCon
    tc (Either Nat' TValue -> Prop
    toType (Either Nat' TValue -> Prop)
    -> (Prop -> Either Nat' TValue) -> Prop -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeEnv -> Prop -> Either Nat' TValue
    evalType TypeEnv
    envTypes (Prop -> Prop) -> [Prop] -> [Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Prop]
    tys)
    >   TVar TVar
    tv | Just (Either Nat' TValue -> Prop
    toType -> Prop
    ty) <- TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    envTypes -> Prop
    ty
    >   prop :: Prop
    prop@TUser {} -> Env -> Prop -> Prop
    evalProp Env
    env (Prop -> Prop
    tNoUser Prop
    prop)
    >   TVar TVar
    tv | Maybe (Either Nat' TValue)
    Nothing <- TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    envTypes -> String -> [String] -> Prop
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "evalProp" [String
    "Could not find type variable `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ TVar -> String
    forall a. PP a => a -> String
    pretty TVar
    tv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "` in the type evaluation environment"]
    >   Prop
    prop -> String -> [String] -> Prop
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "evalProp" [String
    "Cannot use the following as a type constraint: `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Prop -> String
    forall a. PP a => a -> String
    pretty Prop
    prop String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "`"]
    >   where
    >     toType :: Either Nat' TValue -> Prop
    toType = (Nat' -> Prop) -> (TValue -> Prop) -> Either Nat' TValue -> Prop
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either Nat' -> Prop
    tNumTy TValue -> Prop
    tValTy

    Selectors
    ---------

    Apply the the given selector form to the given value.
    Note that record selectors work uniformly on both record
    types and on newtypes.

    > evalSel :: Selector -> Value -> E Value
    > evalSel :: Selector -> Value -> E Value
    evalSel Selector
    sel Value
    val =
    >   case Selector
    sel of
    >     TupleSel Int
    n Maybe Int
    _  -> Int -> Value -> E Value
    tupleSel Int
    n Value
    val
    >     RecordSel Ident
    n Maybe [Ident]
    _ -> Ident -> Value -> E Value
    recordSel Ident
    n Value
    val
    >     ListSel Int
    n Maybe Int
    _   -> Int -> Value -> E Value
    listSel Int
    n Value
    val
    >   where
    >     tupleSel :: Int -> Value -> E Value
    tupleSel Int
    n Value
    v =
    >       case Value
    v of
    >         VTuple [E Value]
    vs   -> [E Value]
    vs [E Value] -> Int -> E Value
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n
    >         Value
    _           -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalSel"
    >                        [String
    "Unexpected value in tuple selection."]
    >     recordSel :: Ident -> Value -> E Value
    recordSel Ident
    n Value
    v =
    >       case Value
    v of
    >         VRecord [(Ident, E Value)]
    _   -> Ident -> Value -> E Value
    lookupRecord Ident
    n Value
    v
    >         Value
    _           -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalSel"
    >                        [String
    "Unexpected value in record selection."]
    >     listSel :: Int -> Value -> E Value
    listSel Int
    n Value
    v =
    >       case Value
    v of
    >         VList Nat'
    _ [E Value]
    vs  -> [E Value]
    vs [E Value] -> Int -> E Value
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n
    >         Value
    _           -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalSel"
    >                        [String
    "Unexpected value in list selection."]

    Update the given value using the given selector and new value.
    Note that record selectors work uniformly on both record
    types and on newtypes.

    > evalSet :: TValue -> E Value -> Selector -> E Value -> E Value
    > evalSet :: TValue -> E Value -> Selector -> E Value -> E Value
    evalSet TValue
    tyv E Value
    val Selector
    sel E Value
    fval =
    >   case (TValue
    tyv, Selector
    sel) of
    >     (TVTuple [TValue]
    ts, TupleSel Int
    n Maybe Int
    _) -> [TValue] -> Int -> E Value
    forall {f :: * -> *} {i} {b}.
    (Applicative f, Integral i) =>
    [b] -> i -> f Value
    updTupleAt [TValue]
    ts Int
    n
    >     (TVRec RecordMap Ident TValue
    fs, RecordSel Ident
    n Maybe [Ident]
    _)  -> RecordMap Ident TValue -> Ident -> E Value
    forall {f :: * -> *} {b}.
    Applicative f =>
    RecordMap Ident b -> Ident -> f Value
    updRecAt RecordMap Ident TValue
    fs Ident
    n
    >     (TVNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident TValue
    fs, RecordSel Ident
    n Maybe [Ident]
    _) -> RecordMap Ident TValue -> Ident -> E Value
    forall {f :: * -> *} {b}.
    Applicative f =>
    RecordMap Ident b -> Ident -> f Value
    updRecAt RecordMap Ident TValue
    fs Ident
    n
    >     (TVSeq Integer
    len TValue
    _, ListSel Int
    n Maybe Int
    _) -> Integer -> Int -> E Value
    forall {f :: * -> *} {a}.
    (Applicative f, Integral a) =>
    Integer -> a -> f Value
    updSeqAt Integer
    len Int
    n
    >     (TValue
    _, Selector
    _) -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalSet" [String
    "type/selector mismatch", TValue -> String
    forall a. Show a => a -> String
    show TValue
    tyv, Selector -> String
    forall a. Show a => a -> String
    show Selector
    sel]
    >   where
    >     updTupleAt :: [b] -> i -> f Value
    updTupleAt [b]
    ts i
    n =
    >       Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> f Value) -> Value -> f Value
    forall a b. (a -> b) -> a -> b
    $ [E Value] -> Value
    VTuple
    >           [ if i
    i i -> i -> Bool
    forall a. Eq a => a -> a -> Bool
    == i
    n then E Value
    fval else
    >               do [E Value]
    vs <- Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >                  [E Value] -> i -> E Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [E Value]
    vs i
    i
    >           | (i
    i,b
    _t) <- [i] -> [b] -> [(i, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [i
    0 ..] [b]
    ts
    >           ]
    >
    >     updRecAt :: RecordMap Ident b -> Ident -> f Value
    updRecAt RecordMap Ident b
    fs Ident
    n =
    >       Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> f Value) -> Value -> f Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord
    >           [ (Ident
    f, if Ident
    f Ident -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ident
    n then E Value
    fval else Ident -> Value -> E Value
    lookupRecord Ident
    f (Value -> E Value) -> E Value -> E Value
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    val)
    >           | (Ident
    f, b
    _t) <- RecordMap Ident b -> [(Ident, b)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident b
    fs
    >           ]
    >
    >     updSeqAt :: Integer -> a -> f Value
    updSeqAt Integer
    len a
    n =
    >       Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> f Value) -> Value -> f Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    len) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >         if Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n then E Value
    fval else
    >              do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >                 Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    len) [E Value]
    vs Integer
    i

    Conditionals
    ------------

    Conditionals are explicitly lazy: Run-time errors in an untaken branch
    are ignored.

    > condValue :: E Bool -> E Value -> E Value -> E Value
    > condValue :: E Bool -> E Value -> E Value -> E Value
    condValue E Bool
    c E Value
    l E Value
    r = E Bool
    c E Bool -> (Bool -> E Value) -> E Value
    forall a b. E a -> (a -> E b) -> E b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Bool
    b -> if Bool
    b then E Value
    l else E Value
    r

    List Comprehensions
    -------------------

    Cryptol list comprehensions consist of one or more parallel branches;
    each branch has one or more matches that bind values to variables.

    The result of evaluating a match in an initial environment is a list
    of extended environments. Each new environment binds the same single
    variable to a different element of the match's list.

    > evalMatch :: Env -> Match -> [Env]
    > evalMatch :: Env -> Match -> [Env]
    evalMatch Env
    env Match
    m =
    >   case Match
    m of
    >     Let Decl
    d -> [ (Name, E Value) -> Env -> Env
    bindVar (Env -> Decl -> (Name, E Value)
    evalDecl Env
    env Decl
    d) Env
    env ]
    >     From Name
    nm Prop
    len Prop
    _ty Expr
    expr -> [ (Name, E Value) -> Env -> Env
    bindVar (Name
    nm, Integer -> E Value
    forall {i}. Integral i => i -> E Value
    get Integer
    i) Env
    env | Integer
    i <- [Integer]
    idxs ]
    >      where
    >       get :: i -> E Value
    get i
    i =
    >         do Value
    v <- Env -> Expr -> E Value
    evalExpr Env
    env Expr
    expr
    >            [E Value] -> i -> E Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex (Value -> [E Value]
    fromVList Value
    v) i
    i
    >
    >       idxs :: [Integer]
    >       idxs :: [Integer]
    idxs =
    >         case TypeEnv -> Prop -> Nat'
    evalNumType (Env -> TypeEnv
    envTypes Env
    env) Prop
    len of
    >         Nat'
    Inf   -> [Integer
    0 ..]
    >         Nat Integer
    n -> [Integer
    0 .. Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]

    > lenMatch :: Env -> Match -> Nat'
    > lenMatch :: Env -> Match -> Nat'
    lenMatch Env
    env Match
    m =
    >   case Match
    m of
    >     Let Decl
    _          -> Integer -> Nat'
    Nat Integer
    1
    >     From Name
    _ Prop
    len Prop
    _ Expr
    _ -> TypeEnv -> Prop -> Nat'
    evalNumType (Env -> TypeEnv
    envTypes Env
    env) Prop
    len

    The result of of evaluating a branch in an initial environment is a
    list of extended environments, each of which extends the initial
    environment with the same set of new variables. The length of the list
    is equal to the product of the lengths of the lists in the matches.

    > evalBranch :: Env -> [Match] -> [Env]
    > evalBranch :: Env -> [Match] -> [Env]
    evalBranch Env
    env [] = [Env
    env]
    > evalBranch Env
    env (Match
    match : [Match]
    matches) =
    >   [ Env
    env'' | Env
    env' <- Env -> Match -> [Env]
    evalMatch Env
    env Match
    match
    >           , Env
    env'' <- Env -> [Match] -> [Env]
    evalBranch Env
    env' [Match]
    matches ]

    > lenBranch :: Env -> [Match] -> Nat'
    > lenBranch :: Env -> [Match] -> Nat'
    lenBranch Env
    _env [] = Integer -> Nat'
    Nat Integer
    1
    > lenBranch Env
    env (Match
    match : [Match]
    matches) =
    >   Nat' -> Nat' -> Nat'
    nMul (Env -> Match -> Nat'
    lenMatch Env
    env Match
    match) (Env -> [Match] -> Nat'
    lenBranch Env
    env [Match]
    matches)

    The head expression of the comprehension can refer to any variable
    bound in any of the parallel branches. So to evaluate the
    comprehension, we zip and merge together the lists of extended
    environments from each branch. The head expression is then evaluated
    separately in each merged environment. The length of the resulting
    list is equal to the minimum length over all parallel branches.

    > evalComp :: Env         -- ^ Starting evaluation environment
    >          -> Expr        -- ^ Head expression of the comprehension
    >          -> [[Match]]   -- ^ List of parallel comprehension branches
    >          -> E Value
    > evalComp :: Env -> Expr -> [[Match]] -> E Value
    evalComp Env
    env Expr
    expr [[Match]]
    branches =
    >     Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList Nat'
    len [ Env -> Expr -> E Value
    evalExpr Env
    e Expr
    expr | Env
    e <- [Env]
    envs ]
    >   where
    >     -- Generate a new environment for each iteration of each
    >     -- parallel branch.
    >     benvs :: [[Env]]
    >     benvs :: [[Env]]
    benvs = ([Match] -> [Env]) -> [[Match]] -> [[Env]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Env -> [Match] -> [Env]
    evalBranch Env
    env) [[Match]]
    branches
    >
    >     -- Zip together the lists of environments from each branch,
    >     -- producing a list of merged environments. Longer branches get
    >     -- truncated to the length of the shortest branch.
    >     envs :: [Env]
    >     envs :: [Env]
    envs = ([Env] -> [Env] -> [Env]) -> [[Env]] -> [Env]
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 ((Env -> Env -> Env) -> [Env] -> [Env] -> [Env]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Env -> Env -> Env
    forall a. Monoid a => a -> a -> a
    mappend) [[Env]]
    benvs
    >
    >     len :: Nat'
    >     len :: Nat'
    len = (Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Nat' -> Nat' -> Nat'
    nMin (([Match] -> Nat') -> [[Match]] -> [Nat']
    forall a b. (a -> b) -> [a] -> [b]
    map (Env -> [Match] -> Nat'
    lenBranch Env
    env) [[Match]]
    branches)

    Declarations
    ------------

    Function `evalDeclGroup` extends the given evaluation environment with
    the result of evaluating the given declaration group. In the case of a
    recursive declaration group, we tie the recursive knot by evaluating
    each declaration in the extended environment `env'` that includes all
    the new bindings.

    > evalDeclGroup :: Env -> DeclGroup -> Env
    > evalDeclGroup :: Env -> DeclGroup -> Env
    evalDeclGroup Env
    env DeclGroup
    dg = do
    >   case DeclGroup
    dg of
    >     NonRecursive Decl
    d ->
    >       (Name, E Value) -> Env -> Env
    bindVar (Env -> Decl -> (Name, E Value)
    evalDecl Env
    env Decl
    d) Env
    env
    >     Recursive [Decl]
    ds ->
    >       let env' :: Env
    env' = ((Name, E Value) -> Env -> Env) -> Env -> [(Name, E Value)] -> Env
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, E Value) -> Env -> Env
    bindVar Env
    env [(Name, E Value)]
    bindings
    >           bindings :: [(Name, E Value)]
    bindings = (Decl -> (Name, E Value)) -> [Decl] -> [(Name, E Value)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Env -> Decl -> (Name, E Value)
    evalDecl Env
    env') [Decl]
    ds
    >       in Env
    env'
    >
    > evalDecl :: Env -> Decl -> (Name, E Value)
    > evalDecl :: Env -> Decl -> (Name, E Value)
    evalDecl Env
    env Decl
    d =
    >   case Decl -> DeclDef
    dDefinition Decl
    d of
    >     DeclDef
    DPrim      -> (Decl -> Name
    dName Decl
    d, Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Name -> Value
    evalPrim (Decl -> Name
    dName Decl
    d)))
    >     DForeign FFIFunType
    _ -> (Decl -> Name
    dName Decl
    d, EvalError -> E Value
    forall a. EvalError -> E a
    cryError (EvalError -> E Value) -> EvalError -> E Value
    forall a b. (a -> b) -> a -> b
    $ Name -> EvalError
    FFINotSupported (Name -> EvalError) -> Name -> EvalError
    forall a b. (a -> b) -> a -> b
    $ Decl -> Name
    dName Decl
    d)
    >     DExpr Expr
    e    -> (Decl -> Name
    dName Decl
    d, Env -> Expr -> E Value
    evalExpr Env
    env Expr
    e)
    >

    Newtypes
    --------

    At runtime, newtypes values are represented in exactly
    the same way as records.  The constructor function for
    newtypes is thus basically just an identity function
    that consumes and ignores its type arguments.

    > evalNewtypeDecl :: Env -> Newtype -> Env
    > evalNewtypeDecl :: Env -> Newtype -> Env
    evalNewtypeDecl Env
    env Newtype
    nt = (Name, E Value) -> Env -> Env
    bindVar (Newtype -> Name
    ntConName Newtype
    nt, Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Value
    val) Env
    env
    >   where
    >     val :: Value
    val = (TParam -> Value -> Value) -> Value -> [TParam] -> Value
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Value -> Value
    tabs Value
    con (Newtype -> [TParam]
    ntParams Newtype
    nt)
    >     con :: Value
    con = (E Value -> E Value) -> Value
    VFun (\E Value
    x -> E Value
    x)
    >     tabs :: TParam -> Value -> Value
    tabs TParam
    tp Value
    body =
    >       case TParam -> Kind
    tpKind TParam
    tp of
    >         Kind
    KType -> (TValue -> E Value) -> Value
    VPoly (\TValue
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Value
    body)
    >         Kind
    KNum  -> (Nat' -> E Value) -> Value
    VNumPoly (\Nat'
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Value
    body)
    >         Kind
    k -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalNewtypeDecl" [String
    "illegal newtype parameter kind", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]

    Primitives
    ==========

    To evaluate a primitive, we look up its implementation by name in a table.

    > evalPrim :: Name -> Value
    > evalPrim :: Name -> Value
    evalPrim Name
    n
    >   | Just PrimIdent
    i <- Name -> Maybe PrimIdent
    asPrim Name
    n, Just Value
    v <- PrimIdent -> Map PrimIdent Value -> Maybe Value
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup PrimIdent
    i Map PrimIdent Value
    primTable = Value
    v
    >   | Bool
    otherwise = String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "evalPrim" [String
    "Unimplemented primitive", Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n)]

    Cryptol primitives fall into several groups, mostly delineated
    by corresponding type classes:

    * Literals: `True`, `False`, `number`, `ratio`

    * Zero: zero

    * Logic: `&&`, `||`, `^`, `complement`

    * Ring: `+`, `-`, `*`, `negate`, `fromInteger`

    * Integral: `/`, `%`, `^^`, `toInteger`

    * Bitvector: `/$` `%$`, `lg2`, `<=$`

    * Comparison: `<`, `>`, `<=`, `>=`, `==`, `!=`

    * Sequences: `#`, `join`, `split`, `take`, `drop`, `reverse`, `transpose`

    * Shifting: `<<`, `>>`, `<<<`, `>>>`

    * Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`

    * Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `fromToBy`,
                    `fromToByLessThan`, `fromToDownBy`, `fromToDownByGreaterThan`,
                    `infFrom`, `infFromThen`

    * Polynomials: `pmult`, `pdiv`, `pmod`

    * Miscellaneous: `error`, `random`, `trace`

    > primTable :: Map PrimIdent Value
    > primTable :: Map PrimIdent Value
    primTable = [Map PrimIdent Value] -> Map PrimIdent Value
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions
    >               [ Map PrimIdent Value
    cryptolPrimTable
    >               , Map PrimIdent Value
    floatPrimTable
    >               ]

    > infixr 0 ~>
    > (~>) :: String -> a -> (String,a)
    > String
    nm ~> :: forall a. String -> a -> (String, a)
    ~> a
    v = (String
    nm,a
    v)

    > cryptolPrimTable :: Map PrimIdent Value
    > cryptolPrimTable :: Map PrimIdent Value
    cryptolPrimTable = [(PrimIdent, Value)] -> Map PrimIdent Value
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Value)] -> Map PrimIdent Value)
    -> [(PrimIdent, Value)] -> Map PrimIdent Value
    forall a b. (a -> b) -> a -> b
    $ ((String, Value) -> (PrimIdent, Value))
    -> [(String, Value)] -> [(PrimIdent, Value)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(String
    n, Value
    v) -> (Text -> PrimIdent
    prelPrim (String -> Text
    T.pack String
    n), Value
    v))
    >
    >   -- Literals
    >   [ String
    "True"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> Bool -> Value
    VBit Bool
    True
    >   , String
    "False"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> Bool -> Value
    VBit Bool
    False
    >   , String
    "number"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    val -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    a ->
    >                     Integer -> TValue -> E Value
    literal Integer
    val TValue
    a
    >   , String
    "fraction"   String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    top -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly \Integer
    bot -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly \Integer
    rnd -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    \TValue
    a   -> Integer -> Integer -> Integer -> TValue -> E Value
    fraction Integer
    top Integer
    bot Integer
    rnd TValue
    a
    >   -- Zero
    >   , String
    "zero"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly (Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> (TValue -> Value) -> TValue -> E Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TValue -> Value
    zero)
    >
    >   -- Logic (bitwise)
    >   , String
    "&&"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
    logicBinary Bool -> Bool -> Bool
    (&&))
    >   , String
    "||"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
    logicBinary Bool -> Bool -> Bool
    (||))
    >   , String
    "^"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
    logicBinary Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=))
    >   , String
    "complement" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary  ((Bool -> Bool) -> TValue -> E Value -> E Value
    logicUnary Bool -> Bool
    not)
    >
    >   -- Ring
    >   , String
    "+"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Integer -> Integer -> E Integer)
    -> (Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    ringBinary
    >                              (\Integer
    x Integer
    y -> Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    y))
    >                              (\Rational
    x Rational
    y -> Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational
    x Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    + Rational
    y))
    >                              ((BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfAdd RoundMode
    fpImplicitRound)
    >                            )
    >   , String
    "-"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Integer -> Integer -> E Integer)
    -> (Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    ringBinary
    >                               (\Integer
    x Integer
    y -> Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    y))
    >                               (\Rational
    x Rational
    y -> Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational
    x Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    - Rational
    y))
    >                               ((BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfSub RoundMode
    fpImplicitRound)
    >                             )
    >   , String
    "*"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary TValue -> E Value -> E Value -> E Value
    ringMul
    >   , String
    "negate"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary  ((Integer -> E Integer)
    -> (Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    ringUnary (\Integer
    x -> Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (- Integer
    x))
    >                                       (\Rational
    x -> Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (- Rational
    x))
    >                                       (\Integer
    _ Integer
    _ BigFloat
    x -> BigFloat -> E BigFloat
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> BigFloat
    FP.bfNeg BigFloat
    x)))
    >   , String
    "fromInteger"String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >                     E Integer
    -> E Rational
    -> (Integer -> Integer -> E BigFloat)
    -> TValue
    -> E Value
    ringNullary (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    x)
    >                                 (Integer -> Rational
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Rational) -> (Value -> Integer) -> Value -> Rational
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> Integer
    fromVInteger (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    x)
    >                                 (\Integer
    e Integer
    p -> Integer -> Integer -> Integer -> BigFloat
    fpFromInteger Integer
    e Integer
    p (Integer -> BigFloat) -> (Value -> Integer) -> Value -> BigFloat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> Integer
    fromVInteger (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    x)
    >                                 TValue
    a
    >
    >   -- Integral
    >   , String
    "toInteger"  String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >                     Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> E Value -> E Integer
    cryToInteger TValue
    a E Value
    x
    >   , String
    "/"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Integer -> Integer -> E Integer)
    -> TValue -> E Value -> E Value -> E Value
    integralBinary Integer -> Integer -> E Integer
    divWrap)
    >   , String
    "%"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Integer -> Integer -> E Integer)
    -> TValue -> E Value -> E Value -> E Value
    integralBinary Integer -> Integer -> E Integer
    modWrap)
    >   , String
    "^^"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    aty -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ety -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    e ->
    >                       TValue -> E Value -> Integer -> E Value
    ringExp TValue
    aty E Value
    a (Integer -> E Value) -> E Integer -> E Value
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TValue -> E Value -> E Integer
    cryToInteger TValue
    ety E Value
    e
    >
    >   -- Field
    >   , String
    "/."         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> Integer -> E Integer)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    fieldBinary Rational -> Rational -> E Rational
    ratDiv Integer -> Integer -> Integer -> E Integer
    zDiv
    >                                         ((BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv RoundMode
    fpImplicitRound)
    >                             )
    >
    >   , String
    "recip"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> E Rational)
    -> (Integer -> Integer -> E Integer)
    -> (Integer -> Integer -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    fieldUnary Rational -> E Rational
    ratRecip Integer -> Integer -> E Integer
    zRecip Integer -> Integer -> BigFloat -> E BigFloat
    fpRecip)
    >
    >   -- Round
    >   , String
    "floor"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor
    >                      (Either EvalError Integer -> E Integer
    forall a. Either EvalError a -> E a
    eitherToE (Either EvalError Integer -> E Integer)
    -> (BF -> Either EvalError Integer) -> BF -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    "floor" RoundMode
    FP.ToNegInf))
    >
    >   , String
    "ceiling"    String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling
    >                      (Either EvalError Integer -> E Integer
    forall a. Either EvalError a -> E a
    eitherToE (Either EvalError Integer -> E Integer)
    -> (BF -> Either EvalError Integer) -> BF -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    "ceiling" RoundMode
    FP.ToPosInf))
    >
    >   , String
    "trunc"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    truncate
    >                      (Either EvalError Integer -> E Integer
    forall a. Either EvalError a -> E a
    eitherToE (Either EvalError Integer -> E Integer)
    -> (BF -> Either EvalError Integer) -> BF -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    "trunc" RoundMode
    FP.ToZero))
    >
    >   , String
    "roundAway"  String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    roundAwayRat
    >                      (Either EvalError Integer -> E Integer
    forall a. Either EvalError a -> E a
    eitherToE (Either EvalError Integer -> E Integer)
    -> (BF -> Either EvalError Integer) -> BF -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    "roundAway" RoundMode
    FP.Away))
    >
    >   , String
    "roundToEven"String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value) -> Value
    unary ((Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    round
    >                      (Either EvalError Integer -> E Integer
    forall a. Either EvalError a -> E a
    eitherToE (Either EvalError Integer -> E Integer)
    -> (BF -> Either EvalError Integer) -> BF -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    "roundToEven" RoundMode
    FP.NearEven))
    >
    >
    >   -- Comparison
    >   , String
    "<"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    LT))
    >   , String
    ">"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    GT))
    >   , String
    "<="         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    GT))
    >   , String
    ">="         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    LT))
    >   , String
    "=="         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ))
    >   , String
    "!="         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder (\Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    EQ))
    >   , String
    "<$"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value -> E Value -> E Value) -> Value
    binary TValue -> E Value -> E Value -> E Value
    signedLessThan
    >
    >   -- Bitvector
    >   , String
    "/$"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    l -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    r ->
    >                       Integer -> Integer -> Value
    vWord Integer
    n (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    divWrap
    >                                          (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    l)
    >                                          (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    r)
    >   , String
    "%$"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    l -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    r ->
    >                       Integer -> Integer -> Value
    vWord Integer
    n (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    modWrap
    >                                          (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    l)
    >                                          (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    r)
    >   , String
    ">>$"        String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> Value
    signedShiftRV
    >   , String
    "lg2"        String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                       Integer -> Integer -> Value
    vWord Integer
    n (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> E Integer) -> E Integer -> E Integer
    forall a b. (a -> E b) -> E a -> E b
    appOp1 Integer -> E Integer
    lg2Wrap (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    v)
    >   -- Rational
    >   , String
    "ratio"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    l -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    r ->
    >                     Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Rational)
    -> E Integer -> E Integer -> E Rational
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Rational
    ratioOp
    >                                          (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l)
    >                                          (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >
    >   -- Z n
    >   , String
    "fromZ"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >                     Integer -> Value
    VInteger (Integer -> Value) -> (Value -> Integer) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    n (Integer -> Integer) -> (Value -> Integer) -> Value -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> Integer
    fromVInteger (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    x
    >
    >   -- Sequences
    >   , String
    "#"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    front -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    back  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _elty  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    l -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    r ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Nat' -> Nat' -> Nat'
    nAdd (Integer -> Nat'
    Nat Integer
    front) Nat'
    back) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                         if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    front then
    >                           do [E Value]
    l' <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l
    >                              Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    front) [E Value]
    l' Integer
    i
    >                          else
    >                           do [E Value]
    r' <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r
    >                              Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    back [E Value]
    r' (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    front)
    >
    >   , String
    "join"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    parts -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    each  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Nat' -> Nat' -> Nat'
    nMul Nat'
    parts (Integer -> Nat'
    Nat Integer
    each)) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                         do let (Integer
    q,Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    i Integer
    each
    >                            [E Value]
    xss <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                            [E Value]
    xs  <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    parts [E Value]
    xss Integer
    q
    >                            Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    each) [E Value]
    xs Integer
    r
    >
    >   , String
    "split"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    parts -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    each  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    val ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    parts ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                         Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    each) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    j ->
    >                           do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >                              Nat' -> [E Value] -> Integer -> E Value
    indexFront (Nat' -> Nat' -> Nat'
    nMul Nat'
    parts (Integer -> Nat'
    Nat Integer
    each)) [E Value]
    vs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    each Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    j)
    >
    >   , String
    "take"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    front -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    back  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun     ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    front ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                                do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                                   Nat' -> [E Value] -> Integer -> E Value
    indexFront (Nat' -> Nat' -> Nat'
    nAdd Nat'
    front Nat'
    back) [E Value]
    vs Integer
    i
    >
    >   , String
    "drop"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    front -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    back -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    back ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                                do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                                   Nat' -> [E Value] -> Integer -> E Value
    indexFront (Nat' -> Nat' -> Nat'
    nAdd (Integer -> Nat'
    Nat Integer
    front) Nat'
    back) [E Value]
    vs (Integer
    frontInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    i)
    >
    >   , String
    "reverse"    String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    n) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                         do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                            Nat' -> [E Value] -> Integer -> E Value
    indexBack (Integer -> Nat'
    Nat Integer
    n) [E Value]
    vs Integer
    i
    >
    >   , String
    "transpose"  String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    rows -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    cols -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    val ->
    >                       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    cols ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    c ->
    >                         Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    rows ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    r ->
    >                         do [E Value]
    xss <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >                            [E Value]
    xs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    rows [E Value]
    xss Integer
    r
    >                            Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    cols [E Value]
    xs Integer
    c
    >
    >   -- Shifting:
    >   , String
    "<<"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
    shiftV Nat' -> TValue -> E Value -> Integer -> Value
    shiftLV
    >   , String
    ">>"         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
    shiftV Nat' -> TValue -> E Value -> Integer -> Value
    shiftRV
    >   , String
    "<<<"        String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value -> Integer -> E Value) -> Value
    rotateV Integer -> E Value -> Integer -> E Value
    rotateLV
    >   , String
    ">>>"        String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value -> Integer -> E Value) -> Value
    rotateV Integer -> E Value -> Integer -> E Value
    rotateRV
    >
    >   -- Indexing:
    >   , String
    "@"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> [E Value] -> Integer -> E Value) -> Value
    indexPrimOne  Nat' -> [E Value] -> Integer -> E Value
    indexFront
    >   , String
    "!"          String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> [E Value] -> Integer -> E Value) -> Value
    indexPrimOne  Nat' -> [E Value] -> Integer -> E Value
    indexBack
    >   , String
    "update"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> Integer -> Integer) -> Value
    updatePrim Nat' -> Integer -> Integer
    updateFront
    >   , String
    "updateEnd"  String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> Integer -> Integer) -> Value
    updatePrim Nat' -> Integer -> Integer
    updateBack
    >
    >   -- Enumerations
    >   , String
    "fromTo"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    lst   -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat (Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    lst Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    first)) ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f [Integer
    first .. Integer
    lst])
    >
    >   , String
    "fromToLessThan" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    bound -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     case Nat'
    bound of
    >                       Nat'
    Inf -> Nat' -> [E Value] -> Value
    VList Nat'
    Inf ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f [Integer
    first ..])
    >                       Nat Integer
    bound' ->
    >                         let len :: Integer
    len = Integer
    bound' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    first in
    >                         Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f (Integer -> [Integer] -> [Integer]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [Integer
    first ..]))
    >
    >   , String
    "fromToBy"   String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    lst    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    stride -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty     -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     let vs :: [E Value]
    vs  = [ Integer -> E Value
    f (Integer
    first Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    stride) | Integer
    i <- [Integer
    0..] ] in
    >                     let len :: Integer
    len = Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + ((Integer
    lstInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    first) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    stride) in
    >                     Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) (Integer -> [E Value] -> [E Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [E Value]
    vs)
    >
    >   , String
    "fromToByLessThan" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    bound  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    stride -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty     -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     let vs :: [E Value]
    vs  = [ Integer -> E Value
    f (Integer
    first Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    stride) | Integer
    i <- [Integer
    0..] ] in
    >                     case Nat'
    bound of
    >                       Nat'
    Inf -> Nat' -> [E Value] -> Value
    VList Nat'
    Inf [E Value]
    vs
    >                       Nat Integer
    bound' ->
    >                         let len :: Integer
    len = (Integer
    bound'Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    firstInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    strideInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    stride in
    >                         Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) (Integer -> [E Value] -> [E Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [E Value]
    vs)
    >
    >   , String
    "fromToDownBy" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    lst    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    stride -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty     -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     let vs :: [E Value]
    vs  = [ Integer -> E Value
    f (Integer
    first Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    stride) | Integer
    i <- [Integer
    0..] ] in
    >                     let len :: Integer
    len = Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + ((Integer
    firstInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    lst) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    stride) in
    >                     Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) (Integer -> [E Value] -> [E Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [E Value]
    vs)
    >
    >   , String
    "fromToDownByGreaterThan" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    lst    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    stride -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty     -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     let vs :: [E Value]
    vs  = [ Integer -> E Value
    f (Integer
    first Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    stride) | Integer
    i <- [Integer
    0..] ] in
    >                     let len :: Integer
    len = (Integer
    firstInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    lstInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    strideInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    stride in
    >                     Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) (Integer -> [E Value] -> [E Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [E Value]
    vs)
    >
    >   , String
    "fromThenTo" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    first -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    next  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    _lst  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly    ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty    -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    len   -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal Integer
    i TValue
    ty in
    >                     Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len)
    >                           ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f (Integer -> [Integer] -> [Integer]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [Integer
    first, Integer
    next ..]))
    >
    >   , String
    "infFrom"    String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    first ->
    >                     do Integer
    x <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ty E Value
    first
    >                        let f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    i) TValue
    ty
    >                        Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList Nat'
    Inf ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f [Integer
    0 ..])
    >
    >   , String
    "infFromThen"String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    first -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    next ->
    >                     do Integer
    x <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ty E Value
    first
    >                        Integer
    y <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ty E Value
    next
    >                        let diff :: Integer
    diff = Integer
    y Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    x
    >                            f :: Integer -> E Value
    f Integer
    i = Integer -> TValue -> E Value
    literal (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    diff Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    i) TValue
    ty
    >                        Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList Nat'
    Inf ((Integer -> E Value) -> [Integer] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> E Value
    f [Integer
    0 ..])
    >
    >   -- Miscellaneous:
    >   , String
    "parmap"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _b -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    f -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    xs ->
    >                        do E Value -> E Value
    f' <- Value -> E Value -> E Value
    fromVFun (Value -> E Value -> E Value) -> E Value -> E (E Value -> E Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    f
    >                           [E Value]
    xs' <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    xs
    >                           -- Note: the reference implementation simply
    >                           -- executes parmap sequentially
    >                           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList Nat'
    n ((E Value -> E Value) -> [E Value] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map E Value -> E Value
    f' [E Value]
    xs')
    >
    >   , String
    "error"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    s ->
    >                       do String
    msg <- E Value -> E String
    evalString E Value
    s
    >                          EvalError -> E Value
    forall a. EvalError -> E a
    cryError (String -> EvalError
    UserError String
    msg)
    >
    >   , String
    "random"     String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    _seed -> EvalError -> E Value
    forall a. EvalError -> E a
    cryError (String -> EvalError
    UserError String
    "random: unimplemented")
    >
    >   , String
    "trace"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    _n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _b -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    s -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                     (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    y ->
    >                        do String
    _ <- E Value -> E String
    evalString E Value
    s -- evaluate and ignore s
    >                           Value
    _ <- E Value
    x -- evaluate and ignore x
    >                           E Value
    y
    >   ]
    >
    >
    > evalString :: E Value -> E String
    > evalString :: E Value -> E String
    evalString E Value
    v =
    >   do [E Value]
    cs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >      [Integer]
    ws <- (E Value -> E Integer) -> [E Value] -> E [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) [E Value]
    cs
    >      String -> E String
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Integer -> Char) -> [Integer] -> String
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger) [Integer]
    ws)
    >
    > unary :: (TValue -> E Value -> E Value) -> Value
    > unary :: (TValue -> E Value -> E Value) -> Value
    unary TValue -> E Value -> E Value
    f = (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >           (E Value -> E Value) -> Value
    VFun  ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x -> TValue -> E Value -> E Value
    f TValue
    ty E Value
    x
    >
    > binary :: (TValue -> E Value -> E Value -> E Value) -> Value
    > binary :: (TValue -> E Value -> E Value -> E Value) -> Value
    binary TValue -> E Value -> E Value -> E Value
    f = (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >            (E Value -> E Value) -> Value
    VFun  ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >            (E Value -> E Value) -> Value
    VFun  ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    y -> TValue -> E Value -> E Value -> E Value
    f TValue
    ty E Value
    x E Value
    y
    >
    > appOp1 :: (a -> E b) -> E a -> E b
    > appOp1 :: forall a b. (a -> E b) -> E a -> E b
    appOp1 a -> E b
    f E a
    x =
    >   do a
    x' <- E a
    x
    >      a -> E b
    f a
    x'
    >
    > appOp2 :: (a -> b -> E c) -> E a -> E b -> E c
    > appOp2 :: forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 a -> b -> E c
    f E a
    x E b
    y =
    >   do a
    x' <- E a
    x
    >      b
    y' <- E b
    y
    >      a -> b -> E c
    f a
    x' b
    y'

    Word operations
    ---------------

    Many Cryptol primitives take numeric arguments in the form of
    bitvectors. For such operations, any output bit that depends on the
    numeric value is strict in *all* bits of the numeric argument. This is
    implemented in function `fromVWord`, which converts a value from a
    big-endian binary format to an integer. The result is an evaluation
    error if any of the input bits contain an evaluation error.

    > fromVWord :: Value -> E Integer
    > fromVWord :: Value -> E Integer
    fromVWord Value
    v = [Bool] -> Integer
    bitsToInteger ([Bool] -> Integer) -> E [Bool] -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (E Value -> E Bool) -> [E Value] -> E [Bool]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Value -> Bool) -> E Value -> E Bool
    forall a b. (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Bool
    fromVBit) (Value -> [E Value]
    fromVList Value
    v)
    >
    > -- | Convert a list of booleans in big-endian format to an integer.
    > bitsToInteger :: [Bool] -> Integer
    > bitsToInteger :: [Bool] -> Integer
    bitsToInteger [Bool]
    bs = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Integer -> Bool -> Integer
    forall {a}. Num a => a -> Bool -> a
    f Integer
    0 [Bool]
    bs
    >   where f :: a -> Bool -> a
    f a
    x Bool
    b = if Bool
    b then a
    2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1 else a
    2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x

    > fromSignedVWord :: Value -> E Integer
    > fromSignedVWord :: Value -> E Integer
    fromSignedVWord Value
    v = [Bool] -> Integer
    signedBitsToInteger ([Bool] -> Integer) -> E [Bool] -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (E Value -> E Bool) -> [E Value] -> E [Bool]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Value -> Bool) -> E Value -> E Bool
    forall a b. (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Value -> Bool
    fromVBit) (Value -> [E Value]
    fromVList Value
    v)
    >
    > -- | Convert a list of booleans in signed big-endian format to an integer.
    > signedBitsToInteger :: [Bool] -> Integer
    > signedBitsToInteger :: [Bool] -> Integer
    signedBitsToInteger [] =
    >   String -> [String] -> Integer
    forall a. String -> [String] -> a
    evalPanic String
    "signedBitsToInteger" [String
    "Bitvector has zero length"]
    > signedBitsToInteger (Bool
    b0 : [Bool]
    bs) = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Integer -> Bool -> Integer
    forall {a}. Num a => a -> Bool -> a
    f (if Bool
    b0 then -Integer
    1 else Integer
    0) [Bool]
    bs
    >   where f :: a -> Bool -> a
    f a
    x Bool
    b = if Bool
    b then a
    2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1 else a
    2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x

    Function `vWord` converts an integer back to the big-endian bitvector
    representation.

    > vWord :: Integer -> Integer -> Value
    > vWord :: Integer -> Integer -> Value
    vWord Integer
    w Integer
    e
    >   | Integer
    w Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) =
    >       String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "vWord" [String
    "Word length too large", Integer -> String
    forall a. Show a => a -> String
    show Integer
    w]
    >   | Bool
    otherwise =
    >       Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) [ Integer -> E Value
    forall {f :: * -> *}. Applicative f => Integer -> f Value
    mkBit Integer
    i | Integer
    i <- [Integer
    wInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1, Integer
    wInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    2 .. Integer
    0 ] ]
    >  where
    >    mkBit :: Integer -> f Value
    mkBit Integer
    i = Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Value
    VBit (Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    e (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)))

    Errors
    ------

    > cryError :: EvalError -> E a
    > cryError :: forall a. EvalError -> E a
    cryError EvalError
    e = EvalError -> E a
    forall a. EvalError -> E a
    Err EvalError
    e

    Zero
    ----

    The `Zero` class has a single method `zero` which computes
    a zero value for all the built-in types for Cryptol.
    For bits, bitvectors and the base numeric types, this
    returns the obvious 0 representation.  For sequences, records,
    and tuples, the zero method operates pointwise the underlying types.
    For functions, `zero` returns the constant function that returns
    `zero` in the codomain.

    > zero :: TValue -> Value
    > zero :: TValue -> Value
    zero TValue
    TVBit          = Bool -> Value
    VBit Bool
    False
    > zero TValue
    TVInteger      = Integer -> Value
    VInteger Integer
    0
    > zero TVIntMod{}     = Integer -> Value
    VInteger Integer
    0
    > zero TValue
    TVRational     = Rational -> Value
    VRational Rational
    0
    > zero (TVFloat Integer
    e Integer
    p)  = BF -> Value
    VFloat (Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p BigFloat
    FP.bfPosZero)
    > zero TVArray{}      = String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "zero" [String
    "Array type not in `Zero`"]
    > zero (TVSeq Integer
    n TValue
    ety)  = Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    n) (Integer -> E Value -> [E Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n (Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    ety)))
    > zero (TVStream TValue
    ety) = Nat' -> [E Value] -> Value
    VList Nat'
    Inf (E Value -> [E Value]
    forall a. a -> [a]
    repeat (Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    ety)))
    > zero (TVTuple [TValue]
    tys)  = [E Value] -> Value
    VTuple ((TValue -> E Value) -> [TValue] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> (TValue -> Value) -> TValue -> E Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TValue -> Value
    zero) [TValue]
    tys)
    > zero (TVRec RecordMap Ident TValue
    fields) = [(Ident, E Value)] -> Value
    VRecord [ (Ident
    f, Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    fty))
    >                               | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fields ]
    > zero (TVFun TValue
    _ TValue
    bty)  = (E Value -> E Value) -> Value
    VFun (\E Value
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    bty))
    > zero (TVAbstract{}) = String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "zero" [String
    "Abstract type not in `Zero`"]
    > zero (TVNewtype{})  = String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic String
    "zero" [String
    "Newtype not in `Zero`"]

    Literals
    --------

    Given a literal integer, construct a value of a type that can represent that literal.

    > literal :: Integer -> TValue -> E Value
    > literal :: Integer -> TValue -> E Value
    literal Integer
    i = TValue -> E Value
    forall {f :: * -> *}. Applicative f => TValue -> f Value
    go
    >   where
    >    go :: TValue -> f Value
    go TValue
    TVInteger  = Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Value
    VInteger Integer
    i)
    >    go TValue
    TVRational = Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational -> Value
    VRational (Integer -> Rational
    forall a. Num a => Integer -> a
    fromInteger Integer
    i))
    >    go (TVIntMod Integer
    n)
    >         | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    n = Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Value
    VInteger Integer
    i)
    >         | Bool
    otherwise = String -> [String] -> f Value
    forall a. String -> [String] -> a
    evalPanic String
    "literal"
    >                            [String
    "Literal out of range for type Z " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n]
    >    go (TVSeq Integer
    w TValue
    a)
    >         | TValue -> Bool
    isTBit TValue
    a = Value -> f Value
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> Value
    vWord Integer
    w Integer
    i)
    >    go TValue
    ty = String -> [String] -> f Value
    forall a. String -> [String] -> a
    evalPanic String
    "literal" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " cannot represent literals"]

    Given a fraction, construct a value of a type that can represent that literal.
    The rounding flag determines the behavior if the literal cannot be represented
    exactly: 0 means report and error, other numbers round to the nearest
    representable value.

    > -- TODO: we should probably be using the rounding mode here...
    > fraction :: Integer -> Integer -> Integer -> TValue -> E Value
    > fraction :: Integer -> Integer -> Integer -> TValue -> E Value
    fraction Integer
    top Integer
    btm Integer
    _rnd TValue
    ty =
    >   case TValue
    ty of
    >     TValue
    TVRational -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational -> Value
    VRational (Integer
    top Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    btm))
    >     TVFloat Integer
    e Integer
    p -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ BF -> Value
    VFloat (BF -> Value) -> BF -> Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p  (BigFloat -> BF) -> BigFloat -> BF
    forall a b. (a -> b) -> a -> b
    $ (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus (BigFloat, Status)
    val
    >       where val :: (BigFloat, Status)
    val  = BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv BFOpts
    opts (Integer -> BigFloat
    FP.bfFromInteger Integer
    top) (Integer -> BigFloat
    FP.bfFromInteger Integer
    btm)
    >             opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts Integer
    e Integer
    p RoundMode
    fpImplicitRound
    >     TValue
    _ -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "fraction" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " cannot represent " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
    >                                 Integer -> String
    forall a. Show a => a -> String
    show Integer
    top String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "/" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    btm]

    Logic
    -----

    Bitwise logic primitives are defined by recursion over the type
    structure. On type `Bit`, the operations are strict in all
    arguments.  For example, `True || error "foo"`
    does not evaluate to `True`, but yields a run-time exception. On other
    types, run-time exceptions on input bits only affect the output bits
    at the same positions.

    > logicUnary :: (Bool -> Bool) -> TValue -> E Value -> E Value
    > logicUnary :: (Bool -> Bool) -> TValue -> E Value -> E Value
    logicUnary Bool -> Bool
    op = TValue -> E Value -> E Value
    go
    >   where
    >     go :: TValue -> E Value -> E Value
    >     go :: TValue -> E Value -> E Value
    go TValue
    ty E Value
    val =
    >       case TValue
    ty of
    >         TValue
    TVBit        -> Bool -> Value
    VBit (Bool -> Value) -> (Value -> Bool) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    op (Bool -> Bool) -> (Value -> Bool) -> Value -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> Bool
    fromVBit (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVSeq Integer
    w TValue
    ety  -> Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (E Value -> E Value) -> [E Value] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> E Value -> E Value
    go TValue
    ety) ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVList (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVStream TValue
    ety -> Nat' -> [E Value] -> Value
    VList Nat'
    Inf ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (E Value -> E Value) -> [E Value] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> E Value -> E Value
    go TValue
    ety) ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVList (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVTuple [TValue]
    etys -> [E Value] -> Value
    VTuple ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TValue -> E Value -> E Value)
    -> [TValue] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> E Value -> E Value
    go [TValue]
    etys ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVTuple (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVRec RecordMap Ident TValue
    fields ->
    >              do Value
    val' <- E Value
    val
    >                 Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord [ (Ident
    f, TValue -> E Value -> E Value
    go TValue
    fty (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    val'))
    >                                | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fields ]
    >         TVFun TValue
    _ TValue
    bty  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun (\E Value
    v -> TValue -> E Value -> E Value
    go TValue
    bty (E Value -> E Value -> E Value
    appFun E Value
    val E Value
    v))
    >         TValue
    TVInteger    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Integer not in class Logic"]
    >         TVIntMod Integer
    _   -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Z not in class Logic"]
    >         TVArray{}    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Array not in class Logic"]
    >         TValue
    TVRational   -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Rational not in class Logic"]
    >         TVFloat{}    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Float not in class Logic"]
    >         TVAbstract{} -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Abstract type not in `Logic`"]
    >         TVNewtype{}  -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicUnary" [String
    "Newtype not in `Logic`"]

    > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
    > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
    logicBinary Bool -> Bool -> Bool
    op = TValue -> E Value -> E Value -> E Value
    go
    >   where
    >     go :: TValue -> E Value -> E Value -> E Value
    >     go :: TValue -> E Value -> E Value -> E Value
    go TValue
    ty E Value
    l E Value
    r =
    >       case TValue
    ty of
    >         TValue
    TVBit ->
    >           Bool -> Value
    VBit (Bool -> Value) -> E Bool -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Bool -> Bool -> Bool
    op (Bool -> Bool -> Bool) -> E Bool -> E (Bool -> Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Bool
    fromVBit (Value -> Bool) -> E Value -> E Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (Bool -> Bool) -> E Bool -> E Bool
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> Bool
    fromVBit (Value -> Bool) -> E Value -> E Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVSeq Integer
    w TValue
    ety  ->
    >           Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((E Value -> E Value -> E Value)
    -> [E Value] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Value
    go TValue
    ety) ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                                 (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                                 (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVStream TValue
    ety ->
    >           Nat' -> [E Value] -> Value
    VList Nat'
    Inf ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((E Value -> E Value -> E Value)
    -> [E Value] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Value
    go TValue
    ety) ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                              (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                              (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVTuple [TValue]
    etys ->
    >           [E Value] -> Value
    VTuple ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TValue -> E Value -> E Value -> E Value)
    -> [TValue] -> [E Value] -> [E Value] -> [E Value]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Value
    go [TValue]
    etys ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                              (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                              (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVRec RecordMap Ident TValue
    fields ->
    >            do Value
    l' <- E Value
    l
    >               Value
    r' <- E Value
    r
    >               Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord
    >                    [ (Ident
    f, TValue -> E Value -> E Value -> E Value
    go TValue
    fty (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    l') (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    r'))
    >                    | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fields
    >                    ]
    >         TVFun TValue
    _ TValue
    bty  -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v ->
    >                            do Value
    l' <- E Value
    l
    >                               Value
    r' <- E Value
    r
    >                               TValue -> E Value -> E Value -> E Value
    go TValue
    bty (Value -> E Value -> E Value
    fromVFun Value
    l' E Value
    v) (Value -> E Value -> E Value
    fromVFun Value
    r' E Value
    v)
    >         TValue
    TVInteger    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Integer not in class Logic"]
    >         TVIntMod Integer
    _   -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Z not in class Logic"]
    >         TVArray{}    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Array not in class Logic"]
    >         TValue
    TVRational   -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Rational not in class Logic"]
    >         TVFloat{}    -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Float not in class Logic"]
    >         TVAbstract{} -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Abstract type not in `Logic`"]
    >         TVNewtype{}  -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "logicBinary" [String
    "Newtype not in `Logic`"]

    Ring Arithmetic
    ---------------

    Ring primitives may be applied to any type that is made up of
    finite bitvectors or one of the numeric base types.
    On type `[n]`, arithmetic operators are strict in
    all input bits, as indicated by the definition of `fromVWord`. For
    example, `[error "foo", True] * 2` does not evaluate to `[True,
    False]`, but to `error "foo"`.

    > ringNullary ::
    >    E Integer ->
    >    E Rational ->
    >    (Integer -> Integer -> E BigFloat) ->
    >    TValue -> E Value
    > ringNullary :: E Integer
    -> E Rational
    -> (Integer -> Integer -> E BigFloat)
    -> TValue
    -> E Value
    ringNullary E Integer
    i E Rational
    q Integer -> Integer -> E BigFloat
    fl = TValue -> E Value
    go
    >   where
    >     go :: TValue -> E Value
    >     go :: TValue -> E Value
    go TValue
    ty =
    >       case TValue
    ty of
    >         TValue
    TVBit ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithNullary" [String
    "Bit not in class Ring"]
    >         TValue
    TVInteger ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Integer
    i
    >         TVIntMod Integer
    n ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> (Integer -> Integer) -> Integer -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    n (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Integer
    i
    >         TValue
    TVRational ->
    >           Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Rational
    q
    >         TVFloat Integer
    e Integer
    p ->
    >           BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Integer -> E BigFloat
    fl Integer
    e Integer
    p
    >         TVArray{} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithNullary" [String
    "Array not in class Ring"]
    >         TVSeq Integer
    w TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Integer -> Value
    vWord Integer
    w (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Integer
    i
    >           | Bool
    otherwise -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) (Integer -> E Value -> [E Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    w (TValue -> E Value
    go TValue
    a))
    >         TVStream TValue
    a ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> [E Value] -> Value
    VList Nat'
    Inf (E Value -> [E Value]
    forall a. a -> [a]
    repeat (TValue -> E Value
    go TValue
    a))
    >         TVFun TValue
    _ TValue
    ety ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun (E Value -> E Value -> E Value
    forall a b. a -> b -> a
    const (TValue -> E Value
    go TValue
    ety))
    >         TVTuple [TValue]
    tys ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [E Value] -> Value
    VTuple ((TValue -> E Value) -> [TValue] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> E Value
    go [TValue]
    tys)
    >         TVRec RecordMap Ident TValue
    fs ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord [ (Ident
    f, TValue -> E Value
    go TValue
    fty) | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithNullary" [String
    "Abstract type not in `Ring`"]
    >         TVNewtype {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithNullary" [String
    "Newtype type not in `Ring`"]

    > ringUnary ::
    >   (Integer -> E Integer) ->
    >   (Rational -> E Rational) ->
    >   (Integer -> Integer -> BigFloat -> E BigFloat) ->
    >   TValue -> E Value -> E Value
    > ringUnary :: (Integer -> E Integer)
    -> (Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    ringUnary Integer -> E Integer
    iop Rational -> E Rational
    qop Integer -> Integer -> BigFloat -> E BigFloat
    flop = TValue -> E Value -> E Value
    go
    >   where
    >     go :: TValue -> E Value -> E Value
    >     go :: TValue -> E Value -> E Value
    go TValue
    ty E Value
    val =
    >       case TValue
    ty of
    >         TValue
    TVBit ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithUnary" [String
    "Bit not in class Ring"]
    >         TValue
    TVInteger ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> E Integer) -> E Integer -> E Integer
    forall a b. (a -> E b) -> E a -> E b
    appOp1 Integer -> E Integer
    iop (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val)
    >         TVArray{} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithUnary" [String
    "Array not in class Ring"]
    >         TVIntMod Integer
    n ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> E Integer) -> E Integer -> E Integer
    forall a b. (a -> E b) -> E a -> E b
    appOp1 (\Integer
    i -> (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    n (Integer -> Integer) -> E Integer -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> E Integer
    iop Integer
    i) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val)
    >         TValue
    TVRational ->
    >           Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Rational -> E Rational) -> E Rational -> E Rational
    forall a b. (a -> E b) -> E a -> E b
    appOp1 Rational -> E Rational
    qop (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val)
    >         TVFloat Integer
    e Integer
    p ->
    >           BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BigFloat -> E BigFloat) -> E BigFloat -> E BigFloat
    forall a b. (a -> E b) -> E a -> E b
    appOp1 (Integer -> Integer -> BigFloat -> E BigFloat
    flop Integer
    e Integer
    p) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val)
    >         TVSeq Integer
    w TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Integer -> Value
    vWord Integer
    w (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> E Integer
    iop (Integer -> E Integer) -> E Integer -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    val))
    >           | Bool
    otherwise -> Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (E Value -> E Value) -> [E Value] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> E Value -> E Value
    go TValue
    a) ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVList (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVStream TValue
    a ->
    >           Nat' -> [E Value] -> Value
    VList Nat'
    Inf ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (E Value -> E Value) -> [E Value] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> E Value -> E Value
    go TValue
    a) ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVList (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVFun TValue
    _ TValue
    ety ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun (\E Value
    x -> TValue -> E Value -> E Value
    go TValue
    ety (E Value -> E Value -> E Value
    appFun E Value
    val E Value
    x))
    >         TVTuple [TValue]
    tys ->
    >           [E Value] -> Value
    VTuple ([E Value] -> Value) -> (Value -> [E Value]) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TValue -> E Value -> E Value)
    -> [TValue] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> E Value -> E Value
    go [TValue]
    tys ([E Value] -> [E Value])
    -> (Value -> [E Value]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [E Value]
    fromVTuple (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    val
    >         TVRec RecordMap Ident TValue
    fs ->
    >           do Value
    val' <- E Value
    val
    >              Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord [ (Ident
    f, TValue -> E Value -> E Value
    go TValue
    fty (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    val'))
    >                             | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithUnary" [String
    "Abstract type not in `Ring`"]
    >         TVNewtype {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithUnary" [String
    "Newtype not in `Ring`"]

    > ringBinary ::
    >   (Integer -> Integer -> E Integer) ->
    >   (Rational -> Rational -> E Rational) ->
    >   (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat) ->
    >   TValue -> E Value -> E Value -> E Value
    > ringBinary :: (Integer -> Integer -> E Integer)
    -> (Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    ringBinary Integer -> Integer -> E Integer
    iop Rational -> Rational -> E Rational
    qop Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat
    flop = TValue -> E Value -> E Value -> E Value
    go
    >   where
    >     go :: TValue -> E Value -> E Value -> E Value
    >     go :: TValue -> E Value -> E Value -> E Value
    go TValue
    ty E Value
    l E Value
    r =
    >       case TValue
    ty of
    >         TValue
    TVBit ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithBinary" [String
    "Bit not in class Ring"]
    >         TValue
    TVInteger ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    iop (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >         TVIntMod Integer
    n ->
    >           Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 (\Integer
    i Integer
    j -> (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    n (Integer -> Integer) -> E Integer -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Integer -> E Integer
    iop Integer
    i Integer
    j) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >         TValue
    TVRational ->
    >           Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Rational -> Rational -> E Rational)
    -> E Rational -> E Rational -> E Rational
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Rational -> Rational -> E Rational
    qop (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >         TVFloat Integer
    e Integer
    p ->
    >           BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >             (BigFloat -> BigFloat -> E BigFloat)
    -> E BigFloat -> E BigFloat -> E BigFloat
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat
    flop Integer
    e Integer
    p) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >         TVArray{} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithBinary" [String
    "Array not in class Ring"]
    >         TVSeq Integer
    w TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Integer -> Value
    vWord Integer
    w (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    iop (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    l) (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    r)
    >           | Bool
    otherwise ->
    >                Nat' -> [E Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((E Value -> E Value -> E Value)
    -> [E Value] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Value
    go TValue
    a) ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                                     (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                                     (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVStream TValue
    a ->
    >           Nat' -> [E Value] -> Value
    VList Nat'
    Inf ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((E Value -> E Value -> E Value)
    -> [E Value] -> [E Value] -> [E Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Value
    go TValue
    a) ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                            (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                            (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVFun TValue
    _ TValue
    ety ->
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ (E Value -> E Value) -> Value
    VFun (\E Value
    x -> TValue -> E Value -> E Value -> E Value
    go TValue
    ety (E Value -> E Value -> E Value
    appFun E Value
    l E Value
    x) (E Value -> E Value -> E Value
    appFun E Value
    r E Value
    x))
    >         TVTuple [TValue]
    tys ->
    >           [E Value] -> Value
    VTuple ([E Value] -> Value) -> E [E Value] -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TValue -> E Value -> E Value -> E Value)
    -> [TValue] -> [E Value] -> [E Value] -> [E Value]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Value
    go [TValue]
    tys ([E Value] -> [E Value] -> [E Value])
    -> E [E Value] -> E ([E Value] -> [E Value])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                          (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Value]) -> E [E Value] -> E [E Value]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
    >                          (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >         TVRec RecordMap Ident TValue
    fs ->
    >           do Value
    l' <- E Value
    l
    >              Value
    r' <- E Value
    r
    >              Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, E Value)] -> Value
    VRecord
    >                [ (Ident
    f, TValue -> E Value -> E Value -> E Value
    go TValue
    fty (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    l') (Ident -> Value -> E Value
    lookupRecord Ident
    f Value
    r'))
    >                | (Ident
    f, TValue
    fty) <- RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithBinary" [String
    "Abstract type not in class `Ring`"]
    >         TVNewtype {} ->
    >           String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "arithBinary" [String
    "Newtype not in class `Ring`"]

    Integral
    ---------

    > cryToInteger :: TValue -> E Value -> E Integer
    > cryToInteger :: TValue -> E Value -> E Integer
    cryToInteger TValue
    ty E Value
    v = case TValue
    ty of
    >   TValue
    TVInteger -> Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >   TVSeq Integer
    _ TValue
    a | TValue -> Bool
    isTBit TValue
    a -> Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    v
    >   TValue
    _ -> String -> [String] -> E Integer
    forall a. String -> [String] -> a
    evalPanic String
    "toInteger" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not an integral type"]
    >
    > integralBinary ::
    >     (Integer -> Integer -> E Integer) ->
    >     TValue -> E Value -> E Value -> E Value
    > integralBinary :: (Integer -> Integer -> E Integer)
    -> TValue -> E Value -> E Value -> E Value
    integralBinary Integer -> Integer -> E Integer
    op TValue
    ty E Value
    x E Value
    y = case TValue
    ty of
    >   TValue
    TVInteger ->
    >       Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    op (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    x) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    y)
    >   TVSeq Integer
    w TValue
    a | TValue -> Bool
    isTBit TValue
    a ->
    >       Integer -> Integer -> Value
    vWord Integer
    w (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Integer -> Integer -> E Integer
    op (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    x) (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    y)
    >
    >   TValue
    _ -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "integralBinary" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not an integral type"]
    >
    > ringExp :: TValue -> E Value -> Integer -> E Value
    > ringExp :: TValue -> E Value -> Integer -> E Value
    ringExp TValue
    a E Value
    v Integer
    i = (E Value -> E Value -> E Value) -> E Value -> [E Value] -> E Value
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (TValue -> E Value -> E Value -> E Value
    ringMul TValue
    a) (Integer -> TValue -> E Value
    literal Integer
    1 TValue
    a) (Integer -> E Value -> [E Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    i E Value
    v)
    >
    > ringMul :: TValue -> E Value -> E Value -> E Value
    > ringMul :: TValue -> E Value -> E Value -> E Value
    ringMul = (Integer -> Integer -> E Integer)
    -> (Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    ringBinary (\Integer
    x Integer
    y -> Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    y))
    >                      (\Rational
    x Rational
    y -> Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational
    x Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * Rational
    y))
    >                      ((BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfMul RoundMode
    fpImplicitRound)

    Signed bitvector division (`/$`) and remainder (`%$`) are defined so
    that division rounds toward zero, and the remainder `x %$ y` has the
    same sign as `x`. Accordingly, they are implemented with Haskell's
    `quot` and `rem` operations.

    > divWrap :: Integer -> Integer -> E Integer
    > divWrap :: Integer -> Integer -> E Integer
    divWrap Integer
    _ Integer
    0 = EvalError -> E Integer
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    > divWrap Integer
    x Integer
    y = Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    y)
    >
    > modWrap :: Integer -> Integer -> E Integer
    > modWrap :: Integer -> Integer -> E Integer
    modWrap Integer
    _ Integer
    0 = EvalError -> E Integer
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    > modWrap Integer
    x Integer
    y = Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    y)
    >
    > lg2Wrap :: Integer -> E Integer
    > lg2Wrap :: Integer -> E Integer
    lg2Wrap Integer
    x = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0 then EvalError -> E Integer
    forall a. EvalError -> E a
    cryError EvalError
    LogNegative else Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer
    lg2 Integer
    x)

    Field
    -----

    Types that represent fields have, in addition to the ring operations,
    a reciprocal operator and a field division operator (not to be
    confused with integral division).

    > fieldUnary :: (Rational -> E Rational) ->
    >               (Integer -> Integer -> E Integer) ->
    >               (Integer -> Integer -> BigFloat -> E BigFloat) ->
    >               TValue -> E Value -> E Value
    > fieldUnary :: (Rational -> E Rational)
    -> (Integer -> Integer -> E Integer)
    -> (Integer -> Integer -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    fieldUnary Rational -> E Rational
    qop Integer -> Integer -> E Integer
    zop Integer -> Integer -> BigFloat -> E BigFloat
    flop TValue
    ty E Value
    v = case TValue
    ty of
    >   TValue
    TVRational  -> Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Rational -> E Rational) -> E Rational -> E Rational
    forall a b. (a -> E b) -> E a -> E b
    appOp1 Rational -> E Rational
    qop (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v)
    >   TVIntMod Integer
    m  -> Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> E Integer) -> E Integer -> E Integer
    forall a b. (a -> E b) -> E a -> E b
    appOp1 (Integer -> Integer -> E Integer
    zop Integer
    m) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v)
    >   TVFloat Integer
    e Integer
    p -> BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BigFloat -> E BigFloat) -> E BigFloat -> E BigFloat
    forall a b. (a -> E b) -> E a -> E b
    appOp1 (Integer -> Integer -> BigFloat -> E BigFloat
    flop Integer
    e Integer
    p) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v)
    >   TValue
    _ -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "fieldUnary" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a Field type"]
    >
    > fieldBinary ::
    >    (Rational -> Rational -> E Rational) ->
    >    (Integer -> Integer -> Integer -> E Integer) ->
    >    (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat) ->
    >    TValue -> E Value -> E Value -> E Value
    > fieldBinary :: (Rational -> Rational -> E Rational)
    -> (Integer -> Integer -> Integer -> E Integer)
    -> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
    -> TValue
    -> E Value
    -> E Value
    -> E Value
    fieldBinary Rational -> Rational -> E Rational
    qop Integer -> Integer -> Integer -> E Integer
    zop Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat
    flop TValue
    ty E Value
    l E Value
    r = case TValue
    ty of
    >   TValue
    TVRational  -> Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                    (Rational -> Rational -> E Rational)
    -> E Rational -> E Rational -> E Rational
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 Rational -> Rational -> E Rational
    qop (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >   TVIntMod Integer
    m  -> Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                    (Integer -> Integer -> E Integer)
    -> E Integer -> E Integer -> E Integer
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 (Integer -> Integer -> Integer -> E Integer
    zop Integer
    m) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >   TVFloat Integer
    e Integer
    p -> BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                       (BigFloat -> BigFloat -> E BigFloat)
    -> E BigFloat -> E BigFloat -> E BigFloat
    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
    appOp2 (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat
    flop Integer
    e Integer
    p) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >   TValue
    _ -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "fieldBinary" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a Field type"]
    >
    > ratDiv :: Rational -> Rational -> E Rational
    > ratDiv :: Rational -> Rational -> E Rational
    ratDiv Rational
    _ Rational
    0 = EvalError -> E Rational
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    > ratDiv Rational
    x Rational
    y = Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational
    x Rational -> Rational -> Rational
    forall a. Fractional a => a -> a -> a
    / Rational
    y)
    >
    > ratRecip :: Rational -> E  Rational
    > ratRecip :: Rational -> E Rational
    ratRecip Rational
    0 = EvalError -> E Rational
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    > ratRecip Rational
    x = Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Rational -> Rational
    forall a. Fractional a => a -> a
    recip Rational
    x)
    >
    > zRecip :: Integer -> Integer -> E Integer
    > zRecip :: Integer -> Integer -> E Integer
    zRecip Integer
    m Integer
    x =
    >   case Integer -> Integer -> Maybe Integer
    Integer.integerRecipMod Integer
    x Integer
    m of
    >     Just Integer
    r  -> Integer -> E Integer
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    r
    >     Maybe Integer
    Nothing -> EvalError -> E Integer
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    >
    > zDiv :: Integer -> Integer -> Integer -> E Integer
    > zDiv :: Integer -> Integer -> Integer -> E Integer
    zDiv Integer
    m Integer
    x Integer
    y = Integer -> Integer
    f (Integer -> Integer) -> E Integer -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Integer -> E Integer
    zRecip Integer
    m Integer
    y
    >   where f :: Integer -> Integer
    f Integer
    yinv = (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    yinv) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m

    Round
    -----

    > roundUnary :: (Rational -> Integer) ->
    >               (BF -> E Integer) ->
    >               TValue -> E Value -> E Value
    > roundUnary :: (Rational -> Integer)
    -> (BF -> E Integer) -> TValue -> E Value -> E Value
    roundUnary Rational -> Integer
    op BF -> E Integer
    flop TValue
    ty E Value
    v = case TValue
    ty of
    >   TValue
    TVRational -> Integer -> Value
    VInteger (Integer -> Value) -> (Value -> Integer) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> Integer
    op (Rational -> Integer) -> (Value -> Rational) -> Value -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> Rational
    fromVRational (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >   TVFloat {} -> Integer -> Value
    VInteger (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BF -> E Integer
    flop (BF -> E Integer) -> (Value -> BF) -> Value -> E Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> BF
    fromVFloat' (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    v)
    >   TValue
    _ -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "roundUnary" [TValue -> String
    forall a. Show a => a -> String
    show TValue
    ty String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a Round type"]
    >

    Haskell's definition of "round" is slightly different, as it does
    "round to even" on ties.

    > roundAwayRat :: Rational -> Integer
    > roundAwayRat :: Rational -> Integer
    roundAwayRat Rational
    x
    >   | Rational
    x Rational -> Rational -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Rational
    0    = Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    floor (Rational
    x Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    + Rational
    0.5)
    >   | Bool
    otherwise = Rational -> Integer
    forall b. Integral b => Rational -> b
    forall a b. (RealFrac a, Integral b) => a -> b
    ceiling (Rational
    x Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    - Rational
    0.5)

    Rational
    ----------

    > ratioOp :: Integer -> Integer -> E Rational
    > ratioOp :: Integer -> Integer -> E Rational
    ratioOp Integer
    _ Integer
    0 = EvalError -> E Rational
    forall a. EvalError -> E a
    cryError EvalError
    DivideByZero
    > ratioOp Integer
    x Integer
    y = Rational -> E Rational
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Rational
    forall a. Num a => Integer -> a
    fromInteger Integer
    x Rational -> Rational -> Rational
    forall a. Fractional a => a -> a -> a
    / Integer -> Rational
    forall a. Num a => Integer -> a
    fromInteger Integer
    y)

    Comparison
    ----------

    Comparison primitives may be applied to any type that is constructed of
    out of base types and tuples, records and finite sequences.
    All such types are compared using a lexicographic ordering of components.
    On bits, we have `False` < `True`. Sequences and
    tuples are compared left-to-right, and record fields are compared in
    alphabetical order.

    Comparisons on base types are strict in both arguments. Comparisons on
    larger types have short-circuiting behavior: A comparison involving an
    error/undefined element will only yield an error if all corresponding
    bits to the *left* of that position are equal.

    > -- | Process two elements based on their lexicographic ordering.
    > cmpOrder :: (Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    > cmpOrder :: (Ordering -> Bool) -> TValue -> E Value -> E Value -> E Value
    cmpOrder Ordering -> Bool
    p TValue
    ty E Value
    l E Value
    r = Bool -> Value
    VBit (Bool -> Value) -> (Ordering -> Bool) -> Ordering -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ordering -> Bool
    p (Ordering -> Value) -> E Ordering -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> E Value -> E Value -> E Ordering
    lexCompare TValue
    ty E Value
    l E Value
    r
    >
    > -- | Lexicographic ordering on two values.
    > lexCompare :: TValue -> E Value -> E Value -> E Ordering
    > lexCompare :: TValue -> E Value -> E Value -> E Ordering
    lexCompare TValue
    ty E Value
    l E Value
    r =
    >   case TValue
    ty of
    >     TValue
    TVBit ->
    >       Bool -> Bool -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Bool -> Bool -> Ordering) -> E Bool -> E (Bool -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Bool
    fromVBit (Value -> Bool) -> E Value -> E Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (Bool -> Ordering) -> E Bool -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> Bool
    fromVBit (Value -> Bool) -> E Value -> E Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >     TValue
    TVInteger ->
    >       Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> E Integer -> E (Integer -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (Integer -> Ordering) -> E Integer -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >     TVIntMod Integer
    _ ->
    >       Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> E Integer -> E (Integer -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (Integer -> Ordering) -> E Integer -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> Integer
    fromVInteger (Value -> Integer) -> E Value -> E Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >     TValue
    TVRational ->
    >       Rational -> Rational -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Rational -> Rational -> Ordering)
    -> E Rational -> E (Rational -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (Rational -> Ordering) -> E Rational -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >     TVFloat{} ->
    >       BigFloat -> BigFloat -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (BigFloat -> BigFloat -> Ordering)
    -> E BigFloat -> E (BigFloat -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E (BigFloat -> Ordering) -> E BigFloat -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r)
    >     TVArray{} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexCompare" [String
    "invalid type"]
    >     TVSeq Integer
    _w TValue
    ety ->
    >       [E Ordering] -> E Ordering
    lexList ([E Ordering] -> E Ordering) -> E [E Ordering] -> E Ordering
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ((E Value -> E Value -> E Ordering)
    -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Ordering
    lexCompare TValue
    ety) ([E Value] -> [E Value] -> [E Ordering])
    -> E [E Value] -> E ([E Value] -> [E Ordering])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                      (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Ordering]) -> E [E Value] -> E [E Ordering]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >     TVStream TValue
    _ ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexCompare" [String
    "invalid type"]
    >     TVFun TValue
    _ TValue
    _ ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexCompare" [String
    "invalid type"]
    >     TVTuple [TValue]
    etys ->
    >       [E Ordering] -> E Ordering
    lexList ([E Ordering] -> E Ordering) -> E [E Ordering] -> E Ordering
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ((TValue -> E Value -> E Value -> E Ordering)
    -> [TValue] -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Ordering
    lexCompare [TValue]
    etys ([E Value] -> [E Value] -> [E Ordering])
    -> E [E Value] -> E ([E Value] -> [E Ordering])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                         (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Ordering]) -> E [E Value] -> E [E Ordering]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >     TVRec RecordMap Ident TValue
    fields ->
    >       do let tys :: [TValue]
    tys = ((Ident, TValue) -> TValue) -> [(Ident, TValue)] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, TValue) -> TValue
    forall a b. (a, b) -> b
    snd (RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fields)
    >          [E Value]
    ls <- ((Ident, E Value) -> E Value) -> [(Ident, E Value)] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, E Value) -> E Value
    forall a b. (a, b) -> b
    snd ([(Ident, E Value)] -> [E Value])
    -> (Value -> [(Ident, E Value)]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Ident, E Value) -> (Ident, E Value) -> Ordering)
    -> [(Ident, E Value)] -> [(Ident, E Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, E Value) -> Ident)
    -> (Ident, E Value) -> (Ident, E Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, E Value) -> Ident
    forall a b. (a, b) -> a
    fst) ([(Ident, E Value)] -> [(Ident, E Value)])
    -> (Value -> [(Ident, E Value)]) -> Value -> [(Ident, E Value)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [(Ident, E Value)]
    fromVRecord (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l
    >          [E Value]
    rs <- ((Ident, E Value) -> E Value) -> [(Ident, E Value)] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, E Value) -> E Value
    forall a b. (a, b) -> b
    snd ([(Ident, E Value)] -> [E Value])
    -> (Value -> [(Ident, E Value)]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Ident, E Value) -> (Ident, E Value) -> Ordering)
    -> [(Ident, E Value)] -> [(Ident, E Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, E Value) -> Ident)
    -> (Ident, E Value) -> (Ident, E Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, E Value) -> Ident
    forall a b. (a, b) -> a
    fst) ([(Ident, E Value)] -> [(Ident, E Value)])
    -> (Value -> [(Ident, E Value)]) -> Value -> [(Ident, E Value)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [(Ident, E Value)]
    fromVRecord (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r
    >          [E Ordering] -> E Ordering
    lexList ((TValue -> E Value -> E Value -> E Ordering)
    -> [TValue] -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Ordering
    lexCompare [TValue]
    tys [E Value]
    ls [E Value]
    rs)
    >     TVAbstract {} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexCompare" [String
    "Abstract type not in `Cmp`"]
    >     TVNewtype {} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexCompare" [String
    "Newtype not in `Cmp`"]
    >
    > lexList :: [E Ordering] -> E Ordering
    > lexList :: [E Ordering] -> E Ordering
    lexList [] = Ordering -> E Ordering
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ordering
    EQ
    > lexList (E Ordering
    e : [E Ordering]
    es) =
    >   E Ordering
    e E Ordering -> (Ordering -> E Ordering) -> E Ordering
    forall a b. E a -> (a -> E b) -> E b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
    >     Ordering
    LT -> Ordering -> E Ordering
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ordering
    LT
    >     Ordering
    EQ -> [E Ordering] -> E Ordering
    lexList [E Ordering]
    es
    >     Ordering
    GT -> Ordering -> E Ordering
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ordering
    GT

    Signed comparisons may be applied to any type made up of non-empty
    bitvectors using finite sequences, tuples and records.
    All such types are compared using a lexicographic
    ordering: Lists and tuples are compared left-to-right, and record
    fields are compared in alphabetical order.

    > signedLessThan :: TValue -> E Value -> E Value -> E Value
    > signedLessThan :: TValue -> E Value -> E Value -> E Value
    signedLessThan TValue
    ty E Value
    l E Value
    r = Bool -> Value
    VBit (Bool -> Value) -> (Ordering -> Bool) -> Ordering -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    LT) (Ordering -> Value) -> E Ordering -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> E Value -> E Value -> E Ordering
    lexSignedCompare TValue
    ty E Value
    l E Value
    r)
    >
    > -- | Lexicographic ordering on two signed values.
    > lexSignedCompare :: TValue -> E Value -> E Value -> E Ordering
    > lexSignedCompare :: TValue -> E Value -> E Value -> E Ordering
    lexSignedCompare TValue
    ty E Value
    l E Value
    r =
    >   case TValue
    ty of
    >     TValue
    TVBit ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TValue
    TVInteger ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVIntMod Integer
    _ ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TValue
    TVRational ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVFloat{} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVArray{} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVSeq Integer
    _w TValue
    ety
    >       | TValue -> Bool
    isTBit TValue
    ety ->
    >           Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> E Integer -> E (Integer -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    l) E (Integer -> Ordering) -> E Integer -> E Ordering
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> E Integer
    fromSignedVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    r)
    >       | Bool
    otherwise ->
    >           [E Ordering] -> E Ordering
    lexList ([E Ordering] -> E Ordering) -> E [E Ordering] -> E Ordering
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ((E Value -> E Value -> E Ordering)
    -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> E Value -> E Value -> E Ordering
    lexSignedCompare TValue
    ety) ([E Value] -> [E Value] -> [E Ordering])
    -> E [E Value] -> E ([E Value] -> [E Ordering])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                            (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Ordering]) -> E [E Value] -> E [E Ordering]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >     TVStream TValue
    _ ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVFun TValue
    _ TValue
    _ ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "invalid type"]
    >     TVTuple [TValue]
    etys ->
    >       [E Ordering] -> E Ordering
    lexList ([E Ordering] -> E Ordering) -> E [E Ordering] -> E Ordering
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ((TValue -> E Value -> E Value -> E Ordering)
    -> [TValue] -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Ordering
    lexSignedCompare [TValue]
    etys ([E Value] -> [E Value] -> [E Ordering])
    -> E [E Value] -> E ([E Value] -> [E Ordering])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
    >                        (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l) E ([E Value] -> [E Ordering]) -> E [E Value] -> E [E Ordering]
    forall a b. E (a -> b) -> E a -> E b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Value -> [E Value]
    fromVTuple (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r))
    >     TVRec RecordMap Ident TValue
    fields ->
    >       do let tys :: [TValue]
    tys    = ((Ident, TValue) -> TValue) -> [(Ident, TValue)] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, TValue) -> TValue
    forall a b. (a, b) -> b
    snd (RecordMap Ident TValue -> [(Ident, TValue)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap Ident TValue
    fields)
    >          [E Value]
    ls <- ((Ident, E Value) -> E Value) -> [(Ident, E Value)] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, E Value) -> E Value
    forall a b. (a, b) -> b
    snd ([(Ident, E Value)] -> [E Value])
    -> (Value -> [(Ident, E Value)]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Ident, E Value) -> (Ident, E Value) -> Ordering)
    -> [(Ident, E Value)] -> [(Ident, E Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, E Value) -> Ident)
    -> (Ident, E Value) -> (Ident, E Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, E Value) -> Ident
    forall a b. (a, b) -> a
    fst) ([(Ident, E Value)] -> [(Ident, E Value)])
    -> (Value -> [(Ident, E Value)]) -> Value -> [(Ident, E Value)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [(Ident, E Value)]
    fromVRecord (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l
    >          [E Value]
    rs <- ((Ident, E Value) -> E Value) -> [(Ident, E Value)] -> [E Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, E Value) -> E Value
    forall a b. (a, b) -> b
    snd ([(Ident, E Value)] -> [E Value])
    -> (Value -> [(Ident, E Value)]) -> Value -> [E Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Ident, E Value) -> (Ident, E Value) -> Ordering)
    -> [(Ident, E Value)] -> [(Ident, E Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, E Value) -> Ident)
    -> (Ident, E Value) -> (Ident, E Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, E Value) -> Ident
    forall a b. (a, b) -> a
    fst) ([(Ident, E Value)] -> [(Ident, E Value)])
    -> (Value -> [(Ident, E Value)]) -> Value -> [(Ident, E Value)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> [(Ident, E Value)]
    fromVRecord (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    r
    >          [E Ordering] -> E Ordering
    lexList ((TValue -> E Value -> E Value -> E Ordering)
    -> [TValue] -> [E Value] -> [E Value] -> [E Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> E Value -> E Value -> E Ordering
    lexSignedCompare [TValue]
    tys [E Value]
    ls [E Value]
    rs)
    >     TVAbstract {} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "Abstract type not in `Cmp`"]
    >     TVNewtype {} ->
    >       String -> [String] -> E Ordering
    forall a. String -> [String] -> a
    evalPanic String
    "lexSignedCompare" [String
    "Newtype type not in `Cmp`"]

    Sequences
    ---------

    > generateV :: Nat' -> (Integer -> E Value) -> Value
    > generateV :: Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    len Integer -> E Value
    f = Nat' -> [E Value] -> Value
    VList Nat'
    len [ Integer -> E Value
    f Integer
    i | Integer
    i <- [Integer]
    idxs ]
    >   where
    >    idxs :: [Integer]
    idxs = case Nat'
    len of
    >             Nat'
    Inf   -> [ Integer
    0 .. ]
    >             Nat Integer
    n -> [ Integer
    0 .. Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1 ]

    Shifting
    --------

    Shift and rotate operations are strict in all bits of the shift/rotate
    amount, but as lazy as possible in the list values.

    > shiftV :: (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
    > shiftV :: (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
    shiftV Nat' -> TValue -> E Value -> Integer -> Value
    op =
    >   (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ix -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >   do Integer
    i <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ix E Value
    x
    >      Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> TValue -> E Value -> Integer -> Value
    op Nat'
    n TValue
    a E Value
    v Integer
    i
    >
    > shiftLV :: Nat' -> TValue -> E Value -> Integer -> Value
    > shiftLV :: Nat' -> TValue -> E Value -> Integer -> Value
    shiftLV Nat'
    w TValue
    a E Value
    v Integer
    amt =
    >   case Nat'
    w of
    >     Nat'
    Inf   -> Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    Inf ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                   Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    Inf [E Value]
    vs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    amt)
    >     Nat Integer
    n -> Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    n) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >                if Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    amt Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    n then
    >                  do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >                     Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    n) [E Value]
    vs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    amt)
    >                else
    >                  Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    a)
    >
    > shiftRV :: Nat' -> TValue -> E Value -> Integer -> Value
    > shiftRV :: Nat' -> TValue -> E Value -> Integer -> Value
    shiftRV Nat'
    w TValue
    a E Value
    v Integer
    amt =
    >   Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    w ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >     if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    amt then
    >       Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TValue -> Value
    zero TValue
    a)
    >     else
    >       do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >          Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    w [E Value]
    vs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    amt)
    >
    > rotateV :: (Integer -> E Value -> Integer -> E Value) -> Value
    > rotateV :: (Integer -> E Value -> Integer -> E Value) -> Value
    rotateV Integer -> E Value -> Integer -> E Value
    op =
    >   (Integer -> E Value) -> Value
    vFinPoly ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ix -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >   do Integer
    i <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ix E Value
    x
    >      Integer -> E Value -> Integer -> E Value
    op Integer
    n E Value
    v Integer
    i
    >
    > rotateLV :: Integer -> E Value -> Integer -> E Value
    > rotateLV :: Integer -> E Value -> Integer -> E Value
    rotateLV Integer
    0 E Value
    v Integer
    _ = E Value
    v
    > rotateLV Integer
    w E Value
    v Integer
    amt =
    >   Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    w) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >     do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >        Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    w) [E Value]
    vs ((Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    amt) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w)
    >
    > rotateRV :: Integer -> E Value -> Integer -> E Value
    > rotateRV :: Integer -> E Value -> Integer -> E Value
    rotateRV Integer
    0 E Value
    v Integer
    _ = E Value
    v
    > rotateRV Integer
    w E Value
    v Integer
    amt =
    >   Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV (Integer -> Nat'
    Nat Integer
    w) ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >     do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >        Nat' -> [E Value] -> Integer -> E Value
    indexFront (Integer -> Nat'
    Nat Integer
    w) [E Value]
    vs ((Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    amt) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w)
    >
    > signedShiftRV :: Value
    > signedShiftRV :: Value
    signedShiftRV =
    >   (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ix -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    v -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    x ->
    >   do Integer
    amt <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ix E Value
    x
    >      Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    n ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >        do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    v
    >           if Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    amt then
    >             Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    n [E Value]
    vs Integer
    0
    >           else
    >             Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    n [E Value]
    vs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    amt)

    Indexing
    --------

    Indexing and update operations are strict in all index bits, but as lazy as
    possible in the list values. An index greater than or equal to the
    length of the list produces a run-time error.

    > -- | Indexing operations that return one element.
    > indexPrimOne :: (Nat' -> [E Value] -> Integer -> E Value) -> Value
    > indexPrimOne :: (Nat' -> [E Value] -> Integer -> E Value) -> Value
    indexPrimOne Nat' -> [E Value] -> Integer -> E Value
    op =
    >   (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _a -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ix -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    l -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    r ->
    >   do [E Value]
    vs <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    l
    >      Integer
    i <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ix E Value
    r
    >      Nat' -> [E Value] -> Integer -> E Value
    op Nat'
    n [E Value]
    vs Integer
    i
    >
    > indexFront :: Nat' -> [E Value] -> Integer -> E Value
    > indexFront :: Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    w [E Value]
    vs Integer
    ix =
    >   case Nat'
    w of
    >     Nat Integer
    n | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    ix Bool -> Bool -> Bool
    && Integer
    ix Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    n -> [E Value] -> Integer -> E Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [E Value]
    vs Integer
    ix
    >     Nat'
    Inf   | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    ix -> [E Value] -> Integer -> E Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [E Value]
    vs Integer
    ix
    >     Nat'
    _ -> EvalError -> E Value
    forall a. EvalError -> E a
    cryError (Maybe Integer -> EvalError
    InvalidIndex (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    ix))
    >
    > indexBack :: Nat' -> [E Value] -> Integer -> E Value
    > indexBack :: Nat' -> [E Value] -> Integer -> E Value
    indexBack Nat'
    w [E Value]
    vs Integer
    ix =
    >   case Nat'
    w of
    >     Nat Integer
    n | Integer
    0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    ix Bool -> Bool -> Bool
    && Integer
    ix Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    n -> [E Value] -> Integer -> E Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [E Value]
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    ix Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)
    >           | Bool
    otherwise -> EvalError -> E Value
    forall a. EvalError -> E a
    cryError (Maybe Integer -> EvalError
    InvalidIndex (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    ix))
    >     Nat'
    Inf               -> String -> [String] -> E Value
    forall a. String -> [String] -> a
    evalPanic String
    "indexBack" [String
    "unexpected infinite sequence"]
    >
    > updatePrim :: (Nat' -> Integer -> Integer) -> Value
    > updatePrim :: (Nat' -> Integer -> Integer) -> Value
    updatePrim Nat' -> Integer -> Integer
    op =
    >   (Nat' -> E Value) -> Value
    VNumPoly ((Nat' -> E Value) -> Value) -> (Nat' -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    len -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    _eltTy -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (TValue -> E Value) -> Value
    VPoly ((TValue -> E Value) -> Value) -> (TValue -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ix -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    xs -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    idx -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >   (E Value -> E Value) -> Value
    VFun ((E Value -> E Value) -> Value) -> (E Value -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \E Value
    val ->
    >   do Integer
    j <- TValue -> E Value -> E Integer
    cryToInteger TValue
    ix E Value
    idx
    >      if Integer -> Nat'
    Nat Integer
    j Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat'
    len then
    >        Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ Nat' -> (Integer -> E Value) -> Value
    generateV Nat'
    len ((Integer -> E Value) -> Value) -> (Integer -> E Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
    >          if Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat' -> Integer -> Integer
    op Nat'
    len Integer
    j then
    >            E Value
    val
    >          else
    >            do [E Value]
    xs' <- Value -> [E Value]
    fromVList (Value -> [E Value]) -> E Value -> E [E Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    xs
    >               Nat' -> [E Value] -> Integer -> E Value
    indexFront Nat'
    len [E Value]
    xs' Integer
    i
    >      else
    >        EvalError -> E Value
    forall a. EvalError -> E a
    cryError (Maybe Integer -> EvalError
    InvalidIndex (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    j))
    >
    > updateFront :: Nat' -> Integer -> Integer
    > updateFront :: Nat' -> Integer -> Integer
    updateFront Nat'
    _ Integer
    j = Integer
    j
    >
    > updateBack :: Nat' -> Integer -> Integer
    > updateBack :: Nat' -> Integer -> Integer
    updateBack Nat'
    Inf Integer
    _j = String -> [String] -> Integer
    forall a. String -> [String] -> a
    evalPanic String
    "Unexpected infinite sequence in updateEnd" []
    > updateBack (Nat Integer
    n) Integer
    j = Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    j Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

    Floating Point Numbers
    ----------------------

    Whenever we do operations that do not have an explicit rounding mode,
    we round towards the closest number, with ties resolved to the even one.

    > fpImplicitRound :: FP.RoundMode
    > fpImplicitRound :: RoundMode
    fpImplicitRound = RoundMode
    FP.NearEven

    We annotate floating point values with their precision.  This is only used
    when pretty printing values.

    > fpToBF :: Integer -> Integer -> BigFloat -> BF
    > fpToBF :: Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p BigFloat
    x = BF { bfValue :: BigFloat
    bfValue = BigFloat
    x, bfExpWidth :: Integer
    bfExpWidth = Integer
    e, bfPrecWidth :: Integer
    bfPrecWidth = Integer
    p }

    The following two functions convert between floaitng point numbers
    and integers.

    > fpFromInteger :: Integer -> Integer -> Integer -> BigFloat
    > fpFromInteger :: Integer -> Integer -> Integer -> BigFloat
    fpFromInteger Integer
    e Integer
    p = (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus ((BigFloat, Status) -> BigFloat)
    -> (Integer -> (BigFloat, Status)) -> Integer -> BigFloat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BFOpts -> BigFloat -> (BigFloat, Status)
    FP.bfRoundFloat BFOpts
    opts (BigFloat -> (BigFloat, Status))
    -> (Integer -> BigFloat) -> Integer -> (BigFloat, Status)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> BigFloat
    FP.bfFromInteger
    >   where opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts Integer
    e Integer
    p RoundMode
    fpImplicitRound

    These functions capture the interactions with rationals.

    This just captures a common pattern for binary floating point primitives.

    > fpBin :: (FP.BFOpts -> BigFloat -> BigFloat -> (BigFloat,FP.Status)) ->
    >          FP.RoundMode -> Integer -> Integer ->
    >          BigFloat -> BigFloat -> E BigFloat
    > fpBin :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f RoundMode
    r Integer
    e Integer
    p BigFloat
    x BigFloat
    y = BigFloat -> E BigFloat
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((BigFloat, Status) -> BigFloat
    FP.fpCheckStatus (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f (Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts Integer
    e Integer
    p RoundMode
    r) BigFloat
    x BigFloat
    y))

    Computes the reciprocal of a floating point number via division.
    This assumes that 1 can be represented exactly, which should be
    true for all supported precisions.

    > fpRecip :: Integer -> Integer -> BigFloat -> E BigFloat
    > fpRecip :: Integer -> Integer -> BigFloat -> E BigFloat
    fpRecip Integer
    e Integer
    p BigFloat
    x = BigFloat -> E BigFloat
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((BigFloat, Status) -> BigFloat
    FP.fpCheckStatus (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv BFOpts
    opts (Integer -> BigFloat
    FP.bfFromInteger Integer
    1) BigFloat
    x))
    >   where opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts Integer
    e Integer
    p RoundMode
    fpImplicitRound

    > floatPrimTable :: Map PrimIdent Value
    > floatPrimTable :: Map PrimIdent Value
    floatPrimTable = [(PrimIdent, Value)] -> Map PrimIdent Value
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Value)] -> Map PrimIdent Value)
    -> [(PrimIdent, Value)] -> Map PrimIdent Value
    forall a b. (a -> b) -> a -> b
    $ ((String, Value) -> (PrimIdent, Value))
    -> [(String, Value)] -> [(PrimIdent, Value)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(String
    n, Value
    v) -> (Text -> PrimIdent
    floatPrim (String -> Text
    T.pack String
    n), Value
    v))
    >    [ String
    "fpNaN"       String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (Integer -> E Value) -> Value
    vFinPoly \Integer
    p ->
    >                         Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ BF -> Value
    VFloat (BF -> Value) -> BF -> Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p BigFloat
    FP.bfNaN
    >
    >    , String
    "fpPosInf"    String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (Integer -> E Value) -> Value
    vFinPoly \Integer
    p ->
    >                         Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $ BF -> Value
    VFloat (BF -> Value) -> BF -> Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p BigFloat
    FP.bfPosInf
    >
    >    , String
    "fpFromBits"  String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (Integer -> E Value) -> Value
    vFinPoly \Integer
    p -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (E Value -> E Value) -> Value
    VFun \E Value
    bvv ->
    >                         BF -> Value
    VFloat (BF -> Value) -> (Integer -> BF) -> Integer -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> Integer -> BF
    FP.floatFromBits Integer
    e Integer
    p (Integer -> Value) -> E Integer -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    bvv)
    >
    >    , String
    "fpToBits"    String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (Integer -> E Value) -> Value
    vFinPoly \Integer
    p -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (E Value -> E Value) -> Value
    VFun \E Value
    fpv ->
    >                         Integer -> Integer -> Value
    vWord (Integer
    e Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    p) (Integer -> Value) -> (Value -> Integer) -> Value -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> Integer
    FP.floatToBits Integer
    e Integer
    p (BigFloat -> Integer) -> (Value -> BigFloat) -> Value -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> BigFloat
    fromVFloat (Value -> Value) -> E Value -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    fpv
    >
    >    , String
    "=.="         String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (E Value -> E Value) -> Value
    VFun \E Value
    xv -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                       (E Value -> E Value) -> Value
    VFun \E Value
    yv ->
    >                        do BigFloat
    x <- Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    xv
    >                           BigFloat
    y <- Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    yv
    >                           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Value
    VBit (BigFloat -> BigFloat -> Ordering
    FP.bfCompare BigFloat
    x BigFloat
    y Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ))
    >
    >    , String
    "fpIsFinite" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                      (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >                      (E Value -> E Value) -> Value
    VFun \E Value
    xv ->
    >                        do BigFloat
    x <- Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    xv
    >                           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Value
    VBit (BigFloat -> Bool
    FP.bfIsFinite BigFloat
    x))
    >
    >    , String
    "fpAdd"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Value
    fpArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfAdd
    >    , String
    "fpSub"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Value
    fpArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfSub
    >    , String
    "fpMul"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Value
    fpArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfMul
    >    , String
    "fpDiv"      String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Value
    fpArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv
    >
    >    , String
    "fpToRational" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >       (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >       (Integer -> E Value) -> Value
    vFinPoly \Integer
    _ -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >       (E Value -> E Value) -> Value
    VFun \E Value
    fpv ->
    >         do BF
    fp <- Value -> BF
    fromVFloat' (Value -> BF) -> E Value -> E BF
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    fpv
    >            Rational -> Value
    VRational (Rational -> Value) -> E Rational -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Either EvalError Rational -> E Rational
    forall a. Either EvalError a -> E a
    eitherToE (String -> BF -> Either EvalError Rational
    FP.floatToRational String
    "fpToRational" BF
    fp))
    >    , String
    "fpFromRational" String -> Value -> (String, Value)
    forall a. String -> a -> (String, a)
    ~>
    >      (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >      (Integer -> E Value) -> Value
    vFinPoly \Integer
    p -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >      (E Value -> E Value) -> Value
    VFun \E Value
    rmv -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >      (E Value -> E Value) -> Value
    VFun \E Value
    rv ->
    >        do Integer
    rm  <- Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    rmv
    >           RoundMode
    rm' <- Either EvalError RoundMode -> E RoundMode
    forall a. Either EvalError a -> E a
    eitherToE (Integer -> Either EvalError RoundMode
    FP.fpRound Integer
    rm)
    >           Rational
    rat <- Value -> Rational
    fromVRational (Value -> Rational) -> E Value -> E Rational
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    rv
    >           Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Value
    VFloat (Integer -> Integer -> RoundMode -> Rational -> BF
    FP.floatFromRational Integer
    e Integer
    p RoundMode
    rm' Rational
    rat))
    >    ]
    >   where
    >   fpArith :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Value
    fpArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f = (Integer -> E Value) -> Value
    vFinPoly \Integer
    e -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >               (Integer -> E Value) -> Value
    vFinPoly \Integer
    p -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >               (E Value -> E Value) -> Value
    VFun \E Value
    vr -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >               (E Value -> E Value) -> Value
    VFun \E Value
    xv -> Value -> E Value
    forall a. a -> E a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> E Value) -> Value -> E Value
    forall a b. (a -> b) -> a -> b
    $
    >               (E Value -> E Value) -> Value
    VFun \E Value
    yv ->
    >                 do Integer
    r <- Value -> E Integer
    fromVWord (Value -> E Integer) -> E Value -> E Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< E Value
    vr
    >                    RoundMode
    rnd <- Either EvalError RoundMode -> E RoundMode
    forall a. Either EvalError a -> E a
    eitherToE (Integer -> Either EvalError RoundMode
    FP.fpRound Integer
    r)
    >                    BigFloat
    x <- Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    xv
    >                    BigFloat
    y <- Value -> BigFloat
    fromVFloat (Value -> BigFloat) -> E Value -> E BigFloat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> E Value
    yv
    >                    BF -> Value
    VFloat (BF -> Value) -> (BigFloat -> BF) -> BigFloat -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BigFloat -> BF
    fpToBF Integer
    e Integer
    p (BigFloat -> Value) -> E BigFloat -> E Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> RoundMode
    -> Integer
    -> Integer
    -> BigFloat
    -> BigFloat
    -> E BigFloat
    fpBin BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    f RoundMode
    rnd Integer
    e Integer
    p BigFloat
    x BigFloat
    y

    Error Handling
    --------------

    The `evalPanic` function is only called if an internal data invariant
    is violated, such as an expression that is not well-typed. Panics
    should (hopefully) never occur in practice; a panic message indicates
    a bug in Cryptol.

    > evalPanic :: String -> [String] -> a
    > evalPanic :: forall a. String -> [String] -> a
    evalPanic String
    cxt = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic (String
    "[Reference Evaluator]" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)

    Pretty Printing
    ---------------

    > ppEValue :: PPOpts -> E Value -> Doc
    > ppEValue :: PPOpts -> E Value -> Doc
    ppEValue PPOpts
    _opts (Err EvalError
    e) = String -> Doc
    text (EvalError -> String
    forall a. Show a => a -> String
    show EvalError
    e)
    > ppEValue PPOpts
    opts (Value Value
    v) = PPOpts -> Value -> Doc
    ppValue PPOpts
    opts Value
    v
    >
    > ppValue :: PPOpts -> Value -> Doc
    > ppValue :: PPOpts -> Value -> Doc
    ppValue PPOpts
    opts Value
    val =
    >   case Value
    val of
    >     VBit Bool
    b     -> String -> Doc
    text (Bool -> String
    forall a. Show a => a -> String
    show Bool
    b)
    >     VInteger Integer
    i -> String -> Doc
    text (Integer -> String
    forall a. Show a => a -> String
    show Integer
    i)
    >     VRational Rational
    q -> String -> Doc
    text (Rational -> String
    forall a. Show a => a -> String
    show Rational
    q)
    >     VFloat BF
    fl -> String -> Doc
    text (Doc -> String
    forall a. Show a => a -> String
    show (PPOpts -> BF -> Doc
    FP.fpPP PPOpts
    opts BF
    fl))
    >     VList Nat'
    l [E Value]
    vs ->
    >       case Nat'
    l of
    >         Nat'
    Inf -> [Doc] -> Doc
    ppList ((E Value -> Doc) -> [E Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> E Value -> Doc
    ppEValue PPOpts
    opts)
    >                   (Int -> [E Value] -> [E Value]
    forall a. Int -> [a] -> [a]
    take (PPOpts -> Int
    useInfLength PPOpts
    opts) [E Value]
    vs) [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Doc
    text String
    "..."])
    >         Nat Integer
    n ->
    >           -- For lists of defined bits, print the value as a numeral.
    >           case (E Value -> Maybe Bool) -> [E Value] -> Maybe [Bool]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse E Value -> Maybe Bool
    isBit [E Value]
    vs of
    >             Just [Bool]
    bs -> PPOpts -> BV -> Doc
    ppBV PPOpts
    opts (Integer -> Integer -> BV
    mkBv Integer
    n ([Bool] -> Integer
    bitsToInteger [Bool]
    bs))
    >             Maybe [Bool]
    Nothing -> [Doc] -> Doc
    ppList ((E Value -> Doc) -> [E Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> E Value -> Doc
    ppEValue PPOpts
    opts) [E Value]
    vs)
    >       where isBit :: E Value -> Maybe Bool
    isBit E Value
    v = case E Value
    v of Value (VBit Bool
    b) -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    b
    >                                 E Value
    _      -> Maybe Bool
    forall a. Maybe a
    Nothing
    >     VTuple [E Value]
    vs  -> [Doc] -> Doc
    ppTuple ((E Value -> Doc) -> [E Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> E Value -> Doc
    ppEValue PPOpts
    opts) [E Value]
    vs)
    >     VRecord [(Ident, E Value)]
    fs -> [Doc] -> Doc
    ppRecord (((Ident, E Value) -> Doc) -> [(Ident, E Value)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, E Value) -> Doc
    forall {a}. PP a => (a, E Value) -> Doc
    ppField [(Ident, E Value)]
    fs)
    >       where ppField :: (a, E Value) -> Doc
    ppField (a
    f,E Value
    r) = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    f Doc -> Doc -> Doc
    <+> Char -> Doc
    char Char
    '=' Doc -> Doc -> Doc
    <+> PPOpts -> E Value -> Doc
    ppEValue PPOpts
    opts E Value
    r
    >     VFun E Value -> E Value
    _     -> String -> Doc
    text String
    "<function>"
    >     VPoly TValue -> E Value
    _    -> String -> Doc
    text String
    "<polymorphic value>"
    >     VNumPoly Nat' -> E Value
    _ -> String -> Doc
    text String
    "<polymorphic value>"

    Module Command
    --------------

    This module implements the core functionality of the `:eval
    <expression>` command for the Cryptol REPL, which prints the result of
    running the reference evaluator on an expression.

    > evaluate :: Expr -> M.ModuleCmd (E Value)
    > evaluate :: Expr -> ModuleCmd (E Value)
    evaluate Expr
    expr ModuleInput IO
    minp = ModuleRes (E Value) -> IO (ModuleRes (E Value))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((E Value, ModuleEnv) -> Either ModuleError (E Value, ModuleEnv)
    forall a b. b -> Either a b
    Right (E Value
    val, ModuleEnv
    modEnv), [])
    >   where
    >     modEnv :: ModuleEnv
    modEnv = ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    M.minpModuleEnv ModuleInput IO
    minp
    >     extDgs :: [DeclGroup]
    extDgs = (ModuleG ModName -> [DeclGroup])
    -> [ModuleG ModName] -> [DeclGroup]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ModuleG ModName -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls (ModuleEnv -> [ModuleG ModName]
    M.loadedModules ModuleEnv
    modEnv) [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ DynamicEnv -> [DeclGroup]
    M.deDecls (ModuleEnv -> DynamicEnv
    M.meDynEnv ModuleEnv
    modEnv)
    >     nts :: [Newtype]
    nts    = Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems (ModuleEnv -> Map Name Newtype
    M.loadedNewtypes ModuleEnv
    modEnv)
    >     env :: Env
    env    = (Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Env -> DeclGroup -> Env
    evalDeclGroup ((Env -> Newtype -> Env) -> Env -> [Newtype] -> Env
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Env -> Newtype -> Env
    evalNewtypeDecl Env
    forall a. Monoid a => a
    mempty [Newtype]
    nts) [DeclGroup]
    extDgs
    >     val :: E Value
    val    = Env -> Expr -> E Value
    evalExpr Env
    env Expr
    expr