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

Overview
========

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

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

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

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

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

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

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

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

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

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

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

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

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

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

> instance Monad E where
>   E a
m >>= :: forall a b. E a -> (a -> E b) -> E b
>>= a -> E b
f =
>     case E a
m of
>       Value a
x -> a -> E b
f a
x
>       Err EvalError
r   -> forall a. EvalError -> E a
Err EvalError
r
>
> eitherToE :: Either EvalError a -> E a
> eitherToE :: forall a. Either EvalError a -> E a
eitherToE (Left EvalError
e)  = forall a. EvalError -> E a
Err EvalError
e
> eitherToE (Right a
x) = 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
_        = 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
_            = 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
_             = forall a. String -> [String] -> a
evalPanic String
"fromVRational" [String
"Expected a rational"]
>
> fromVFloat :: Value -> BigFloat
> fromVFloat :: Value -> BigFloat
fromVFloat = BF -> BigFloat
bfValue 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
_ -> 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
_            = 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
_           = 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
_            = 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
_        = 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 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  -> 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     = forall a. String -> [String] -> a
evalPanic String
"vFinPoly" [String
"Expected finite numeric type"]


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

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

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


Evaluation
==========

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

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

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

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


Selectors
---------

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

> evalSel :: Selector -> Value -> E Value
> evalSel :: Selector -> Value -> E Value
evalSel Selector
sel Value
val =
>   case Selector
sel of
>     TupleSel Int
n Maybe Int
_  -> Int -> Value -> E Value
tupleSel Int
n Value
val
>     RecordSel Ident
n Maybe [Ident]
_ -> Ident -> Value -> E Value
recordSel Ident
n Value
val
>     ListSel Int
n Maybe Int
_   -> Int -> Value -> E Value
listSel Int
n Value
val
>   where
>     tupleSel :: Int -> Value -> E Value
tupleSel Int
n Value
v =
>       case Value
v of
>         VTuple [E Value]
vs   -> [E Value]
vs forall a. [a] -> Int -> a
!! Int
n
>         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
_           -> forall a. String -> [String] -> a
evalPanic String
"evalSel"
>                        [String
"Unexpected value in record selection."]
>     listSel :: Int -> Value -> E Value
listSel Int
n Value
v =
>       case Value
v of
>         VList Nat'
_ [E Value]
vs  -> [E Value]
vs forall a. [a] -> Int -> a
!! Int
n
>         Value
_           -> forall a. String -> [String] -> a
evalPanic String
"evalSel"
>                        [String
"Unexpected value in list selection."]


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

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

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

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

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

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

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

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

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

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

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

> evalComp :: Env         -- ^ Starting evaluation environment
>          -> Expr        -- ^ Head expression of the comprehension
>          -> [[Match]]   -- ^ List of parallel comprehension branches
>          -> E Value
> evalComp :: Env -> Expr -> [[Match]] -> E Value
evalComp Env
env Expr
expr [[Match]]
branches =
>     forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 = 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 = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Monoid a => a -> a -> a
mappend) [[Env]]
benvs
>
>     len :: Nat'
>     len :: Nat'
len = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Nat' -> Nat' -> Nat'
nMin (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' = 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 = 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, forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Value
evalPrim (Decl -> Name
dName Decl
d)))
>     DForeign FFIFunType
_ -> (Decl -> Name
dName Decl
d, forall a. EvalError -> E a
cryError forall a b. (a -> b) -> a -> b
$ Name -> EvalError
FFINotSupported forall a b. (a -> b) -> a -> b
$ Decl -> Name
dName Decl
d)
>     DExpr Expr
e    -> (Decl -> Name
dName Decl
d, Env -> Expr -> E Value
evalExpr Env
env Expr
e)
>

Newtypes
--------

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

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

Primitives
==========

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

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

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

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

* Zero: zero

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

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

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

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

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

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

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

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

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

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

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

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

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


> cryptolPrimTable :: Map PrimIdent Value
> cryptolPrimTable :: Map PrimIdent Value
cryptolPrimTable = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ 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"       forall a. String -> a -> (String, a)
~> Bool -> Value
VBit Bool
True
>   , String
"False"      forall a. String -> a -> (String, a)
~> Bool -> Value
VBit Bool
False
>   , String
"number"     forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
val -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
a ->
>                     Integer -> TValue -> E Value
literal Integer
val TValue
a
>   , String
"fraction"   forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly \Integer
top -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly \Integer
bot -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly \Integer
rnd -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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"       forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> Value
zero)
>
>   -- Logic (bitwise)
>   , String
"&&"         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
"||"         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
"^"          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 forall a. Eq a => a -> a -> Bool
(/=))
>   , String
"complement" 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
"+"          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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
x forall a. Num a => a -> a -> a
+ Integer
y))
>                              (\Rational
x Rational
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational
x 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
"-"          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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
x forall a. Num a => a -> a -> a
- Integer
y))
>                               (\Rational
x Rational
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational
x 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
"*"          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"     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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (- Integer
x))
>                                       (\Rational
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (- Rational
x))
>                                       (\Integer
_ Integer
_ BigFloat
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> BigFloat
FP.bfNeg BigFloat
x)))
>   , String
"fromInteger"forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
x)
>                                 (forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
fromVInteger 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
x)
>                                 TValue
a
>
>   -- Integral
>   , String
"toInteger"  forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
x ->
>                     Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> E Value -> E Integer
cryToInteger TValue
a E Value
x
>   , String
"/"          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
"%"          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
"^^"         forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
aty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ety -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
e ->
>                       TValue -> E Value -> Integer -> E Value
ringExp TValue
aty E Value
a 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
"/."         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"      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"      forall a. String -> a -> (String, a)
~> (TValue -> E Value -> E Value) -> Value
unary ((Rational -> Integer)
-> (BF -> E Integer) -> TValue -> E Value -> E Value
roundUnary forall a b. (RealFrac a, Integral b) => a -> b
floor
>                      (forall a. Either EvalError a -> E a
eitherToE 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"    forall a. String -> a -> (String, a)
~> (TValue -> E Value -> E Value) -> Value
unary ((Rational -> Integer)
-> (BF -> E Integer) -> TValue -> E Value -> E Value
roundUnary forall a b. (RealFrac a, Integral b) => a -> b
ceiling
>                      (forall a. Either EvalError a -> E a
eitherToE 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"      forall a. String -> a -> (String, a)
~> (TValue -> E Value -> E Value) -> Value
unary ((Rational -> Integer)
-> (BF -> E Integer) -> TValue -> E Value -> E Value
roundUnary forall a b. (RealFrac a, Integral b) => a -> b
truncate
>                      (forall a. Either EvalError a -> E a
eitherToE 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"  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
>                      (forall a. Either EvalError a -> E a
eitherToE 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"forall a. String -> a -> (String, a)
~> (TValue -> E Value -> E Value) -> Value
unary ((Rational -> Integer)
-> (BF -> E Integer) -> TValue -> E Value -> E Value
roundUnary forall a b. (RealFrac a, Integral b) => a -> b
round
>                      (forall a. Either EvalError a -> E a
eitherToE 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
"<"          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 forall a. Eq a => a -> a -> Bool
== Ordering
LT))
>   , String
">"          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 forall a. Eq a => a -> a -> Bool
== Ordering
GT))
>   , String
"<="         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 forall a. Eq a => a -> a -> Bool
/= Ordering
GT))
>   , String
">="         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 forall a. Eq a => a -> a -> Bool
/= Ordering
LT))
>   , String
"=="         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 forall a. Eq a => a -> a -> Bool
== Ordering
EQ))
>   , String
"!="         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 forall a. Eq a => a -> a -> Bool
/= Ordering
EQ))
>   , String
"<$"         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
"/$"         forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
r ->
>                       Integer -> Integer -> Value
vWord Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
divWrap
>                                          (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
l)
>                                          (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
r)
>   , String
"%$"         forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
r ->
>                       Integer -> Integer -> Value
vWord Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
modWrap
>                                          (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
l)
>                                          (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
r)
>   , String
">>$"        forall a. String -> a -> (String, a)
~> Value
signedShiftRV
>   , String
"lg2"        forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v ->
>                       Integer -> Integer -> Value
vWord Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 Integer -> E Integer
lg2Wrap (Value -> E Integer
fromVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
v)
>   -- Rational
>   , String
"ratio"      forall a. String -> a -> (String, a)
~> (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
r ->
>                     Rational -> Value
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Rational
ratioOp
>                                          (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l)
>                                          (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>
>   -- Z n
>   , String
"fromZ"      forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
x ->
>                     Integer -> Value
VInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Integral a => a -> a -> a
mod Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
x
>
>   -- Sequences
>   , String
"#"          forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
front -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
back  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_elty  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
r ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Nat' -> Nat' -> Nat'
nAdd (Integer -> Nat'
Nat Integer
front) Nat'
back) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                         if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
front then
>                           do [E Value]
l' <- Value -> [E Value]
fromVList 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 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 forall a. Num a => a -> a -> a
- Integer
front)
>
>   , String
"join"       forall a. String -> a -> (String, a)
~> (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
parts -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
each  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Nat' -> Nat' -> Nat'
nMul Nat'
parts (Integer -> Nat'
Nat Integer
each)) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                         do let (Integer
q,Integer
r) = forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
>                            [E Value]
xss <- Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v
>                            [E Value]
xs  <- Value -> [E Value]
fromVList 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"      forall a. String -> a -> (String, a)
~> (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
parts -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
each  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
val ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
parts forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                         forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Integer -> Nat'
Nat Integer
each) forall a b. (a -> b) -> a -> b
$ \Integer
j ->
>                           do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Num a => a -> a -> a
* Integer
each forall a. Num a => a -> a -> a
+ Integer
j)
>
>   , String
"take"       forall a. String -> a -> (String, a)
~> (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
front -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
back  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
_a    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun     forall a b. (a -> b) -> a -> b
$ \E Value
v ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
front forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                                do [E Value]
vs <- Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v
>                                   Nat' -> [E Value] -> Integer -> E Value
indexFront (Nat' -> Nat' -> Nat'
nAdd Nat'
front Nat'
back) [E Value]
vs Integer
i
>
>   , String
"drop"       forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
front -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
back -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
back forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                                do [E Value]
vs <- Value -> [E Value]
fromVList 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
frontforall a. Num a => a -> a -> a
+Integer
i)
>
>   , String
"reverse"    forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Integer -> Nat'
Nat Integer
n) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                         do [E Value]
vs <- Value -> [E Value]
fromVList 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"  forall a. String -> a -> (String, a)
~> (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
rows -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
cols -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
val ->
>                       forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
cols forall a b. (a -> b) -> a -> b
$ \Integer
c ->
>                         forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
rows forall a b. (a -> b) -> a -> b
$ \Integer
r ->
>                         do [E Value]
xss <- Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val
>                            [E Value]
xs <- Value -> [E Value]
fromVList 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
"<<"         forall a. String -> a -> (String, a)
~> (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
shiftV Nat' -> TValue -> E Value -> Integer -> Value
shiftLV
>   , String
">>"         forall a. String -> a -> (String, a)
~> (Nat' -> TValue -> E Value -> Integer -> Value) -> Value
shiftV Nat' -> TValue -> E Value -> Integer -> Value
shiftRV
>   , String
"<<<"        forall a. String -> a -> (String, a)
~> (Integer -> E Value -> Integer -> E Value) -> Value
rotateV Integer -> E Value -> Integer -> E Value
rotateLV
>   , String
">>>"        forall a. String -> a -> (String, a)
~> (Integer -> E Value -> Integer -> E Value) -> Value
rotateV Integer -> E Value -> Integer -> E Value
rotateRV
>
>   -- Indexing:
>   , String
"@"          forall a. String -> a -> (String, a)
~> (Nat' -> [E Value] -> Integer -> E Value) -> Value
indexPrimOne  Nat' -> [E Value] -> Integer -> E Value
indexFront
>   , String
"!"          forall a. String -> a -> (String, a)
~> (Nat' -> [E Value] -> Integer -> E Value) -> Value
indexPrimOne  Nat' -> [E Value] -> Integer -> E Value
indexBack
>   , String
"update"     forall a. String -> a -> (String, a)
~> (Nat' -> Integer -> Integer) -> Value
updatePrim Nat' -> Integer -> Integer
updateFront
>   , String
"updateEnd"  forall a. String -> a -> (String, a)
~> (Nat' -> Integer -> Integer) -> Value
updatePrim Nat' -> Integer -> Integer
updateBack
>
>   -- Enumerations
>   , String
"fromTo"     forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
lst   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat (Integer
1 forall a. Num a => a -> a -> a
+ Integer
lst forall a. Num a => a -> a -> a
- Integer
first)) (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f [Integer
first .. Integer
lst])
>
>   , String
"fromToLessThan" forall a. String -> a -> (String, a)
~>
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
bound -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     case Nat'
bound of
>                       Nat'
Inf -> Nat' -> [E Value] -> Value
VList Nat'
Inf (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f [Integer
first ..])
>                       Nat Integer
bound' ->
>                         let len :: Integer
len = Integer
bound' forall a. Num a => a -> a -> a
- Integer
first in
>                         Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [Integer
first ..]))
>
>   , String
"fromToBy"   forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
lst    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
stride -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     let vs :: [E Value]
vs  = [ Integer -> E Value
f (Integer
first forall a. Num a => a -> a -> a
+ Integer
iforall a. Num a => a -> a -> a
*Integer
stride) | Integer
i <- [Integer
0..] ] in
>                     let len :: Integer
len = Integer
1 forall a. Num a => a -> a -> a
+ ((Integer
lstforall a. Num a => a -> a -> a
-Integer
first) forall a. Integral a => a -> a -> a
`div` Integer
stride) in
>                     Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [E Value]
vs)
>
>   , String
"fromToByLessThan" forall a. String -> a -> (String, a)
~>
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
bound  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
stride -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     let vs :: [E Value]
vs  = [ Integer -> E Value
f (Integer
first forall a. Num a => a -> a -> a
+ Integer
iforall a. Num a => a -> a -> a
*Integer
stride) | Integer
i <- [Integer
0..] ] in
>                     case Nat'
bound of
>                       Nat'
Inf -> Nat' -> [E Value] -> Value
VList Nat'
Inf [E Value]
vs
>                       Nat Integer
bound' ->
>                         let len :: Integer
len = (Integer
bound'forall a. Num a => a -> a -> a
-Integer
firstforall a. Num a => a -> a -> a
+Integer
strideforall a. Num a => a -> a -> a
-Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
stride in
>                         Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [E Value]
vs)
>
>   , String
"fromToDownBy" forall a. String -> a -> (String, a)
~>
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
lst    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
stride -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     let vs :: [E Value]
vs  = [ Integer -> E Value
f (Integer
first forall a. Num a => a -> a -> a
- Integer
iforall a. Num a => a -> a -> a
*Integer
stride) | Integer
i <- [Integer
0..] ] in
>                     let len :: Integer
len = Integer
1 forall a. Num a => a -> a -> a
+ ((Integer
firstforall a. Num a => a -> a -> a
-Integer
lst) forall a. Integral a => a -> a -> a
`div` Integer
stride) in
>                     Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [E Value]
vs)
>
>   , String
"fromToDownByGreaterThan" forall a. String -> a -> (String, a)
~>
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
lst    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
stride -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     let vs :: [E Value]
vs  = [ Integer -> E Value
f (Integer
first forall a. Num a => a -> a -> a
- Integer
iforall a. Num a => a -> a -> a
*Integer
stride) | Integer
i <- [Integer
0..] ] in
>                     let len :: Integer
len = (Integer
firstforall a. Num a => a -> a -> a
-Integer
lstforall a. Num a => a -> a -> a
+Integer
strideforall a. Num a => a -> a -> a
-Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
stride in
>                     Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [E Value]
vs)
>
>   , String
"fromThenTo" forall a. String -> a -> (String, a)
~> (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
first -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
next  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
_lst  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly    forall a b. (a -> b) -> a -> b
$ \TValue
ty    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Integer -> E Value) -> Value
vFinPoly forall a b. (a -> b) -> a -> b
$ \Integer
len   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     let f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal Integer
i TValue
ty in
>                     Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
len)
>                           (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f (forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [Integer
first, Integer
next ..]))
>
>   , String
"infFrom"    forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun 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 forall a. Num a => a -> a -> a
+ Integer
i) TValue
ty
>                        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> [E Value] -> Value
VList Nat'
Inf (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f [Integer
0 ..])
>
>   , String
"infFromThen"forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
first -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun 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 forall a. Num a => a -> a -> a
- Integer
x
>                            f :: Integer -> E Value
f Integer
i = Integer -> TValue -> E Value
literal (Integer
x forall a. Num a => a -> a -> a
+ Integer
diff forall a. Num a => a -> a -> a
* Integer
i) TValue
ty
>                        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> [E Value] -> Value
VList Nat'
Inf (forall a b. (a -> b) -> [a] -> [b]
map Integer -> E Value
f [Integer
0 ..])
>
>   -- Miscellaneous:
>   , String
"parmap"     forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
f -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
xs ->
>                        do E Value -> E Value
f' <- Value -> E Value -> E Value
fromVFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
f
>                           [E Value]
xs' <- Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
xs
>                           -- Note: the reference implementation simply
>                           -- executes parmap sequentially
>                           forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> [E Value] -> Value
VList Nat'
n (forall a b. (a -> b) -> [a] -> [b]
map E Value -> E Value
f' [E Value]
xs')
>
>   , String
"error"      forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
s ->
>                       do String
msg <- E Value -> E String
evalString E Value
s
>                          forall a. EvalError -> E a
cryError (String -> EvalError
UserError String
msg)
>
>   , String
"random"     forall a. String -> a -> (String, a)
~> (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
_seed -> forall a. EvalError -> E a
cryError (String -> EvalError
UserError String
"random: unimplemented")
>
>   , String
"trace"      forall a. String -> a -> (String, a)
~> (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
_n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>                     (E Value -> E Value) -> Value
VFun 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v
>      [Integer]
ws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Value -> E Integer
fromVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) [E Value]
cs
>      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ \TValue
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>           (E Value -> E Value) -> Value
VFun  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 forall a b. (a -> b) -> a -> b
$ \TValue
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>            (E Value -> E Value) -> Value
VFun  forall a b. (a -> b) -> a -> b
$ \E Value
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>            (E Value -> E Value) -> Value
VFun  forall a b. (a -> b) -> a -> b
$ \E Value
y -> TValue -> E Value -> E Value -> E Value
f TValue
ty E Value
x E Value
y
>
> appOp1 :: (a -> E b) -> E a -> E b
> appOp1 :: forall a b. (a -> E b) -> E a -> E b
appOp1 a -> E b
f E a
x =
>   do a
x' <- E a
x
>      a -> E b
f a
x'
>
> appOp2 :: (a -> b -> E c) -> E a -> E b -> E c
> appOp2 :: forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 a -> b -> E c
f E a
x E b
y =
>   do a
x' <- E a
x
>      b
y' <- E b
y
>      a -> b -> E c
f a
x' b
y'

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

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

> fromVWord :: Value -> E Integer
> fromVWord :: Value -> E Integer
fromVWord Value
v = [Bool] -> Integer
bitsToInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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 forall a. Num a => a -> a -> a
* a
x forall a. Num a => a -> a -> a
+ a
1 else a
2 forall a. Num a => a -> a -> a
* a
x

> fromSignedVWord :: Value -> E Integer
> fromSignedVWord :: Value -> E Integer
fromSignedVWord Value
v = [Bool] -> Integer
signedBitsToInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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 [] =
>   forall a. String -> [String] -> a
evalPanic String
"signedBitsToInteger" [String
"Bitvector has zero length"]
> signedBitsToInteger (Bool
b0 : [Bool]
bs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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 forall a. Num a => a -> a -> a
* a
x forall a. Num a => a -> a -> a
+ a
1 else a
2 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 forall a. Ord a => a -> a -> Bool
> forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) =
>       forall a. String -> [String] -> a
evalPanic String
"vWord" [String
"Word length too large", forall a. Show a => a -> String
show Integer
w]
>   | Bool
otherwise =
>       Nat' -> [E Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) [ forall {f :: * -> *}. Applicative f => Integer -> f Value
mkBit Integer
i | Integer
i <- [Integer
wforall a. Num a => a -> a -> a
-Integer
1, Integer
wforall a. Num a => a -> a -> a
-Integer
2 .. Integer
0 ] ]
>  where
>    mkBit :: Integer -> f Value
mkBit Integer
i = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Value
VBit (forall a. Bits a => a -> Int -> Bool
testBit Integer
e (forall a. Num a => Integer -> a
fromInteger Integer
i)))

Errors
------

> cryError :: EvalError -> E a
> cryError :: forall a. EvalError -> E a
cryError EvalError
e = 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{}      = 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) (forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (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 (forall a. a -> [a]
repeat (forall (f :: * -> *) a. Applicative f => a -> f a
pure (TValue -> Value
zero TValue
ety)))
> zero (TVTuple [TValue]
tys)  = [E Value] -> Value
VTuple (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a. Applicative f => a -> f a
pure 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, forall (f :: * -> *) a. Applicative f => a -> f a
pure (TValue -> Value
zero TValue
fty))
>                               | (Ident
f, TValue
fty) <- 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
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (TValue -> Value
zero TValue
bty))
> zero (TVAbstract{}) = forall a. String -> [String] -> a
evalPanic String
"zero" [String
"Abstract type not in `Zero`"]
> zero (TVNewtype{})  = forall a. String -> [String] -> a
evalPanic String
"zero" [String
"Newtype not in `Zero`"]

Literals
--------

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

> literal :: Integer -> TValue -> E Value
> literal :: Integer -> TValue -> E Value
literal Integer
i = forall {f :: * -> *}. Applicative f => TValue -> f Value
go
>   where
>    go :: TValue -> f Value
go TValue
TVInteger  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Value
VInteger Integer
i)
>    go TValue
TVRational = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> Value
VRational (forall a. Num a => Integer -> a
fromInteger Integer
i))
>    go (TVIntMod Integer
n)
>         | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
n = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Value
VInteger Integer
i)
>         | Bool
otherwise = forall a. String -> [String] -> a
evalPanic String
"literal"
>                            [String
"Literal out of range for type Z " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n]
>    go (TVSeq Integer
w TValue
a)
>         | TValue -> Bool
isTBit TValue
a = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Value
vWord Integer
w Integer
i)
>    go TValue
ty = forall a. String -> [String] -> a
evalPanic String
"literal" [forall a. Show a => a -> String
show TValue
ty 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> Value
VRational (Integer
top forall a. Integral a => a -> a -> Ratio a
% Integer
btm))
>     TVFloat Integer
e Integer
p -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ BF -> Value
VFloat forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> BigFloat -> BF
fpToBF Integer
e Integer
p  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
_ -> forall a. String -> [String] -> a
evalPanic String
"fraction" [forall a. Show a => a -> String
show TValue
ty forall a. [a] -> [a] -> [a]
++ String
" cannot represent " forall a. [a] -> [a] -> [a]
++
>                                 forall a. Show a => a -> String
show Integer
top forall a. [a] -> [a] -> [a]
++ String
"/" forall a. [a] -> [a] -> [a]
++ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
op forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Bool
fromVBit 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (TValue -> E Value -> E Value
go TValue
ety) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVList 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (TValue -> E Value -> E Value
go TValue
ety) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val
>         TVTuple [TValue]
etys -> [E Value] -> Value
VTuple forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> E Value -> E Value
go [TValue]
etys forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVTuple 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
>                 forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fields ]
>         TVFun TValue
_ TValue
bty  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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    -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Integer not in class Logic"]
>         TVIntMod Integer
_   -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Z not in class Logic"]
>         TVArray{}    -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Array not in class Logic"]
>         TValue
TVRational   -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Rational not in class Logic"]
>         TVFloat{}    -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Float not in class Logic"]
>         TVAbstract{} -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Abstract type not in `Logic`"]
>         TVNewtype{}  -> forall a. String -> [String] -> a
evalPanic String
"logicUnary" [String
"Newtype not in `Logic`"]

> logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
> logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
logicBinary Bool -> Bool -> Bool
op = TValue -> E Value -> E Value -> E Value
go
>   where
>     go :: TValue -> E Value -> E Value -> E Value
>     go :: TValue -> E Value -> E Value -> E Value
go TValue
ty E Value
l E Value
r =
>       case TValue
ty of
>         TValue
TVBit ->
>           Bool -> Value
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bool -> Bool -> Bool
op forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Bool
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> Bool
fromVBit 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Value
go TValue
ety) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                                 (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                                 (Value -> [E Value]
fromVList 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Value
go TValue
ety) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                              (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                              (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r))
>         TVTuple [TValue]
etys ->
>           [E Value] -> Value
VTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> E Value -> E Value -> E Value
go [TValue]
etys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                              (Value -> [E Value]
fromVTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                              (Value -> [E Value]
fromVTuple 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
>               forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fields
>                    ]
>         TVFun TValue
_ TValue
bty  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (E Value -> E Value) -> Value
VFun 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    -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Integer not in class Logic"]
>         TVIntMod Integer
_   -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Z not in class Logic"]
>         TVArray{}    -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Array not in class Logic"]
>         TValue
TVRational   -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Rational not in class Logic"]
>         TVFloat{}    -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Float not in class Logic"]
>         TVAbstract{} -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Abstract type not in `Logic`"]
>         TVNewtype{}  -> forall a. String -> [String] -> a
evalPanic String
"logicBinary" [String
"Newtype not in `Logic`"]


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

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

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

> ringUnary ::
>   (Integer -> E Integer) ->
>   (Rational -> E Rational) ->
>   (Integer -> Integer -> BigFloat -> E BigFloat) ->
>   TValue -> E Value -> E Value
> ringUnary :: (Integer -> E Integer)
-> (Rational -> E Rational)
-> (Integer -> Integer -> BigFloat -> E BigFloat)
-> TValue
-> E Value
-> E Value
ringUnary Integer -> E Integer
iop Rational -> E Rational
qop Integer -> Integer -> BigFloat -> E BigFloat
flop = TValue -> E Value -> E Value
go
>   where
>     go :: TValue -> E Value -> E Value
>     go :: TValue -> E Value -> E Value
go TValue
ty E Value
val =
>       case TValue
ty of
>         TValue
TVBit ->
>           forall a. String -> [String] -> a
evalPanic String
"arithUnary" [String
"Bit not in class Ring"]
>         TValue
TVInteger ->
>           Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 Integer -> E Integer
iop (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val)
>         TVArray{} ->
>           forall a. String -> [String] -> a
evalPanic String
"arithUnary" [String
"Array not in class Ring"]
>         TVIntMod Integer
n ->
>           Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 (\Integer
i -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Integral a => a -> a -> a
mod Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> E Integer
iop Integer
i) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val)
>         TValue
TVRational ->
>           Rational -> Value
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 Rational -> E Rational
qop (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val)
>         TVFloat Integer
e Integer
p ->
>           BF -> Value
VFloat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
fpToBF Integer
e Integer
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 (Integer -> Integer -> BigFloat -> E BigFloat
flop Integer
e Integer
p) (Value -> BigFloat
fromVFloat 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> E Integer
iop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Value -> E Integer
fromVWord 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (TValue -> E Value -> E Value
go TValue
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVList 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (TValue -> E Value -> E Value
go TValue
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
val
>         TVFun TValue
_ TValue
ety ->
>           forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> E Value -> E Value
go [TValue]
tys forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [E Value]
fromVTuple 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
>              forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fs ]
>         TVAbstract {} ->
>           forall a. String -> [String] -> a
evalPanic String
"arithUnary" [String
"Abstract type not in `Ring`"]
>         TVNewtype {} ->
>           forall a. String -> [String] -> a
evalPanic String
"arithUnary" [String
"Newtype not in `Ring`"]

> ringBinary ::
>   (Integer -> Integer -> E Integer) ->
>   (Rational -> Rational -> E Rational) ->
>   (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat) ->
>   TValue -> E Value -> E Value -> E Value
> ringBinary :: (Integer -> Integer -> E Integer)
-> (Rational -> Rational -> E Rational)
-> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat)
-> TValue
-> E Value
-> E Value
-> E Value
ringBinary Integer -> Integer -> E Integer
iop Rational -> Rational -> E Rational
qop Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat
flop = TValue -> E Value -> E Value -> E Value
go
>   where
>     go :: TValue -> E Value -> E Value -> E Value
>     go :: TValue -> E Value -> E Value -> E Value
go TValue
ty E Value
l E Value
r =
>       case TValue
ty of
>         TValue
TVBit ->
>           forall a. String -> [String] -> a
evalPanic String
"arithBinary" [String
"Bit not in class Ring"]
>         TValue
TVInteger ->
>           Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
iop (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>         TVIntMod Integer
n ->
>           Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 (\Integer
i Integer
j -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Integral a => a -> a -> a
mod Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> E Integer
iop Integer
i Integer
j) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>         TValue
TVRational ->
>           Rational -> Value
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Rational -> Rational -> E Rational
qop (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>         TVFloat Integer
e Integer
p ->
>           BF -> Value
VFloat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
fpToBF Integer
e Integer
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>             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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> BigFloat
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>         TVArray{} ->
>           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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
iop (Value -> E Integer
fromVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
l) (Value -> E Integer
fromVWord 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Value
go TValue
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                                     (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                                     (Value -> [E Value]
fromVList 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Value
go TValue
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                            (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                            (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r))
>         TVFun TValue
_ TValue
ety ->
>           forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> E Value -> E Value -> E Value
go [TValue]
tys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                          (Value -> [E Value]
fromVTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
>                          (Value -> [E Value]
fromVTuple 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
>              forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fs ]
>         TVAbstract {} ->
>           forall a. String -> [String] -> a
evalPanic String
"arithBinary" [String
"Abstract type not in class `Ring`"]
>         TVNewtype {} ->
>           forall a. String -> [String] -> a
evalPanic String
"arithBinary" [String
"Newtype not in class `Ring`"]


Integral
---------

> cryToInteger :: TValue -> E Value -> E Integer
> cryToInteger :: TValue -> E Value -> E Integer
cryToInteger TValue
ty E Value
v = case TValue
ty of
>   TValue
TVInteger -> Value -> Integer
fromVInteger 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
v
>   TValue
_ -> forall a. String -> [String] -> a
evalPanic String
"toInteger" [forall a. Show a => a -> String
show TValue
ty 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
op (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
x) (Value -> Integer
fromVInteger 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Integer -> Integer -> E Integer
op (Value -> E Integer
fromVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
x) (Value -> E Integer
fromVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
y)
>
>   TValue
_ -> forall a. String -> [String] -> a
evalPanic String
"integralBinary" [forall a. Show a => a -> String
show TValue
ty 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 = 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) (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
x forall a. Num a => a -> a -> a
* Integer
y))
>                      (\Rational
x Rational
y -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational
x 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 = forall a. EvalError -> E a
cryError EvalError
DivideByZero
> divWrap Integer
x Integer
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
x forall a. Integral a => a -> a -> a
`quot` Integer
y)
>
> modWrap :: Integer -> Integer -> E Integer
> modWrap :: Integer -> Integer -> E Integer
modWrap Integer
_ Integer
0 = forall a. EvalError -> E a
cryError EvalError
DivideByZero
> modWrap Integer
x Integer
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
x forall a. Integral a => a -> a -> a
`rem` Integer
y)
>
> lg2Wrap :: Integer -> E Integer
> lg2Wrap :: Integer -> E Integer
lg2Wrap Integer
x = if Integer
x forall a. Ord a => a -> a -> Bool
< Integer
0 then forall a. EvalError -> E a
cryError EvalError
LogNegative else 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 Rational -> E Rational
qop (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v)
>   TVIntMod Integer
m  -> Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 (Integer -> Integer -> E Integer
zop Integer
m) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v)
>   TVFloat Integer
e Integer
p -> BF -> Value
VFloat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
fpToBF Integer
e Integer
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> E b) -> E a -> E b
appOp1 (Integer -> Integer -> BigFloat -> E BigFloat
flop Integer
e Integer
p) (Value -> BigFloat
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v)
>   TValue
_ -> forall a. String -> [String] -> a
evalPanic String
"fieldUnary" [forall a. Show a => a -> String
show TValue
ty 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                    forall a b c. (a -> b -> E c) -> E a -> E b -> E c
appOp2 Rational -> Rational -> E Rational
qop (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>   TVIntMod Integer
m  -> Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>   TVFloat Integer
e Integer
p -> BF -> Value
VFloat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
fpToBF Integer
e Integer
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                       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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) (Value -> BigFloat
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>   TValue
_ -> forall a. String -> [String] -> a
evalPanic String
"fieldBinary" [forall a. Show a => a -> String
show TValue
ty 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 = forall a. EvalError -> E a
cryError EvalError
DivideByZero
> ratDiv Rational
x Rational
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational
x forall a. Fractional a => a -> a -> a
/ Rational
y)
>
> ratRecip :: Rational -> E  Rational
> ratRecip :: Rational -> E Rational
ratRecip Rational
0 = forall a. EvalError -> E a
cryError EvalError
DivideByZero
> ratRecip Rational
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Fractional a => a -> a
recip Rational
x)
>
> zRecip :: Integer -> Integer -> E Integer
> zRecip :: Integer -> Integer -> E Integer
zRecip Integer
m Integer
x =
>   case Integer -> Integer -> Maybe Integer
Integer.integerRecipMod Integer
x Integer
m of
>     Just Integer
r  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
r
>     Maybe Integer
Nothing -> forall a. EvalError -> E a
cryError EvalError
DivideByZero
>
> zDiv :: Integer -> Integer -> Integer -> E Integer
> zDiv :: Integer -> Integer -> Integer -> E Integer
zDiv Integer
m Integer
x Integer
y = Integer -> Integer
f 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 forall a. Num a => a -> a -> a
* Integer
yinv) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Integer
op forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v
>   TVFloat {} -> Integer -> Value
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BF -> E Integer
flop forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> BF
fromVFloat' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
v)
>   TValue
_ -> forall a. String -> [String] -> a
evalPanic String
"roundUnary" [forall a. Show a => a -> String
show TValue
ty 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 forall a. Ord a => a -> a -> Bool
>= Rational
0    = forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
x forall a. Num a => a -> a -> a
+ Rational
0.5)
>   | Bool
otherwise = forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Rational
x 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 = forall a. EvalError -> E a
cryError EvalError
DivideByZero
> ratioOp Integer
x Integer
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Num a => Integer -> a
fromInteger Integer
x forall a. Fractional a => a -> a -> a
/ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordering -> Bool
p 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 ->
>       forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Bool
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> Bool
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>     TValue
TVInteger ->
>       forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>     TVIntMod Integer
_ ->
>       forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> Integer
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>     TValue
TVRational ->
>       forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> Rational
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>     TVFloat{} ->
>       forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> BigFloat
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> BigFloat
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r)
>     TVArray{} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexCompare" [String
"invalid type"]
>     TVSeq Integer
_w TValue
ety ->
>       [E Ordering] -> E Ordering
lexList forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Ordering
lexCompare TValue
ety) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                      (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r))
>     TVStream TValue
_ ->
>       forall a. String -> [String] -> a
evalPanic String
"lexCompare" [String
"invalid type"]
>     TVFun TValue
_ TValue
_ ->
>       forall a. String -> [String] -> a
evalPanic String
"lexCompare" [String
"invalid type"]
>     TVTuple [TValue]
etys ->
>       [E Ordering] -> E Ordering
lexList forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> E Value -> E Value -> E Ordering
lexCompare [TValue]
etys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                         (Value -> [E Value]
fromVTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> [E Value]
fromVTuple 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fields)
>          [E Value]
ls <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [(Ident, E Value)]
fromVRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l
>          [E Value]
rs <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [(Ident, E Value)]
fromVRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r
>          [E Ordering] -> E Ordering
lexList (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 {} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexCompare" [String
"Abstract type not in `Cmp`"]
>     TVNewtype {} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexCompare" [String
"Newtype not in `Cmp`"]
>
> lexList :: [E Ordering] -> E Ordering
> lexList :: [E Ordering] -> E Ordering
lexList [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Ordering
EQ
> lexList (E Ordering
e : [E Ordering]
es) =
>   E Ordering
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
>     Ordering
LT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Ordering
LT
>     Ordering
EQ -> [E Ordering] -> E Ordering
lexList [E Ordering]
es
>     Ordering
GT -> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
== Ordering
LT) 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 ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TValue
TVInteger ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVIntMod Integer
_ ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TValue
TVRational ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVFloat{} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVArray{} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVSeq Integer
_w TValue
ety
>       | TValue -> Bool
isTBit TValue
ety ->
>           forall a. Ord a => a -> a -> Ordering
compare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> E Integer
fromSignedVWord forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< E Value
r)
>       | Bool
otherwise ->
>           [E Ordering] -> E Ordering
lexList forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> E Value -> E Value -> E Ordering
lexSignedCompare TValue
ety) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                            (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r))
>     TVStream TValue
_ ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVFun TValue
_ TValue
_ ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"invalid type"]
>     TVTuple [TValue]
etys ->
>       [E Ordering] -> E Ordering
lexList forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> E Value -> E Value -> E Ordering
lexSignedCompare [TValue]
etys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
>                        (Value -> [E Value]
fromVTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Value -> [E Value]
fromVTuple 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    = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident TValue
fields)
>          [E Value]
ls <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [(Ident, E Value)]
fromVRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
l
>          [E Value]
rs <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [(Ident, E Value)]
fromVRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
r
>          [E Ordering] -> E Ordering
lexList (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 {} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"Abstract type not in `Cmp`"]
>     TVNewtype {} ->
>       forall a. String -> [String] -> a
evalPanic String
"lexSignedCompare" [String
"Newtype type not in `Cmp`"]


Sequences
---------

> generateV :: Nat' -> (Integer -> E Value) -> Value
> generateV :: Nat' -> (Integer -> E Value) -> Value
generateV Nat'
len Integer -> E Value
f = Nat' -> [E Value] -> Value
VList Nat'
len [ Integer -> E Value
f Integer
i | Integer
i <- [Integer]
idxs ]
>   where
>    idxs :: [Integer]
idxs = case Nat'
len of
>             Nat'
Inf   -> [ Integer
0 .. ]
>             Nat Integer
n -> [ Integer
0 .. Integer
nforall 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 forall a b. (a -> b) -> a -> b
$ \Nat'
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ix -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
x ->
>   do Integer
i <- TValue -> E Value -> E Integer
cryToInteger TValue
ix E Value
x
>      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Num a => a -> a -> a
+ Integer
amt)
>     Nat Integer
n -> Nat' -> (Integer -> E Value) -> Value
generateV (Integer -> Nat'
Nat Integer
n) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>                if Integer
i forall a. Num a => a -> a -> a
+ Integer
amt forall a. Ord a => a -> a -> Bool
< Integer
n then
>                  do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Num a => a -> a -> a
+ Integer
amt)
>                else
>                  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 forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>     if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
amt then
>       forall (f :: * -> *) a. Applicative f => a -> f a
pure (TValue -> Value
zero TValue
a)
>     else
>       do [E Value]
vs <- Value -> [E Value]
fromVList 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 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 forall a b. (a -> b) -> a -> b
$ \Integer
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ix -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun 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 =
>   forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Integer -> Nat'
Nat Integer
w) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>     do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Num a => a -> a -> a
+ Integer
amt) 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 =
>   forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV (Integer -> Nat'
Nat Integer
w) forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>     do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Num a => a -> a -> a
- Integer
amt) forall a. Integral a => a -> a -> a
`mod` Integer
w)
>
> signedShiftRV :: Value
> signedShiftRV :: Value
signedShiftRV =
>   (Nat' -> E Value) -> Value
VNumPoly forall a b. (a -> b) -> a -> b
$ \Nat'
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ix -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
x ->
>   do Integer
amt <- TValue -> E Value -> E Integer
cryToInteger TValue
ix E Value
x
>      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
n forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>        do [E Value]
vs <- Value -> [E Value]
fromVList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E Value
v
>           if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
amt then
>             Nat' -> [E Value] -> Integer -> E Value
indexFront Nat'
n [E Value]
vs Integer
0
>           else
>             Nat' -> [E Value] -> Integer -> E Value
indexFront Nat'
n [E Value]
vs (Integer
i 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 forall a b. (a -> b) -> a -> b
$ \Nat'
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ix -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
r ->
>   do [E Value]
vs <- Value -> [E Value]
fromVList 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 forall a. Ord a => a -> a -> Bool
<= Integer
ix Bool -> Bool -> Bool
&& Integer
ix forall a. Ord a => a -> a -> Bool
< Integer
n -> forall i a. Integral i => [a] -> i -> a
genericIndex [E Value]
vs Integer
ix
>     Nat'
Inf   | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
ix -> forall i a. Integral i => [a] -> i -> a
genericIndex [E Value]
vs Integer
ix
>     Nat'
_ -> forall a. EvalError -> E a
cryError (Maybe Integer -> EvalError
InvalidIndex (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 forall a. Ord a => a -> a -> Bool
<= Integer
ix Bool -> Bool -> Bool
&& Integer
ix forall a. Ord a => a -> a -> Bool
< Integer
n -> forall i a. Integral i => [a] -> i -> a
genericIndex [E Value]
vs (Integer
n forall a. Num a => a -> a -> a
- Integer
ix forall a. Num a => a -> a -> a
- Integer
1)
>           | Bool
otherwise -> forall a. EvalError -> E a
cryError (Maybe Integer -> EvalError
InvalidIndex (forall a. a -> Maybe a
Just Integer
ix))
>     Nat'
Inf               -> 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 forall a b. (a -> b) -> a -> b
$ \Nat'
len -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
_eltTy -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (TValue -> E Value) -> Value
VPoly forall a b. (a -> b) -> a -> b
$ \TValue
ix -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun forall a b. (a -> b) -> a -> b
$ \E Value
idx -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
>   (E Value -> E Value) -> Value
VFun 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 forall a. Ord a => a -> a -> Bool
< Nat'
len then
>        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Nat' -> (Integer -> E Value) -> Value
generateV Nat'
len forall a b. (a -> b) -> a -> b
$ \Integer
i ->
>          if Integer
i 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 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
>        forall a. EvalError -> E a
cryError (Maybe Integer -> EvalError
InvalidIndex (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 = forall a. String -> [String] -> a
evalPanic String
"Unexpected infinite sequence in updateEnd" []
> updateBack (Nat Integer
n) Integer
j = Integer
n forall a. Num a => a -> a -> a
- Integer
j forall a. Num a => a -> a -> a
- Integer
1

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

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

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

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

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


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

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


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

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

> evalPanic :: String -> [String] -> a
> evalPanic :: forall a. String -> [String] -> a
evalPanic String
cxt = forall a. HasCallStack => String -> [String] -> a
panic (String
"[Reference Evaluator]" 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 (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 (forall a. Show a => a -> String
show Bool
b)
>     VInteger Integer
i -> String -> Doc
text (forall a. Show a => a -> String
show Integer
i)
>     VRational Rational
q -> String -> Doc
text (forall a. Show a => a -> String
show Rational
q)
>     VFloat BF
fl -> String -> Doc
text (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 (forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> E Value -> Doc
ppEValue PPOpts
opts)
>                   (forall a. Int -> [a] -> [a]
take (PPOpts -> Int
useInfLength PPOpts
opts) [E Value]
vs) forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"..."])
>         Nat Integer
n ->
>           -- For lists of defined bits, print the value as a numeral.
>           case 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 (forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> E Value -> Doc
ppEValue PPOpts
opts) [E Value]
vs)
>       where isBit :: E Value -> Maybe Bool
isBit E Value
v = case E Value
v of Value (VBit Bool
b) -> forall a. a -> Maybe a
Just Bool
b
>                                 E Value
_      -> forall a. Maybe a
Nothing
>     VTuple [E Value]
vs  -> [Doc] -> Doc
ppTuple (forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> E Value -> Doc
ppEValue PPOpts
opts) [E Value]
vs)
>     VRecord [(Ident, E Value)]
fs -> [Doc] -> Doc
ppRecord (forall a b. (a -> b) -> [a] -> [b]
map 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) = forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> PPOpts -> E Value -> Doc
ppEValue PPOpts
opts E Value
r
>     VFun E Value -> E Value
_     -> String -> Doc
text String
"<function>"
>     VPoly TValue -> E Value
_    -> String -> Doc
text String
"<polymorphic value>"
>     VNumPoly Nat' -> E Value
_ -> String -> Doc
text String
"<polymorphic value>"

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

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

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