    > -- |
    > -- Module      :  Cryptol.Eval.Reference
    > -- Description :  The reference implementation of the Cryptol evaluation semantics.
    > -- Copyright   :  (c) 2013-2016 Galois, Inc.
    > -- License     :  BSD3
    > -- Maintainer  :  cryptol@galois.com
    > -- Stability   :  provisional
    > -- Portability :  portable
    >
    > {-# LANGUAGE PatternGuards #-}
    >
    > module Cryptol.Eval.Reference
    >   ( Value(..)
    >   , evaluate
    >   , ppValue
    >   ) where
    >
    > import Control.Applicative (liftA2)
    > import Data.Bits
    > import Data.List
    >   (genericDrop, genericIndex, genericLength, genericReplicate, genericSplitAt,
    >    genericTake, sortBy)
    > import Data.Ord (comparing)
    > import Data.Map (Map)
    > import qualified Data.Map as Map
    > import Data.Semigroup (Semigroup(..))
    > import qualified Data.Text as T (pack)
    >
    > import Cryptol.ModuleSystem.Name (asPrim)
    > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
    > import Cryptol.TypeCheck.AST
    > import Cryptol.Eval.Monad (EvalError(..), PPOpts(..))
    > import Cryptol.Eval.Type (TValue(..), isTBit, evalValType, evalNumType, tvSeq)
    > import Cryptol.Eval.Value (mkBv, ppBV)
    > import Cryptol.Prims.Eval (lg2)
    > import Cryptol.Utils.Ident (Ident, mkIdent)
    > import Cryptol.Utils.Panic (panic)
    > import Cryptol.Utils.PP
    >
    > import qualified Cryptol.ModuleSystem as M
    > import qualified Cryptol.ModuleSystem.Env as M (loadedModules)

    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`                 |
    | `[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 Cryptol value type `t` as a complete partial order (cpo)
    *M*(`t`). To each Cryptol expression `e : t` we assign a meaning
    *M*(`e`) in *M*(`t`); in particular, recursive Cryptol programs of
    type `t` are modeled as least fixed points in *M*(`t`). In other words,
    this is a domain-theoretic denotational semantics.

    Evaluating a Cryptol expression of type `Bit` may result in:

    - a defined value `True` or `False`

    - a run-time error, or

    - non-termination.

    Accordingly, *M*(`Bit`) is a flat cpo with values for `True`,
    `False`, run-time errors of type `EvalError`, and $\bot$; we
    represent it with the Haskell type `Either EvalError Bool`.

    Similarly, *M*(`Integer`) is a flat cpo with values for integers,
    run-time errors, and $\bot$; we represent it with the Haskell type
    `Either EvalError Integer`.

    The cpos for lists, tuples, and records are cartesian products. The
    cpo ordering is pointwise, and the bottom element $\bot$ is the
    list/tuple/record whose elements are all $\bot$. Trivial types `[0]t`,
    `()` and `{}` denote single-element cpos where the unique value
    `[]`/`()`/`{}` *is* the bottom element $\bot$. *M*(`a -> b`) is the
    continuous function space *M*(`a`) $\to$ *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 *M*(`t[t1/a1 ... tn/an]`).

    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 (Either EvalError Bool) -- ^ @ Bit    @ booleans
    >   | VInteger (Either EvalError Integer) -- ^ @ Integer @ integers
    >   | VList Nat' [Value]           -- ^ @ [n]a   @ finite or infinite lists
    >   | VTuple [Value]               -- ^ @ ( .. ) @ tuples
    >   | VRecord [(Ident, Value)]     -- ^ @ { .. } @ records
    >   | VFun (Value -> Value)        -- ^ functions
    >   | VPoly (TValue -> Value)      -- ^ polymorphic values (kind *)
    >   | VNumPoly (Nat' -> Value)     -- ^ polymorphic values (kind #)

    Invariant: Undefinedness and run-time exceptions are only allowed
    inside the argument of a `VBit` or `VInteger` constructor. All other
    `Value` and list constructors should evaluate without error. For
    example, a non-terminating computation at type `(Bit,Bit)` must be
    represented as `VTuple [VBit undefined, VBit undefined]`, and not
    simply as `undefined`. Similarly, an expression like `1/0:[2]` that
    raises a run-time error must be encoded as `VList (Nat 2) [VBit (Left
    e), VBit (Left e)]` where `e = DivideByZero`.

    Copy Functions
    --------------

    Functions `copyBySchema` and `copyByTValue` make a copy of the given
    value, building the spine based only on the type without forcing the
    value argument. This ensures that undefinedness appears inside `VBit`
    and `VInteger` values only, and never on any constructors of the
    `Value` type. In turn, this gives the appropriate semantics to
    recursive definitions: The bottom value for a compound type is equal
    to a value of the same type where every individual bit is bottom.

    For each Cryptol type `t`, the cpo *M*(`t`) can be represented as a
    subset of values of type `Value` that satisfy the datatype invariant.
    This subset consists precisely of the output range of `copyByTValue
    t`. Similarly, the range of output values of `copyBySchema` yields the
    cpo that represents any given schema.

    > copyBySchema :: Env -> Schema -> Value -> Value
    > copyBySchema :: Env -> Schema -> Value -> Value
    copyBySchema env0 :: Env
    env0 (Forall params :: [TParam]
    params _props :: [Prop]
    _props ty :: Prop
    ty) = [TParam] -> Env -> Value -> Value
    go [TParam]
    params Env
    env0
    >   where
    >     go :: [TParam] -> Env -> Value -> Value
    >     go :: [TParam] -> Env -> Value -> Value
    go []       env :: Env
    env v :: Value
    v = TValue -> Value -> Value
    copyByTValue (HasCallStack => TypeEnv -> Prop -> TValue
    TypeEnv -> Prop -> TValue
    evalValType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty) Value
    v
    >     go (p :: TParam
    p : ps :: [TParam]
    ps) env :: Env
    env v :: Value
    v =
    >       case Value
    v of
    >         VPoly    f :: TValue -> Value
    f -> (TValue -> Value) -> Value
    VPoly    ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \t :: TValue
    t -> [TParam] -> Env -> Value -> Value
    go [TParam]
    ps (TVar -> Either Nat' TValue -> Env -> Env
    bindType (TParam -> TVar
    tpVar TParam
    p) (TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right TValue
    t) Env
    env) (TValue -> Value
    f TValue
    t)
    >         VNumPoly f :: Nat' -> Value
    f -> (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n -> [TParam] -> Env -> Value -> Value
    go [TParam]
    ps (TVar -> Either Nat' TValue -> Env -> Env
    bindType (TParam -> TVar
    tpVar TParam
    p) (Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left Nat'
    n)  Env
    env) (Nat' -> Value
    f Nat'
    n)
    >         _          -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "copyBySchema" ["Expected polymorphic value"]
    >
    > copyByTValue :: TValue -> Value -> Value
    > copyByTValue :: TValue -> Value -> Value
    copyByTValue = TValue -> Value -> Value
    go
    >   where
    >     go :: TValue -> Value -> Value
    >     go :: TValue -> Value -> Value
    go ty :: TValue
    ty val :: Value
    val =
    >       case TValue
    ty of
    >         TVBit        -> Either EvalError Bool -> Value
    VBit (Value -> Either EvalError Bool
    fromVBit Value
    val)
    >         TVInteger    -> Either EvalError Integer -> Value
    VInteger (Value -> Either EvalError Integer
    fromVInteger Value
    val)
    >         TVIntMod _   -> Either EvalError Integer -> Value
    VInteger (Value -> Either EvalError Integer
    fromVInteger Value
    val)
    >         TVSeq w :: Integer
    w ety :: TValue
    ety  -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    ety) (Integer -> [Value] -> [Value]
    forall a. Integer -> [a] -> [a]
    copyList Integer
    w (Value -> [Value]
    fromVList Value
    val)))
    >         TVStream ety :: TValue
    ety -> Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    ety) ([Value] -> [Value]
    forall a. [a] -> [a]
    copyStream (Value -> [Value]
    fromVList Value
    val)))
    >         TVTuple etys :: [TValue]
    etys -> [Value] -> Value
    VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> Value -> Value
    go [TValue]
    etys (Integer -> [Value] -> [Value]
    forall a. Integer -> [a] -> [a]
    copyList ([TValue] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [TValue]
    etys) (Value -> [Value]
    fromVTuple Value
    val)))
    >         TVRec fields :: [(Ident, TValue)]
    fields -> [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value -> Value
    go TValue
    fty (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    val)) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fields ]
    >         TVFun _ bty :: TValue
    bty  -> (Value -> Value) -> Value
    VFun (\v :: Value
    v -> TValue -> Value -> Value
    go TValue
    bty (Value -> Value -> Value
    fromVFun Value
    val Value
    v))
    >         TVAbstract {} -> Value
    val
    >
    > copyStream :: [a] -> [a]
    > copyStream :: [a] -> [a]
    copyStream xs :: [a]
    xs = [a] -> a
    forall a. [a] -> a
    head [a]
    xs a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> [a]
    forall a. [a] -> [a]
    copyStream ([a] -> [a]
    forall a. [a] -> [a]
    tail [a]
    xs)
    >
    > copyList :: Integer -> [a] -> [a]
    > copyList :: Integer -> [a] -> [a]
    copyList 0 _ = []
    > copyList n :: Integer
    n xs :: [a]
    xs = [a] -> a
    forall a. [a] -> a
    head [a]
    xs a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : Integer -> [a] -> [a]
    forall a. Integer -> [a] -> [a]
    copyList (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1) ([a] -> [a]
    forall a. [a] -> [a]
    tail [a]
    xs)

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

    > -- | Destructor for @VBit@.
    > fromVBit :: Value -> Either EvalError Bool
    > fromVBit :: Value -> Either EvalError Bool
    fromVBit (VBit b :: Either EvalError Bool
    b) = Either EvalError Bool
    b
    > fromVBit _        = String -> [String] -> Either EvalError Bool
    forall a. String -> [String] -> a
    evalPanic "fromVBit" ["Expected a bit"]
    >
    > -- | Destructor for @VInteger@.
    > fromVInteger :: Value -> Either EvalError Integer
    > fromVInteger :: Value -> Either EvalError Integer
    fromVInteger (VInteger i :: Either EvalError Integer
    i) = Either EvalError Integer
    i
    > fromVInteger _            = String -> [String] -> Either EvalError Integer
    forall a. String -> [String] -> a
    evalPanic "fromVInteger" ["Expected an integer"]
    >
    > -- | Destructor for @VList@.
    > fromVList :: Value -> [Value]
    > fromVList :: Value -> [Value]
    fromVList (VList _ vs :: [Value]
    vs) = [Value]
    vs
    > fromVList _            = String -> [String] -> [Value]
    forall a. String -> [String] -> a
    evalPanic "fromVList" ["Expected a list"]
    >
    > -- | Destructor for @VTuple@.
    > fromVTuple :: Value -> [Value]
    > fromVTuple :: Value -> [Value]
    fromVTuple (VTuple vs :: [Value]
    vs) = [Value]
    vs
    > fromVTuple _           = String -> [String] -> [Value]
    forall a. String -> [String] -> a
    evalPanic "fromVTuple" ["Expected a tuple"]
    >
    > -- | Destructor for @VRecord@.
    > fromVRecord :: Value -> [(Ident, Value)]
    > fromVRecord :: Value -> [(Ident, Value)]
    fromVRecord (VRecord fs :: [(Ident, Value)]
    fs) = [(Ident, Value)]
    fs
    > fromVRecord _            = String -> [String] -> [(Ident, Value)]
    forall a. String -> [String] -> a
    evalPanic "fromVRecord" ["Expected a record"]
    >
    > -- | Destructor for @VFun@.
    > fromVFun :: Value -> (Value -> Value)
    > fromVFun :: Value -> Value -> Value
    fromVFun (VFun f :: Value -> Value
    f) = Value -> Value
    f
    > fromVFun _        = String -> [String] -> Value -> Value
    forall a. String -> [String] -> a
    evalPanic "fromVFun" ["Expected a function"]
    >
    > -- | Destructor for @VPoly@.
    > fromVPoly :: Value -> (TValue -> Value)
    > fromVPoly :: Value -> TValue -> Value
    fromVPoly (VPoly f :: TValue -> Value
    f) = TValue -> Value
    f
    > fromVPoly _         = String -> [String] -> TValue -> Value
    forall a. String -> [String] -> a
    evalPanic "fromVPoly" ["Expected a polymorphic value"]
    >
    > -- | Destructor for @VNumPoly@.
    > fromVNumPoly :: Value -> (Nat' -> Value)
    > fromVNumPoly :: Value -> Nat' -> Value
    fromVNumPoly (VNumPoly f :: Nat' -> Value
    f) = Nat' -> Value
    f
    > fromVNumPoly _            = String -> [String] -> Nat' -> Value
    forall a. String -> [String] -> a
    evalPanic "fromVNumPoly" ["Expected a polymorphic value"]
    >
    > -- | Look up a field in a record.
    > lookupRecord :: Ident -> Value -> Value
    > lookupRecord :: Ident -> Value -> Value
    lookupRecord f :: Ident
    f v :: Value
    v =
    >   case Ident -> [(Ident, Value)] -> Maybe Value
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Ident
    f (Value -> [(Ident, Value)]
    fromVRecord Value
    v) of
    >     Just val :: Value
    val -> Value
    val
    >     Nothing  -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "lookupRecord" ["Malformed record"]
    >
    > -- | Polymorphic function values that expect a finite numeric type.
    > vFinPoly :: (Integer -> Value) -> Value
    > vFinPoly :: (Integer -> Value) -> Value
    vFinPoly f :: Integer -> Value
    f = (Nat' -> Value) -> Value
    VNumPoly Nat' -> Value
    g
    >   where
    >     g :: Nat' -> Value
    g (Nat n :: Integer
    n) = Integer -> Value
    f Integer
    n
    >     g Inf     = String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "vFinPoly" ["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 Value
    envVars       :: !(Map Name Value)
    >   , Env -> TypeEnv
    envTypes      :: !(Map TVar (Either Nat' TValue))
    >   }
    >
    > instance Semigroup Env where
    >   l :: Env
    l <> :: Env -> Env -> Env
    <> r :: Env
    r = $WEnv :: Map Name Value -> TypeEnv -> Env
    Env
    >     { envVars :: Map Name Value
    envVars  = Map Name Value -> Map Name Value -> Map Name Value
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (Env -> Map Name Value
    envVars  Env
    l) (Env -> Map Name Value
    envVars  Env
    r)
    >     , envTypes :: TypeEnv
    envTypes = TypeEnv -> TypeEnv -> TypeEnv
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (Env -> TypeEnv
    envTypes Env
    l) (Env -> TypeEnv
    envTypes Env
    r)
    >     }
    >
    > instance Monoid Env where
    >   mempty :: Env
    mempty = $WEnv :: Map Name Value -> TypeEnv -> Env
    Env
    >     { envVars :: Map Name Value
    envVars  = Map Name Value
    forall k a. Map k a
    Map.empty
    >     , envTypes :: TypeEnv
    envTypes = TypeEnv
    forall k a. Map k a
    Map.empty
    >     }
    >   mappend :: Env -> Env -> Env
    mappend l :: Env
    l r :: Env
    r = Env
    l Env -> Env -> Env
    forall a. Semigroup a => a -> a -> a
    <> Env
    r
    >
    > -- | Bind a variable in the evaluation environment.
    > bindVar :: (Name, Value) -> Env -> Env
    > bindVar :: (Name, Value) -> Env -> Env
    bindVar (n :: Name
    n, val :: Value
    val) env :: Env
    env = Env
    env { envVars :: Map Name Value
    envVars = Name -> Value -> Map Name Value -> Map Name Value
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n Value
    val (Env -> Map Name 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 p :: TVar
    p ty :: Either Nat' TValue
    ty env :: Env
    env = Env
    env { envTypes :: TypeEnv
    envTypes = TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert 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
    >          -> Value
    > evalExpr :: Env -> Expr -> Value
    evalExpr env :: Env
    env expr :: Expr
    expr =
    >   case Expr
    expr of
    >
    >     EList es :: [Expr]
    es _ty :: Prop
    _ty  -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat ([Expr] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Expr]
    es)) [ Env -> Expr -> Value
    evalExpr Env
    env Expr
    e | Expr
    e <- [Expr]
    es ]
    >     ETuple es :: [Expr]
    es     -> [Value] -> Value
    VTuple [ Env -> Expr -> Value
    evalExpr Env
    env Expr
    e | Expr
    e <- [Expr]
    es ]
    >     ERec fields :: [(Ident, Expr)]
    fields   -> [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, Env -> Expr -> Value
    evalExpr Env
    env Expr
    e) | (f :: Ident
    f, e :: Expr
    e) <- [(Ident, Expr)]
    fields ]
    >     ESel e :: Expr
    e sel :: Selector
    sel    -> Value -> Selector -> Value
    evalSel (Env -> Expr -> Value
    evalExpr Env
    env Expr
    e) Selector
    sel
    >     ESet e :: Expr
    e sel :: Selector
    sel v :: Expr
    v  -> Value -> Selector -> Value -> Value
    evalSet (Env -> Expr -> Value
    evalExpr Env
    env Expr
    e) Selector
    sel (Env -> Expr -> Value
    evalExpr Env
    env Expr
    v)
    >
    >     EIf c :: Expr
    c t :: Expr
    t f :: Expr
    f ->
    >       Either EvalError Bool -> Value -> Value -> Value
    condValue (Value -> Either EvalError Bool
    fromVBit (Env -> Expr -> Value
    evalExpr Env
    env Expr
    c)) (Env -> Expr -> Value
    evalExpr Env
    env Expr
    t) (Env -> Expr -> Value
    evalExpr Env
    env Expr
    f)
    >
    >     EComp _n :: Prop
    _n _ty :: Prop
    _ty e :: Expr
    e branches :: [[Match]]
    branches ->
    >       Env -> Expr -> [[Match]] -> Value
    evalComp Env
    env Expr
    e [[Match]]
    branches
    >
    >     EVar n :: Name
    n ->
    >       case Name -> Map Name Value -> Maybe Value
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n (Env -> Map Name Value
    envVars Env
    env) of
    >         Just val :: Value
    val -> Value
    val
    >         Nothing  -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "evalExpr" ["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]
    ++ "` is not defined" ]
    >
    >     ETAbs tv :: TParam
    tv b :: Expr
    b ->
    >       case TParam -> Kind
    tpKind TParam
    tv of
    >         KType -> (TValue -> Value) -> Value
    VPoly    ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty -> Env -> Expr -> 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
    >         KNum  -> (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n  -> Env -> Expr -> 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
    >         k :: Kind
    k     -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "evalExpr" ["Invalid kind on type abstraction", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]
    >
    >     ETApp e :: Expr
    e ty :: Prop
    ty ->
    >       case Env -> Expr -> Value
    evalExpr Env
    env Expr
    e of
    >         VPoly f :: TValue -> Value
    f     -> TValue -> Value
    f (TValue -> Value) -> TValue -> Value
    forall a b. (a -> b) -> a -> b
    $! (HasCallStack => TypeEnv -> Prop -> TValue
    TypeEnv -> Prop -> TValue
    evalValType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty)
    >         VNumPoly f :: Nat' -> Value
    f  -> Nat' -> Value
    f (Nat' -> Value) -> Nat' -> Value
    forall a b. (a -> b) -> a -> b
    $! (HasCallStack => TypeEnv -> Prop -> Nat'
    TypeEnv -> Prop -> Nat'
    evalNumType (Env -> TypeEnv
    envTypes Env
    env) Prop
    ty)
    >         _           -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "evalExpr" ["Expected a polymorphic value"]
    >
    >     EApp e1 :: Expr
    e1 e2 :: Expr
    e2     -> Value -> Value -> Value
    fromVFun (Env -> Expr -> Value
    evalExpr Env
    env Expr
    e1) (Env -> Expr -> Value
    evalExpr Env
    env Expr
    e2)
    >     EAbs n :: Name
    n _ty :: Prop
    _ty b :: Expr
    b   -> (Value -> Value) -> Value
    VFun (\v :: Value
    v -> Env -> Expr -> Value
    evalExpr ((Name, Value) -> Env -> Env
    bindVar (Name
    n, Value
    v) Env
    env) Expr
    b)
    >     EProofAbs _ e :: Expr
    e  -> Env -> Expr -> Value
    evalExpr Env
    env Expr
    e
    >     EProofApp e :: Expr
    e    -> Env -> Expr -> Value
    evalExpr Env
    env Expr
    e
    >     EWhere e :: Expr
    e dgs :: [DeclGroup]
    dgs   -> Env -> Expr -> Value
    evalExpr ((Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Env -> DeclGroup -> Env
    evalDeclGroup Env
    env [DeclGroup]
    dgs) Expr
    e

    Selectors
    ---------

    Apply the the given selector form to the given value.

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

    Update the given value using the given selector and new value.

    > evalSet :: Value -> Selector -> Value -> Value
    > evalSet :: Value -> Selector -> Value -> Value
    evalSet val :: Value
    val sel :: Selector
    sel fval :: Value
    fval =
    >   case Selector
    sel of
    >     TupleSel n :: Int
    n _  -> Int -> Value
    updTupleAt Int
    n
    >     RecordSel n :: Ident
    n _ -> Ident -> Value
    updRecAt Ident
    n
    >     ListSel n :: Int
    n _   -> Int -> Value
    updSeqAt Int
    n
    >   where
    >     updTupleAt :: Int -> Value
    updTupleAt n :: Int
    n =
    >       case Value
    val of
    >         VTuple vs :: [Value]
    vs | (as :: [Value]
    as,_:bs :: [Value]
    bs) <- Int -> [Value] -> ([Value], [Value])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Value]
    vs ->
    >           [Value] -> Value
    VTuple ([Value]
    as [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Value
    fval Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    bs)
    >         _ -> String -> Value
    forall a. String -> a
    bad "Invalid tuple upldate."
    >
    >     updRecAt :: Ident -> Value
    updRecAt n :: Ident
    n =
    >       case Value
    val of
    >         VRecord vs :: [(Ident, Value)]
    vs | (as :: [(Ident, Value)]
    as, (i :: Ident
    i,_) : bs :: [(Ident, Value)]
    bs) <- ((Ident, Value) -> Bool)
    -> [(Ident, Value)] -> ([(Ident, Value)], [(Ident, Value)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break ((Ident
    nIdent -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Ident -> Bool)
    -> ((Ident, Value) -> Ident) -> (Ident, Value) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, Value) -> Ident
    forall a b. (a, b) -> a
    fst) [(Ident, Value)]
    vs ->
    >           [(Ident, Value)] -> Value
    VRecord ([(Ident, Value)]
    as [(Ident, Value)] -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. [a] -> [a] -> [a]
    ++ (Ident
    i,Value
    fval) (Ident, Value) -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. a -> [a] -> [a]
    : [(Ident, Value)]
    bs)
    >         _ -> String -> Value
    forall a. String -> a
    bad "Invalid record update."
    >
    >     updSeqAt :: Int -> Value
    updSeqAt n :: Int
    n =
    >       case Value
    val of
    >         VList i :: Nat'
    i vs :: [Value]
    vs | (as :: [Value]
    as, _ : bs :: [Value]
    bs) <- Int -> [Value] -> ([Value], [Value])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Value]
    vs ->
    >           Nat' -> [Value] -> Value
    VList Nat'
    i ([Value]
    as [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Value
    fval Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    bs)
    >         _ -> String -> Value
    forall a. String -> a
    bad "Invalid sequence update."
    >
    >     bad :: String -> a
    bad msg :: String
    msg = String -> [String] -> a
    forall a. String -> [String] -> a
    evalPanic "evalSet" [String
    msg]

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

    We evaluate conditionals on larger types by pushing the conditionals
    down to the individual bits.

    > condValue :: Either EvalError Bool -> Value -> Value -> Value
    > condValue :: Either EvalError Bool -> Value -> Value -> Value
    condValue c :: Either EvalError Bool
    c l :: Value
    l r :: Value
    r =
    >   case Value
    l of
    >     VBit b :: Either EvalError Bool
    b     -> Either EvalError Bool -> Value
    VBit (Either EvalError Bool
    -> Either EvalError Bool
    -> Either EvalError Bool
    -> Either EvalError Bool
    forall e a. Either e Bool -> Either e a -> Either e a -> Either e a
    condBit Either EvalError Bool
    c Either EvalError Bool
    b (Value -> Either EvalError Bool
    fromVBit Value
    r))
    >     VInteger i :: Either EvalError Integer
    i -> Either EvalError Integer -> Value
    VInteger (Either EvalError Bool
    -> Either EvalError Integer
    -> Either EvalError Integer
    -> Either EvalError Integer
    forall e a. Either e Bool -> Either e a -> Either e a -> Either e a
    condBit Either EvalError Bool
    c Either EvalError Integer
    i (Value -> Either EvalError Integer
    fromVInteger Value
    r))
    >     VList n :: Nat'
    n vs :: [Value]
    vs -> Nat' -> [Value] -> Value
    VList Nat'
    n ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c) [Value]
    vs (Value -> [Value]
    fromVList Value
    r))
    >     VTuple vs :: [Value]
    vs  -> [Value] -> Value
    VTuple ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c) [Value]
    vs (Value -> [Value]
    fromVTuple Value
    r))
    >     VRecord fs :: [(Ident, Value)]
    fs -> [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c Value
    v (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    r)) | (f :: Ident
    f, v :: Value
    v) <- [(Ident, Value)]
    fs ]
    >     VFun f :: Value -> Value
    f     -> (Value -> Value) -> Value
    VFun (\v :: Value
    v -> Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c (Value -> Value
    f Value
    v) (Value -> Value -> Value
    fromVFun Value
    r Value
    v))
    >     VPoly f :: TValue -> Value
    f    -> (TValue -> Value) -> Value
    VPoly (\t :: TValue
    t -> Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c (TValue -> Value
    f TValue
    t) (Value -> TValue -> Value
    fromVPoly Value
    r TValue
    t))
    >     VNumPoly f :: Nat' -> Value
    f -> (Nat' -> Value) -> Value
    VNumPoly (\n :: Nat'
    n -> Either EvalError Bool -> Value -> Value -> Value
    condValue Either EvalError Bool
    c (Nat' -> Value
    f Nat'
    n) (Value -> Nat' -> Value
    fromVNumPoly Value
    r Nat'
    n))

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

    > condBit :: Either e Bool -> Either e a -> Either e a -> Either e a
    > condBit :: Either e Bool -> Either e a -> Either e a -> Either e a
    condBit (Left e :: e
    e)  _ _ = e -> Either e a
    forall a b. a -> Either a b
    Left e
    e
    > condBit (Right b :: Bool
    b) x :: Either e a
    x y :: Either e a
    y = if Bool
    b then Either e a
    x else Either e a
    y

    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
    env m :: Match
    m =
    >   case Match
    m of
    >     Let d :: Decl
    d ->
    >       [ (Name, Value) -> Env -> Env
    bindVar (Env -> Decl -> (Name, Value)
    evalDecl Env
    env Decl
    d) Env
    env ]
    >     From n :: Name
    n _l :: Prop
    _l _ty :: Prop
    _ty expr :: Expr
    expr ->
    >       [ (Name, Value) -> Env -> Env
    bindVar (Name
    n, Value
    v) Env
    env | Value
    v <- Value -> [Value]
    fromVList (Env -> Expr -> Value
    evalExpr Env
    env Expr
    expr) ]

    > lenMatch :: Env -> Match -> Nat'
    > lenMatch :: Env -> Match -> Nat'
    lenMatch env :: Env
    env m :: Match
    m =
    >   case Match
    m of
    >     Let _          -> Integer -> Nat'
    Nat 1
    >     From _ len :: Prop
    len _ _ -> HasCallStack => TypeEnv -> Prop -> Nat'
    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
    env]
    > evalBranch env :: Env
    env (match :: Match
    match : matches :: [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
    _env [] = Integer -> Nat'
    Nat 1
    > lenBranch env :: Env
    env (match :: Match
    match : matches :: [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
    >          -> Value
    > evalComp :: Env -> Expr -> [[Match]] -> Value
    evalComp env :: Env
    env expr :: Expr
    expr branches :: [[Match]]
    branches = Nat' -> [Value] -> Value
    VList Nat'
    len [ Env -> Expr -> 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 (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 (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
    env dg :: DeclGroup
    dg = do
    >   case DeclGroup
    dg of
    >     NonRecursive d :: Decl
    d ->
    >       (Name, Value) -> Env -> Env
    bindVar (Env -> Decl -> (Name, Value)
    evalDecl Env
    env Decl
    d) Env
    env
    >     Recursive ds :: [Decl]
    ds ->
    >       let env' :: Env
    env' = ((Name, Value) -> Env -> Env) -> Env -> [(Name, Value)] -> Env
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, Value) -> Env -> Env
    bindVar Env
    env [(Name, Value)]
    bindings
    >           bindings :: [(Name, Value)]
    bindings = (Decl -> (Name, Value)) -> [Decl] -> [(Name, Value)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Env -> Decl -> (Name, Value)
    evalDeclRecursive Env
    env') [Decl]
    ds
    >       in Env
    env'

    To evaluate a declaration in a non-recursive context, we need only
    evaluate the expression on the right-hand side or look up the
    appropriate primitive.

    > evalDecl :: Env -> Decl -> (Name, Value)
    > evalDecl :: Env -> Decl -> (Name, Value)
    evalDecl env :: Env
    env d :: Decl
    d =
    >   case Decl -> DeclDef
    dDefinition Decl
    d of
    >     DPrim   -> (Decl -> Name
    dName Decl
    d, Name -> Value
    evalPrim (Decl -> Name
    dName Decl
    d))
    >     DExpr e :: Expr
    e -> (Decl -> Name
    dName Decl
    d, Env -> Expr -> Value
    evalExpr Env
    env Expr
    e)

    To evaluate a declaration in a recursive context, we must perform a
    type-directed copy to build the spine of the value. This ensures that
    the definedness invariant for type `Value` will be maintained.

    > evalDeclRecursive :: Env -> Decl -> (Name, Value)
    > evalDeclRecursive :: Env -> Decl -> (Name, Value)
    evalDeclRecursive env :: Env
    env d :: Decl
    d =
    >   case Decl -> DeclDef
    dDefinition Decl
    d of
    >     DPrim   -> (Decl -> Name
    dName Decl
    d, Name -> Value
    evalPrim (Decl -> Name
    dName Decl
    d))
    >     DExpr e :: Expr
    e -> (Decl -> Name
    dName Decl
    d, Env -> Schema -> Value -> Value
    copyBySchema Env
    env (Decl -> Schema
    dSignature Decl
    d) (Env -> Expr -> Value
    evalExpr Env
    env Expr
    e))

    Primitives
    ==========

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

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

    Cryptol primitives fall into several groups:

    * Logic: `&&`, `||`, `^`, `complement`, `zero`, `True`, `False`

    * Arithmetic: `+`, `-`, `*`, `/`, `%`, `^^`, `lg2`, `negate`, `number`

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

    * Sequences: `#`, `join`, `split`, `splitAt`, `reverse`, `transpose`

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

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

    * Enumerations: `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`

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

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

    > primTable :: Map Ident Value
    > primTable :: Map Ident Value
    primTable = [(Ident, Value)] -> Map Ident Value
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Ident, Value)] -> Map Ident Value)
    -> [(Ident, Value)] -> Map Ident Value
    forall a b. (a -> b) -> a -> b
    $ ((String, Value) -> (Ident, Value))
    -> [(String, Value)] -> [(Ident, Value)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(n :: String
    n, v :: Value
    v) -> (Text -> Ident
    mkIdent (String -> Text
    T.pack String
    n), Value
    v))
    >
    >   -- Logic (bitwise):
    >   [ ("&&"         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
    logicBinary Bool -> Bool -> Bool
    (&&)))
    >   , ("||"         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
    logicBinary Bool -> Bool -> Bool
    (||)))
    >   , ("^"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
    logicBinary Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=)))
    >   , ("complement" , (TValue -> Value -> Value) -> Value
    unary  ((Bool -> Bool) -> TValue -> Value -> Value
    logicUnary Bool -> Bool
    not))
    >   , ("zero"       , (TValue -> Value) -> Value
    VPoly (Either EvalError Bool -> TValue -> Value
    logicNullary (Bool -> Either EvalError Bool
    forall a b. b -> Either a b
    Right Bool
    False)))
    >   , ("True"       , Either EvalError Bool -> Value
    VBit (Bool -> Either EvalError Bool
    forall a b. b -> Either a b
    Right Bool
    True))
    >   , ("False"      , Either EvalError Bool -> Value
    VBit (Bool -> Either EvalError Bool
    forall a b. b -> Either a b
    Right Bool
    False))
    >
    >   -- Arithmetic:
    >   , ("+"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary (\x :: Integer
    x y :: Integer
    y -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    y))))
    >   , ("-"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary (\x :: Integer
    x y :: Integer
    y -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    y))))
    >   , ("*"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary (\x :: Integer
    x y :: Integer
    y -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    y))))
    >   , ("/"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary Integer -> Integer -> Either EvalError Integer
    divWrap))
    >   , ("%"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary Integer -> Integer -> Either EvalError Integer
    modWrap))
    >   , ("/$"         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    signedArithBinary Integer -> Integer -> Either EvalError Integer
    divWrap))
    >   , ("%$"         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    signedArithBinary Integer -> Integer -> Either EvalError Integer
    modWrap))
    >   , ("^^"         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary Integer -> Integer -> Either EvalError Integer
    expWrap))
    >   , ("lg2"        , (TValue -> Value -> Value) -> Value
    unary  ((Integer -> Either EvalError Integer) -> TValue -> Value -> Value
    arithUnary Integer -> Either EvalError Integer
    lg2Wrap))
    >   , ("negate"     , (TValue -> Value -> Value) -> Value
    unary  ((Integer -> Either EvalError Integer) -> TValue -> Value -> Value
    arithUnary (\x :: Integer
    x -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (- Integer
    x))))
    >   , ("number"     , (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \val :: Integer
    val ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >                     Either EvalError Integer -> TValue -> Value
    arithNullary (Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right Integer
    val) TValue
    a)
    >   , ("toInteger"  , (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_bits :: Integer
    _bits ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x ->
    >                     Either EvalError Integer -> Value
    VInteger (Value -> Either EvalError Integer
    fromVWord Value
    x))
    >   , ("fromInteger", (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x ->
    >                     Either EvalError Integer -> TValue -> Value
    arithNullary (Value -> Either EvalError Integer
    fromVInteger Value
    x) TValue
    a)
    >
    >   -- Comparison:
    >   , ("<"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    LT)))
    >   , (">"          , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    GT)))
    >   , ("<="         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    GT)))
    >   , (">="         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    LT)))
    >   , ("=="         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ)))
    >   , ("!="         , (TValue -> Value -> Value -> Value) -> Value
    binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder (\o :: Ordering
    o -> Ordering
    o Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    EQ)))
    >   , ("<$"         , (TValue -> Value -> Value -> Value) -> Value
    binary TValue -> Value -> Value -> Value
    signedLessThan)
    >
    >   -- Sequences:
    >   , ("#"          , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \front :: Nat'
    front ->
    >                     (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \back :: Nat'
    back  ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_elty :: TValue
    _elty  ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \l :: Value
    l ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \r :: Value
    r ->
    >                     Nat' -> [Value] -> Value
    VList (Nat' -> Nat' -> Nat'
    nAdd Nat'
    front Nat'
    back) (Value -> [Value]
    fromVList Value
    l [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Value -> [Value]
    fromVList Value
    r))
    >
    >   , ("join"       , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \parts :: Nat'
    parts ->
    >                     (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \each :: Nat'
    each  ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \xss :: Value
    xss ->
    >                       case Nat'
    each of
    >                         -- special case when the inner sequences are of length 0
    >                         Nat 0 -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat 0) []
    >                         _ -> Nat' -> [Value] -> Value
    VList (Nat' -> Nat' -> Nat'
    nMul Nat'
    parts Nat'
    each)
    >                              ([[Value]] -> [Value]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ((Value -> [Value]) -> [Value] -> [[Value]]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> [Value]
    fromVList (Value -> [Value]
    fromVList Value
    xss))))
    >
    >   , ("split"      , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \parts :: Nat'
    parts ->
    >                     (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \each :: Integer
    each  ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \val :: Value
    val ->
    >                     Nat' -> [Value] -> Value
    VList Nat'
    parts (Nat' -> Integer -> [Value] -> [Value]
    splitV Nat'
    parts Integer
    each (Value -> [Value]
    fromVList Value
    val)))
    >
    >   , ("splitAt"    , (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \front :: Integer
    front ->
    >                     (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \back :: Nat'
    back ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >                     let (xs :: [Value]
    xs, ys :: [Value]
    ys) = Integer -> [Value] -> ([Value], [Value])
    forall i a. Integral i => i -> [a] -> ([a], [a])
    genericSplitAt Integer
    front (Value -> [Value]
    fromVList Value
    v)
    >                     in [Value] -> Value
    VTuple [Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    front) [Value]
    xs, Nat' -> [Value] -> Value
    VList Nat'
    back [Value]
    ys])
    >
    >   , ("reverse"    , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >                     Nat' -> [Value] -> Value
    VList Nat'
    n ([Value] -> [Value]
    forall a. [a] -> [a]
    reverse (Value -> [Value]
    fromVList Value
    v)))
    >
    >   , ("transpose"  , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \rows :: Nat'
    rows ->
    >                     (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \cols :: Nat'
    cols ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >                     Nat' -> [Value] -> Value
    VList Nat'
    cols
    >                     (([Value] -> Value) -> [[Value]] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat' -> [Value] -> Value
    VList Nat'
    rows) (Nat' -> [[Value]] -> [[Value]]
    transposeV Nat'
    cols ((Value -> [Value]) -> [Value] -> [[Value]]
    forall a b. (a -> b) -> [a] -> [b]
    map Value -> [Value]
    fromVList (Value -> [Value]
    fromVList Value
    v)))))
    >
    >   -- Shifting:
    >   , ("<<"         , (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
    shiftV Nat' -> Value -> [Value] -> Integer -> [Value]
    shiftLV)
    >   , (">>"         , (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
    shiftV Nat' -> Value -> [Value] -> Integer -> [Value]
    shiftRV)
    >   , ("<<<"        , (Integer -> [Value] -> Integer -> [Value]) -> Value
    rotateV Integer -> [Value] -> Integer -> [Value]
    rotateLV)
    >   , (">>>"        , (Integer -> [Value] -> Integer -> [Value]) -> Value
    rotateV Integer -> [Value] -> Integer -> [Value]
    rotateRV)
    >   , (">>$"        , Value
    signedShiftRV)
    >
    >   -- Indexing:
    >   , ("@"          , (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
    indexPrimOne  Nat' -> TValue -> [Value] -> Integer -> Value
    indexFront)
    >   , ("!"          , (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
    indexPrimOne  Nat' -> TValue -> [Value] -> Integer -> Value
    indexBack)
    >   , ("update"     , (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
    updatePrim Nat' -> [Value] -> Integer -> Value -> [Value]
    updateFront)
    >   , ("updateEnd"  , (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
    updatePrim Nat' -> [Value] -> Integer -> Value -> [Value]
    updateBack)
    >
    >   -- Enumerations:
    >   , ("fromTo"     , (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \first :: Integer
    first ->
    >                     (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \lst :: Integer
    lst   ->
    >                     (TValue -> Value) -> Value
    VPoly    ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty  ->
    >                     let f :: Integer -> Value
    f i :: Integer
    i = Either EvalError Integer -> TValue -> Value
    arithNullary (Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right Integer
    i) TValue
    ty
    >                     in Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat (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 -> Value) -> [Integer] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> Value
    f [Integer
    first .. Integer
    lst]))
    >
    >   , ("fromThenTo" , (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \first :: Integer
    first ->
    >                     (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \next :: Integer
    next  ->
    >                     (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_lst :: Integer
    _lst  ->
    >                     (TValue -> Value) -> Value
    VPoly    ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty    ->
    >                     (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \len :: Integer
    len   ->
    >                     let f :: Integer -> Value
    f i :: Integer
    i = Either EvalError Integer -> TValue -> Value
    arithNullary (Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right Integer
    i) TValue
    ty
    >                     in Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    len) ((Integer -> Value) -> [Integer] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> Value
    f (Integer -> [Integer] -> [Integer]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    len [Integer
    first, Integer
    next ..])))
    >
    >   , ("infFrom"    , (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \first :: Value
    first ->
    >                     let f :: Integer -> Value
    f i :: Integer
    i = (Integer -> Either EvalError Integer) -> TValue -> Value -> Value
    arithUnary (\x :: Integer
    x -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    i)) TValue
    ty Value
    first
    >                     in Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Integer -> Value) -> [Integer] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> Value
    f [0 ..]))
    >
    >   , ("infFromThen", (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \first :: Value
    first ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \next :: Value
    next ->
    >                     let f :: Integer -> Value
    f i :: Integer
    i = (Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary (\x :: Integer
    x y :: Integer
    y -> Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + (Integer
    y Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    x) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    i)) TValue
    ty Value
    first Value
    next
    >                     in Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Integer -> Value) -> [Integer] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> Value
    f [0 ..]))
    >
    >   -- Miscellaneous:
    >   , ("error"      , (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >                     (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_ ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_s :: Value
    _s -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left (String -> EvalError
    UserError "error")) TValue
    a)
    >                     -- TODO: obtain error string from argument s
    >
    >   , ("random"     , (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_seed :: Value
    _seed ->
    >                     Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left (String -> EvalError
    UserError "random: unimplemented")) TValue
    a)
    >
    >   , ("trace"      , (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_n :: Nat'
    _n ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_a :: TValue
    _a ->
    >                     (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_b :: TValue
    _b ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_s :: Value
    _s ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_x :: Value
    _x ->
    >                     (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \y :: Value
    y -> Value
    y)
    >   ]
    >
    > unary :: (TValue -> Value -> Value) -> Value
    > unary :: (TValue -> Value -> Value) -> Value
    unary f :: TValue -> Value -> Value
    f = (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty -> (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x -> TValue -> Value -> Value
    f TValue
    ty Value
    x
    >
    > binary :: (TValue -> Value -> Value -> Value) -> Value
    > binary :: (TValue -> Value -> Value -> Value) -> Value
    binary f :: TValue -> Value -> Value -> Value
    f = (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty -> (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x -> (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \y :: Value
    y -> TValue -> Value -> Value -> Value
    f TValue
    ty Value
    x Value
    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 -> Either EvalError Integer
    > fromVWord :: Value -> Either EvalError Integer
    fromVWord v :: Value
    v = ([Bool] -> Integer)
    -> Either EvalError [Bool] -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Bool] -> Integer
    bitsToInteger ((Value -> Either EvalError Bool)
    -> [Value] -> Either EvalError [Bool]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Value -> Either EvalError Bool
    fromVBit (Value -> [Value]
    fromVList Value
    v))
    >
    > -- | Convert a list of booleans in big-endian format to an integer.
    > bitsToInteger :: [Bool] -> Integer
    > bitsToInteger :: [Bool] -> Integer
    bitsToInteger bs :: [Bool]
    bs = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
    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 0 [Bool]
    bs
    >   where f :: a -> Bool -> a
    f x :: a
    x b :: Bool
    b = if Bool
    b then 2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + 1 else 2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x

    > fromSignedVWord :: Value -> Either EvalError Integer
    > fromSignedVWord :: Value -> Either EvalError Integer
    fromSignedVWord v :: Value
    v = ([Bool] -> Integer)
    -> Either EvalError [Bool] -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Bool] -> Integer
    signedBitsToInteger ((Value -> Either EvalError Bool)
    -> [Value] -> Either EvalError [Bool]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Value -> Either EvalError Bool
    fromVBit (Value -> [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 "signedBitsToInteger" ["Bitvector has zero length"]
    > signedBitsToInteger (b0 :: Bool
    b0 : bs :: [Bool]
    bs) = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
    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 -1 else 0) [Bool]
    bs
    >   where f :: a -> Bool -> a
    f x :: a
    x b :: Bool
    b = if Bool
    b then 2 a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + 1 else 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. If an integer-producing function raises a run-time
    exception, then the output bitvector will contain the exception in all
    bit positions.

    > vWord :: Integer -> Either EvalError Integer -> Value
    > vWord :: Integer -> Either EvalError Integer -> Value
    vWord w :: Integer
    w e :: Either EvalError Integer
    e = Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) [ Either EvalError Bool -> Value
    VBit ((Integer -> Bool)
    -> Either EvalError Integer -> Either EvalError Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Integer -> Bool
    forall a. Bits a => Integer -> a -> Bool
    test Integer
    i) Either EvalError Integer
    e) | Integer
    i <- [Integer
    wInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -1, Integer
    wInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -2 .. 0] ]
    >   where test :: Integer -> a -> Bool
    test i :: Integer
    i x :: a
    x = a -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit a
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)

    Logic
    -----

    Bitwise logic primitives are defined by recursion over the type
    structure. On type `Bit`, we use `fmap` and `liftA2` to make these
    operations 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.

    > logicNullary :: Either EvalError Bool -> TValue -> Value
    > logicNullary :: Either EvalError Bool -> TValue -> Value
    logicNullary b :: Either EvalError Bool
    b = TValue -> Value
    go
    >   where
    >     go :: TValue -> Value
    go TVBit          = Either EvalError Bool -> Value
    VBit Either EvalError Bool
    b
    >     go TVInteger      = Either EvalError Integer -> Value
    VInteger ((Bool -> Integer)
    -> Either EvalError Bool -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\c :: Bool
    c -> if Bool
    c then -1 else 0) Either EvalError Bool
    b)
    >     go (TVIntMod _)   = Either EvalError Integer -> Value
    VInteger ((Bool -> Integer)
    -> Either EvalError Bool -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Bool -> Integer
    forall a b. a -> b -> a
    const 0) Either EvalError Bool
    b)
    >     go (TVSeq n :: Integer
    n ety :: TValue
    ety)  = Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    n) (Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n (TValue -> Value
    go TValue
    ety))
    >     go (TVStream ety :: TValue
    ety) = Nat' -> [Value] -> Value
    VList Nat'
    Inf (Value -> [Value]
    forall a. a -> [a]
    repeat (TValue -> Value
    go TValue
    ety))
    >     go (TVTuple tys :: [TValue]
    tys)  = [Value] -> Value
    VTuple ((TValue -> Value) -> [TValue] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> Value
    go [TValue]
    tys)
    >     go (TVRec fields :: [(Ident, TValue)]
    fields) = [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value
    go TValue
    fty) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fields ]
    >     go (TVFun _ bty :: TValue
    bty)  = (Value -> Value) -> Value
    VFun (\_ -> TValue -> Value
    go TValue
    bty)
    >     go (TVAbstract {}) =
    >        String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicUnary" ["Abstract type not in `Logic`"]
    >
    > logicUnary :: (Bool -> Bool) -> TValue -> Value -> Value
    > logicUnary :: (Bool -> Bool) -> TValue -> Value -> Value
    logicUnary op :: Bool -> Bool
    op = TValue -> Value -> Value
    go
    >   where
    >     go :: TValue -> Value -> Value
    >     go :: TValue -> Value -> Value
    go ty :: TValue
    ty val :: Value
    val =
    >       case TValue
    ty of
    >         TVBit        -> Either EvalError Bool -> Value
    VBit ((Bool -> Bool) -> Either EvalError Bool -> Either EvalError Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Bool -> Bool
    op (Value -> Either EvalError Bool
    fromVBit Value
    val))
    >         TVInteger    -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicUnary" ["Integer not in class Logic"]
    >         TVIntMod _   -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicUnary" ["Z not in class Logic"]
    >         TVSeq w :: Integer
    w ety :: TValue
    ety  -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    ety) (Value -> [Value]
    fromVList Value
    val))
    >         TVStream ety :: TValue
    ety -> Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    ety) (Value -> [Value]
    fromVList Value
    val))
    >         TVTuple etys :: [TValue]
    etys -> [Value] -> Value
    VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> Value -> Value
    go [TValue]
    etys (Value -> [Value]
    fromVTuple Value
    val))
    >         TVRec fields :: [(Ident, TValue)]
    fields -> [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value -> Value
    go TValue
    fty (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    val)) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fields ]
    >         TVFun _ bty :: TValue
    bty  -> (Value -> Value) -> Value
    VFun (\v :: Value
    v -> TValue -> Value -> Value
    go TValue
    bty (Value -> Value -> Value
    fromVFun Value
    val Value
    v))
    >         TVAbstract {} ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicUnary" ["Abstract type not in `Logic`"]
    >
    > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
    > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
    logicBinary op :: Bool -> Bool -> Bool
    op = TValue -> Value -> Value -> Value
    go
    >   where
    >     go :: TValue -> Value -> Value -> Value
    >     go :: TValue -> Value -> Value -> Value
    go ty :: TValue
    ty l :: Value
    l r :: Value
    r =
    >       case TValue
    ty of
    >         TVBit        -> Either EvalError Bool -> Value
    VBit ((Bool -> Bool -> Bool)
    -> Either EvalError Bool
    -> Either EvalError Bool
    -> Either EvalError Bool
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Bool -> Bool -> Bool
    op (Value -> Either EvalError Bool
    fromVBit Value
    l) (Value -> Either EvalError Bool
    fromVBit Value
    r))
    >         TVInteger    -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicBinary" ["Integer not in class Logic"]
    >         TVIntMod _   -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicBinary" ["Z not in class Logic"]
    >         TVSeq w :: Integer
    w ety :: TValue
    ety  -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Value
    go TValue
    ety) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >         TVStream ety :: TValue
    ety -> Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Value
    go TValue
    ety) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >         TVTuple etys :: [TValue]
    etys -> [Value] -> Value
    VTuple ((TValue -> Value -> Value -> Value)
    -> [TValue] -> [Value] -> [Value] -> [Value]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Value
    go [TValue]
    etys (Value -> [Value]
    fromVTuple Value
    l) (Value -> [Value]
    fromVTuple Value
    r))
    >         TVRec fields :: [(Ident, TValue)]
    fields -> [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value -> Value -> Value
    go TValue
    fty (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    l) (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    r))
    >                                 | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fields ]
    >         TVFun _ bty :: TValue
    bty  -> (Value -> Value) -> Value
    VFun (\v :: Value
    v -> TValue -> Value -> Value -> Value
    go TValue
    bty (Value -> Value -> Value
    fromVFun Value
    l Value
    v) (Value -> Value -> Value
    fromVFun Value
    r Value
    v))
    >         TVAbstract {} ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "logicBinary" ["Abstract type not in `Logic`"]

    Arithmetic
    ----------

    Arithmetic primitives may be applied to any type that is made up of
    finite bitvectors. 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", error "foo"]`.

    Signed arithmetic primitives may be applied to any type that is made
    up of non-empty finite bitvectors.

    > arithNullary :: Either EvalError Integer -> TValue -> Value
    > arithNullary :: Either EvalError Integer -> TValue -> Value
    arithNullary i :: Either EvalError Integer
    i = TValue -> Value
    go
    >   where
    >     go :: TValue -> Value
    >     go :: TValue -> Value
    go ty :: TValue
    ty =
    >       case TValue
    ty of
    >         TVBit ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithNullary" ["Bit not in class Arith"]
    >         TVInteger ->
    >           Either EvalError Integer -> Value
    VInteger Either EvalError Integer
    i
    >         TVIntMod n :: Integer
    n ->
    >           Either EvalError Integer -> Value
    VInteger ((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)
    -> Either EvalError Integer -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Either EvalError Integer
    i)
    >         TVSeq w :: Integer
    w a :: TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Either EvalError Integer -> Value
    vWord Integer
    w Either EvalError Integer
    i
    >           | Bool
    otherwise -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) (Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    w (TValue -> Value
    go TValue
    a))
    >         TVStream a :: TValue
    a ->
    >           Nat' -> [Value] -> Value
    VList Nat'
    Inf (Value -> [Value]
    forall a. a -> [a]
    repeat (TValue -> Value
    go TValue
    a))
    >         TVFun _ ety :: TValue
    ety ->
    >           (Value -> Value) -> Value
    VFun (Value -> Value -> Value
    forall a b. a -> b -> a
    const (TValue -> Value
    go TValue
    ety))
    >         TVTuple tys :: [TValue]
    tys ->
    >           [Value] -> Value
    VTuple ((TValue -> Value) -> [TValue] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> Value
    go [TValue]
    tys)
    >         TVRec fs :: [(Ident, TValue)]
    fs ->
    >           [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value
    go TValue
    fty) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithNullary" ["Absrat type not in `Arith`"]
    >
    > arithUnary :: (Integer -> Either EvalError Integer)
    >            -> TValue -> Value -> Value
    > arithUnary :: (Integer -> Either EvalError Integer) -> TValue -> Value -> Value
    arithUnary op :: Integer -> Either EvalError Integer
    op = TValue -> Value -> Value
    go
    >   where
    >     go :: TValue -> Value -> Value
    >     go :: TValue -> Value -> Value
    go ty :: TValue
    ty val :: Value
    val =
    >       case TValue
    ty of
    >         TVBit ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithUnary" ["Bit not in class Arith"]
    >         TVInteger ->
    >           Either EvalError Integer -> Value
    VInteger (Either EvalError Integer -> Value)
    -> Either EvalError Integer -> Value
    forall a b. (a -> b) -> a -> b
    $
    >           case Value -> Either EvalError Integer
    fromVInteger Value
    val of
    >             Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >             Right i :: Integer
    i -> Integer -> Either EvalError Integer
    op Integer
    i
    >         TVIntMod n :: Integer
    n ->
    >           Either EvalError Integer -> Value
    VInteger (Either EvalError Integer -> Value)
    -> Either EvalError Integer -> Value
    forall a b. (a -> b) -> a -> b
    $
    >           case Value -> Either EvalError Integer
    fromVInteger Value
    val of
    >             Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >             Right i :: 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)
    -> Either EvalError Integer -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Either EvalError Integer
    op Integer
    i
    >         TVSeq w :: Integer
    w a :: TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Either EvalError Integer -> Value
    vWord Integer
    w (Integer -> Either EvalError Integer
    op (Integer -> Either EvalError Integer)
    -> Either EvalError Integer -> Either EvalError Integer
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Value -> Either EvalError Integer
    fromVWord Value
    val)
    >           | Bool
    otherwise -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    a) (Value -> [Value]
    fromVList Value
    val))
    >         TVStream a :: TValue
    a ->
    >           Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Value -> Value) -> [Value] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Value -> Value
    go TValue
    a) (Value -> [Value]
    fromVList Value
    val))
    >         TVFun _ ety :: TValue
    ety ->
    >           (Value -> Value) -> Value
    VFun (\x :: Value
    x -> TValue -> Value -> Value
    go TValue
    ety (Value -> Value -> Value
    fromVFun Value
    val Value
    x))
    >         TVTuple tys :: [TValue]
    tys ->
    >           [Value] -> Value
    VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> Value -> Value
    go [TValue]
    tys (Value -> [Value]
    fromVTuple Value
    val))
    >         TVRec fs :: [(Ident, TValue)]
    fs ->
    >           [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value -> Value
    go TValue
    fty (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    val)) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithUnary" ["Absrat type not in `Arith`"]
    >
    > arithBinary :: (Integer -> Integer -> Either EvalError Integer)
    >             -> TValue -> Value -> Value -> Value
    > arithBinary :: (Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    arithBinary = (Value -> Either EvalError Integer)
    -> (Integer -> Integer -> Either EvalError Integer)
    -> TValue
    -> Value
    -> Value
    -> Value
    arithBinaryGeneric Value -> Either EvalError Integer
    fromVWord
    >
    > signedArithBinary :: (Integer -> Integer -> Either EvalError Integer)
    >                   -> TValue -> Value -> Value -> Value
    > signedArithBinary :: (Integer -> Integer -> Either EvalError Integer)
    -> TValue -> Value -> Value -> Value
    signedArithBinary = (Value -> Either EvalError Integer)
    -> (Integer -> Integer -> Either EvalError Integer)
    -> TValue
    -> Value
    -> Value
    -> Value
    arithBinaryGeneric Value -> Either EvalError Integer
    fromSignedVWord
    >
    > arithBinaryGeneric :: (Value -> Either EvalError Integer)
    >                    -> (Integer -> Integer -> Either EvalError Integer)
    >                    -> TValue -> Value -> Value -> Value
    > arithBinaryGeneric :: (Value -> Either EvalError Integer)
    -> (Integer -> Integer -> Either EvalError Integer)
    -> TValue
    -> Value
    -> Value
    -> Value
    arithBinaryGeneric fromWord :: Value -> Either EvalError Integer
    fromWord op :: Integer -> Integer -> Either EvalError Integer
    op = TValue -> Value -> Value -> Value
    go
    >   where
    >     go :: TValue -> Value -> Value -> Value
    >     go :: TValue -> Value -> Value -> Value
    go ty :: TValue
    ty l :: Value
    l r :: Value
    r =
    >       case TValue
    ty of
    >         TVBit ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithBinary" ["Bit not in class Arith"]
    >         TVInteger ->
    >           Either EvalError Integer -> Value
    VInteger (Either EvalError Integer -> Value)
    -> Either EvalError Integer -> Value
    forall a b. (a -> b) -> a -> b
    $
    >           case Value -> Either EvalError Integer
    fromVInteger Value
    l of
    >             Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >             Right i :: Integer
    i ->
    >               case Value -> Either EvalError Integer
    fromVInteger Value
    r of
    >                 Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >                 Right j :: Integer
    j -> Integer -> Integer -> Either EvalError Integer
    op Integer
    i Integer
    j
    >         TVIntMod n :: Integer
    n ->
    >           Either EvalError Integer -> Value
    VInteger (Either EvalError Integer -> Value)
    -> Either EvalError Integer -> Value
    forall a b. (a -> b) -> a -> b
    $
    >           case Value -> Either EvalError Integer
    fromVInteger Value
    l of
    >             Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >             Right i :: Integer
    i ->
    >               case Value -> Either EvalError Integer
    fromVInteger Value
    r of
    >                 Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >                 Right j :: 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)
    -> Either EvalError Integer -> Either EvalError Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Integer -> Either EvalError Integer
    op Integer
    i Integer
    j
    >         TVSeq w :: Integer
    w a :: TValue
    a
    >           | TValue -> Bool
    isTBit TValue
    a  -> Integer -> Either EvalError Integer -> Value
    vWord Integer
    w (Either EvalError Integer -> Value)
    -> Either EvalError Integer -> Value
    forall a b. (a -> b) -> a -> b
    $
    >                          case Value -> Either EvalError Integer
    fromWord Value
    l of
    >                            Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >                            Right i :: Integer
    i ->
    >                              case Value -> Either EvalError Integer
    fromWord Value
    r of
    >                                Left e :: EvalError
    e -> EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    e
    >                                Right j :: Integer
    j -> Integer -> Integer -> Either EvalError Integer
    op Integer
    i Integer
    j
    >           | Bool
    otherwise -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    w) ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Value
    go TValue
    a) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >         TVStream a :: TValue
    a ->
    >           Nat' -> [Value] -> Value
    VList Nat'
    Inf ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Value
    go TValue
    a) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >         TVFun _ ety :: TValue
    ety ->
    >           (Value -> Value) -> Value
    VFun (\x :: Value
    x -> TValue -> Value -> Value -> Value
    go TValue
    ety (Value -> Value -> Value
    fromVFun Value
    l Value
    x) (Value -> Value -> Value
    fromVFun Value
    r Value
    x))
    >         TVTuple tys :: [TValue]
    tys ->
    >           [Value] -> Value
    VTuple ((TValue -> Value -> Value -> Value)
    -> [TValue] -> [Value] -> [Value] -> [Value]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Value
    go [TValue]
    tys (Value -> [Value]
    fromVTuple Value
    l) (Value -> [Value]
    fromVTuple Value
    r))
    >         TVRec fs :: [(Ident, TValue)]
    fs ->
    >           [(Ident, Value)] -> Value
    VRecord [ (Ident
    f, TValue -> Value -> Value -> Value
    go TValue
    fty (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    l) (Ident -> Value -> Value
    lookupRecord Ident
    f Value
    r)) | (f :: Ident
    f, fty :: TValue
    fty) <- [(Ident, TValue)]
    fs ]
    >         TVAbstract {} ->
    >           String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "arithBinary" ["Abstract type not in class `Arith`"]

    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 -> Either EvalError Integer
    > divWrap :: Integer -> Integer -> Either EvalError Integer
    divWrap _ 0 = EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    DivideByZero
    > divWrap x :: Integer
    x y :: Integer
    y = Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    y)
    >
    > modWrap :: Integer -> Integer -> Either EvalError Integer
    > modWrap :: Integer -> Integer -> Either EvalError Integer
    modWrap _ 0 = EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    DivideByZero
    > modWrap x :: Integer
    x y :: Integer
    y = Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    y)
    >
    > expWrap :: Integer -> Integer -> Either EvalError Integer
    > expWrap :: Integer -> Integer -> Either EvalError Integer
    expWrap x :: Integer
    x y :: Integer
    y = if Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0 then EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    NegativeExponent else Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer
    x Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    y)
    >
    > lg2Wrap :: Integer -> Either EvalError Integer
    > lg2Wrap :: Integer -> Either EvalError Integer
    lg2Wrap x :: Integer
    x = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0 then EvalError -> Either EvalError Integer
    forall a b. a -> Either a b
    Left EvalError
    LogNegative else Integer -> Either EvalError Integer
    forall a b. b -> Either a b
    Right (Integer -> Integer
    lg2 Integer
    x)

    Comparison
    ----------

    Comparison primitives may be applied to any type that contains a
    finite number of bits. All such types are compared using a
    lexicographic ordering on bits, where `False` < `True`. Lists and
    tuples are compared left-to-right, and record fields are compared in
    alphabetical order.

    Comparisons on type `Bit` 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 -> Value -> Value -> Value
    > cmpOrder :: (Ordering -> Bool) -> TValue -> Value -> Value -> Value
    cmpOrder p :: Ordering -> Bool
    p ty :: TValue
    ty l :: Value
    l r :: Value
    r = Either EvalError Bool -> Value
    VBit ((Ordering -> Bool)
    -> Either EvalError Ordering -> Either EvalError Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Ordering -> Bool
    p (TValue -> Value -> Value -> Either EvalError Ordering
    lexCompare TValue
    ty Value
    l Value
    r))
    >
    > -- | Lexicographic ordering on two values.
    > lexCompare :: TValue -> Value -> Value -> Either EvalError Ordering
    > lexCompare :: TValue -> Value -> Value -> Either EvalError Ordering
    lexCompare ty :: TValue
    ty l :: Value
    l r :: Value
    r =
    >   case TValue
    ty of
    >     TVBit ->
    >       Bool -> Bool -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Bool -> Bool -> Ordering)
    -> Either EvalError Bool -> Either EvalError (Bool -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Value -> Either EvalError Bool
    fromVBit Value
    l Either EvalError (Bool -> Ordering)
    -> Either EvalError Bool -> Either EvalError Ordering
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Value -> Either EvalError Bool
    fromVBit Value
    r
    >     TVInteger ->
    >       Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> Either EvalError Integer
    -> Either EvalError (Integer -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Value -> Either EvalError Integer
    fromVInteger Value
    l Either EvalError (Integer -> Ordering)
    -> Either EvalError Integer -> Either EvalError Ordering
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Value -> Either EvalError Integer
    fromVInteger Value
    r
    >     TVIntMod _ ->
    >       Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> Either EvalError Integer
    -> Either EvalError (Integer -> Ordering)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Value -> Either EvalError Integer
    fromVInteger Value
    l Either EvalError (Integer -> Ordering)
    -> Either EvalError Integer -> Either EvalError Ordering
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Value -> Either EvalError Integer
    fromVInteger Value
    r
    >     TVSeq _w :: Integer
    _w ety :: TValue
    ety ->
    >       [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((Value -> Value -> Either EvalError Ordering)
    -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Either EvalError Ordering
    lexCompare TValue
    ety) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >     TVStream _ ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexCompare" ["invalid type"]
    >     TVFun _ _ ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexCompare" ["invalid type"]
    >     TVTuple etys :: [TValue]
    etys ->
    >       [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
    -> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
    lexCompare [TValue]
    etys (Value -> [Value]
    fromVTuple Value
    l) (Value -> [Value]
    fromVTuple Value
    r))
    >     TVRec fields :: [(Ident, TValue)]
    fields ->
    >       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 (((Ident, TValue) -> (Ident, TValue) -> Ordering)
    -> [(Ident, TValue)] -> [(Ident, TValue)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, TValue) -> Ident)
    -> (Ident, TValue) -> (Ident, TValue) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, TValue) -> Ident
    forall a b. (a, b) -> a
    fst) [(Ident, TValue)]
    fields)
    >           ls :: [Value]
    ls     = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Value) -> Value
    forall a b. (a, b) -> b
    snd (((Ident, Value) -> (Ident, Value) -> Ordering)
    -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, Value) -> Ident)
    -> (Ident, Value) -> (Ident, Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, Value) -> Ident
    forall a b. (a, b) -> a
    fst) (Value -> [(Ident, Value)]
    fromVRecord Value
    l))
    >           rs :: [Value]
    rs     = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Value) -> Value
    forall a b. (a, b) -> b
    snd (((Ident, Value) -> (Ident, Value) -> Ordering)
    -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, Value) -> Ident)
    -> (Ident, Value) -> (Ident, Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, Value) -> Ident
    forall a b. (a, b) -> a
    fst) (Value -> [(Ident, Value)]
    fromVRecord Value
    r))
    >        in [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
    -> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
    lexCompare [TValue]
    tys [Value]
    ls [Value]
    rs)
    >     TVAbstract {} ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexCompare" ["Abstract type not in `Cmp`"]
    >
    > lexList :: [Either EvalError Ordering] -> Either EvalError Ordering
    > lexList :: [Either EvalError Ordering] -> Either EvalError Ordering
    lexList [] = Ordering -> Either EvalError Ordering
    forall a b. b -> Either a b
    Right Ordering
    EQ
    > lexList (e :: Either EvalError Ordering
    e : es :: [Either EvalError Ordering]
    es) =
    >   case Either EvalError Ordering
    e of
    >     Left err :: EvalError
    err -> EvalError -> Either EvalError Ordering
    forall a b. a -> Either a b
    Left EvalError
    err
    >     Right LT -> Ordering -> Either EvalError Ordering
    forall a b. b -> Either a b
    Right Ordering
    LT
    >     Right EQ -> [Either EvalError Ordering] -> Either EvalError Ordering
    lexList [Either EvalError Ordering]
    es
    >     Right GT -> Ordering -> Either EvalError Ordering
    forall a b. b -> Either a b
    Right Ordering
    GT

    Signed comparisons may be applied to any type made up of non-empty
    bitvectors. 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 -> Value -> Value -> Value
    > signedLessThan :: TValue -> Value -> Value -> Value
    signedLessThan ty :: TValue
    ty l :: Value
    l r :: Value
    r = Either EvalError Bool -> Value
    VBit ((Ordering -> Bool)
    -> Either EvalError Ordering -> Either EvalError Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    LT) (TValue -> Value -> Value -> Either EvalError Ordering
    lexSignedCompare TValue
    ty Value
    l Value
    r))
    >
    > -- | Lexicographic ordering on two signed values.
    > lexSignedCompare :: TValue -> Value -> Value -> Either EvalError Ordering
    > lexSignedCompare :: TValue -> Value -> Value -> Either EvalError Ordering
    lexSignedCompare ty :: TValue
    ty l :: Value
    l r :: Value
    r =
    >   case TValue
    ty of
    >     TVBit ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["invalid type"]
    >     TVInteger ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["invalid type"]
    >     TVIntMod _ ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["invalid type"]
    >     TVSeq _w :: Integer
    _w ety :: TValue
    ety
    >       | TValue -> Bool
    isTBit TValue
    ety ->
    >         case Value -> Either EvalError Integer
    fromSignedVWord Value
    l of
    >           Left e :: EvalError
    e -> EvalError -> Either EvalError Ordering
    forall a b. a -> Either a b
    Left EvalError
    e
    >           Right i :: Integer
    i ->
    >             case Value -> Either EvalError Integer
    fromSignedVWord Value
    r of
    >               Left e :: EvalError
    e -> EvalError -> Either EvalError Ordering
    forall a b. a -> Either a b
    Left EvalError
    e
    >               Right j :: Integer
    j -> Ordering -> Either EvalError Ordering
    forall a b. b -> Either a b
    Right (Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    i Integer
    j)
    >       | Bool
    otherwise ->
    >         [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((Value -> Value -> Either EvalError Ordering)
    -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (TValue -> Value -> Value -> Either EvalError Ordering
    lexSignedCompare TValue
    ety) (Value -> [Value]
    fromVList Value
    l) (Value -> [Value]
    fromVList Value
    r))
    >     TVStream _ ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["invalid type"]
    >     TVFun _ _ ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["invalid type"]
    >     TVTuple etys :: [TValue]
    etys ->
    >       [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
    -> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
    lexSignedCompare [TValue]
    etys (Value -> [Value]
    fromVTuple Value
    l) (Value -> [Value]
    fromVTuple Value
    r))
    >     TVRec fields :: [(Ident, TValue)]
    fields ->
    >       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 (((Ident, TValue) -> (Ident, TValue) -> Ordering)
    -> [(Ident, TValue)] -> [(Ident, TValue)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, TValue) -> Ident)
    -> (Ident, TValue) -> (Ident, TValue) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, TValue) -> Ident
    forall a b. (a, b) -> a
    fst) [(Ident, TValue)]
    fields)
    >           ls :: [Value]
    ls     = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Value) -> Value
    forall a b. (a, b) -> b
    snd (((Ident, Value) -> (Ident, Value) -> Ordering)
    -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, Value) -> Ident)
    -> (Ident, Value) -> (Ident, Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, Value) -> Ident
    forall a b. (a, b) -> a
    fst) (Value -> [(Ident, Value)]
    fromVRecord Value
    l))
    >           rs :: [Value]
    rs     = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Value) -> Value
    forall a b. (a, b) -> b
    snd (((Ident, Value) -> (Ident, Value) -> Ordering)
    -> [(Ident, Value)] -> [(Ident, Value)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Ident, Value) -> Ident)
    -> (Ident, Value) -> (Ident, Value) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Ident, Value) -> Ident
    forall a b. (a, b) -> a
    fst) (Value -> [(Ident, Value)]
    fromVRecord Value
    r))
    >        in [Either EvalError Ordering] -> Either EvalError Ordering
    lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
    -> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
    lexSignedCompare [TValue]
    tys [Value]
    ls [Value]
    rs)
    >     TVAbstract {} ->
    >       String -> [String] -> Either EvalError Ordering
    forall a. String -> [String] -> a
    evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]

    Sequences
    ---------

    > -- | Split a list into 'w' pieces, each of length 'k'.
    > splitV :: Nat' -> Integer -> [Value] -> [Value]
    > splitV :: Nat' -> Integer -> [Value] -> [Value]
    splitV w :: Nat'
    w k :: Integer
    k xs :: [Value]
    xs =
    >   case Nat'
    w of
    >     Nat 0 -> []
    >     Nat n :: Integer
    n -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    k) [Value]
    ys Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : Nat' -> Integer -> [Value] -> [Value]
    splitV (Integer -> Nat'
    Nat (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1)) Integer
    k [Value]
    zs
    >     Inf   -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    k) [Value]
    ys Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : Nat' -> Integer -> [Value] -> [Value]
    splitV Nat'
    Inf Integer
    k [Value]
    zs
    >   where
    >     (ys :: [Value]
    ys, zs :: [Value]
    zs) = Integer -> [Value] -> ([Value], [Value])
    forall i a. Integral i => i -> [a] -> ([a], [a])
    genericSplitAt Integer
    k [Value]
    xs
    >
    > -- | Transpose a list of length-'w' lists into 'w' lists.
    > transposeV :: Nat' -> [[Value]] -> [[Value]]
    > transposeV :: Nat' -> [[Value]] -> [[Value]]
    transposeV w :: Nat'
    w xss :: [[Value]]
    xss =
    >   case Nat'
    w of
    >     Nat 0 -> []
    >     Nat n :: Integer
    n -> [Value]
    heads [Value] -> [[Value]] -> [[Value]]
    forall a. a -> [a] -> [a]
    : Nat' -> [[Value]] -> [[Value]]
    transposeV (Integer -> Nat'
    Nat (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1)) [[Value]]
    tails
    >     Inf   -> [Value]
    heads [Value] -> [[Value]] -> [[Value]]
    forall a. a -> [a] -> [a]
    : Nat' -> [[Value]] -> [[Value]]
    transposeV Nat'
    Inf [[Value]]
    tails
    >   where
    >     (heads :: [Value]
    heads, tails :: [[Value]]
    tails) = [[Value]] -> ([Value], [[Value]])
    dest [[Value]]
    xss
    >
    >     -- Split a list of non-empty lists into
    >     -- a list of heads and a list of tails
    >     dest :: [[Value]] -> ([Value], [[Value]])
    >     dest :: [[Value]] -> ([Value], [[Value]])
    dest [] = ([], [])
    >     dest ([] : _) = String -> [String] -> ([Value], [[Value]])
    forall a. String -> [String] -> a
    evalPanic "transposeV" ["Expected non-empty list"]
    >     dest ((y :: Value
    y : ys :: [Value]
    ys) : yss :: [[Value]]
    yss) = (Value
    y Value -> [Value] -> [Value]
    forall a. a -> [a] -> [a]
    : [Value]
    zs, [Value]
    ys [Value] -> [[Value]] -> [[Value]]
    forall a. a -> [a] -> [a]
    : [[Value]]
    zss)
    >       where (zs :: [Value]
    zs, zss :: [[Value]]
    zss) = [[Value]] -> ([Value], [[Value]])
    dest [[Value]]
    yss

    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' -> Value -> [Value] -> Integer -> [Value]) -> Value
    > shiftV :: (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
    shiftV op :: Nat' -> Value -> [Value] -> Integer -> [Value]
    op =
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n ->
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_ix :: Nat'
    _ix ->
    >   (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x ->
    >   TValue -> Value -> Value
    copyByTValue (Nat' -> TValue -> TValue
    tvSeq Nat'
    n TValue
    a) (Value -> Value) -> Value -> Value
    forall a b. (a -> b) -> a -> b
    $
    >   case Value -> Either EvalError Integer
    fromVWord Value
    x of
    >     Left e :: EvalError
    e -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left EvalError
    e) (Nat' -> TValue -> TValue
    tvSeq Nat'
    n TValue
    a)
    >     Right i :: Integer
    i -> Nat' -> [Value] -> Value
    VList Nat'
    n (Nat' -> Value -> [Value] -> Integer -> [Value]
    op Nat'
    n (Either EvalError Bool -> TValue -> Value
    logicNullary (Bool -> Either EvalError Bool
    forall a b. b -> Either a b
    Right Bool
    False) TValue
    a) (Value -> [Value]
    fromVList Value
    v) Integer
    i)
    >
    > shiftLV :: Nat' -> Value -> [Value] -> Integer -> [Value]
    > shiftLV :: Nat' -> Value -> [Value] -> Integer -> [Value]
    shiftLV w :: Nat'
    w z :: Value
    z vs :: [Value]
    vs i :: Integer
    i =
    >   case Nat'
    w of
    >     Nat n :: Integer
    n -> Integer -> [Value] -> [Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    n Integer
    i) [Value]
    vs [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    n Integer
    i) Value
    z
    >     Inf   -> Integer -> [Value] -> [Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop Integer
    i [Value]
    vs
    >
    > shiftRV :: Nat' -> Value -> [Value] -> Integer -> [Value]
    > shiftRV :: Nat' -> Value -> [Value] -> Integer -> [Value]
    shiftRV w :: Nat'
    w z :: Value
    z vs :: [Value]
    vs i :: Integer
    i =
    >   case Nat'
    w of
    >     Nat n :: Integer
    n -> Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    n Integer
    i) Value
    z [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [Value] -> [Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    n Integer
    i) [Value]
    vs
    >     Inf   -> Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    i Value
    z [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ [Value]
    vs
    >
    > rotateV :: (Integer -> [Value] -> Integer -> [Value]) -> Value
    > rotateV :: (Integer -> [Value] -> Integer -> [Value]) -> Value
    rotateV op :: Integer -> [Value] -> Integer -> [Value]
    op =
    >   (Integer -> Value) -> Value
    vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Integer
    n ->
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_ix :: Nat'
    _ix ->
    >   (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x ->
    >   TValue -> Value -> Value
    copyByTValue (Integer -> TValue -> TValue
    TVSeq Integer
    n TValue
    a) (Value -> Value) -> Value -> Value
    forall a b. (a -> b) -> a -> b
    $
    >   case Value -> Either EvalError Integer
    fromVWord Value
    x of
    >     Left e :: EvalError
    e -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    n) (Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n (Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left EvalError
    e) TValue
    a))
    >     Right i :: Integer
    i -> Nat' -> [Value] -> Value
    VList (Integer -> Nat'
    Nat Integer
    n) (Integer -> [Value] -> Integer -> [Value]
    op Integer
    n (Value -> [Value]
    fromVList Value
    v) Integer
    i)
    >
    > rotateLV :: Integer -> [Value] -> Integer -> [Value]
    > rotateLV :: Integer -> [Value] -> Integer -> [Value]
    rotateLV 0 vs :: [Value]
    vs _ = [Value]
    vs
    > rotateLV w :: Integer
    w vs :: [Value]
    vs i :: Integer
    i = [Value]
    ys [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ [Value]
    xs
    >   where (xs :: [Value]
    xs, ys :: [Value]
    ys) = Integer -> [Value] -> ([Value], [Value])
    forall i a. Integral i => i -> [a] -> ([a], [a])
    genericSplitAt (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w) [Value]
    vs
    >
    > rotateRV :: Integer -> [Value] -> Integer -> [Value]
    > rotateRV :: Integer -> [Value] -> Integer -> [Value]
    rotateRV 0 vs :: [Value]
    vs _ = [Value]
    vs
    > rotateRV w :: Integer
    w vs :: [Value]
    vs i :: Integer
    i = [Value]
    ys [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ [Value]
    xs
    >   where (xs :: [Value]
    xs, ys :: [Value]
    ys) = Integer -> [Value] -> ([Value], [Value])
    forall i a. Integral i => i -> [a] -> ([a], [a])
    genericSplitAt ((Integer
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w) [Value]
    vs
    >
    > signedShiftRV :: Value
    > signedShiftRV :: Value
    signedShiftRV =
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n ->
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_ix :: Nat'
    _ix ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \v :: Value
    v ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Value
    x ->
    >   TValue -> Value -> Value
    copyByTValue (Nat' -> TValue -> TValue
    tvSeq Nat'
    n TValue
    TVBit) (Value -> Value) -> Value -> Value
    forall a b. (a -> b) -> a -> b
    $
    >   case Value -> Either EvalError Integer
    fromVWord Value
    x of
    >     Left e :: EvalError
    e -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left EvalError
    e) (Nat' -> TValue -> TValue
    tvSeq Nat'
    n TValue
    TVBit)
    >     Right i :: Integer
    i -> Nat' -> [Value] -> Value
    VList Nat'
    n ([Value] -> Value) -> [Value] -> Value
    forall a b. (a -> b) -> a -> b
    $
    >       let vs :: [Value]
    vs = Value -> [Value]
    fromVList Value
    v
    >           z :: Value
    z = [Value] -> Value
    forall a. [a] -> a
    head [Value]
    vs in
    >       case Nat'
    n of
    >         Nat m :: Integer
    m -> Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    m Integer
    i) Value
    z [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [Value] -> [Value]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake (Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    m Integer
    i) [Value]
    vs
    >         Inf   -> Integer -> Value -> [Value]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    i Value
    z [Value] -> [Value] -> [Value]
    forall a. [a] -> [a] -> [a]
    ++ [Value]
    vs

    Indexing
    --------

    Indexing 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' -> TValue -> [Value] -> Integer -> Value) -> Value
    > indexPrimOne :: (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
    indexPrimOne op :: Nat' -> TValue -> [Value] -> Integer -> Value
    op =
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n ->
    >   (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \a :: TValue
    a ->
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_w :: Nat'
    _w ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \l :: Value
    l ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \r :: Value
    r ->
    >   TValue -> Value -> Value
    copyByTValue TValue
    a (Value -> Value) -> Value -> Value
    forall a b. (a -> b) -> a -> b
    $
    >   case Value -> Either EvalError Integer
    fromVWord Value
    r of
    >     Left e :: EvalError
    e -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left EvalError
    e) TValue
    a
    >     Right i :: Integer
    i -> Nat' -> TValue -> [Value] -> Integer -> Value
    op Nat'
    n TValue
    a (Value -> [Value]
    fromVList Value
    l) Integer
    i
    >
    > indexFront :: Nat' -> TValue -> [Value] -> Integer -> Value
    > indexFront :: Nat' -> TValue -> [Value] -> Integer -> Value
    indexFront w :: Nat'
    w a :: TValue
    a vs :: [Value]
    vs ix :: Integer
    ix =
    >   case Nat'
    w of
    >     Nat n :: Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    ix -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left (Integer -> EvalError
    InvalidIndex Integer
    ix)) TValue
    a
    >     _               -> [Value] -> Integer -> Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [Value]
    vs Integer
    ix
    >
    > indexBack :: Nat' -> TValue -> [Value] -> Integer -> Value
    > indexBack :: Nat' -> TValue -> [Value] -> Integer -> Value
    indexBack w :: Nat'
    w a :: TValue
    a vs :: [Value]
    vs ix :: Integer
    ix =
    >   case Nat'
    w of
    >     Nat n :: Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    ix    -> [Value] -> Integer -> Value
    forall i a. Integral i => [a] -> i -> a
    genericIndex [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
    - 1)
    >           | Bool
    otherwise -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left (Integer -> EvalError
    InvalidIndex Integer
    ix)) TValue
    a
    >     Inf               -> String -> [String] -> Value
    forall a. String -> [String] -> a
    evalPanic "indexBack" ["unexpected infinite sequence"]
    >
    > updatePrim :: (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
    > updatePrim :: (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
    updatePrim op :: Nat' -> [Value] -> Integer -> Value -> [Value]
    op =
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \len :: Nat'
    len ->
    >   (TValue -> Value) -> Value
    VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \eltTy :: TValue
    eltTy ->
    >   (Nat' -> Value) -> Value
    VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \_idxLen :: Nat'
    _idxLen ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \xs :: Value
    xs ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \idx :: Value
    idx ->
    >   (Value -> Value) -> Value
    VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \val :: Value
    val ->
    >   TValue -> Value -> Value
    copyByTValue (Nat' -> TValue -> TValue
    tvSeq Nat'
    len TValue
    eltTy) (Value -> Value) -> Value -> Value
    forall a b. (a -> b) -> a -> b
    $
    >   case Value -> Either EvalError Integer
    fromVWord Value
    idx of
    >     Left e :: EvalError
    e -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left EvalError
    e) (Nat' -> TValue -> TValue
    tvSeq Nat'
    len TValue
    eltTy)
    >     Right i :: Integer
    i
    >       | Integer -> Nat'
    Nat Integer
    i Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat'
    len -> Nat' -> [Value] -> Value
    VList Nat'
    len (Nat' -> [Value] -> Integer -> Value -> [Value]
    op Nat'
    len (Value -> [Value]
    fromVList Value
    xs) Integer
    i Value
    val)
    >       | Bool
    otherwise   -> Either EvalError Bool -> TValue -> Value
    logicNullary (EvalError -> Either EvalError Bool
    forall a b. a -> Either a b
    Left (Integer -> EvalError
    InvalidIndex Integer
    i)) (Nat' -> TValue -> TValue
    tvSeq Nat'
    len TValue
    eltTy)
    >
    > updateFront :: Nat' -> [Value] -> Integer -> Value -> [Value]
    > updateFront :: Nat' -> [Value] -> Integer -> Value -> [Value]
    updateFront _ vs :: [Value]
    vs i :: Integer
    i x :: Value
    x = [Value] -> Integer -> Value -> [Value]
    forall a. [a] -> Integer -> a -> [a]
    updateAt [Value]
    vs Integer
    i Value
    x
    >
    > updateBack :: Nat' -> [Value] -> Integer -> Value -> [Value]
    > updateBack :: Nat' -> [Value] -> Integer -> Value -> [Value]
    updateBack Inf _vs :: [Value]
    _vs _i :: Integer
    _i _x :: Value
    _x = String -> [String] -> [Value]
    forall a. String -> [String] -> a
    evalPanic "Unexpected infinite sequence in updateEnd" []
    > updateBack (Nat n :: Integer
    n) vs :: [Value]
    vs i :: Integer
    i x :: Value
    x = [Value] -> Integer -> Value -> [Value]
    forall a. [a] -> Integer -> a -> [a]
    updateAt [Value]
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1) Value
    x
    >
    > updateAt :: [a] -> Integer -> a -> [a]
    > updateAt :: [a] -> Integer -> a -> [a]
    updateAt []       _ _ = []
    > updateAt (_ : xs :: [a]
    xs) 0 y :: a
    y = a
    y a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    xs
    > updateAt (x :: a
    x : xs :: [a]
    xs) i :: Integer
    i y :: a
    y = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> Integer -> a -> [a]
    forall a. [a] -> Integer -> a -> [a]
    updateAt [a]
    xs (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1) a
    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 :: String -> [String] -> a
    evalPanic cxt :: String
    cxt = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic ("[Reference Evaluator]" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)

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

    > ppValue :: PPOpts -> Value -> Doc
    > ppValue :: PPOpts -> Value -> Doc
    ppValue opts :: PPOpts
    opts val :: Value
    val =
    >   case Value
    val of
    >     VBit b :: Either EvalError Bool
    b     -> String -> Doc
    text ((EvalError -> String)
    -> (Bool -> String) -> Either EvalError Bool -> String
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either EvalError -> String
    forall a. Show a => a -> String
    show Bool -> String
    forall a. Show a => a -> String
    show Either EvalError Bool
    b)
    >     VInteger i :: Either EvalError Integer
    i -> String -> Doc
    text ((EvalError -> String)
    -> (Integer -> String) -> Either EvalError Integer -> String
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either EvalError -> String
    forall a. Show a => a -> String
    show Integer -> String
    forall a. Show a => a -> String
    show Either EvalError Integer
    i)
    >     VList l :: Nat'
    l vs :: [Value]
    vs ->
    >       case Nat'
    l of
    >         Inf -> [Doc] -> Doc
    ppList ((Value -> Doc) -> [Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> Value -> Doc
    ppValue PPOpts
    opts) (Int -> [Value] -> [Value]
    forall a. Int -> [a] -> [a]
    take (PPOpts -> Int
    useInfLength PPOpts
    opts) [Value]
    vs) [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Doc
    text "..."])
    >         Nat n :: Integer
    n ->
    >           -- For lists of defined bits, print the value as a numeral.
    >           case (Value -> Maybe Bool) -> [Value] -> Maybe [Bool]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Value -> Maybe Bool
    isBit [Value]
    vs of
    >             Just bs :: [Bool]
    bs -> PPOpts -> BV -> Doc
    ppBV PPOpts
    opts (Integer -> Integer -> BV
    mkBv Integer
    n ([Bool] -> Integer
    bitsToInteger [Bool]
    bs))
    >             Nothing -> [Doc] -> Doc
    ppList ((Value -> Doc) -> [Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> Value -> Doc
    ppValue PPOpts
    opts) [Value]
    vs)
    >       where ppList :: [Doc] -> Doc
    ppList docs :: [Doc]
    docs = Doc -> Doc
    brackets ([Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma [Doc]
    docs))
    >             isBit :: Value -> Maybe Bool
    isBit v :: Value
    v = case Value
    v of VBit (Right b :: Bool
    b) -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    b
    >                                 _              -> Maybe Bool
    forall a. Maybe a
    Nothing
    >     VTuple vs :: [Value]
    vs  -> Doc -> Doc
    parens ([Doc] -> Doc
    sep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ((Value -> Doc) -> [Value] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (PPOpts -> Value -> Doc
    ppValue PPOpts
    opts) [Value]
    vs)))
    >     VRecord fs :: [(Ident, Value)]
    fs -> Doc -> Doc
    braces ([Doc] -> Doc
    sep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma (((Ident, Value) -> Doc) -> [(Ident, Value)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Value) -> Doc
    forall a. PP a => (a, Value) -> Doc
    ppField [(Ident, Value)]
    fs)))
    >       where ppField :: (a, Value) -> Doc
    ppField (f :: a
    f,r :: Value
    r) = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    f Doc -> Doc -> Doc
    <+> Char -> Doc
    char '=' Doc -> Doc -> Doc
    <+> PPOpts -> Value -> Doc
    ppValue PPOpts
    opts Value
    r
    >     VFun _     -> String -> Doc
    text "<function>"
    >     VPoly _    -> String -> Doc
    text "<polymorphic value>"
    >     VNumPoly _ -> String -> Doc
    text "<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 Value
    > evaluate :: Expr -> ModuleCmd Value
    evaluate expr :: Expr
    expr (_,modEnv :: ModuleEnv
    modEnv) = (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
    -> IO (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Value, ModuleEnv) -> Either ModuleError (Value, ModuleEnv)
    forall a b. b -> Either a b
    Right (Env -> Expr -> Value
    evalExpr Env
    env Expr
    expr, ModuleEnv
    modEnv), [])
    >   where
    >     extDgs :: [DeclGroup]
    extDgs = (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Module -> [DeclGroup]
    mDecls (ModuleEnv -> [Module]
    M.loadedModules ModuleEnv
    modEnv)
    >     env :: Env
    env = (Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Env -> DeclGroup -> Env
    evalDeclGroup Env
    forall a. Monoid a => a
    mempty [DeclGroup]
    extDgs