>
>
>
>
>
>
>
>
>
> {-# LANGUAGE PatternGuards #-}
>
> module Cryptol.Eval.Reference
> ( Value(..)
> , evaluate
> , ppValue
> ) where
>
> import Control.Applicative (liftA2)
> import Data.Bits
> import Data.List
> (genericDrop, genericIndex, genericLength, genericReplicate, genericSplitAt,
> genericTake, sortBy)
> import Data.Ord (comparing)
> import Data.Map (Map)
> import qualified Data.Map as Map
> import Data.Semigroup (Semigroup(..))
> import qualified Data.Text as T (pack)
>
> import Cryptol.ModuleSystem.Name (asPrim)
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
> import Cryptol.TypeCheck.AST
> import Cryptol.Eval.Monad (EvalError(..), PPOpts(..))
> import Cryptol.Eval.Type (TValue(..), isTBit, evalValType, evalNumType, tvSeq)
> import Cryptol.Eval.Value (mkBv, ppBV)
> import Cryptol.Prims.Eval (lg2)
> import Cryptol.Utils.Ident (Ident, mkIdent)
> import Cryptol.Utils.Panic (panic)
> import Cryptol.Utils.PP
>
> import qualified Cryptol.ModuleSystem as M
> import qualified Cryptol.ModuleSystem.Env as M (loadedModules)
Overview
========
This file describes the semantics of the explicitly-typed Cryptol
language (i.e., terms after type checking). Issues related to type
inference, type functions, and type constraints are beyond the scope
of this document.
Cryptol Types
Cryptol types come in two kinds: numeric types (kind `#`) and value
types (kind `*`). While value types are inhabited by well-typed
Cryptol expressions, numeric types are only used as parameters to
other types; they have no inhabitants. In this implementation we
represent numeric types as values of the Haskell type `Nat'` of
natural numbers with infinity; value types are represented as values
of type `TValue`.
The value types of Cryptol, along with their Haskell representations,
are as follows:
| Cryptol type | Description | `TValue` representation |
|:----------------- |:-------------- |:--------------------------- |
| `Bit` | booleans | `TVBit` |
| `Integer` | integers | `TVInteger` |
| `[n]a` | finite lists | `TVSeq n a` |
| `[inf]a` | infinite lists | `TVStream a` |
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
| `{x:a, y:b, z:c}` | records | `TVRec [(x,a),(y,b),(z,c)]` |
| `a -> b` | functions | `TVFun a b` |
We model each Cryptol value type `t` as a complete partial order (cpo)
*M*(`t`). To each Cryptol expression `e : t` we assign a meaning
*M*(`e`) in *M*(`t`); in particular, recursive Cryptol programs of
type `t` are modeled as least fixed points in *M*(`t`). In other words,
this is a domain-theoretic denotational semantics.
Evaluating a Cryptol expression of type `Bit` may result in:
- a defined value `True` or `False`
- a run-time error, or
- non-termination.
Accordingly, *M*(`Bit`) is a flat cpo with values for `True`,
`False`, run-time errors of type `EvalError`, and $\bot$; we
represent it with the Haskell type `Either EvalError Bool`.
Similarly, *M*(`Integer`) is a flat cpo with values for integers,
run-time errors, and $\bot$; we represent it with the Haskell type
`Either EvalError Integer`.
The cpos for lists, tuples, and records are cartesian products. The
cpo ordering is pointwise, and the bottom element $\bot$ is the
list/tuple/record whose elements are all $\bot$. Trivial types `[0]t`,
`()` and `{}` denote single-element cpos where the unique value
`[]`/`()`/`{}` *is* the bottom element $\bot$. *M*(`a -> b`) is the
continuous function space *M*(`a`) $\to$ *M*(`b`).
Type schemas of the form `{a1 ... an} (p1 ... pk) => t` classify
polymorphic values in Cryptol. These are represented with the Haskell
type `Schema`. The meaning of a schema is cpo whose elements are
functions: For each valid instantiation `t1 ... tn` of the type
parameters `a1 ... an` that satisfies the constraints `p1 ... pk`, the
function returns a value in *M*(`t[t1/a1 ... tn/an]`).
Values
The Haskell code in this module defines the semantics of typed Cryptol
terms by providing an evaluator to an appropriate `Value` type.
>
> data Value
> = VBit (Either EvalError Bool)
> | VInteger (Either EvalError Integer)
> | VList Nat' [Value]
> | VTuple [Value]
> | VRecord [(Ident, Value)]
> | VFun (Value -> Value)
> | VPoly (TValue -> Value)
> | VNumPoly (Nat' -> Value)
Invariant: Undefinedness and run-time exceptions are only allowed
inside the argument of a `VBit` or `VInteger` constructor. All other
`Value` and list constructors should evaluate without error. For
example, a non-terminating computation at type `(Bit,Bit)` must be
represented as `VTuple [VBit undefined, VBit undefined]`, and not
simply as `undefined`. Similarly, an expression like `1/0:[2]` that
raises a run-time error must be encoded as `VList (Nat 2) [VBit (Left
e), VBit (Left e)]` where `e = DivideByZero`.
Copy Functions
Functions `copyBySchema` and `copyByTValue` make a copy of the given
value, building the spine based only on the type without forcing the
value argument. This ensures that undefinedness appears inside `VBit`
and `VInteger` values only, and never on any constructors of the
`Value` type. In turn, this gives the appropriate semantics to
recursive definitions: The bottom value for a compound type is equal
to a value of the same type where every individual bit is bottom.
For each Cryptol type `t`, the cpo *M*(`t`) can be represented as a
subset of values of type `Value` that satisfy the datatype invariant.
This subset consists precisely of the output range of `copyByTValue
t`. Similarly, the range of output values of `copyBySchema` yields the
cpo that represents any given schema.
> copyBySchema :: Env -> Schema -> Value -> Value
> copyBySchema :: Env -> Schema -> Value -> Value
copyBySchema env0 :: Env
env0 (Forall params :: [TParam]
params _props :: [Prop]
_props ty :: Prop
ty) = [TParam] -> Env -> Value -> Value
go [TParam]
params Env
env0
> where
> go :: [TParam] -> Env -> Value -> Value
> go :: [TParam] -> Env -> Value -> Value
go [] env :: Env
env v :: Value
v = TValue -> Value -> Value
copyByTValue (HasCallStack => TypeEnv -> Prop -> TValue
TypeEnv -> Prop -> TValue
evalValType (Env -> TypeEnv
envTypes Env
env) Prop
ty) Value
v
> go (p :: TParam
p : ps :: [TParam]
ps) env :: Env
env v :: Value
v =
> case Value
v of
> VPoly f :: TValue -> Value
f -> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \t :: TValue
t -> [TParam] -> Env -> Value -> Value
go [TParam]
ps (TVar -> Either Nat' TValue -> Env -> Env
bindType (TParam -> TVar
tpVar TParam
p) (TValue -> Either Nat' TValue
forall a b. b -> Either a b
Right TValue
t) Env
env) (TValue -> Value
f TValue
t)
> VNumPoly f :: Nat' -> Value
f -> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n -> [TParam] -> Env -> Value -> Value
go [TParam]
ps (TVar -> Either Nat' TValue -> Env -> Env
bindType (TParam -> TVar
tpVar TParam
p) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) Env
env) (Nat' -> Value
f Nat'
n)
> _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "copyBySchema" ["Expected polymorphic value"]
>
> copyByTValue :: TValue -> Value -> Value
> copyByTValue :: TValue -> Value -> Value
copyByTValue = TValue -> Value -> Value
go
> where
> go :: TValue -> Value -> Value
> go :: TValue -> Value -> Value
go ty :: TValue
ty val :: Value
val =
> case TValue
ty of
> TVBit -> Either EvalError Bool -> Value
VBit (Value -> Either EvalError Bool
fromVBit Value
val)
> TVInteger -> Either EvalError Integer -> Value
VInteger (Value -> Either EvalError Integer
fromVInteger Value
val)
> TVIntMod _ -> Either EvalError Integer -> Value
VInteger (Value -> Either EvalError Integer
fromVInteger Value
val)
> TVSeq w :: Integer
w ety :: TValue
ety -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
ety) (Integer -> [Value] -> [Value]
forall a. Integer -> [a] -> [a]
copyList Integer
w (Value -> [Value]
fromVList Value
val)))
> TVStream ety :: TValue
ety -> Nat' -> [Value] -> Value
VList Nat'
Inf ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
ety) ([Value] -> [Value]
forall a. [a] -> [a]
copyStream (Value -> [Value]
fromVList Value
val)))
> TVTuple etys :: [TValue]
etys -> [Value] -> Value
VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> Value -> Value
go [TValue]
etys (Integer -> [Value] -> [Value]
forall a. Integer -> [a] -> [a]
copyList ([TValue] -> Integer
forall i a. Num i => [a] -> i
genericLength [TValue]
etys) (Value -> [Value]
fromVTuple Value
val)))
> TVRec fields :: [(Ident, TValue)]
fields -> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value -> Value
go TValue
fty (Ident -> Value -> Value
lookupRecord Ident
f Value
val)) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fields ]
> TVFun _ bty :: TValue
bty -> (Value -> Value) -> Value
VFun (\v :: Value
v -> TValue -> Value -> Value
go TValue
bty (Value -> Value -> Value
fromVFun Value
val Value
v))
> TVAbstract {} -> Value
val
>
> copyStream :: [a] -> [a]
> copyStream :: [a] -> [a]
copyStream xs :: [a]
xs = [a] -> a
forall a. [a] -> a
head [a]
xs a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
forall a. [a] -> [a]
copyStream ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)
>
> copyList :: Integer -> [a] -> [a]
> copyList :: Integer -> [a] -> [a]
copyList 0 _ = []
> copyList n :: Integer
n xs :: [a]
xs = [a] -> a
forall a. [a] -> a
head [a]
xs a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Integer -> [a] -> [a]
forall a. Integer -> [a] -> [a]
copyList (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs)
Operations on Values
>
> fromVBit :: Value -> Either EvalError Bool
> fromVBit :: Value -> Either EvalError Bool
fromVBit (VBit b :: Either EvalError Bool
b) = Either EvalError Bool
b
> fromVBit _ = String -> [String] -> Either EvalError Bool
forall a. String -> [String] -> a
evalPanic "fromVBit" ["Expected a bit"]
>
>
> fromVInteger :: Value -> Either EvalError Integer
> fromVInteger :: Value -> Either EvalError Integer
fromVInteger (VInteger i :: Either EvalError Integer
i) = Either EvalError Integer
i
> fromVInteger _ = String -> [String] -> Either EvalError Integer
forall a. String -> [String] -> a
evalPanic "fromVInteger" ["Expected an integer"]
>
>
> fromVList :: Value -> [Value]
> fromVList :: Value -> [Value]
fromVList (VList _ vs :: [Value]
vs) = [Value]
vs
> fromVList _ = String -> [String] -> [Value]
forall a. String -> [String] -> a
evalPanic "fromVList" ["Expected a list"]
>
>
> fromVTuple :: Value -> [Value]
> fromVTuple :: Value -> [Value]
fromVTuple (VTuple vs :: [Value]
vs) = [Value]
vs
> fromVTuple _ = String -> [String] -> [Value]
forall a. String -> [String] -> a
evalPanic "fromVTuple" ["Expected a tuple"]
>
>
> fromVRecord :: Value -> [(Ident, Value)]
> fromVRecord :: Value -> [(Ident, Value)]
fromVRecord (VRecord fs :: [(Ident, Value)]
fs) = [(Ident, Value)]
fs
> fromVRecord _ = String -> [String] -> [(Ident, Value)]
forall a. String -> [String] -> a
evalPanic "fromVRecord" ["Expected a record"]
>
>
> fromVFun :: Value -> (Value -> Value)
> fromVFun :: Value -> Value -> Value
fromVFun (VFun f :: Value -> Value
f) = Value -> Value
f
> fromVFun _ = String -> [String] -> Value -> Value
forall a. String -> [String] -> a
evalPanic "fromVFun" ["Expected a function"]
>
>
> fromVPoly :: Value -> (TValue -> Value)
> fromVPoly :: Value -> TValue -> Value
fromVPoly (VPoly f :: TValue -> Value
f) = TValue -> Value
f
> fromVPoly _ = String -> [String] -> TValue -> Value
forall a. String -> [String] -> a
evalPanic "fromVPoly" ["Expected a polymorphic value"]
>
>
> fromVNumPoly :: Value -> (Nat' -> Value)
> fromVNumPoly :: Value -> Nat' -> Value
fromVNumPoly (VNumPoly f :: Nat' -> Value
f) = Nat' -> Value
f
> fromVNumPoly _ = String -> [String] -> Nat' -> Value
forall a. String -> [String] -> a
evalPanic "fromVNumPoly" ["Expected a polymorphic value"]
>
>
> lookupRecord :: Ident -> Value -> Value
> lookupRecord :: Ident -> Value -> Value
lookupRecord f :: Ident
f v :: Value
v =
> case Ident -> [(Ident, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f (Value -> [(Ident, Value)]
fromVRecord Value
v) of
> Just val :: Value
val -> Value
val
> Nothing -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "lookupRecord" ["Malformed record"]
>
>
> vFinPoly :: (Integer -> Value) -> Value
> vFinPoly :: (Integer -> Value) -> Value
vFinPoly f :: Integer -> Value
f = (Nat' -> Value) -> Value
VNumPoly Nat' -> Value
g
> where
> g :: Nat' -> Value
g (Nat n :: Integer
n) = Integer -> Value
f Integer
n
> g Inf = String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "vFinPoly" ["Expected finite numeric type"]
Environments
An evaluation environment keeps track of the values of term variables
and type variables that are in scope at any point.
> data Env = Env
> { Env -> Map Name Value
envVars :: !(Map Name Value)
> , Env -> TypeEnv
envTypes :: !(Map TVar (Either Nat' TValue))
> }
>
> instance Semigroup Env where
> l :: Env
l <> :: Env -> Env -> Env
<> r :: Env
r = $WEnv :: Map Name Value -> TypeEnv -> Env
Env
> { envVars :: Map Name Value
envVars = Map Name Value -> Map Name Value -> Map Name Value
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Env -> Map Name Value
envVars Env
l) (Env -> Map Name Value
envVars Env
r)
> , envTypes :: TypeEnv
envTypes = TypeEnv -> TypeEnv -> TypeEnv
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Env -> TypeEnv
envTypes Env
l) (Env -> TypeEnv
envTypes Env
r)
> }
>
> instance Monoid Env where
> mempty :: Env
mempty = $WEnv :: Map Name Value -> TypeEnv -> Env
Env
> { envVars :: Map Name Value
envVars = Map Name Value
forall k a. Map k a
Map.empty
> , envTypes :: TypeEnv
envTypes = TypeEnv
forall k a. Map k a
Map.empty
> }
> mappend :: Env -> Env -> Env
mappend l :: Env
l r :: Env
r = Env
l Env -> Env -> Env
forall a. Semigroup a => a -> a -> a
<> Env
r
>
>
> bindVar :: (Name, Value) -> Env -> Env
> bindVar :: (Name, Value) -> Env -> Env
bindVar (n :: Name
n, val :: Value
val) env :: Env
env = Env
env { envVars :: Map Name Value
envVars = Name -> Value -> Map Name Value -> Map Name Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n Value
val (Env -> Map Name Value
envVars Env
env) }
>
>
> bindType :: TVar -> Either Nat' TValue -> Env -> Env
> bindType :: TVar -> Either Nat' TValue -> Env -> Env
bindType p :: TVar
p ty :: Either Nat' TValue
ty env :: Env
env = Env
env { envTypes :: TypeEnv
envTypes = TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
p Either Nat' TValue
ty (Env -> TypeEnv
envTypes Env
env) }
Evaluation
==========
The meaning *M*(`expr`) of a Cryptol expression `expr` is defined by
recursion over its structure. For an expression that contains free
variables, the meaning also depends on the environment `env`, which
assigns values to those variables.
> evalExpr :: Env
> -> Expr
> -> Value
> evalExpr :: Env -> Expr -> Value
evalExpr env :: Env
env expr :: Expr
expr =
> case Expr
expr of
>
> EList es :: [Expr]
es _ty :: Prop
_ty -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat ([Expr] -> Integer
forall i a. Num i => [a] -> i
genericLength [Expr]
es)) [ Env -> Expr -> Value
evalExpr Env
env Expr
e | Expr
e <- [Expr]
es ]
> ETuple es :: [Expr]
es -> [Value] -> Value
VTuple [ Env -> Expr -> Value
evalExpr Env
env Expr
e | Expr
e <- [Expr]
es ]
> ERec fields :: [(Ident, Expr)]
fields -> [(Ident, Value)] -> Value
VRecord [ (Ident
f, Env -> Expr -> Value
evalExpr Env
env Expr
e) | (f :: Ident
f, e :: Expr
e) <- [(Ident, Expr)]
fields ]
> ESel e :: Expr
e sel :: Selector
sel -> Value -> Selector -> Value
evalSel (Env -> Expr -> Value
evalExpr Env
env Expr
e) Selector
sel
> ESet e :: Expr
e sel :: Selector
sel v :: Expr
v -> Value -> Selector -> Value -> Value
evalSet (Env -> Expr -> Value
evalExpr Env
env Expr
e) Selector
sel (Env -> Expr -> Value
evalExpr Env
env Expr
v)
>
> EIf c :: Expr
c t :: Expr
t f :: Expr
f ->
> Either EvalError Bool -> Value -> Value -> Value
condValue (Value -> Either EvalError Bool
fromVBit (Env -> Expr -> Value
evalExpr Env
env Expr
c)) (Env -> Expr -> Value
evalExpr Env
env Expr
t) (Env -> Expr -> Value
evalExpr Env
env Expr
f)
>
> EComp _n :: Prop
_n _ty :: Prop
_ty e :: Expr
e branches :: [[Match]]
branches ->
> Env -> Expr -> [[Match]] -> Value
evalComp Env
env Expr
e [[Match]]
branches
>
> EVar n :: Name
n ->
> case Name -> Map Name Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n (Env -> Map Name Value
envVars Env
env) of
> Just val :: Value
val -> Value
val
> Nothing -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalExpr" ["var `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "` is not defined" ]
>
> ETAbs tv :: TParam
tv b :: Expr
b ->
> case TParam -> Kind
tpKind TParam
tv of
> KType -> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty -> Env -> Expr -> Value
evalExpr (TVar -> Either Nat' TValue -> Env -> Env
bindType (TParam -> TVar
tpVar TParam
tv) (TValue -> Either Nat' TValue
forall a b. b -> Either a b
Right TValue
ty) Env
env) Expr
b
> KNum -> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n -> Env -> Expr -> Value
evalExpr (TVar -> Either Nat' TValue -> Env -> Env
bindType (TParam -> TVar
tpVar TParam
tv) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) Env
env) Expr
b
> k :: Kind
k -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalExpr" ["Invalid kind on type abstraction", Kind -> String
forall a. Show a => a -> String
show Kind
k]
>
> ETApp e :: Expr
e ty :: Prop
ty ->
> case Env -> Expr -> Value
evalExpr Env
env Expr
e of
> VPoly f :: TValue -> Value
f -> TValue -> Value
f (TValue -> Value) -> TValue -> Value
forall a b. (a -> b) -> a -> b
$! (HasCallStack => TypeEnv -> Prop -> TValue
TypeEnv -> Prop -> TValue
evalValType (Env -> TypeEnv
envTypes Env
env) Prop
ty)
> VNumPoly f :: Nat' -> Value
f -> Nat' -> Value
f (Nat' -> Value) -> Nat' -> Value
forall a b. (a -> b) -> a -> b
$! (HasCallStack => TypeEnv -> Prop -> Nat'
TypeEnv -> Prop -> Nat'
evalNumType (Env -> TypeEnv
envTypes Env
env) Prop
ty)
> _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalExpr" ["Expected a polymorphic value"]
>
> EApp e1 :: Expr
e1 e2 :: Expr
e2 -> Value -> Value -> Value
fromVFun (Env -> Expr -> Value
evalExpr Env
env Expr
e1) (Env -> Expr -> Value
evalExpr Env
env Expr
e2)
> EAbs n :: Name
n _ty :: Prop
_ty b :: Expr
b -> (Value -> Value) -> Value
VFun (\v :: Value
v -> Env -> Expr -> Value
evalExpr ((Name, Value) -> Env -> Env
bindVar (Name
n, Value
v) Env
env) Expr
b)
> EProofAbs _ e :: Expr
e -> Env -> Expr -> Value
evalExpr Env
env Expr
e
> EProofApp e :: Expr
e -> Env -> Expr -> Value
evalExpr Env
env Expr
e
> EWhere e :: Expr
e dgs :: [DeclGroup]
dgs -> Env -> Expr -> Value
evalExpr ((Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Env -> DeclGroup -> Env
evalDeclGroup Env
env [DeclGroup]
dgs) Expr
e
Selectors
Apply the the given selector form to the given value.
> evalSel :: Value -> Selector -> Value
> evalSel :: Value -> Selector -> Value
evalSel val :: Value
val sel :: Selector
sel =
> case Selector
sel of
> TupleSel n :: Int
n _ -> Int -> Value -> Value
tupleSel Int
n Value
val
> RecordSel n :: Ident
n _ -> Ident -> Value -> Value
recordSel Ident
n Value
val
> ListSel n :: Int
n _ -> Int -> Value -> Value
listSel Int
n Value
val
> where
> tupleSel :: Int -> Value -> Value
tupleSel n :: Int
n v :: Value
v =
> case Value
v of
> VTuple vs :: [Value]
vs -> [Value]
vs [Value] -> Int -> Value
forall a. [a] -> Int -> a
!! Int
n
> _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalSel"
> ["Unexpected value in tuple selection."]
> recordSel :: Ident -> Value -> Value
recordSel n :: Ident
n v :: Value
v =
> case Value
v of
> VRecord _ -> Ident -> Value -> Value
lookupRecord Ident
n Value
v
> _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalSel"
> ["Unexpected value in record selection."]
> listSel :: Int -> Value -> Value
listSel n :: Int
n v :: Value
v =
> case Value
v of
> VList _ vs :: [Value]
vs -> [Value]
vs [Value] -> Int -> Value
forall a. [a] -> Int -> a
!! Int
n
> _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalSel"
> ["Unexpected value in list selection."]
Update the given value using the given selector and new value.
> evalSet :: Value -> Selector -> Value -> Value
> evalSet :: Value -> Selector -> Value -> Value
evalSet val :: Value
val sel :: Selector
sel fval :: Value
fval =
> case Selector
sel of
> TupleSel n :: Int
n _ -> Int -> Value
updTupleAt Int
n
> RecordSel n :: Ident
n _ -> Ident -> Value
updRecAt Ident
n
> ListSel n :: Int
n _ -> Int -> Value
updSeqAt Int
n
> where
> updTupleAt :: Int -> Value
updTupleAt n :: Int
n =
> case Value
val of
> VTuple vs :: [Value]
vs | (as :: [Value]
as,_:bs :: [Value]
bs) <- Int -> [Value] -> ([Value], [Value])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Value]
vs ->
> [Value] -> Value
VTuple ([Value]
as [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Value
fval Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
bs)
> _ -> String -> Value
forall a. String -> a
bad "Invalid tuple upldate."
>
> updRecAt :: Ident -> Value
updRecAt n :: Ident
n =
> case Value
val of
> VRecord vs :: [(Ident, Value)]
vs | (as :: [(Ident, Value)]
as, (i :: Ident
i,_) : bs :: [(Ident, Value)]
bs) <- ((Ident, Value) -> Bool)
-> [(Ident, Value)] -> ([(Ident, Value)], [(Ident, Value)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ((Ident
nIdent -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
==) (Ident -> Bool)
-> ((Ident, Value) -> Ident) -> (Ident, Value) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst) [(Ident, Value)]
vs ->
> [(Ident, Value)] -> Value
VRecord ([(Ident, Value)]
as [(Ident, Value)] -> [(Ident, Value)] -> [(Ident, Value)]
forall a. [a] -> [a] -> [a]
++ (Ident
i,Value
fval) (Ident, Value) -> [(Ident, Value)] -> [(Ident, Value)]
forall a. a -> [a] -> [a]
: [(Ident, Value)]
bs)
> _ -> String -> Value
forall a. String -> a
bad "Invalid record update."
>
> updSeqAt :: Int -> Value
updSeqAt n :: Int
n =
> case Value
val of
> VList i :: Nat'
i vs :: [Value]
vs | (as :: [Value]
as, _ : bs :: [Value]
bs) <- Int -> [Value] -> ([Value], [Value])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Value]
vs ->
> Nat' -> [Value] -> Value
VList Nat'
i ([Value]
as [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Value
fval Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
bs)
> _ -> String -> Value
forall a. String -> a
bad "Invalid sequence update."
>
> bad :: String -> a
bad msg :: String
msg = String -> [String] -> a
forall a. String -> [String] -> a
evalPanic "evalSet" [String
msg]
Conditionals
We evaluate conditionals on larger types by pushing the conditionals
down to the individual bits.
> condValue :: Either EvalError Bool -> Value -> Value -> Value
> condValue :: Either EvalError Bool -> Value -> Value -> Value
condValue c :: Either EvalError Bool
c l :: Value
l r :: Value
r =
> case Value
l of
> VBit b :: Either EvalError Bool
b -> Either EvalError Bool -> Value
VBit (Either EvalError Bool
-> Either EvalError Bool
-> Either EvalError Bool
-> Either EvalError Bool
forall e a. Either e Bool -> Either e a -> Either e a -> Either e a
condBit Either EvalError Bool
c Either EvalError Bool
b (Value -> Either EvalError Bool
fromVBit Value
r))
> VInteger i :: Either EvalError Integer
i -> Either EvalError Integer -> Value
VInteger (Either EvalError Bool
-> Either EvalError Integer
-> Either EvalError Integer
-> Either EvalError Integer
forall e a. Either e Bool -> Either e a -> Either e a -> Either e a
condBit Either EvalError Bool
c Either EvalError Integer
i (Value -> Either EvalError Integer
fromVInteger Value
r))
> VList n :: Nat'
n vs :: [Value]
vs -> Nat' -> [Value] -> Value
VList Nat'
n ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c) [Value]
vs (Value -> [Value]
fromVList Value
r))
> VTuple vs :: [Value]
vs -> [Value] -> Value
VTuple ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c) [Value]
vs (Value -> [Value]
fromVTuple Value
r))
> VRecord fs :: [(Ident, Value)]
fs -> [(Ident, Value)] -> Value
VRecord [ (Ident
f, Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c Value
v (Ident -> Value -> Value
lookupRecord Ident
f Value
r)) | (f :: Ident
f, v :: Value
v) <- [(Ident, Value)]
fs ]
> VFun f :: Value -> Value
f -> (Value -> Value) -> Value
VFun (\v :: Value
v -> Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c (Value -> Value
f Value
v) (Value -> Value -> Value
fromVFun Value
r Value
v))
> VPoly f :: TValue -> Value
f -> (TValue -> Value) -> Value
VPoly (\t :: TValue
t -> Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c (TValue -> Value
f TValue
t) (Value -> TValue -> Value
fromVPoly Value
r TValue
t))
> VNumPoly f :: Nat' -> Value
f -> (Nat' -> Value) -> Value
VNumPoly (\n :: Nat'
n -> Either EvalError Bool -> Value -> Value -> Value
condValue Either EvalError Bool
c (Nat' -> Value
f Nat'
n) (Value -> Nat' -> Value
fromVNumPoly Value
r Nat'
n))
Conditionals are explicitly lazy: Run-time errors in an untaken branch
are ignored.
> condBit :: Either e Bool -> Either e a -> Either e a -> Either e a
> condBit :: Either e Bool -> Either e a -> Either e a -> Either e a
condBit (Left e :: e
e) _ _ = e -> Either e a
forall a b. a -> Either a b
Left e
e
> condBit (Right b :: Bool
b) x :: Either e a
x y :: Either e a
y = if Bool
b then Either e a
x else Either e a
y
List Comprehensions
Cryptol list comprehensions consist of one or more parallel branches;
each branch has one or more matches that bind values to variables.
The result of evaluating a match in an initial environment is a list
of extended environments. Each new environment binds the same single
variable to a different element of the match's list.
> evalMatch :: Env -> Match -> [Env]
> evalMatch :: Env -> Match -> [Env]
evalMatch env :: Env
env m :: Match
m =
> case Match
m of
> Let d :: Decl
d ->
> [ (Name, Value) -> Env -> Env
bindVar (Env -> Decl -> (Name, Value)
evalDecl Env
env Decl
d) Env
env ]
> From n :: Name
n _l :: Prop
_l _ty :: Prop
_ty expr :: Expr
expr ->
> [ (Name, Value) -> Env -> Env
bindVar (Name
n, Value
v) Env
env | Value
v <- Value -> [Value]
fromVList (Env -> Expr -> Value
evalExpr Env
env Expr
expr) ]
> lenMatch :: Env -> Match -> Nat'
> lenMatch :: Env -> Match -> Nat'
lenMatch env :: Env
env m :: Match
m =
> case Match
m of
> Let _ -> Integer -> Nat'
Nat 1
> From _ len :: Prop
len _ _ -> HasCallStack => TypeEnv -> Prop -> Nat'
TypeEnv -> Prop -> Nat'
evalNumType (Env -> TypeEnv
envTypes Env
env) Prop
len
The result of of evaluating a branch in an initial environment is a
list of extended environments, each of which extends the initial
environment with the same set of new variables. The length of the list
is equal to the product of the lengths of the lists in the matches.
> evalBranch :: Env -> [Match] -> [Env]
> evalBranch :: Env -> [Match] -> [Env]
evalBranch env :: Env
env [] = [Env
env]
> evalBranch env :: Env
env (match :: Match
match : matches :: [Match]
matches) =
> [ Env
env'' | Env
env' <- Env -> Match -> [Env]
evalMatch Env
env Match
match
> , Env
env'' <- Env -> [Match] -> [Env]
evalBranch Env
env' [Match]
matches ]
> lenBranch :: Env -> [Match] -> Nat'
> lenBranch :: Env -> [Match] -> Nat'
lenBranch _env :: Env
_env [] = Integer -> Nat'
Nat 1
> lenBranch env :: Env
env (match :: Match
match : matches :: [Match]
matches) =
> Nat' -> Nat' -> Nat'
nMul (Env -> Match -> Nat'
lenMatch Env
env Match
match) (Env -> [Match] -> Nat'
lenBranch Env
env [Match]
matches)
The head expression of the comprehension can refer to any variable
bound in any of the parallel branches. So to evaluate the
comprehension, we zip and merge together the lists of extended
environments from each branch. The head expression is then evaluated
separately in each merged environment. The length of the resulting
list is equal to the minimum length over all parallel branches.
> evalComp :: Env
> -> Expr
> -> [[Match]]
> -> Value
> evalComp :: Env -> Expr -> [[Match]] -> Value
evalComp env :: Env
env expr :: Expr
expr branches :: [[Match]]
branches = Nat' -> [Value] -> Value
VList Nat'
len [ Env -> Expr -> Value
evalExpr Env
e Expr
expr | Env
e <- [Env]
envs ]
> where
>
>
> benvs :: [[Env]]
> benvs :: [[Env]]
benvs = ([Match] -> [Env]) -> [[Match]] -> [[Env]]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [Match] -> [Env]
evalBranch Env
env) [[Match]]
branches
>
>
>
>
> envs :: [Env]
> envs :: [Env]
envs = ([Env] -> [Env] -> [Env]) -> [[Env]] -> [Env]
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((Env -> Env -> Env) -> [Env] -> [Env] -> [Env]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Env -> Env -> Env
forall a. Monoid a => a -> a -> a
mappend) [[Env]]
benvs
>
> len :: Nat'
> len :: Nat'
len = (Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Nat' -> Nat' -> Nat'
nMin (([Match] -> Nat') -> [[Match]] -> [Nat']
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [Match] -> Nat'
lenBranch Env
env) [[Match]]
branches)
Declarations
Function `evalDeclGroup` extends the given evaluation environment with
the result of evaluating the given declaration group. In the case of a
recursive declaration group, we tie the recursive knot by evaluating
each declaration in the extended environment `env'` that includes all
the new bindings.
> evalDeclGroup :: Env -> DeclGroup -> Env
> evalDeclGroup :: Env -> DeclGroup -> Env
evalDeclGroup env :: Env
env dg :: DeclGroup
dg = do
> case DeclGroup
dg of
> NonRecursive d :: Decl
d ->
> (Name, Value) -> Env -> Env
bindVar (Env -> Decl -> (Name, Value)
evalDecl Env
env Decl
d) Env
env
> Recursive ds :: [Decl]
ds ->
> let env' :: Env
env' = ((Name, Value) -> Env -> Env) -> Env -> [(Name, Value)] -> Env
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Value) -> Env -> Env
bindVar Env
env [(Name, Value)]
bindings
> bindings :: [(Name, Value)]
bindings = (Decl -> (Name, Value)) -> [Decl] -> [(Name, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Decl -> (Name, Value)
evalDeclRecursive Env
env') [Decl]
ds
> in Env
env'
To evaluate a declaration in a non-recursive context, we need only
evaluate the expression on the right-hand side or look up the
appropriate primitive.
> evalDecl :: Env -> Decl -> (Name, Value)
> evalDecl :: Env -> Decl -> (Name, Value)
evalDecl env :: Env
env d :: Decl
d =
> case Decl -> DeclDef
dDefinition Decl
d of
> DPrim -> (Decl -> Name
dName Decl
d, Name -> Value
evalPrim (Decl -> Name
dName Decl
d))
> DExpr e :: Expr
e -> (Decl -> Name
dName Decl
d, Env -> Expr -> Value
evalExpr Env
env Expr
e)
To evaluate a declaration in a recursive context, we must perform a
type-directed copy to build the spine of the value. This ensures that
the definedness invariant for type `Value` will be maintained.
> evalDeclRecursive :: Env -> Decl -> (Name, Value)
> evalDeclRecursive :: Env -> Decl -> (Name, Value)
evalDeclRecursive env :: Env
env d :: Decl
d =
> case Decl -> DeclDef
dDefinition Decl
d of
> DPrim -> (Decl -> Name
dName Decl
d, Name -> Value
evalPrim (Decl -> Name
dName Decl
d))
> DExpr e :: Expr
e -> (Decl -> Name
dName Decl
d, Env -> Schema -> Value -> Value
copyBySchema Env
env (Decl -> Schema
dSignature Decl
d) (Env -> Expr -> Value
evalExpr Env
env Expr
e))
Primitives
==========
To evaluate a primitive, we look up its implementation by name in a table.
> evalPrim :: Name -> Value
> evalPrim :: Name -> Value
evalPrim n :: Name
n
> | Just i :: Ident
i <- Name -> Maybe Ident
asPrim Name
n, Just v :: Value
v <- Ident -> Map Ident Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i Map Ident Value
primTable = Value
v
> | Bool
otherwise = String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "evalPrim" ["Unimplemented primitive", Name -> String
forall a. Show a => a -> String
show Name
n]
Cryptol primitives fall into several groups:
* Logic: `&&`, `||`, `^`, `complement`, `zero`, `True`, `False`
* Arithmetic: `+`, `-`, `*`, `/`, `%`, `^^`, `lg2`, `negate`, `number`
* Comparison: `<`, `>`, `<=`, `>=`, `==`, `!=`
* Sequences: `#`, `join`, `split`, `splitAt`, `reverse`, `transpose`
* Shifting: `<<`, `>>`, `<<<`, `>>>`
* Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`
* Enumerations: `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`
* Polynomials: `pmult`, `pdiv`, `pmod`
* Miscellaneous: `error`, `random`, `trace`
> primTable :: Map Ident Value
> primTable :: Map Ident Value
primTable = [(Ident, Value)] -> Map Ident Value
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Ident, Value)] -> Map Ident Value)
-> [(Ident, Value)] -> Map Ident Value
forall a b. (a -> b) -> a -> b
$ ((String, Value) -> (Ident, Value))
-> [(String, Value)] -> [(Ident, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: String
n, v :: Value
v) -> (Text -> Ident
mkIdent (String -> Text
T.pack String
n), Value
v))
>
>
> [ ("&&" , (TValue -> Value -> Value -> Value) -> Value
binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
logicBinary Bool -> Bool -> Bool
(&&)))
> , ("||" , (TValue -> Value -> Value -> Value) -> Value
binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
logicBinary Bool -> Bool -> Bool
(||)))
> , ("^" , (TValue -> Value -> Value -> Value) -> Value
binary ((Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
logicBinary Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)))
> , ("complement" , (TValue -> Value -> Value) -> Value
unary ((Bool -> Bool) -> TValue -> Value -> Value
logicUnary Bool -> Bool
not))
> , ("zero" , (TValue -> Value) -> Value
VPoly (Either EvalError Bool -> TValue -> Value
logicNullary (Bool -> Either EvalError Bool
forall a b. b -> Either a b
Right Bool
False)))
> , ("True" , Either EvalError Bool -> Value
VBit (Bool -> Either EvalError Bool
forall a b. b -> Either a b
Right Bool
True))
> , ("False" , Either EvalError Bool -> Value
VBit (Bool -> Either EvalError Bool
forall a b. b -> Either a b
Right Bool
False))
>
>
> , ("+" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary (\x :: Integer
x y :: Integer
y -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y))))
> , ("-" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary (\x :: Integer
x y :: Integer
y -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y))))
> , ("*" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary (\x :: Integer
x y :: Integer
y -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y))))
> , ("/" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary Integer -> Integer -> Either EvalError Integer
divWrap))
> , ("%" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary Integer -> Integer -> Either EvalError Integer
modWrap))
> , ("/$" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
signedArithBinary Integer -> Integer -> Either EvalError Integer
divWrap))
> , ("%$" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
signedArithBinary Integer -> Integer -> Either EvalError Integer
modWrap))
> , ("^^" , (TValue -> Value -> Value -> Value) -> Value
binary ((Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary Integer -> Integer -> Either EvalError Integer
expWrap))
> , ("lg2" , (TValue -> Value -> Value) -> Value
unary ((Integer -> Either EvalError Integer) -> TValue -> Value -> Value
arithUnary Integer -> Either EvalError Integer
lg2Wrap))
> , ("negate" , (TValue -> Value -> Value) -> Value
unary ((Integer -> Either EvalError Integer) -> TValue -> Value -> Value
arithUnary (\x :: Integer
x -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (- Integer
x))))
> , ("number" , (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \val :: Integer
val ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> Either EvalError Integer -> TValue -> Value
arithNullary (Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right Integer
val) TValue
a)
> , ("toInteger" , (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_bits :: Integer
_bits ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x ->
> Either EvalError Integer -> Value
VInteger (Value -> Either EvalError Integer
fromVWord Value
x))
> , ("fromInteger", (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x ->
> Either EvalError Integer -> TValue -> Value
arithNullary (Value -> Either EvalError Integer
fromVInteger Value
x) TValue
a)
>
>
> , ("<" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT)))
> , (">" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT)))
> , ("<=" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT)))
> , (">=" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
LT)))
> , ("==" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ)))
> , ("!=" , (TValue -> Value -> Value -> Value) -> Value
binary ((Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder (\o :: Ordering
o -> Ordering
o Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
EQ)))
> , ("<$" , (TValue -> Value -> Value -> Value) -> Value
binary TValue -> Value -> Value -> Value
signedLessThan)
>
>
> , ("#" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \front :: Nat'
front ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \back :: Nat'
back ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_elty :: TValue
_elty ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \l :: Value
l ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \r :: Value
r ->
> Nat' -> [Value] -> Value
VList (Nat' -> Nat' -> Nat'
nAdd Nat'
front Nat'
back) (Value -> [Value]
fromVList Value
l [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Value -> [Value]
fromVList Value
r))
>
> , ("join" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \parts :: Nat'
parts ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \each :: Nat'
each ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \xss :: Value
xss ->
> case Nat'
each of
>
> Nat 0 -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat 0) []
> _ -> Nat' -> [Value] -> Value
VList (Nat' -> Nat' -> Nat'
nMul Nat'
parts Nat'
each)
> ([[Value]] -> [Value]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Value -> [Value]) -> [Value] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map Value -> [Value]
fromVList (Value -> [Value]
fromVList Value
xss))))
>
> , ("split" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \parts :: Nat'
parts ->
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \each :: Integer
each ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \val :: Value
val ->
> Nat' -> [Value] -> Value
VList Nat'
parts (Nat' -> Integer -> [Value] -> [Value]
splitV Nat'
parts Integer
each (Value -> [Value]
fromVList Value
val)))
>
> , ("splitAt" , (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \front :: Integer
front ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \back :: Nat'
back ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> let (xs :: [Value]
xs, ys :: [Value]
ys) = Integer -> [Value] -> ([Value], [Value])
forall i a. Integral i => i -> [a] -> ([a], [a])
genericSplitAt Integer
front (Value -> [Value]
fromVList Value
v)
> in [Value] -> Value
VTuple [Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
front) [Value]
xs, Nat' -> [Value] -> Value
VList Nat'
back [Value]
ys])
>
> , ("reverse" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> Nat' -> [Value] -> Value
VList Nat'
n ([Value] -> [Value]
forall a. [a] -> [a]
reverse (Value -> [Value]
fromVList Value
v)))
>
> , ("transpose" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \rows :: Nat'
rows ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \cols :: Nat'
cols ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> Nat' -> [Value] -> Value
VList Nat'
cols
> (([Value] -> Value) -> [[Value]] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Nat' -> [Value] -> Value
VList Nat'
rows) (Nat' -> [[Value]] -> [[Value]]
transposeV Nat'
cols ((Value -> [Value]) -> [Value] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map Value -> [Value]
fromVList (Value -> [Value]
fromVList Value
v)))))
>
>
> , ("<<" , (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
shiftV Nat' -> Value -> [Value] -> Integer -> [Value]
shiftLV)
> , (">>" , (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
shiftV Nat' -> Value -> [Value] -> Integer -> [Value]
shiftRV)
> , ("<<<" , (Integer -> [Value] -> Integer -> [Value]) -> Value
rotateV Integer -> [Value] -> Integer -> [Value]
rotateLV)
> , (">>>" , (Integer -> [Value] -> Integer -> [Value]) -> Value
rotateV Integer -> [Value] -> Integer -> [Value]
rotateRV)
> , (">>$" , Value
signedShiftRV)
>
>
> , ("@" , (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
indexPrimOne Nat' -> TValue -> [Value] -> Integer -> Value
indexFront)
> , ("!" , (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
indexPrimOne Nat' -> TValue -> [Value] -> Integer -> Value
indexBack)
> , ("update" , (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
updatePrim Nat' -> [Value] -> Integer -> Value -> [Value]
updateFront)
> , ("updateEnd" , (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
updatePrim Nat' -> [Value] -> Integer -> Value -> [Value]
updateBack)
>
>
> , ("fromTo" , (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \first :: Integer
first ->
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \lst :: Integer
lst ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty ->
> let f :: Integer -> Value
f i :: Integer
i = Either EvalError Integer -> TValue -> Value
arithNullary (Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right Integer
i) TValue
ty
> in Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat (1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lst Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
first)) ((Integer -> Value) -> [Integer] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Value
f [Integer
first .. Integer
lst]))
>
> , ("fromThenTo" , (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \first :: Integer
first ->
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \next :: Integer
next ->
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_lst :: Integer
_lst ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty ->
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \len :: Integer
len ->
> let f :: Integer -> Value
f i :: Integer
i = Either EvalError Integer -> TValue -> Value
arithNullary (Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right Integer
i) TValue
ty
> in Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
len) ((Integer -> Value) -> [Integer] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Value
f (Integer -> [Integer] -> [Integer]
forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
len [Integer
first, Integer
next ..])))
>
> , ("infFrom" , (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \first :: Value
first ->
> let f :: Integer -> Value
f i :: Integer
i = (Integer -> Either EvalError Integer) -> TValue -> Value -> Value
arithUnary (\x :: Integer
x -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i)) TValue
ty Value
first
> in Nat' -> [Value] -> Value
VList Nat'
Inf ((Integer -> Value) -> [Integer] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Value
f [0 ..]))
>
> , ("infFromThen", (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \first :: Value
first ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \next :: Value
next ->
> let f :: Integer -> Value
f i :: Integer
i = (Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary (\x :: Integer
x y :: Integer
y -> Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
x) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i)) TValue
ty Value
first Value
next
> in Nat' -> [Value] -> Value
VList Nat'
Inf ((Integer -> Value) -> [Integer] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Value
f [0 ..]))
>
>
> , ("error" , (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_ ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_s :: Value
_s -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left (String -> EvalError
UserError "error")) TValue
a)
>
>
> , ("random" , (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_seed :: Value
_seed ->
> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left (String -> EvalError
UserError "random: unimplemented")) TValue
a)
>
> , ("trace" , (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_n :: Nat'
_n ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_b :: TValue
_b ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_s :: Value
_s ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_x :: Value
_x ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \y :: Value
y -> Value
y)
> ]
>
> unary :: (TValue -> Value -> Value) -> Value
> unary :: (TValue -> Value -> Value) -> Value
unary f :: TValue -> Value -> Value
f = (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty -> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x -> TValue -> Value -> Value
f TValue
ty Value
x
>
> binary :: (TValue -> Value -> Value -> Value) -> Value
> binary :: (TValue -> Value -> Value -> Value) -> Value
binary f :: TValue -> Value -> Value -> Value
f = (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty -> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x -> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \y :: Value
y -> TValue -> Value -> Value -> Value
f TValue
ty Value
x Value
y
Word operations
Many Cryptol primitives take numeric arguments in the form of
bitvectors. For such operations, any output bit that depends on the
numeric value is strict in *all* bits of the numeric argument. This is
implemented in function `fromVWord`, which converts a value from a
big-endian binary format to an integer. The result is an evaluation
error if any of the input bits contain an evaluation error.
> fromVWord :: Value -> Either EvalError Integer
> fromVWord :: Value -> Either EvalError Integer
fromVWord v :: Value
v = ([Bool] -> Integer)
-> Either EvalError [Bool] -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Integer
bitsToInteger ((Value -> Either EvalError Bool)
-> [Value] -> Either EvalError [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Either EvalError Bool
fromVBit (Value -> [Value]
fromVList Value
v))
>
>
> bitsToInteger :: [Bool] -> Integer
> bitsToInteger :: [Bool] -> Integer
bitsToInteger bs :: [Bool]
bs = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Integer -> Bool -> Integer
forall a. Num a => a -> Bool -> a
f 0 [Bool]
bs
> where f :: a -> Bool -> a
f x :: a
x b :: Bool
b = if Bool
b then 2 a -> a -> a
forall a. Num a => a -> a -> a
* a
x a -> a -> a
forall a. Num a => a -> a -> a
+ 1 else 2 a -> a -> a
forall a. Num a => a -> a -> a
* a
x
> fromSignedVWord :: Value -> Either EvalError Integer
> fromSignedVWord :: Value -> Either EvalError Integer
fromSignedVWord v :: Value
v = ([Bool] -> Integer)
-> Either EvalError [Bool] -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Integer
signedBitsToInteger ((Value -> Either EvalError Bool)
-> [Value] -> Either EvalError [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Either EvalError Bool
fromVBit (Value -> [Value]
fromVList Value
v))
>
>
> signedBitsToInteger :: [Bool] -> Integer
> signedBitsToInteger :: [Bool] -> Integer
signedBitsToInteger [] = String -> [String] -> Integer
forall a. String -> [String] -> a
evalPanic "signedBitsToInteger" ["Bitvector has zero length"]
> signedBitsToInteger (b0 :: Bool
b0 : bs :: [Bool]
bs) = (Integer -> Bool -> Integer) -> Integer -> [Bool] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Integer -> Bool -> Integer
forall a. Num a => a -> Bool -> a
f (if Bool
b0 then -1 else 0) [Bool]
bs
> where f :: a -> Bool -> a
f x :: a
x b :: Bool
b = if Bool
b then 2 a -> a -> a
forall a. Num a => a -> a -> a
* a
x a -> a -> a
forall a. Num a => a -> a -> a
+ 1 else 2 a -> a -> a
forall a. Num a => a -> a -> a
* a
x
Function `vWord` converts an integer back to the big-endian bitvector
representation. If an integer-producing function raises a run-time
exception, then the output bitvector will contain the exception in all
bit positions.
> vWord :: Integer -> Either EvalError Integer -> Value
> vWord :: Integer -> Either EvalError Integer -> Value
vWord w :: Integer
w e :: Either EvalError Integer
e = Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) [ Either EvalError Bool -> Value
VBit ((Integer -> Bool)
-> Either EvalError Integer -> Either EvalError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Bool
forall a. Bits a => Integer -> a -> Bool
test Integer
i) Either EvalError Integer
e) | Integer
i <- [Integer
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1, Integer
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-2 .. 0] ]
> where test :: Integer -> a -> Bool
test i :: Integer
i x :: a
x = a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
Logic
Bitwise logic primitives are defined by recursion over the type
structure. On type `Bit`, we use `fmap` and `liftA2` to make these
operations strict in all arguments. For example, `True || error "foo"`
does not evaluate to `True`, but yields a run-time exception. On other
types, run-time exceptions on input bits only affect the output bits
at the same positions.
> logicNullary :: Either EvalError Bool -> TValue -> Value
> logicNullary :: Either EvalError Bool -> TValue -> Value
logicNullary b :: Either EvalError Bool
b = TValue -> Value
go
> where
> go :: TValue -> Value
go TVBit = Either EvalError Bool -> Value
VBit Either EvalError Bool
b
> go TVInteger = Either EvalError Integer -> Value
VInteger ((Bool -> Integer)
-> Either EvalError Bool -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\c :: Bool
c -> if Bool
c then -1 else 0) Either EvalError Bool
b)
> go (TVIntMod _) = Either EvalError Integer -> Value
VInteger ((Bool -> Integer)
-> Either EvalError Bool -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Bool -> Integer
forall a b. a -> b -> a
const 0) Either EvalError Bool
b)
> go (TVSeq n :: Integer
n ety :: TValue
ety) = Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
n) (Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (TValue -> Value
go TValue
ety))
> go (TVStream ety :: TValue
ety) = Nat' -> [Value] -> Value
VList Nat'
Inf (Value -> [Value]
forall a. a -> [a]
repeat (TValue -> Value
go TValue
ety))
> go (TVTuple tys :: [TValue]
tys) = [Value] -> Value
VTuple ((TValue -> Value) -> [TValue] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> Value
go [TValue]
tys)
> go (TVRec fields :: [(Ident, TValue)]
fields) = [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value
go TValue
fty) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fields ]
> go (TVFun _ bty :: TValue
bty) = (Value -> Value) -> Value
VFun (\_ -> TValue -> Value
go TValue
bty)
> go (TVAbstract {}) =
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicUnary" ["Abstract type not in `Logic`"]
>
> logicUnary :: (Bool -> Bool) -> TValue -> Value -> Value
> logicUnary :: (Bool -> Bool) -> TValue -> Value -> Value
logicUnary op :: Bool -> Bool
op = TValue -> Value -> Value
go
> where
> go :: TValue -> Value -> Value
> go :: TValue -> Value -> Value
go ty :: TValue
ty val :: Value
val =
> case TValue
ty of
> TVBit -> Either EvalError Bool -> Value
VBit ((Bool -> Bool) -> Either EvalError Bool -> Either EvalError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
op (Value -> Either EvalError Bool
fromVBit Value
val))
> TVInteger -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicUnary" ["Integer not in class Logic"]
> TVIntMod _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicUnary" ["Z not in class Logic"]
> TVSeq w :: Integer
w ety :: TValue
ety -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
ety) (Value -> [Value]
fromVList Value
val))
> TVStream ety :: TValue
ety -> Nat' -> [Value] -> Value
VList Nat'
Inf ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
ety) (Value -> [Value]
fromVList Value
val))
> TVTuple etys :: [TValue]
etys -> [Value] -> Value
VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> Value -> Value
go [TValue]
etys (Value -> [Value]
fromVTuple Value
val))
> TVRec fields :: [(Ident, TValue)]
fields -> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value -> Value
go TValue
fty (Ident -> Value -> Value
lookupRecord Ident
f Value
val)) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fields ]
> TVFun _ bty :: TValue
bty -> (Value -> Value) -> Value
VFun (\v :: Value
v -> TValue -> Value -> Value
go TValue
bty (Value -> Value -> Value
fromVFun Value
val Value
v))
> TVAbstract {} ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicUnary" ["Abstract type not in `Logic`"]
>
> logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
> logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
logicBinary op :: Bool -> Bool -> Bool
op = TValue -> Value -> Value -> Value
go
> where
> go :: TValue -> Value -> Value -> Value
> go :: TValue -> Value -> Value -> Value
go ty :: TValue
ty l :: Value
l r :: Value
r =
> case TValue
ty of
> TVBit -> Either EvalError Bool -> Value
VBit ((Bool -> Bool -> Bool)
-> Either EvalError Bool
-> Either EvalError Bool
-> Either EvalError Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
op (Value -> Either EvalError Bool
fromVBit Value
l) (Value -> Either EvalError Bool
fromVBit Value
r))
> TVInteger -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicBinary" ["Integer not in class Logic"]
> TVIntMod _ -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicBinary" ["Z not in class Logic"]
> TVSeq w :: Integer
w ety :: TValue
ety -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Value
go TValue
ety) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVStream ety :: TValue
ety -> Nat' -> [Value] -> Value
VList Nat'
Inf ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Value
go TValue
ety) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVTuple etys :: [TValue]
etys -> [Value] -> Value
VTuple ((TValue -> Value -> Value -> Value)
-> [TValue] -> [Value] -> [Value] -> [Value]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Value
go [TValue]
etys (Value -> [Value]
fromVTuple Value
l) (Value -> [Value]
fromVTuple Value
r))
> TVRec fields :: [(Ident, TValue)]
fields -> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value -> Value -> Value
go TValue
fty (Ident -> Value -> Value
lookupRecord Ident
f Value
l) (Ident -> Value -> Value
lookupRecord Ident
f Value
r))
> | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fields ]
> TVFun _ bty :: TValue
bty -> (Value -> Value) -> Value
VFun (\v :: Value
v -> TValue -> Value -> Value -> Value
go TValue
bty (Value -> Value -> Value
fromVFun Value
l Value
v) (Value -> Value -> Value
fromVFun Value
r Value
v))
> TVAbstract {} ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "logicBinary" ["Abstract type not in `Logic`"]
Arithmetic
Arithmetic primitives may be applied to any type that is made up of
finite bitvectors. On type `[n]`, arithmetic operators are strict in
all input bits, as indicated by the definition of `fromVWord`. For
example, `[error "foo", True] * 2` does not evaluate to `[True,
False]`, but to `[error "foo", error "foo"]`.
Signed arithmetic primitives may be applied to any type that is made
up of non-empty finite bitvectors.
> arithNullary :: Either EvalError Integer -> TValue -> Value
> arithNullary :: Either EvalError Integer -> TValue -> Value
arithNullary i :: Either EvalError Integer
i = TValue -> Value
go
> where
> go :: TValue -> Value
> go :: TValue -> Value
go ty :: TValue
ty =
> case TValue
ty of
> TVBit ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithNullary" ["Bit not in class Arith"]
> TVInteger ->
> Either EvalError Integer -> Value
VInteger Either EvalError Integer
i
> TVIntMod n :: Integer
n ->
> Either EvalError Integer -> Value
VInteger ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
n (Integer -> Integer)
-> Either EvalError Integer -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either EvalError Integer
i)
> TVSeq w :: Integer
w a :: TValue
a
> | TValue -> Bool
isTBit TValue
a -> Integer -> Either EvalError Integer -> Value
vWord Integer
w Either EvalError Integer
i
> | Bool
otherwise -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) (Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
w (TValue -> Value
go TValue
a))
> TVStream a :: TValue
a ->
> Nat' -> [Value] -> Value
VList Nat'
Inf (Value -> [Value]
forall a. a -> [a]
repeat (TValue -> Value
go TValue
a))
> TVFun _ ety :: TValue
ety ->
> (Value -> Value) -> Value
VFun (Value -> Value -> Value
forall a b. a -> b -> a
const (TValue -> Value
go TValue
ety))
> TVTuple tys :: [TValue]
tys ->
> [Value] -> Value
VTuple ((TValue -> Value) -> [TValue] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> Value
go [TValue]
tys)
> TVRec fs :: [(Ident, TValue)]
fs ->
> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value
go TValue
fty) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fs ]
> TVAbstract {} ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithNullary" ["Absrat type not in `Arith`"]
>
> arithUnary :: (Integer -> Either EvalError Integer)
> -> TValue -> Value -> Value
> arithUnary :: (Integer -> Either EvalError Integer) -> TValue -> Value -> Value
arithUnary op :: Integer -> Either EvalError Integer
op = TValue -> Value -> Value
go
> where
> go :: TValue -> Value -> Value
> go :: TValue -> Value -> Value
go ty :: TValue
ty val :: Value
val =
> case TValue
ty of
> TVBit ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithUnary" ["Bit not in class Arith"]
> TVInteger ->
> Either EvalError Integer -> Value
VInteger (Either EvalError Integer -> Value)
-> Either EvalError Integer -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVInteger Value
val of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i -> Integer -> Either EvalError Integer
op Integer
i
> TVIntMod n :: Integer
n ->
> Either EvalError Integer -> Value
VInteger (Either EvalError Integer -> Value)
-> Either EvalError Integer -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVInteger Value
val of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i -> (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
n (Integer -> Integer)
-> Either EvalError Integer -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Either EvalError Integer
op Integer
i
> TVSeq w :: Integer
w a :: TValue
a
> | TValue -> Bool
isTBit TValue
a -> Integer -> Either EvalError Integer -> Value
vWord Integer
w (Integer -> Either EvalError Integer
op (Integer -> Either EvalError Integer)
-> Either EvalError Integer -> Either EvalError Integer
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Value -> Either EvalError Integer
fromVWord Value
val)
> | Bool
otherwise -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
a) (Value -> [Value]
fromVList Value
val))
> TVStream a :: TValue
a ->
> Nat' -> [Value] -> Value
VList Nat'
Inf ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Value -> Value
go TValue
a) (Value -> [Value]
fromVList Value
val))
> TVFun _ ety :: TValue
ety ->
> (Value -> Value) -> Value
VFun (\x :: Value
x -> TValue -> Value -> Value
go TValue
ety (Value -> Value -> Value
fromVFun Value
val Value
x))
> TVTuple tys :: [TValue]
tys ->
> [Value] -> Value
VTuple ((TValue -> Value -> Value) -> [TValue] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> Value -> Value
go [TValue]
tys (Value -> [Value]
fromVTuple Value
val))
> TVRec fs :: [(Ident, TValue)]
fs ->
> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value -> Value
go TValue
fty (Ident -> Value -> Value
lookupRecord Ident
f Value
val)) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fs ]
> TVAbstract {} ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithUnary" ["Absrat type not in `Arith`"]
>
> arithBinary :: (Integer -> Integer -> Either EvalError Integer)
> -> TValue -> Value -> Value -> Value
> arithBinary :: (Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
arithBinary = (Value -> Either EvalError Integer)
-> (Integer -> Integer -> Either EvalError Integer)
-> TValue
-> Value
-> Value
-> Value
arithBinaryGeneric Value -> Either EvalError Integer
fromVWord
>
> signedArithBinary :: (Integer -> Integer -> Either EvalError Integer)
> -> TValue -> Value -> Value -> Value
> signedArithBinary :: (Integer -> Integer -> Either EvalError Integer)
-> TValue -> Value -> Value -> Value
signedArithBinary = (Value -> Either EvalError Integer)
-> (Integer -> Integer -> Either EvalError Integer)
-> TValue
-> Value
-> Value
-> Value
arithBinaryGeneric Value -> Either EvalError Integer
fromSignedVWord
>
> arithBinaryGeneric :: (Value -> Either EvalError Integer)
> -> (Integer -> Integer -> Either EvalError Integer)
> -> TValue -> Value -> Value -> Value
> arithBinaryGeneric :: (Value -> Either EvalError Integer)
-> (Integer -> Integer -> Either EvalError Integer)
-> TValue
-> Value
-> Value
-> Value
arithBinaryGeneric fromWord :: Value -> Either EvalError Integer
fromWord op :: Integer -> Integer -> Either EvalError Integer
op = TValue -> Value -> Value -> Value
go
> where
> go :: TValue -> Value -> Value -> Value
> go :: TValue -> Value -> Value -> Value
go ty :: TValue
ty l :: Value
l r :: Value
r =
> case TValue
ty of
> TVBit ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithBinary" ["Bit not in class Arith"]
> TVInteger ->
> Either EvalError Integer -> Value
VInteger (Either EvalError Integer -> Value)
-> Either EvalError Integer -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVInteger Value
l of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i ->
> case Value -> Either EvalError Integer
fromVInteger Value
r of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right j :: Integer
j -> Integer -> Integer -> Either EvalError Integer
op Integer
i Integer
j
> TVIntMod n :: Integer
n ->
> Either EvalError Integer -> Value
VInteger (Either EvalError Integer -> Value)
-> Either EvalError Integer -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVInteger Value
l of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i ->
> case Value -> Either EvalError Integer
fromVInteger Value
r of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right j :: Integer
j -> (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
n (Integer -> Integer)
-> Either EvalError Integer -> Either EvalError Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> Either EvalError Integer
op Integer
i Integer
j
> TVSeq w :: Integer
w a :: TValue
a
> | TValue -> Bool
isTBit TValue
a -> Integer -> Either EvalError Integer -> Value
vWord Integer
w (Either EvalError Integer -> Value)
-> Either EvalError Integer -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromWord Value
l of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i ->
> case Value -> Either EvalError Integer
fromWord Value
r of
> Left e :: EvalError
e -> EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
e
> Right j :: Integer
j -> Integer -> Integer -> Either EvalError Integer
op Integer
i Integer
j
> | Bool
otherwise -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
w) ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Value
go TValue
a) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVStream a :: TValue
a ->
> Nat' -> [Value] -> Value
VList Nat'
Inf ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Value
go TValue
a) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVFun _ ety :: TValue
ety ->
> (Value -> Value) -> Value
VFun (\x :: Value
x -> TValue -> Value -> Value -> Value
go TValue
ety (Value -> Value -> Value
fromVFun Value
l Value
x) (Value -> Value -> Value
fromVFun Value
r Value
x))
> TVTuple tys :: [TValue]
tys ->
> [Value] -> Value
VTuple ((TValue -> Value -> Value -> Value)
-> [TValue] -> [Value] -> [Value] -> [Value]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Value
go [TValue]
tys (Value -> [Value]
fromVTuple Value
l) (Value -> [Value]
fromVTuple Value
r))
> TVRec fs :: [(Ident, TValue)]
fs ->
> [(Ident, Value)] -> Value
VRecord [ (Ident
f, TValue -> Value -> Value -> Value
go TValue
fty (Ident -> Value -> Value
lookupRecord Ident
f Value
l) (Ident -> Value -> Value
lookupRecord Ident
f Value
r)) | (f :: Ident
f, fty :: TValue
fty) <- [(Ident, TValue)]
fs ]
> TVAbstract {} ->
> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "arithBinary" ["Abstract type not in class `Arith`"]
Signed bitvector division (`/$`) and remainder (`%$`) are defined so
that division rounds toward zero, and the remainder `x %$ y` has the
same sign as `x`. Accordingly, they are implemented with Haskell's
`quot` and `rem` operations.
> divWrap :: Integer -> Integer -> Either EvalError Integer
> divWrap :: Integer -> Integer -> Either EvalError Integer
divWrap _ 0 = EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
DivideByZero
> divWrap x :: Integer
x y :: Integer
y = Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
>
> modWrap :: Integer -> Integer -> Either EvalError Integer
> modWrap :: Integer -> Integer -> Either EvalError Integer
modWrap _ 0 = EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
DivideByZero
> modWrap x :: Integer
x y :: Integer
y = Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
>
> expWrap :: Integer -> Integer -> Either EvalError Integer
> expWrap :: Integer -> Integer -> Either EvalError Integer
expWrap x :: Integer
x y :: Integer
y = if Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
NegativeExponent else Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)
>
> lg2Wrap :: Integer -> Either EvalError Integer
> lg2Wrap :: Integer -> Either EvalError Integer
lg2Wrap x :: Integer
x = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then EvalError -> Either EvalError Integer
forall a b. a -> Either a b
Left EvalError
LogNegative else Integer -> Either EvalError Integer
forall a b. b -> Either a b
Right (Integer -> Integer
lg2 Integer
x)
Comparison
Comparison primitives may be applied to any type that contains a
finite number of bits. All such types are compared using a
lexicographic ordering on bits, where `False` < `True`. Lists and
tuples are compared left-to-right, and record fields are compared in
alphabetical order.
Comparisons on type `Bit` are strict in both arguments. Comparisons on
larger types have short-circuiting behavior: A comparison involving an
error/undefined element will only yield an error if all corresponding
bits to the *left* of that position are equal.
>
> cmpOrder :: (Ordering -> Bool) -> TValue -> Value -> Value -> Value
> cmpOrder :: (Ordering -> Bool) -> TValue -> Value -> Value -> Value
cmpOrder p :: Ordering -> Bool
p ty :: TValue
ty l :: Value
l r :: Value
r = Either EvalError Bool -> Value
VBit ((Ordering -> Bool)
-> Either EvalError Ordering -> Either EvalError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ordering -> Bool
p (TValue -> Value -> Value -> Either EvalError Ordering
lexCompare TValue
ty Value
l Value
r))
>
>
> lexCompare :: TValue -> Value -> Value -> Either EvalError Ordering
> lexCompare :: TValue -> Value -> Value -> Either EvalError Ordering
lexCompare ty :: TValue
ty l :: Value
l r :: Value
r =
> case TValue
ty of
> TVBit ->
> Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bool -> Bool -> Ordering)
-> Either EvalError Bool -> Either EvalError (Bool -> Ordering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Either EvalError Bool
fromVBit Value
l Either EvalError (Bool -> Ordering)
-> Either EvalError Bool -> Either EvalError Ordering
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Either EvalError Bool
fromVBit Value
r
> TVInteger ->
> Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> Either EvalError Integer
-> Either EvalError (Integer -> Ordering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Either EvalError Integer
fromVInteger Value
l Either EvalError (Integer -> Ordering)
-> Either EvalError Integer -> Either EvalError Ordering
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Either EvalError Integer
fromVInteger Value
r
> TVIntMod _ ->
> Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> Either EvalError Integer
-> Either EvalError (Integer -> Ordering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Either EvalError Integer
fromVInteger Value
l Either EvalError (Integer -> Ordering)
-> Either EvalError Integer -> Either EvalError Ordering
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Either EvalError Integer
fromVInteger Value
r
> TVSeq _w :: Integer
_w ety :: TValue
ety ->
> [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((Value -> Value -> Either EvalError Ordering)
-> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Either EvalError Ordering
lexCompare TValue
ety) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVStream _ ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexCompare" ["invalid type"]
> TVFun _ _ ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexCompare" ["invalid type"]
> TVTuple etys :: [TValue]
etys ->
> [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
-> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
lexCompare [TValue]
etys (Value -> [Value]
fromVTuple Value
l) (Value -> [Value]
fromVTuple Value
r))
> TVRec fields :: [(Ident, TValue)]
fields ->
> let tys :: [TValue]
tys = ((Ident, TValue) -> TValue) -> [(Ident, TValue)] -> [TValue]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, TValue) -> TValue
forall a b. (a, b) -> b
snd (((Ident, TValue) -> (Ident, TValue) -> Ordering)
-> [(Ident, TValue)] -> [(Ident, TValue)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, TValue) -> Ident)
-> (Ident, TValue) -> (Ident, TValue) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, TValue) -> Ident
forall a b. (a, b) -> a
fst) [(Ident, TValue)]
fields)
> ls :: [Value]
ls = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Value
forall a b. (a, b) -> b
snd (((Ident, Value) -> (Ident, Value) -> Ordering)
-> [(Ident, Value)] -> [(Ident, Value)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, Value) -> Ident)
-> (Ident, Value) -> (Ident, Value) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst) (Value -> [(Ident, Value)]
fromVRecord Value
l))
> rs :: [Value]
rs = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Value
forall a b. (a, b) -> b
snd (((Ident, Value) -> (Ident, Value) -> Ordering)
-> [(Ident, Value)] -> [(Ident, Value)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, Value) -> Ident)
-> (Ident, Value) -> (Ident, Value) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst) (Value -> [(Ident, Value)]
fromVRecord Value
r))
> in [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
-> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
lexCompare [TValue]
tys [Value]
ls [Value]
rs)
> TVAbstract {} ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexCompare" ["Abstract type not in `Cmp`"]
>
> lexList :: [Either EvalError Ordering] -> Either EvalError Ordering
> lexList :: [Either EvalError Ordering] -> Either EvalError Ordering
lexList [] = Ordering -> Either EvalError Ordering
forall a b. b -> Either a b
Right Ordering
EQ
> lexList (e :: Either EvalError Ordering
e : es :: [Either EvalError Ordering]
es) =
> case Either EvalError Ordering
e of
> Left err :: EvalError
err -> EvalError -> Either EvalError Ordering
forall a b. a -> Either a b
Left EvalError
err
> Right LT -> Ordering -> Either EvalError Ordering
forall a b. b -> Either a b
Right Ordering
LT
> Right EQ -> [Either EvalError Ordering] -> Either EvalError Ordering
lexList [Either EvalError Ordering]
es
> Right GT -> Ordering -> Either EvalError Ordering
forall a b. b -> Either a b
Right Ordering
GT
Signed comparisons may be applied to any type made up of non-empty
bitvectors. All such types are compared using a lexicographic
ordering: Lists and tuples are compared left-to-right, and record
fields are compared in alphabetical order.
> signedLessThan :: TValue -> Value -> Value -> Value
> signedLessThan :: TValue -> Value -> Value -> Value
signedLessThan ty :: TValue
ty l :: Value
l r :: Value
r = Either EvalError Bool -> Value
VBit ((Ordering -> Bool)
-> Either EvalError Ordering -> Either EvalError Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT) (TValue -> Value -> Value -> Either EvalError Ordering
lexSignedCompare TValue
ty Value
l Value
r))
>
>
> lexSignedCompare :: TValue -> Value -> Value -> Either EvalError Ordering
> lexSignedCompare :: TValue -> Value -> Value -> Either EvalError Ordering
lexSignedCompare ty :: TValue
ty l :: Value
l r :: Value
r =
> case TValue
ty of
> TVBit ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["invalid type"]
> TVInteger ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["invalid type"]
> TVIntMod _ ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["invalid type"]
> TVSeq _w :: Integer
_w ety :: TValue
ety
> | TValue -> Bool
isTBit TValue
ety ->
> case Value -> Either EvalError Integer
fromSignedVWord Value
l of
> Left e :: EvalError
e -> EvalError -> Either EvalError Ordering
forall a b. a -> Either a b
Left EvalError
e
> Right i :: Integer
i ->
> case Value -> Either EvalError Integer
fromSignedVWord Value
r of
> Left e :: EvalError
e -> EvalError -> Either EvalError Ordering
forall a b. a -> Either a b
Left EvalError
e
> Right j :: Integer
j -> Ordering -> Either EvalError Ordering
forall a b. b -> Either a b
Right (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
i Integer
j)
> | Bool
otherwise ->
> [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((Value -> Value -> Either EvalError Ordering)
-> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (TValue -> Value -> Value -> Either EvalError Ordering
lexSignedCompare TValue
ety) (Value -> [Value]
fromVList Value
l) (Value -> [Value]
fromVList Value
r))
> TVStream _ ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["invalid type"]
> TVFun _ _ ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["invalid type"]
> TVTuple etys :: [TValue]
etys ->
> [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
-> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
lexSignedCompare [TValue]
etys (Value -> [Value]
fromVTuple Value
l) (Value -> [Value]
fromVTuple Value
r))
> TVRec fields :: [(Ident, TValue)]
fields ->
> let tys :: [TValue]
tys = ((Ident, TValue) -> TValue) -> [(Ident, TValue)] -> [TValue]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, TValue) -> TValue
forall a b. (a, b) -> b
snd (((Ident, TValue) -> (Ident, TValue) -> Ordering)
-> [(Ident, TValue)] -> [(Ident, TValue)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, TValue) -> Ident)
-> (Ident, TValue) -> (Ident, TValue) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, TValue) -> Ident
forall a b. (a, b) -> a
fst) [(Ident, TValue)]
fields)
> ls :: [Value]
ls = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Value
forall a b. (a, b) -> b
snd (((Ident, Value) -> (Ident, Value) -> Ordering)
-> [(Ident, Value)] -> [(Ident, Value)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, Value) -> Ident)
-> (Ident, Value) -> (Ident, Value) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst) (Value -> [(Ident, Value)]
fromVRecord Value
l))
> rs :: [Value]
rs = ((Ident, Value) -> Value) -> [(Ident, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Value
forall a b. (a, b) -> b
snd (((Ident, Value) -> (Ident, Value) -> Ordering)
-> [(Ident, Value)] -> [(Ident, Value)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, Value) -> Ident)
-> (Ident, Value) -> (Ident, Value) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst) (Value -> [(Ident, Value)]
fromVRecord Value
r))
> in [Either EvalError Ordering] -> Either EvalError Ordering
lexList ((TValue -> Value -> Value -> Either EvalError Ordering)
-> [TValue] -> [Value] -> [Value] -> [Either EvalError Ordering]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue -> Value -> Value -> Either EvalError Ordering
lexSignedCompare [TValue]
tys [Value]
ls [Value]
rs)
> TVAbstract {} ->
> String -> [String] -> Either EvalError Ordering
forall a. String -> [String] -> a
evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]
Sequences
>
> splitV :: Nat' -> Integer -> [Value] -> [Value]
> splitV :: Nat' -> Integer -> [Value] -> [Value]
splitV w :: Nat'
w k :: Integer
k xs :: [Value]
xs =
> case Nat'
w of
> Nat 0 -> []
> Nat n :: Integer
n -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
k) [Value]
ys Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: Nat' -> Integer -> [Value] -> [Value]
splitV (Integer -> Nat'
Nat (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)) Integer
k [Value]
zs
> Inf -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
k) [Value]
ys Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: Nat' -> Integer -> [Value] -> [Value]
splitV Nat'
Inf Integer
k [Value]
zs
> where
> (ys :: [Value]
ys, zs :: [Value]
zs) = Integer -> [Value] -> ([Value], [Value])
forall i a. Integral i => i -> [a] -> ([a], [a])
genericSplitAt Integer
k [Value]
xs
>
>
> transposeV :: Nat' -> [[Value]] -> [[Value]]
> transposeV :: Nat' -> [[Value]] -> [[Value]]
transposeV w :: Nat'
w xss :: [[Value]]
xss =
> case Nat'
w of
> Nat 0 -> []
> Nat n :: Integer
n -> [Value]
heads [Value] -> [[Value]] -> [[Value]]
forall a. a -> [a] -> [a]
: Nat' -> [[Value]] -> [[Value]]
transposeV (Integer -> Nat'
Nat (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)) [[Value]]
tails
> Inf -> [Value]
heads [Value] -> [[Value]] -> [[Value]]
forall a. a -> [a] -> [a]
: Nat' -> [[Value]] -> [[Value]]
transposeV Nat'
Inf [[Value]]
tails
> where
> (heads :: [Value]
heads, tails :: [[Value]]
tails) = [[Value]] -> ([Value], [[Value]])
dest [[Value]]
xss
>
>
>
> dest :: [[Value]] -> ([Value], [[Value]])
> dest :: [[Value]] -> ([Value], [[Value]])
dest [] = ([], [])
> dest ([] : _) = String -> [String] -> ([Value], [[Value]])
forall a. String -> [String] -> a
evalPanic "transposeV" ["Expected non-empty list"]
> dest ((y :: Value
y : ys :: [Value]
ys) : yss :: [[Value]]
yss) = (Value
y Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
zs, [Value]
ys [Value] -> [[Value]] -> [[Value]]
forall a. a -> [a] -> [a]
: [[Value]]
zss)
> where (zs :: [Value]
zs, zss :: [[Value]]
zss) = [[Value]] -> ([Value], [[Value]])
dest [[Value]]
yss
Shifting
Shift and rotate operations are strict in all bits of the shift/rotate
amount, but as lazy as possible in the list values.
> shiftV :: (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
> shiftV :: (Nat' -> Value -> [Value] -> Integer -> [Value]) -> Value
shiftV op :: Nat' -> Value -> [Value] -> Integer -> [Value]
op =
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_ix :: Nat'
_ix ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x ->
> TValue -> Value -> Value
copyByTValue (Nat' -> TValue -> TValue
tvSeq Nat'
n TValue
a) (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVWord Value
x of
> Left e :: EvalError
e -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left EvalError
e) (Nat' -> TValue -> TValue
tvSeq Nat'
n TValue
a)
> Right i :: Integer
i -> Nat' -> [Value] -> Value
VList Nat'
n (Nat' -> Value -> [Value] -> Integer -> [Value]
op Nat'
n (Either EvalError Bool -> TValue -> Value
logicNullary (Bool -> Either EvalError Bool
forall a b. b -> Either a b
Right Bool
False) TValue
a) (Value -> [Value]
fromVList Value
v) Integer
i)
>
> shiftLV :: Nat' -> Value -> [Value] -> Integer -> [Value]
> shiftLV :: Nat' -> Value -> [Value] -> Integer -> [Value]
shiftLV w :: Nat'
w z :: Value
z vs :: [Value]
vs i :: Integer
i =
> case Nat'
w of
> Nat n :: Integer
n -> Integer -> [Value] -> [Value]
forall i a. Integral i => i -> [a] -> [a]
genericDrop (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
n Integer
i) [Value]
vs [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
n Integer
i) Value
z
> Inf -> Integer -> [Value] -> [Value]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
i [Value]
vs
>
> shiftRV :: Nat' -> Value -> [Value] -> Integer -> [Value]
> shiftRV :: Nat' -> Value -> [Value] -> Integer -> [Value]
shiftRV w :: Nat'
w z :: Value
z vs :: [Value]
vs i :: Integer
i =
> case Nat'
w of
> Nat n :: Integer
n -> Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
n Integer
i) Value
z [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Integer -> [Value] -> [Value]
forall i a. Integral i => i -> [a] -> [a]
genericTake (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
n Integer
i) [Value]
vs
> Inf -> Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
i Value
z [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ [Value]
vs
>
> rotateV :: (Integer -> [Value] -> Integer -> [Value]) -> Value
> rotateV :: (Integer -> [Value] -> Integer -> [Value]) -> Value
rotateV op :: Integer -> [Value] -> Integer -> [Value]
op =
> (Integer -> Value) -> Value
vFinPoly ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Integer
n ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_ix :: Nat'
_ix ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x ->
> TValue -> Value -> Value
copyByTValue (Integer -> TValue -> TValue
TVSeq Integer
n TValue
a) (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVWord Value
x of
> Left e :: EvalError
e -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
n) (Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left EvalError
e) TValue
a))
> Right i :: Integer
i -> Nat' -> [Value] -> Value
VList (Integer -> Nat'
Nat Integer
n) (Integer -> [Value] -> Integer -> [Value]
op Integer
n (Value -> [Value]
fromVList Value
v) Integer
i)
>
> rotateLV :: Integer -> [Value] -> Integer -> [Value]
> rotateLV :: Integer -> [Value] -> Integer -> [Value]
rotateLV 0 vs :: [Value]
vs _ = [Value]
vs
> rotateLV w :: Integer
w vs :: [Value]
vs i :: Integer
i = [Value]
ys [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ [Value]
xs
> where (xs :: [Value]
xs, ys :: [Value]
ys) = Integer -> [Value] -> ([Value], [Value])
forall i a. Integral i => i -> [a] -> ([a], [a])
genericSplitAt (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
w) [Value]
vs
>
> rotateRV :: Integer -> [Value] -> Integer -> [Value]
> rotateRV :: Integer -> [Value] -> Integer -> [Value]
rotateRV 0 vs :: [Value]
vs _ = [Value]
vs
> rotateRV w :: Integer
w vs :: [Value]
vs i :: Integer
i = [Value]
ys [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ [Value]
xs
> where (xs :: [Value]
xs, ys :: [Value]
ys) = Integer -> [Value] -> ([Value], [Value])
forall i a. Integral i => i -> [a] -> ([a], [a])
genericSplitAt ((Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
w) [Value]
vs
>
> signedShiftRV :: Value
> signedShiftRV :: Value
signedShiftRV =
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_ix :: Nat'
_ix ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \v :: Value
v ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Value
x ->
> TValue -> Value -> Value
copyByTValue (Nat' -> TValue -> TValue
tvSeq Nat'
n TValue
TVBit) (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVWord Value
x of
> Left e :: EvalError
e -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left EvalError
e) (Nat' -> TValue -> TValue
tvSeq Nat'
n TValue
TVBit)
> Right i :: Integer
i -> Nat' -> [Value] -> Value
VList Nat'
n ([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$
> let vs :: [Value]
vs = Value -> [Value]
fromVList Value
v
> z :: Value
z = [Value] -> Value
forall a. [a] -> a
head [Value]
vs in
> case Nat'
n of
> Nat m :: Integer
m -> Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
m Integer
i) Value
z [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ Integer -> [Value] -> [Value]
forall i a. Integral i => i -> [a] -> [a]
genericTake (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
m Integer
i) [Value]
vs
> Inf -> Integer -> Value -> [Value]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
i Value
z [Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++ [Value]
vs
Indexing
Indexing operations are strict in all index bits, but as lazy as
possible in the list values. An index greater than or equal to the
length of the list produces a run-time error.
>
> indexPrimOne :: (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
> indexPrimOne :: (Nat' -> TValue -> [Value] -> Integer -> Value) -> Value
indexPrimOne op :: Nat' -> TValue -> [Value] -> Integer -> Value
op =
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_w :: Nat'
_w ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \l :: Value
l ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \r :: Value
r ->
> TValue -> Value -> Value
copyByTValue TValue
a (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVWord Value
r of
> Left e :: EvalError
e -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left EvalError
e) TValue
a
> Right i :: Integer
i -> Nat' -> TValue -> [Value] -> Integer -> Value
op Nat'
n TValue
a (Value -> [Value]
fromVList Value
l) Integer
i
>
> indexFront :: Nat' -> TValue -> [Value] -> Integer -> Value
> indexFront :: Nat' -> TValue -> [Value] -> Integer -> Value
indexFront w :: Nat'
w a :: TValue
a vs :: [Value]
vs ix :: Integer
ix =
> case Nat'
w of
> Nat n :: Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
ix -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left (Integer -> EvalError
InvalidIndex Integer
ix)) TValue
a
> _ -> [Value] -> Integer -> Value
forall i a. Integral i => [a] -> i -> a
genericIndex [Value]
vs Integer
ix
>
> indexBack :: Nat' -> TValue -> [Value] -> Integer -> Value
> indexBack :: Nat' -> TValue -> [Value] -> Integer -> Value
indexBack w :: Nat'
w a :: TValue
a vs :: [Value]
vs ix :: Integer
ix =
> case Nat'
w of
> Nat n :: Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
ix -> [Value] -> Integer -> Value
forall i a. Integral i => [a] -> i -> a
genericIndex [Value]
vs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
ix Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)
> | Bool
otherwise -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left (Integer -> EvalError
InvalidIndex Integer
ix)) TValue
a
> Inf -> String -> [String] -> Value
forall a. String -> [String] -> a
evalPanic "indexBack" ["unexpected infinite sequence"]
>
> updatePrim :: (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
> updatePrim :: (Nat' -> [Value] -> Integer -> Value -> [Value]) -> Value
updatePrim op :: Nat' -> [Value] -> Integer -> Value -> [Value]
op =
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \len :: Nat'
len ->
> (TValue -> Value) -> Value
VPoly ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \eltTy :: TValue
eltTy ->
> (Nat' -> Value) -> Value
VNumPoly ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \_idxLen :: Nat'
_idxLen ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \xs :: Value
xs ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \idx :: Value
idx ->
> (Value -> Value) -> Value
VFun ((Value -> Value) -> Value) -> (Value -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \val :: Value
val ->
> TValue -> Value -> Value
copyByTValue (Nat' -> TValue -> TValue
tvSeq Nat'
len TValue
eltTy) (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
> case Value -> Either EvalError Integer
fromVWord Value
idx of
> Left e :: EvalError
e -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left EvalError
e) (Nat' -> TValue -> TValue
tvSeq Nat'
len TValue
eltTy)
> Right i :: Integer
i
> | Integer -> Nat'
Nat Integer
i Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
< Nat'
len -> Nat' -> [Value] -> Value
VList Nat'
len (Nat' -> [Value] -> Integer -> Value -> [Value]
op Nat'
len (Value -> [Value]
fromVList Value
xs) Integer
i Value
val)
> | Bool
otherwise -> Either EvalError Bool -> TValue -> Value
logicNullary (EvalError -> Either EvalError Bool
forall a b. a -> Either a b
Left (Integer -> EvalError
InvalidIndex Integer
i)) (Nat' -> TValue -> TValue
tvSeq Nat'
len TValue
eltTy)
>
> updateFront :: Nat' -> [Value] -> Integer -> Value -> [Value]
> updateFront :: Nat' -> [Value] -> Integer -> Value -> [Value]
updateFront _ vs :: [Value]
vs i :: Integer
i x :: Value
x = [Value] -> Integer -> Value -> [Value]
forall a. [a] -> Integer -> a -> [a]
updateAt [Value]
vs Integer
i Value
x
>
> updateBack :: Nat' -> [Value] -> Integer -> Value -> [Value]
> updateBack :: Nat' -> [Value] -> Integer -> Value -> [Value]
updateBack Inf _vs :: [Value]
_vs _i :: Integer
_i _x :: Value
_x = String -> [String] -> [Value]
forall a. String -> [String] -> a
evalPanic "Unexpected infinite sequence in updateEnd" []
> updateBack (Nat n :: Integer
n) vs :: [Value]
vs i :: Integer
i x :: Value
x = [Value] -> Integer -> Value -> [Value]
forall a. [a] -> Integer -> a -> [a]
updateAt [Value]
vs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) Value
x
>
> updateAt :: [a] -> Integer -> a -> [a]
> updateAt :: [a] -> Integer -> a -> [a]
updateAt [] _ _ = []
> updateAt (_ : xs :: [a]
xs) 0 y :: a
y = a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
> updateAt (x :: a
x : xs :: [a]
xs) i :: Integer
i y :: a
y = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> Integer -> a -> [a]
forall a. [a] -> Integer -> a -> [a]
updateAt [a]
xs (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) a
y
Error Handling
The `evalPanic` function is only called if an internal data invariant
is violated, such as an expression that is not well-typed. Panics
should (hopefully) never occur in practice; a panic message indicates
a bug in Cryptol.
> evalPanic :: String -> [String] -> a
> evalPanic :: String -> [String] -> a
evalPanic cxt :: String
cxt = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic ("[Reference Evaluator]" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cxt)
Pretty Printing
> ppValue :: PPOpts -> Value -> Doc
> ppValue :: PPOpts -> Value -> Doc
ppValue opts :: PPOpts
opts val :: Value
val =
> case Value
val of
> VBit b :: Either EvalError Bool
b -> String -> Doc
text ((EvalError -> String)
-> (Bool -> String) -> Either EvalError Bool -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EvalError -> String
forall a. Show a => a -> String
show Bool -> String
forall a. Show a => a -> String
show Either EvalError Bool
b)
> VInteger i :: Either EvalError Integer
i -> String -> Doc
text ((EvalError -> String)
-> (Integer -> String) -> Either EvalError Integer -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EvalError -> String
forall a. Show a => a -> String
show Integer -> String
forall a. Show a => a -> String
show Either EvalError Integer
i)
> VList l :: Nat'
l vs :: [Value]
vs ->
> case Nat'
l of
> Inf -> [Doc] -> Doc
ppList ((Value -> Doc) -> [Value] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> Value -> Doc
ppValue PPOpts
opts) (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take (PPOpts -> Int
useInfLength PPOpts
opts) [Value]
vs) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text "..."])
> Nat n :: Integer
n ->
>
> case (Value -> Maybe Bool) -> [Value] -> Maybe [Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Maybe Bool
isBit [Value]
vs of
> Just bs :: [Bool]
bs -> PPOpts -> BV -> Doc
ppBV PPOpts
opts (Integer -> Integer -> BV
mkBv Integer
n ([Bool] -> Integer
bitsToInteger [Bool]
bs))
> Nothing -> [Doc] -> Doc
ppList ((Value -> Doc) -> [Value] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> Value -> Doc
ppValue PPOpts
opts) [Value]
vs)
> where ppList :: [Doc] -> Doc
ppList docs :: [Doc]
docs = Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
docs))
> isBit :: Value -> Maybe Bool
isBit v :: Value
v = case Value
v of VBit (Right b :: Bool
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
> _ -> Maybe Bool
forall a. Maybe a
Nothing
> VTuple vs :: [Value]
vs -> Doc -> Doc
parens ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Value -> Doc) -> [Value] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> Value -> Doc
ppValue PPOpts
opts) [Value]
vs)))
> VRecord fs :: [(Ident, Value)]
fs -> Doc -> Doc
braces ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (((Ident, Value) -> Doc) -> [(Ident, Value)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Doc
forall a. PP a => (a, Value) -> Doc
ppField [(Ident, Value)]
fs)))
> where ppField :: (a, Value) -> Doc
ppField (f :: a
f,r :: Value
r) = a -> Doc
forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char '=' Doc -> Doc -> Doc
<+> PPOpts -> Value -> Doc
ppValue PPOpts
opts Value
r
> VFun _ -> String -> Doc
text "<function>"
> VPoly _ -> String -> Doc
text "<polymorphic value>"
> VNumPoly _ -> String -> Doc
text "<polymorphic value>"
Module Command
This module implements the core functionality of the `:eval
<expression>` command for the Cryptol REPL, which prints the result of
running the reference evaluator on an expression.
> evaluate :: Expr -> M.ModuleCmd Value
> evaluate :: Expr -> ModuleCmd Value
evaluate expr :: Expr
expr (_,modEnv :: ModuleEnv
modEnv) = (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
-> IO (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Value, ModuleEnv) -> Either ModuleError (Value, ModuleEnv)
forall a b. b -> Either a b
Right (Env -> Expr -> Value
evalExpr Env
env Expr
expr, ModuleEnv
modEnv), [])
> where
> extDgs :: [DeclGroup]
extDgs = (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Module -> [DeclGroup]
mDecls (ModuleEnv -> [Module]
M.loadedModules ModuleEnv
modEnv)
> env :: Env
env = (Env -> DeclGroup -> Env) -> Env -> [DeclGroup] -> Env
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Env -> DeclGroup -> Env
evalDeclGroup Env
forall a. Monoid a => a
mempty [DeclGroup]
extDgs