> -- |
> -- Module      :  Cryptol.Eval.Reference
> -- Description :  The reference implementation of the Cryptol evaluation semantics.
> -- Copyright   :  (c) 2013-2020 Galois, Inc.
> -- License     :  BSD3
> -- Maintainer  :  cryptol@galois.com
> -- Stability   :  provisional
> -- Portability :  portable
>
> {-# LANGUAGE BlockArguments #-}
> {-# LANGUAGE PatternGuards #-}
> {-# LANGUAGE LambdaCase #-}
>
> module Cryptol.Eval.Reference
>   ( Value(..)
>   , E(..)
>   , evaluate
>   , evalExpr
>   , evalDeclGroup
>   , ppValue
>   , ppEValue
>   ) where
>
> import Data.Bits
> import Data.Ratio((%))
> import Data.List
>   (genericIndex, genericLength, genericReplicate, genericTake, sortBy)
> import Data.Ord (comparing)
> import Data.Map (Map)
> import qualified Data.Map as Map
> import qualified Data.IntMap as IntMap
> import qualified Data.Text as T (pack)
> import LibBF (BigFloat)
> import qualified LibBF as FP
> import qualified GHC.Integer.GMP.Internals as Integer
>
> import Cryptol.ModuleSystem.Name (asPrim)
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
> import Cryptol.TypeCheck.AST
> import Cryptol.Backend.FloatHelpers (BF(..))
> import qualified Cryptol.Backend.FloatHelpers as FP
> import Cryptol.Backend.Monad (EvalError(..), PPOpts(..))
> import Cryptol.Eval.Type (TValue(..), isTBit, evalValType, evalNumType, TypeEnv)
> import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
> import Cryptol.Utils.Panic (panic)
> import Cryptol.Utils.PP
> import Cryptol.Utils.RecordMap
>
> import 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`                 |
| `Z n`             | integers modulo n | `TVIntMod n`                |
| `Rational`        | rationals         | `TVRational`                |
| `Float e p`       | floating point    | `TVFloat`                   |
| `Array`           | arrays            | `TVArray`                   |
| `[n]a`            | finite lists      | `TVSeq n a`                 |
| `[inf]a`          | infinite lists    | `TVStream a`                |
| `(a, b, c)`       | tuples            | `TVTuple [a,b,c]`           |
| `{x:a, y:b, z:c}` | records           | `TVRec [(x,a),(y,b),(z,c)]` |
| `a -> b`          | functions         | `TVFun a b`                 |

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

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

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

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

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

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

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

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

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

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

Values
------

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

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

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

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


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

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

> data Env = Env
>   { Env -> Map Name (E Value)
envVars       :: !(Map Name (E Value))
>   , Env -> TypeEnv
envTypes      :: !TypeEnv
>   }
>
> instance Semigroup Env where
>   Env
l <> :: Env -> Env -> Env
<> Env
r = Env :: Map Name (E Value) -> TypeEnv -> Env
Env
>     { envVars :: Map Name (E Value)
envVars  = Map Name (E Value) -> Map Name (E Value) -> Map Name (E Value)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Env -> Map Name (E Value)
envVars  Env
l) (Env -> Map Name (E Value)
envVars  Env
r)
>     , envTypes :: TypeEnv
envTypes = TypeEnv -> TypeEnv -> TypeEnv
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (Env -> TypeEnv
envTypes Env
l) (Env -> TypeEnv
envTypes Env
r)
>     }
>
> instance Monoid Env where
>   mempty :: Env
mempty = Env :: Map Name (E Value) -> TypeEnv -> Env
Env
>     { envVars :: Map Name (E Value)
envVars  = Map Name (E Value)
forall k a. Map k a
Map.empty
>     , envTypes :: TypeEnv
envTypes = TypeEnv
forall a. IntMap a
IntMap.empty
>     }
>   mappend :: Env -> Env -> Env
mappend Env
l 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, E Value) -> Env -> Env
> bindVar :: (Name, E Value) -> Env -> Env
bindVar (Name
n, E Value
val) Env
env = Env
env { envVars :: Map Name (E Value)
envVars = Name -> E Value -> Map Name (E Value) -> Map Name (E Value)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n E Value
val (Env -> Map Name (E Value)
envVars Env
env) }
>
> -- | Bind a type variable of kind # or *.
> bindType :: TVar -> Either Nat' TValue -> Env -> Env
> bindType :: TVar -> Either Nat' TValue -> Env -> Env
bindType TVar
p Either Nat' TValue
ty Env
env = Env
env { envTypes :: TypeEnv
envTypes = Key -> Either Nat' TValue -> TypeEnv -> TypeEnv
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (TVar -> Key
tvUnique TVar
p) Either Nat' TValue
ty (Env -> TypeEnv
envTypes Env
env) }


Evaluation
==========

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

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


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


Selectors
---------

Apply the the given selector form to the given value.

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

> evalComp :: Env         -- ^ Starting evaluation environment
>          -> Expr        -- ^ Head expression of the comprehension
>          -> [[Match]]   -- ^ List of parallel comprehension branches
>          -> E Value
> evalComp :: Env -> Expr -> [[Match]] -> E Value
evalComp Env
env Expr
expr [[Match]]
branches = Value -> E Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> E Value) -> Value -> E Value
forall a b. (a -> b) -> a -> b
$ Nat' -> [E Value] -> Value
VList Nat'
len [ Env -> Expr -> E Value
evalExpr Env
e Expr
expr | Env
e <- [Env]
envs ]
>   where
>     -- Generate a new environment for each iteration of each
>     -- parallel branch.
>     benvs :: [[Env]]
>     benvs :: [[Env]]
benvs = ([Match] -> [Env]) -> [[Match]] -> [[Env]]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [Match] -> [Env]
evalBranch Env
env) [[Match]]
branches
>
>     -- Zip together the lists of environments from each branch,
>     -- producing a list of merged environments. Longer branches get
>     -- truncated to the length of the shortest branch.
>     envs :: [Env]
>     envs :: [Env]
envs = ([Env] -> [Env] -> [Env]) -> [[Env]] -> [Env]
forall (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 DeclGroup
dg = do
>   case DeclGroup
dg of
>     NonRecursive Decl
d ->
>       (Name, E Value) -> Env -> Env
bindVar (Env -> Decl -> (Name, E Value)
evalDecl Env
env Decl
d) Env
env
>     Recursive [Decl]
ds ->
>       let env' :: Env
env' = ((Name, E Value) -> Env -> Env) -> Env -> [(Name, E Value)] -> Env
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, E Value) -> Env -> Env
bindVar Env
env [(Name, E Value)]
bindings
>           bindings :: [(Name, E Value)]
bindings = (Decl -> (Name, E Value)) -> [Decl] -> [(Name, E Value)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Decl -> (Name, E Value)
evalDecl Env
env') [Decl]
ds
>       in Env
env'
>
> evalDecl :: Env -> Decl -> (Name, E Value)
> evalDecl :: Env -> Decl -> (Name, E Value)
evalDecl Env
env Decl
d =
>   case Decl -> DeclDef
dDefinition Decl
d of
>     DeclDef
DPrim   -> (Decl -> Name
dName Decl
d, Value -> E Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Value
evalPrim (Decl -> Name
dName Decl
d)))
>     DExpr Expr
e -> (Decl -> Name
dName Decl
d, Env -> Expr -> E 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 Name
n
>   | Just PrimIdent
i <- Name -> Maybe PrimIdent
asPrim Name
n, Just Value
v <- PrimIdent -> Map PrimIdent Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent Value
primTable = Value
v
>   | Bool
otherwise = String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic String
"evalPrim" [String
"Unimplemented primitive", Name -> String
forall a. Show a => a -> String
show Name
n]

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

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

* Zero: zero

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

Errors
------

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

Zero
----

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

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


Literals
--------

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

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


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

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


Logic
-----

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

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

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


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

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

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

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

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


Integral
---------

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


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

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


Field
-----

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

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

Round
-----

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

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

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


Rational
----------

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


Comparison
----------

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

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

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

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

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


Sequences
---------

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


Shifting
--------

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

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

Indexing
--------

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

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

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

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

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

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

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


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

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

These functions capture the interactions with rationals.


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

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


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

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


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


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

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

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

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

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

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

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

> evaluate :: Expr -> M.ModuleCmd (E Value)
> evaluate :: Expr -> ModuleCmd (E Value)
evaluate Expr
expr (EvalOpts
_, String -> IO ByteString
_, ModuleEnv
modEnv) = (Either ModuleError (E Value, ModuleEnv), [ModuleWarning])
-> IO (Either ModuleError (E Value, ModuleEnv), [ModuleWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return ((E Value, ModuleEnv) -> Either ModuleError (E Value, ModuleEnv)
forall a b. b -> Either a b
Right (Env -> Expr -> E 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