module Michelson.Typed.Arith
( ArithOp (..)
, UnaryArithOp (..)
, ToIntArithOp (..)
, ArithError (..)
, ShiftArithErrorType (..)
, MutezArithErrorType (..)
, Add
, Sub
, Mul
, Abs
, Neg
, Or
, And
, Xor
, Not
, Lsl
, Lsr
, Compare
, Eq'
, Neq
, Lt
, Gt
, Le
, Ge
, compareOp
, Bls12381MulBadOrder
) where
import Data.Bits (complement, shift, (.&.), (.|.))
import Data.Constraint (Dict(..))
import Fmt (Buildable(build))
import Michelson.Typed.Annotation (AnnConvergeError, Notes(..), converge, convergeAnns, starNotes)
import Michelson.Typed.T (T(..))
import Michelson.Typed.Value (Comparable, Value'(..))
import Tezos.Core (addMutez, mulMutez, subMutez, timestampFromSeconds, timestampToSeconds)
import qualified Tezos.Crypto.BLS12381 as BLS
import Util.TypeLits
class (Typeable n, Typeable m) =>
ArithOp aop (n :: T) (m :: T) where
type ArithRes aop n m :: T
convergeArith
:: proxy aop
-> Notes n
-> Notes m
-> Either AnnConvergeError (Notes (ArithRes aop n m))
evalOp
:: proxy aop
-> Value' instr n
-> Value' instr m
-> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))
commutativityProof :: Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof = Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall a. Maybe a
Nothing
data ShiftArithErrorType
= LslOverflow
| LsrUnderflow
deriving stock (Int -> ShiftArithErrorType -> ShowS
[ShiftArithErrorType] -> ShowS
ShiftArithErrorType -> String
(Int -> ShiftArithErrorType -> ShowS)
-> (ShiftArithErrorType -> String)
-> ([ShiftArithErrorType] -> ShowS)
-> Show ShiftArithErrorType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShiftArithErrorType] -> ShowS
$cshowList :: [ShiftArithErrorType] -> ShowS
show :: ShiftArithErrorType -> String
$cshow :: ShiftArithErrorType -> String
showsPrec :: Int -> ShiftArithErrorType -> ShowS
$cshowsPrec :: Int -> ShiftArithErrorType -> ShowS
Show, ShiftArithErrorType -> ShiftArithErrorType -> Bool
(ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> Eq ShiftArithErrorType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c/= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
== :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c== :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
Eq, Eq ShiftArithErrorType
Eq ShiftArithErrorType
-> (ShiftArithErrorType -> ShiftArithErrorType -> Ordering)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType -> ShiftArithErrorType -> Bool)
-> (ShiftArithErrorType
-> ShiftArithErrorType -> ShiftArithErrorType)
-> (ShiftArithErrorType
-> ShiftArithErrorType -> ShiftArithErrorType)
-> Ord ShiftArithErrorType
ShiftArithErrorType -> ShiftArithErrorType -> Bool
ShiftArithErrorType -> ShiftArithErrorType -> Ordering
ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
$cmin :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
max :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
$cmax :: ShiftArithErrorType -> ShiftArithErrorType -> ShiftArithErrorType
>= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c>= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
> :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c> :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
<= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c<= :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
< :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
$c< :: ShiftArithErrorType -> ShiftArithErrorType -> Bool
compare :: ShiftArithErrorType -> ShiftArithErrorType -> Ordering
$ccompare :: ShiftArithErrorType -> ShiftArithErrorType -> Ordering
$cp1Ord :: Eq ShiftArithErrorType
Ord, (forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x)
-> (forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType)
-> Generic ShiftArithErrorType
forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType
forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ShiftArithErrorType x -> ShiftArithErrorType
$cfrom :: forall x. ShiftArithErrorType -> Rep ShiftArithErrorType x
Generic)
instance NFData ShiftArithErrorType
data MutezArithErrorType
= AddOverflow
| MulOverflow
| SubUnderflow
deriving stock (Int -> MutezArithErrorType -> ShowS
[MutezArithErrorType] -> ShowS
MutezArithErrorType -> String
(Int -> MutezArithErrorType -> ShowS)
-> (MutezArithErrorType -> String)
-> ([MutezArithErrorType] -> ShowS)
-> Show MutezArithErrorType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MutezArithErrorType] -> ShowS
$cshowList :: [MutezArithErrorType] -> ShowS
show :: MutezArithErrorType -> String
$cshow :: MutezArithErrorType -> String
showsPrec :: Int -> MutezArithErrorType -> ShowS
$cshowsPrec :: Int -> MutezArithErrorType -> ShowS
Show, MutezArithErrorType -> MutezArithErrorType -> Bool
(MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> Eq MutezArithErrorType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c/= :: MutezArithErrorType -> MutezArithErrorType -> Bool
== :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c== :: MutezArithErrorType -> MutezArithErrorType -> Bool
Eq, Eq MutezArithErrorType
Eq MutezArithErrorType
-> (MutezArithErrorType -> MutezArithErrorType -> Ordering)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType -> MutezArithErrorType -> Bool)
-> (MutezArithErrorType
-> MutezArithErrorType -> MutezArithErrorType)
-> (MutezArithErrorType
-> MutezArithErrorType -> MutezArithErrorType)
-> Ord MutezArithErrorType
MutezArithErrorType -> MutezArithErrorType -> Bool
MutezArithErrorType -> MutezArithErrorType -> Ordering
MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
$cmin :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
max :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
$cmax :: MutezArithErrorType -> MutezArithErrorType -> MutezArithErrorType
>= :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c>= :: MutezArithErrorType -> MutezArithErrorType -> Bool
> :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c> :: MutezArithErrorType -> MutezArithErrorType -> Bool
<= :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c<= :: MutezArithErrorType -> MutezArithErrorType -> Bool
< :: MutezArithErrorType -> MutezArithErrorType -> Bool
$c< :: MutezArithErrorType -> MutezArithErrorType -> Bool
compare :: MutezArithErrorType -> MutezArithErrorType -> Ordering
$ccompare :: MutezArithErrorType -> MutezArithErrorType -> Ordering
$cp1Ord :: Eq MutezArithErrorType
Ord, (forall x. MutezArithErrorType -> Rep MutezArithErrorType x)
-> (forall x. Rep MutezArithErrorType x -> MutezArithErrorType)
-> Generic MutezArithErrorType
forall x. Rep MutezArithErrorType x -> MutezArithErrorType
forall x. MutezArithErrorType -> Rep MutezArithErrorType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MutezArithErrorType x -> MutezArithErrorType
$cfrom :: forall x. MutezArithErrorType -> Rep MutezArithErrorType x
Generic)
instance NFData MutezArithErrorType
data ArithError n m
= MutezArithError MutezArithErrorType n m
| ShiftArithError ShiftArithErrorType n m
deriving stock (Int -> ArithError n m -> ShowS
[ArithError n m] -> ShowS
ArithError n m -> String
(Int -> ArithError n m -> ShowS)
-> (ArithError n m -> String)
-> ([ArithError n m] -> ShowS)
-> Show (ArithError n m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n m. (Show n, Show m) => Int -> ArithError n m -> ShowS
forall n m. (Show n, Show m) => [ArithError n m] -> ShowS
forall n m. (Show n, Show m) => ArithError n m -> String
showList :: [ArithError n m] -> ShowS
$cshowList :: forall n m. (Show n, Show m) => [ArithError n m] -> ShowS
show :: ArithError n m -> String
$cshow :: forall n m. (Show n, Show m) => ArithError n m -> String
showsPrec :: Int -> ArithError n m -> ShowS
$cshowsPrec :: forall n m. (Show n, Show m) => Int -> ArithError n m -> ShowS
Show, ArithError n m -> ArithError n m -> Bool
(ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> Eq (ArithError n m)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
/= :: ArithError n m -> ArithError n m -> Bool
$c/= :: forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
== :: ArithError n m -> ArithError n m -> Bool
$c== :: forall n m.
(Eq n, Eq m) =>
ArithError n m -> ArithError n m -> Bool
Eq, Eq (ArithError n m)
Eq (ArithError n m)
-> (ArithError n m -> ArithError n m -> Ordering)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> Bool)
-> (ArithError n m -> ArithError n m -> ArithError n m)
-> (ArithError n m -> ArithError n m -> ArithError n m)
-> Ord (ArithError n m)
ArithError n m -> ArithError n m -> Bool
ArithError n m -> ArithError n m -> Ordering
ArithError n m -> ArithError n m -> ArithError n m
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall n m. (Ord n, Ord m) => Eq (ArithError n m)
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Ordering
forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
min :: ArithError n m -> ArithError n m -> ArithError n m
$cmin :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
max :: ArithError n m -> ArithError n m -> ArithError n m
$cmax :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> ArithError n m
>= :: ArithError n m -> ArithError n m -> Bool
$c>= :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
> :: ArithError n m -> ArithError n m -> Bool
$c> :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
<= :: ArithError n m -> ArithError n m -> Bool
$c<= :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
< :: ArithError n m -> ArithError n m -> Bool
$c< :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Bool
compare :: ArithError n m -> ArithError n m -> Ordering
$ccompare :: forall n m.
(Ord n, Ord m) =>
ArithError n m -> ArithError n m -> Ordering
$cp1Ord :: forall n m. (Ord n, Ord m) => Eq (ArithError n m)
Ord, (forall x. ArithError n m -> Rep (ArithError n m) x)
-> (forall x. Rep (ArithError n m) x -> ArithError n m)
-> Generic (ArithError n m)
forall x. Rep (ArithError n m) x -> ArithError n m
forall x. ArithError n m -> Rep (ArithError n m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n m x. Rep (ArithError n m) x -> ArithError n m
forall n m x. ArithError n m -> Rep (ArithError n m) x
$cto :: forall n m x. Rep (ArithError n m) x -> ArithError n m
$cfrom :: forall n m x. ArithError n m -> Rep (ArithError n m) x
Generic)
instance (NFData n, NFData m) => NFData (ArithError n m)
class UnaryArithOp aop (n :: T) where
type UnaryArithRes aop n :: T
evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
class ToIntArithOp (n :: T) where
evalToIntOp :: Value' instr n -> Value' instr 'TInt
data Add
data Sub
data Mul
data Abs
data Neg
data Or
data And
data Xor
data Not
data Lsl
data Lsr
data Compare
data Eq'
data Neq
data Lt
data Gt
data Le
data Ge
instance ArithOp Add 'TNat 'TInt where
type ArithRes Add 'TNat 'TInt = 'TInt
convergeArith :: proxy Add
-> Notes 'TNat
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TInt))
convergeArith proxy Add
_ Notes 'TNat
_ Notes 'TInt
n2 = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n2
evalOp :: proxy Add
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr (ArithRes Add 'TNat 'TInt))
evalOp proxy Add
_ (VNat Natural
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TNat 'TInt ~ ArithRes Add 'TInt 'TNat,
ArithOp Add 'TInt 'TNat)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TNat where
type ArithRes Add 'TInt 'TNat = 'TInt
convergeArith :: proxy Add
-> Notes 'TInt
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TNat))
convergeArith proxy Add
_ Notes 'TInt
n1 Notes 'TNat
_ = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n1
evalOp :: proxy Add
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr (ArithRes Add 'TInt 'TNat))
evalOp proxy Add
_ (VInt Integer
i) (VNat Natural
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TInt 'TNat ~ ArithRes Add 'TNat 'TInt,
ArithOp Add 'TNat 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TNat 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TNat 'TNat where
type ArithRes Add 'TNat 'TNat = 'TNat
convergeArith :: proxy Add
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Add 'TNat 'TNat))
convergeArith proxy Add
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Add
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Add 'TNat 'TNat))
evalOp proxy Add
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TNat 'TNat ~ ArithRes Add 'TNat 'TNat,
ArithOp Add 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Add 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TInt where
type ArithRes Add 'TInt 'TInt = 'TInt
convergeArith :: proxy Add
-> Notes 'TInt
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TInt))
convergeArith proxy Add
_ Notes 'TInt
n1 Notes 'TInt
n2 = Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TInt
n1 Notes 'TInt
n2
evalOp :: proxy Add
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr (ArithRes Add 'TInt 'TInt))
evalOp proxy Add
_ (VInt Integer
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TInt 'TInt ~ ArithRes Add 'TInt 'TInt,
ArithOp Add 'TInt 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Add 'TInt 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TTimestamp 'TInt where
type ArithRes Add 'TTimestamp 'TInt = 'TTimestamp
convergeArith :: proxy Add
-> Notes 'TTimestamp
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Add 'TTimestamp 'TInt))
convergeArith proxy Add
_ Notes 'TTimestamp
n1 Notes 'TInt
_ = Notes 'TTimestamp -> Either AnnConvergeError (Notes 'TTimestamp)
forall a b. b -> Either a b
Right Notes 'TTimestamp
n1
evalOp :: proxy Add
-> Value' instr 'TTimestamp
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr (ArithRes Add 'TTimestamp 'TInt))
evalOp proxy Add
_ (VTimestamp Timestamp
i) (VInt Integer
j) =
Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp)
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp))
-> Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TTimestamp 'TInt ~ ArithRes Add 'TInt 'TTimestamp,
ArithOp Add 'TInt 'TTimestamp)
commutativityProof = Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)
-> Maybe
(Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp))
forall a. a -> Maybe a
Just Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TInt 'TTimestamp)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TInt 'TTimestamp where
type ArithRes Add 'TInt 'TTimestamp = 'TTimestamp
convergeArith :: proxy Add
-> Notes 'TInt
-> Notes 'TTimestamp
-> Either AnnConvergeError (Notes (ArithRes Add 'TInt 'TTimestamp))
convergeArith proxy Add
_ Notes 'TInt
_ Notes 'TTimestamp
n2 = Notes 'TTimestamp -> Either AnnConvergeError (Notes 'TTimestamp)
forall a b. b -> Either a b
Right Notes 'TTimestamp
n2
evalOp :: proxy Add
-> Value' instr 'TInt
-> Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
(Value' instr (ArithRes Add 'TInt 'TTimestamp))
evalOp proxy Add
_ (VInt Integer
i) (VTimestamp Timestamp
j) =
Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
(Value' instr 'TTimestamp)
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
(Value' instr 'TTimestamp))
-> Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
(Value' instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TInt 'TTimestamp ~ ArithRes Add 'TTimestamp 'TInt,
ArithOp Add 'TTimestamp 'TInt)
commutativityProof = Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt)
-> Maybe
(Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt))
forall a. a -> Maybe a
Just Dict ('TTimestamp ~ 'TTimestamp, ArithOp Add 'TTimestamp 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TMutez 'TMutez where
type ArithRes Add 'TMutez 'TMutez = 'TMutez
convergeArith :: proxy Add
-> Notes 'TMutez
-> Notes 'TMutez
-> Either AnnConvergeError (Notes (ArithRes Add 'TMutez 'TMutez))
convergeArith proxy Add
_ Notes 'TMutez
n1 Notes 'TMutez
n2 = Notes 'TMutez
-> Notes 'TMutez -> Either AnnConvergeError (Notes 'TMutez)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TMutez
n1 Notes 'TMutez
n2
evalOp :: proxy Add
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr (ArithRes Add 'TMutez 'TMutez))
evalOp proxy Add
_ n :: Value' instr 'TMutez
n@(VMutez Mutez
i) m :: Value' instr 'TMutez
m@(VMutez Mutez
j) = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr (ArithRes Add 'TMutez 'TMutez))
res
where
res :: Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
res = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
-> (Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
AddOverflow Value' instr 'TMutez
n Value' instr 'TMutez
m) (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Mutez -> Maybe Mutez
`addMutez` Mutez
j
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TMutez 'TMutez ~ ArithRes Add 'TMutez 'TMutez,
ArithOp Add 'TMutez 'TMutez)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Add 'TMutez 'TMutez)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381Fr 'TBls12381Fr where
type ArithRes Add 'TBls12381Fr 'TBls12381Fr = 'TBls12381Fr
convergeArith :: proxy Add
-> Notes 'TBls12381Fr
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Add 'TBls12381Fr 'TBls12381Fr))
convergeArith proxy Add
_ Notes 'TBls12381Fr
n1 Notes 'TBls12381Fr
n2 = Notes 'TBls12381Fr
-> Notes 'TBls12381Fr
-> Either AnnConvergeError (Notes 'TBls12381Fr)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBls12381Fr
n1 Notes 'TBls12381Fr
n2
evalOp :: proxy Add
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Add 'TBls12381Fr 'TBls12381Fr))
evalOp proxy Add
_ (VBls12381Fr Bls12381Fr
i) (VBls12381Fr Bls12381Fr
j) =
Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381Fr
i Bls12381Fr
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TBls12381Fr 'TBls12381Fr
~ ArithRes Add 'TBls12381Fr 'TBls12381Fr,
ArithOp Add 'TBls12381Fr 'TBls12381Fr)
commutativityProof = Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Add 'TBls12381Fr 'TBls12381Fr)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Add 'TBls12381Fr 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Add 'TBls12381Fr 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381G1 'TBls12381G1 where
type ArithRes Add 'TBls12381G1 'TBls12381G1 = 'TBls12381G1
convergeArith :: proxy Add
-> Notes 'TBls12381G1
-> Notes 'TBls12381G1
-> Either
AnnConvergeError (Notes (ArithRes Add 'TBls12381G1 'TBls12381G1))
convergeArith proxy Add
_ Notes 'TBls12381G1
n1 Notes 'TBls12381G1
n2 = Notes 'TBls12381G1
-> Notes 'TBls12381G1
-> Either AnnConvergeError (Notes 'TBls12381G1)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBls12381G1
n1 Notes 'TBls12381G1
n2
evalOp :: proxy Add
-> Value' instr 'TBls12381G1
-> Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
(Value' instr (ArithRes Add 'TBls12381G1 'TBls12381G1))
evalOp proxy Add
_ (VBls12381G1 Bls12381G1
i) (VBls12381G1 Bls12381G1
j) =
Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
(Value' instr 'TBls12381G1)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
(Value' instr 'TBls12381G1))
-> Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381G1))
(Value' instr 'TBls12381G1)
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381G1 -> Bls12381G1 -> Bls12381G1
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381G1
i Bls12381G1
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TBls12381G1 'TBls12381G1
~ ArithRes Add 'TBls12381G1 'TBls12381G1,
ArithOp Add 'TBls12381G1 'TBls12381G1)
commutativityProof = Dict
('TBls12381G1 ~ 'TBls12381G1,
ArithOp Add 'TBls12381G1 'TBls12381G1)
-> Maybe
(Dict
('TBls12381G1 ~ 'TBls12381G1,
ArithOp Add 'TBls12381G1 'TBls12381G1))
forall a. a -> Maybe a
Just Dict
('TBls12381G1 ~ 'TBls12381G1,
ArithOp Add 'TBls12381G1 'TBls12381G1)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Add 'TBls12381G2 'TBls12381G2 where
type ArithRes Add 'TBls12381G2 'TBls12381G2 = 'TBls12381G2
convergeArith :: proxy Add
-> Notes 'TBls12381G2
-> Notes 'TBls12381G2
-> Either
AnnConvergeError (Notes (ArithRes Add 'TBls12381G2 'TBls12381G2))
convergeArith proxy Add
_ Notes 'TBls12381G2
n1 Notes 'TBls12381G2
n2 = Notes 'TBls12381G2
-> Notes 'TBls12381G2
-> Either AnnConvergeError (Notes 'TBls12381G2)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBls12381G2
n1 Notes 'TBls12381G2
n2
evalOp :: proxy Add
-> Value' instr 'TBls12381G2
-> Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
(Value' instr (ArithRes Add 'TBls12381G2 'TBls12381G2))
evalOp proxy Add
_ (VBls12381G2 Bls12381G2
i) (VBls12381G2 Bls12381G2
j) =
Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
(Value' instr 'TBls12381G2)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
(Value' instr 'TBls12381G2))
-> Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381G2))
(Value' instr 'TBls12381G2)
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381G2 -> Bls12381G2 -> Bls12381G2
forall a. CurveObject a => a -> a -> a
BLS.add Bls12381G2
i Bls12381G2
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Add 'TBls12381G2 'TBls12381G2
~ ArithRes Add 'TBls12381G2 'TBls12381G2,
ArithOp Add 'TBls12381G2 'TBls12381G2)
commutativityProof = Dict
('TBls12381G2 ~ 'TBls12381G2,
ArithOp Add 'TBls12381G2 'TBls12381G2)
-> Maybe
(Dict
('TBls12381G2 ~ 'TBls12381G2,
ArithOp Add 'TBls12381G2 'TBls12381G2))
forall a. a -> Maybe a
Just Dict
('TBls12381G2 ~ 'TBls12381G2,
ArithOp Add 'TBls12381G2 'TBls12381G2)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Sub 'TNat 'TInt where
type ArithRes Sub 'TNat 'TInt = 'TInt
convergeArith :: proxy Sub
-> Notes 'TNat
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TInt))
convergeArith proxy Sub
_ Notes 'TNat
_ Notes 'TInt
n2 = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n2
evalOp :: proxy Sub
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr (ArithRes Sub 'TNat 'TInt))
evalOp proxy Sub
_ (VNat Natural
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j)
instance ArithOp Sub 'TInt 'TNat where
type ArithRes Sub 'TInt 'TNat = 'TInt
convergeArith :: proxy Sub
-> Notes 'TInt
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TNat))
convergeArith proxy Sub
_ Notes 'TInt
n1 Notes 'TNat
_ = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n1
evalOp :: proxy Sub
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr (ArithRes Sub 'TInt 'TNat))
evalOp proxy Sub
_ (VInt Integer
i) (VNat Natural
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
instance ArithOp Sub 'TNat 'TNat where
type ArithRes Sub 'TNat 'TNat = 'TInt
convergeArith :: proxy Sub
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TNat))
convergeArith proxy Sub
_ Notes 'TNat
n1 Notes 'TNat
n2 = (Notes 'TInt -> Notes 'TNat -> Notes 'TInt
forall a b. a -> b -> a
const Notes 'TInt
forall (t :: T). SingI t => Notes t
starNotes) (Notes 'TNat -> Notes 'TInt)
-> Either AnnConvergeError (Notes 'TNat)
-> Either AnnConvergeError (Notes 'TInt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Sub
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Sub 'TNat 'TNat))
evalOp proxy Sub
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
instance ArithOp Sub 'TInt 'TInt where
type ArithRes Sub 'TInt 'TInt = 'TInt
convergeArith :: proxy Sub
-> Notes 'TInt
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Sub 'TInt 'TInt))
convergeArith proxy Sub
_ Notes 'TInt
n1 Notes 'TInt
n2 = Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TInt
n1 Notes 'TInt
n2
evalOp :: proxy Sub
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr (ArithRes Sub 'TInt 'TInt))
evalOp proxy Sub
_ (VInt Integer
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j)
instance ArithOp Sub 'TTimestamp 'TInt where
type ArithRes Sub 'TTimestamp 'TInt = 'TTimestamp
convergeArith :: proxy Sub
-> Notes 'TTimestamp
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TInt))
convergeArith proxy Sub
_ Notes 'TTimestamp
n1 Notes 'TInt
_ = Notes 'TTimestamp -> Either AnnConvergeError (Notes 'TTimestamp)
forall a b. b -> Either a b
Right Notes 'TTimestamp
n1
evalOp :: proxy Sub
-> Value' instr 'TTimestamp
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr (ArithRes Sub 'TTimestamp 'TInt))
evalOp proxy Sub
_ (VTimestamp Timestamp
i) (VInt Integer
j) =
Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp)
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp))
-> Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
(Value' instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' instr 'TTimestamp)
-> Timestamp -> Value' instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds (Integer -> Timestamp) -> Integer -> Timestamp
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
instance ArithOp Sub 'TTimestamp 'TTimestamp where
type ArithRes Sub 'TTimestamp 'TTimestamp = 'TInt
convergeArith :: proxy Sub
-> Notes 'TTimestamp
-> Notes 'TTimestamp
-> Either
AnnConvergeError (Notes (ArithRes Sub 'TTimestamp 'TTimestamp))
convergeArith proxy Sub
_ (NTTimestamp TypeAnn
a) (NTTimestamp TypeAnn
b) = TypeAnn -> Notes 'TInt
NTInt (TypeAnn -> Notes 'TInt)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TInt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b)
evalOp :: proxy Sub
-> Value' instr 'TTimestamp
-> Value' instr 'TTimestamp
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
(Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
evalOp proxy Sub
_ (VTimestamp Timestamp
i) (VTimestamp Timestamp
j) =
Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Value' instr 'TInt) -> Integer -> Value' instr 'TInt
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
j
instance ArithOp Sub 'TMutez 'TMutez where
type ArithRes Sub 'TMutez 'TMutez = 'TMutez
convergeArith :: proxy Sub
-> Notes 'TMutez
-> Notes 'TMutez
-> Either AnnConvergeError (Notes (ArithRes Sub 'TMutez 'TMutez))
convergeArith proxy Sub
_ Notes 'TMutez
n1 Notes 'TMutez
n2 = Notes 'TMutez
-> Notes 'TMutez -> Either AnnConvergeError (Notes 'TMutez)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TMutez
n1 Notes 'TMutez
n2
evalOp :: proxy Sub
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr (ArithRes Sub 'TMutez 'TMutez))
evalOp proxy Sub
_ n :: Value' instr 'TMutez
n@(VMutez Mutez
i) m :: Value' instr 'TMutez
m@(VMutez Mutez
j) = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr (ArithRes Sub 'TMutez 'TMutez))
res
where
res :: Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
res = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
-> (Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TMutez
-> Value' instr 'TMutez
-> ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
SubUnderflow Value' instr 'TMutez
n Value' instr 'TMutez
m) (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Mutez -> Maybe Mutez
`subMutez` Mutez
j
instance ArithOp Mul 'TNat 'TInt where
type ArithRes Mul 'TNat 'TInt = 'TInt
convergeArith :: proxy Mul
-> Notes 'TNat
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TInt))
convergeArith proxy Mul
_ Notes 'TNat
_ Notes 'TInt
n2 = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n2
evalOp :: proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr (ArithRes Mul 'TNat 'TInt))
evalOp proxy Mul
_ (VNat Natural
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TNat 'TInt ~ ArithRes Mul 'TInt 'TNat,
ArithOp Mul 'TInt 'TNat)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TNat where
type ArithRes Mul 'TInt 'TNat = 'TInt
convergeArith :: proxy Mul
-> Notes 'TInt
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TNat))
convergeArith proxy Mul
_ Notes 'TInt
n1 Notes 'TNat
_ = Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall a b. b -> Either a b
Right Notes 'TInt
n1
evalOp :: proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr (ArithRes Mul 'TInt 'TNat))
evalOp proxy Mul
_ (VInt Integer
i) (VNat Natural
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TInt 'TNat ~ ArithRes Mul 'TNat 'TInt,
ArithOp Mul 'TNat 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TNat 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TNat where
type ArithRes Mul 'TNat 'TNat = 'TNat
convergeArith :: proxy Mul
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TNat))
convergeArith proxy Mul
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Mul 'TNat 'TNat))
evalOp proxy Mul
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TNat 'TNat ~ ArithRes Mul 'TNat 'TNat,
ArithOp Mul 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Mul 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TInt where
type ArithRes Mul 'TInt 'TInt = 'TInt
convergeArith :: proxy Mul
-> Notes 'TInt
-> Notes 'TInt
-> Either AnnConvergeError (Notes (ArithRes Mul 'TInt 'TInt))
convergeArith proxy Mul
_ Notes 'TInt
n1 Notes 'TInt
n2 = Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TInt
n1 Notes 'TInt
n2
evalOp :: proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr (ArithRes Mul 'TInt 'TInt))
evalOp proxy Mul
_ (VInt Integer
i) (VInt Integer
j) = Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. b -> Either a b
Right (Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt))
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TInt))
(Value' instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TInt 'TInt ~ ArithRes Mul 'TInt 'TInt,
ArithOp Mul 'TInt 'TInt)
commutativityProof = Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt)
-> Maybe (Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt))
forall a. a -> Maybe a
Just Dict ('TInt ~ 'TInt, ArithOp Mul 'TInt 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TMutez where
type ArithRes Mul 'TNat 'TMutez = 'TMutez
convergeArith :: proxy Mul
-> Notes 'TNat
-> Notes 'TMutez
-> Either AnnConvergeError (Notes (ArithRes Mul 'TNat 'TMutez))
convergeArith proxy Mul
_ Notes 'TNat
_ Notes 'TMutez
n2 = Notes 'TMutez -> Either AnnConvergeError (Notes 'TMutez)
forall a b. b -> Either a b
Right Notes 'TMutez
n2
evalOp :: proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr (ArithRes Mul 'TNat 'TMutez))
evalOp proxy Mul
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TMutez
m@(VMutez Mutez
j) = Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr (ArithRes Mul 'TNat 'TMutez))
res
where
res :: Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
res = Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
-> (Mutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TMutez
-> ArithError (Value' instr 'TNat) (Value' instr 'TMutez)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
MulOverflow Value' instr 'TNat
n Value' instr 'TMutez
m) (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TMutez))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
j Mutez -> Natural -> Maybe Mutez
forall a. Integral a => Mutez -> a -> Maybe Mutez
`mulMutez` Natural
i
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TNat 'TMutez ~ ArithRes Mul 'TMutez 'TNat,
ArithOp Mul 'TMutez 'TNat)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TMutez 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TMutez 'TNat where
type ArithRes Mul 'TMutez 'TNat = 'TMutez
convergeArith :: proxy Mul
-> Notes 'TMutez
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Mul 'TMutez 'TNat))
convergeArith proxy Mul
_ Notes 'TMutez
n1 Notes 'TNat
_ = Notes 'TMutez -> Either AnnConvergeError (Notes 'TMutez)
forall a b. b -> Either a b
Right Notes 'TMutez
n1
evalOp :: proxy Mul
-> Value' instr 'TMutez
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr (ArithRes Mul 'TMutez 'TNat))
evalOp proxy Mul
_ n :: Value' instr 'TMutez
n@(VMutez Mutez
i) m :: Value' instr 'TNat
m@(VNat Natural
j) = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr (ArithRes Mul 'TMutez 'TNat))
res
where
res :: Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
res = Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
-> (Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez))
-> ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ MutezArithErrorType
-> Value' instr 'TMutez
-> Value' instr 'TNat
-> ArithError (Value' instr 'TMutez) (Value' instr 'TNat)
forall n m. MutezArithErrorType -> n -> m -> ArithError n m
MutezArithError MutezArithErrorType
MulOverflow Value' instr 'TMutez
n Value' instr 'TNat
m) (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall a b. b -> Either a b
Right (Value' instr 'TMutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez))
-> (Mutez -> Value' instr 'TMutez)
-> Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez) (Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez))
-> Maybe Mutez
-> Either
(ArithError (Value' instr 'TMutez) (Value' instr 'TNat))
(Value' instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez
i Mutez -> Natural -> Maybe Mutez
forall a. Integral a => Mutez -> a -> Maybe Mutez
`mulMutez` Natural
j
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TMutez 'TNat ~ ArithRes Mul 'TNat 'TMutez,
ArithOp Mul 'TNat 'TMutez)
commutativityProof = Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez)
-> Maybe (Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez))
forall a. a -> Maybe a
Just Dict ('TMutez ~ 'TMutez, ArithOp Mul 'TNat 'TMutez)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TInt 'TBls12381Fr where
type ArithRes Mul 'TInt 'TBls12381Fr = 'TBls12381Fr
convergeArith :: proxy Mul
-> Notes 'TInt
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TInt 'TBls12381Fr))
convergeArith proxy Mul
_ (NTInt TypeAnn
n1) Notes 'TBls12381Fr
_ = Notes 'TBls12381Fr -> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. b -> Either a b
Right (Notes 'TBls12381Fr
-> Either AnnConvergeError (Notes 'TBls12381Fr))
-> Notes 'TBls12381Fr
-> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ (TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
n1)
evalOp :: proxy Mul
-> Value' instr 'TInt
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Mul 'TInt 'TBls12381Fr))
evalOp proxy Mul
_ (VInt Integer
i) (VBls12381Fr Bls12381Fr
j) = Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Integer -> Bls12381Fr
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TInt 'TBls12381Fr ~ ArithRes Mul 'TBls12381Fr 'TInt,
ArithOp Mul 'TBls12381Fr 'TInt)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TInt)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TNat 'TBls12381Fr where
type ArithRes Mul 'TNat 'TBls12381Fr = 'TBls12381Fr
convergeArith :: proxy Mul
-> Notes 'TNat
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TNat 'TBls12381Fr))
convergeArith proxy Mul
_ (NTNat TypeAnn
n1) Notes 'TBls12381Fr
_ = Notes 'TBls12381Fr -> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. b -> Either a b
Right (TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
n1)
evalOp :: proxy Mul
-> Value' instr 'TNat
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Mul 'TNat 'TBls12381Fr))
evalOp proxy Mul
_ (VNat Natural
i) (VBls12381Fr Bls12381Fr
j) = Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Natural -> Bls12381Fr
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TNat 'TBls12381Fr ~ ArithRes Mul 'TBls12381Fr 'TNat,
ArithOp Mul 'TBls12381Fr 'TNat)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TBls12381Fr 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TInt where
type ArithRes Mul 'TBls12381Fr 'TInt = 'TBls12381Fr
convergeArith :: proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TInt
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381Fr 'TInt))
convergeArith proxy Mul
_ Notes 'TBls12381Fr
n1 Notes 'TInt
_ = Notes 'TBls12381Fr -> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. b -> Either a b
Right Notes 'TBls12381Fr
n1
evalOp :: proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TInt
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
(Value' instr (ArithRes Mul 'TBls12381Fr 'TInt))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VInt Integer
j) = Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TInt))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Integer -> Bls12381Fr
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381Fr 'TInt ~ ArithRes Mul 'TInt 'TBls12381Fr,
ArithOp Mul 'TInt 'TBls12381Fr)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TInt 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TNat where
type ArithRes Mul 'TBls12381Fr 'TNat = 'TBls12381Fr
convergeArith :: proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TNat
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381Fr 'TNat))
convergeArith proxy Mul
_ Notes 'TBls12381Fr
n1 Notes 'TNat
_ = Notes 'TBls12381Fr -> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. b -> Either a b
Right Notes 'TBls12381Fr
n1
evalOp :: proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
(Value' instr (ArithRes Mul 'TBls12381Fr 'TNat))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VNat Natural
j) = Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError (Value' instr 'TBls12381Fr) (Value' instr 'TNat))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Natural -> Bls12381Fr
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381Fr 'TNat ~ ArithRes Mul 'TNat 'TBls12381Fr,
ArithOp Mul 'TNat 'TBls12381Fr)
commutativityProof = Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict ('TBls12381Fr ~ 'TBls12381Fr, ArithOp Mul 'TNat 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381Fr 'TBls12381Fr where
type ArithRes Mul 'TBls12381Fr 'TBls12381Fr = 'TBls12381Fr
convergeArith :: proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381Fr 'TBls12381Fr))
convergeArith proxy Mul
_ Notes 'TBls12381Fr
n1 Notes 'TBls12381Fr
_ = Notes 'TBls12381Fr -> Either AnnConvergeError (Notes 'TBls12381Fr)
forall a b. b -> Either a b
Right Notes 'TBls12381Fr
n1
evalOp :: proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381Fr Bls12381Fr
i) (VBls12381Fr Bls12381Fr
j) = Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr))
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr
i Bls12381Fr -> Bls12381Fr -> Bls12381Fr
forall a. Num a => a -> a -> a
* Bls12381Fr
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381Fr 'TBls12381Fr
~ ArithRes Mul 'TBls12381Fr 'TBls12381Fr,
ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
commutativityProof = Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
-> Maybe
(Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Mul 'TBls12381Fr 'TBls12381Fr))
forall a. a -> Maybe a
Just Dict
('TBls12381Fr ~ 'TBls12381Fr,
ArithOp Mul 'TBls12381Fr 'TBls12381Fr)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Mul 'TBls12381G1 'TBls12381Fr where
type ArithRes Mul 'TBls12381G1 'TBls12381Fr = 'TBls12381G1
convergeArith :: proxy Mul
-> Notes 'TBls12381G1
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381G1 'TBls12381Fr))
convergeArith proxy Mul
_ Notes 'TBls12381G1
n1 Notes 'TBls12381Fr
_ = Notes 'TBls12381G1 -> Either AnnConvergeError (Notes 'TBls12381G1)
forall a b. b -> Either a b
Right Notes 'TBls12381G1
n1
evalOp :: proxy Mul
-> Value' instr 'TBls12381G1
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Mul 'TBls12381G1 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381G1 Bls12381G1
i) (VBls12381Fr Bls12381Fr
j) = Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G1)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G1))
-> Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381G1) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G1)
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381Fr -> Bls12381G1 -> Bls12381G1
forall scalar point.
MultiplyPoint scalar point =>
scalar -> point -> point
BLS.multiply Bls12381Fr
j Bls12381G1
i)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381G1 'TBls12381Fr
~ ArithRes Mul 'TBls12381Fr 'TBls12381G1,
ArithOp Mul 'TBls12381Fr 'TBls12381G1)
commutativityProof = Maybe
$ Dict
(ArithRes Mul 'TBls12381G1 'TBls12381Fr
~ ArithRes Mul 'TBls12381Fr 'TBls12381G1,
ArithOp Mul 'TBls12381Fr 'TBls12381G1)
forall a. Maybe a
Nothing
instance ArithOp Mul 'TBls12381G2 'TBls12381Fr where
type ArithRes Mul 'TBls12381G2 'TBls12381Fr = 'TBls12381G2
convergeArith :: proxy Mul
-> Notes 'TBls12381G2
-> Notes 'TBls12381Fr
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381G2 'TBls12381Fr))
convergeArith proxy Mul
_ Notes 'TBls12381G2
n1 Notes 'TBls12381Fr
_ = Notes 'TBls12381G2 -> Either AnnConvergeError (Notes 'TBls12381G2)
forall a b. b -> Either a b
Right Notes 'TBls12381G2
n1
evalOp :: proxy Mul
-> Value' instr 'TBls12381G2
-> Value' instr 'TBls12381Fr
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
(Value' instr (ArithRes Mul 'TBls12381G2 'TBls12381Fr))
evalOp proxy Mul
_ (VBls12381G2 Bls12381G2
i) (VBls12381Fr Bls12381Fr
j) = Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G2)
forall a b. b -> Either a b
Right (Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G2))
-> Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381G2) (Value' instr 'TBls12381Fr))
(Value' instr 'TBls12381G2)
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381Fr -> Bls12381G2 -> Bls12381G2
forall scalar point.
MultiplyPoint scalar point =>
scalar -> point -> point
BLS.multiply Bls12381Fr
j Bls12381G2
i)
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381G2 'TBls12381Fr
~ ArithRes Mul 'TBls12381Fr 'TBls12381G2,
ArithOp Mul 'TBls12381Fr 'TBls12381G2)
commutativityProof = Maybe
$ Dict
(ArithRes Mul 'TBls12381G2 'TBls12381Fr
~ ArithRes Mul 'TBls12381Fr 'TBls12381G2,
ArithOp Mul 'TBls12381Fr 'TBls12381G2)
forall a. Maybe a
Nothing
instance Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G1 =>
ArithOp Mul 'TBls12381Fr 'TBls12381G1 where
type ArithRes Mul 'TBls12381Fr 'TBls12381G1 = 'TBls12381G1
convergeArith :: proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TBls12381G1
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381Fr 'TBls12381G1))
convergeArith = Text
-> proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TBls12381G1
-> Either AnnConvergeError (Notes 'TBls12381G1)
forall a. HasCallStack => Text -> a
error Text
"impossible"
evalOp :: proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G1))
(Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G1))
evalOp = Text
-> proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G1
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G1))
(Value' instr 'TBls12381G1)
forall a. HasCallStack => Text -> a
error Text
"impossible"
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381Fr 'TBls12381G1
~ ArithRes Mul 'TBls12381G1 'TBls12381Fr,
ArithOp Mul 'TBls12381G1 'TBls12381Fr)
commutativityProof = Text
-> Maybe
(Dict
('TBls12381G1 ~ 'TBls12381G1,
ArithOp Mul 'TBls12381G1 'TBls12381Fr))
forall a. HasCallStack => Text -> a
error Text
"impossible"
instance Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G2 =>
ArithOp Mul 'TBls12381Fr 'TBls12381G2 where
type ArithRes Mul 'TBls12381Fr 'TBls12381G2 = 'TBls12381G2
convergeArith :: proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TBls12381G2
-> Either
AnnConvergeError (Notes (ArithRes Mul 'TBls12381Fr 'TBls12381G2))
convergeArith = Text
-> proxy Mul
-> Notes 'TBls12381Fr
-> Notes 'TBls12381G2
-> Either AnnConvergeError (Notes 'TBls12381G2)
forall a. HasCallStack => Text -> a
error Text
"impossible"
evalOp :: proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G2))
(Value' instr (ArithRes Mul 'TBls12381Fr 'TBls12381G2))
evalOp = Text
-> proxy Mul
-> Value' instr 'TBls12381Fr
-> Value' instr 'TBls12381G2
-> Either
(ArithError
(Value' instr 'TBls12381Fr) (Value' instr 'TBls12381G2))
(Value' instr 'TBls12381G2)
forall a. HasCallStack => Text -> a
error Text
"impossible"
commutativityProof :: Maybe
$ Dict
(ArithRes Mul 'TBls12381Fr 'TBls12381G2
~ ArithRes Mul 'TBls12381G2 'TBls12381Fr,
ArithOp Mul 'TBls12381G2 'TBls12381Fr)
commutativityProof = Text
-> Maybe
(Dict
('TBls12381G2 ~ 'TBls12381G2,
ArithOp Mul 'TBls12381G2 'TBls12381Fr))
forall a. HasCallStack => Text -> a
error Text
"impossible"
type family Bls12381MulBadOrder a1 a2 where
Bls12381MulBadOrder a1 a2 = TypeError
('Text "Multiplication of "
':<>: 'ShowType a2 ':<>: 'Text " and "
':<>: 'ShowType a1 ':<>: 'Text " works only other way around"
)
instance UnaryArithOp Abs 'TInt where
type UnaryArithRes Abs 'TInt = 'TNat
evalUnaryArithOp :: proxy Abs
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Abs 'TInt)
evalUnaryArithOp proxy Abs
_ (VInt Integer
i) = Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
i)
instance UnaryArithOp Neg 'TInt where
type UnaryArithRes Neg 'TInt = 'TInt
evalUnaryArithOp :: proxy Neg
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Neg 'TInt)
evalUnaryArithOp proxy Neg
_ (VInt Integer
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (-Integer
i)
instance UnaryArithOp Neg 'TNat where
type UnaryArithRes Neg 'TNat = 'TInt
evalUnaryArithOp :: proxy Neg
-> Value' instr 'TNat -> Value' instr (UnaryArithRes Neg 'TNat)
evalUnaryArithOp proxy Neg
_ (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (- Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
instance UnaryArithOp Neg 'TBls12381Fr where
type UnaryArithRes Neg 'TBls12381Fr = 'TBls12381Fr
evalUnaryArithOp :: proxy Neg
-> Value' instr 'TBls12381Fr
-> Value' instr (UnaryArithRes Neg 'TBls12381Fr)
evalUnaryArithOp proxy Neg
_ (VBls12381Fr Bls12381Fr
i) = Bls12381Fr -> Value' instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Bls12381Fr -> Bls12381Fr
forall a. CurveObject a => a -> a
BLS.negate Bls12381Fr
i)
instance UnaryArithOp Neg 'TBls12381G1 where
type UnaryArithRes Neg 'TBls12381G1 = 'TBls12381G1
evalUnaryArithOp :: proxy Neg
-> Value' instr 'TBls12381G1
-> Value' instr (UnaryArithRes Neg 'TBls12381G1)
evalUnaryArithOp proxy Neg
_ (VBls12381G1 Bls12381G1
i) = Bls12381G1 -> Value' instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 (Bls12381G1 -> Bls12381G1
forall a. CurveObject a => a -> a
BLS.negate Bls12381G1
i)
instance UnaryArithOp Neg 'TBls12381G2 where
type UnaryArithRes Neg 'TBls12381G2 = 'TBls12381G2
evalUnaryArithOp :: proxy Neg
-> Value' instr 'TBls12381G2
-> Value' instr (UnaryArithRes Neg 'TBls12381G2)
evalUnaryArithOp proxy Neg
_ (VBls12381G2 Bls12381G2
i) = Bls12381G2 -> Value' instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 (Bls12381G2 -> Bls12381G2
forall a. CurveObject a => a -> a
BLS.negate Bls12381G2
i)
instance ArithOp Or 'TNat 'TNat where
type ArithRes Or 'TNat 'TNat = 'TNat
convergeArith :: proxy Or
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Or 'TNat 'TNat))
convergeArith proxy Or
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Or
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Or 'TNat 'TNat))
evalOp proxy Or
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.|. Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Or 'TNat 'TNat ~ ArithRes Or 'TNat 'TNat,
ArithOp Or 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Or 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Or 'TBool 'TBool where
type ArithRes Or 'TBool 'TBool = 'TBool
convergeArith :: proxy Or
-> Notes 'TBool
-> Notes 'TBool
-> Either AnnConvergeError (Notes (ArithRes Or 'TBool 'TBool))
convergeArith proxy Or
_ Notes 'TBool
n1 Notes 'TBool
n2 = Notes 'TBool
-> Notes 'TBool -> Either AnnConvergeError (Notes 'TBool)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBool
n1 Notes 'TBool
n2
evalOp :: proxy Or
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr (ArithRes Or 'TBool 'TBool))
evalOp proxy Or
_ (VBool Bool
i) (VBool Bool
j) = Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. b -> Either a b
Right (Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool))
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.|. Bool
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Or 'TBool 'TBool ~ ArithRes Or 'TBool 'TBool,
ArithOp Or 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp Or 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp And 'TInt 'TNat where
type ArithRes And 'TInt 'TNat = 'TNat
convergeArith :: proxy And
-> Notes 'TInt
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes And 'TInt 'TNat))
convergeArith proxy And
_ Notes 'TInt
_ Notes 'TNat
n2 = Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall a b. b -> Either a b
Right Notes 'TNat
n2
evalOp :: proxy And
-> Value' instr 'TInt
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr (ArithRes And 'TInt 'TNat))
evalOp proxy And
_ (VInt Integer
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TInt) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j))
instance ArithOp And 'TNat 'TNat where
type ArithRes And 'TNat 'TNat = 'TNat
convergeArith :: proxy And
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes And 'TNat 'TNat))
convergeArith proxy And
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy And
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes And 'TNat 'TNat))
evalOp proxy And
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
.&. Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes And 'TNat 'TNat ~ ArithRes And 'TNat 'TNat,
ArithOp And 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp And 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp And 'TBool 'TBool where
type ArithRes And 'TBool 'TBool = 'TBool
convergeArith :: proxy And
-> Notes 'TBool
-> Notes 'TBool
-> Either AnnConvergeError (Notes (ArithRes And 'TBool 'TBool))
convergeArith proxy And
_ Notes 'TBool
n1 Notes 'TBool
n2 = Notes 'TBool
-> Notes 'TBool -> Either AnnConvergeError (Notes 'TBool)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBool
n1 Notes 'TBool
n2
evalOp :: proxy And
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr (ArithRes And 'TBool 'TBool))
evalOp proxy And
_ (VBool Bool
i) (VBool Bool
j) = Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. b -> Either a b
Right (Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool))
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.&. Bool
j)
commutativityProof :: Maybe
$ Dict
(ArithRes And 'TBool 'TBool ~ ArithRes And 'TBool 'TBool,
ArithOp And 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp And 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Xor 'TNat 'TNat where
type ArithRes Xor 'TNat 'TNat = 'TNat
convergeArith :: proxy Xor
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Xor 'TNat 'TNat))
convergeArith proxy Xor
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Xor
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Xor 'TNat 'TNat))
evalOp proxy Xor
_ (VNat Natural
i) (VNat Natural
j) = Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural
i Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`xor` Natural
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Xor 'TNat 'TNat ~ ArithRes Xor 'TNat 'TNat,
ArithOp Xor 'TNat 'TNat)
commutativityProof = Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat)
-> Maybe (Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat))
forall a. a -> Maybe a
Just Dict ('TNat ~ 'TNat, ArithOp Xor 'TNat 'TNat)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Xor 'TBool 'TBool where
type ArithRes Xor 'TBool 'TBool = 'TBool
convergeArith :: proxy Xor
-> Notes 'TBool
-> Notes 'TBool
-> Either AnnConvergeError (Notes (ArithRes Xor 'TBool 'TBool))
convergeArith proxy Xor
_ Notes 'TBool
n1 Notes 'TBool
n2 = Notes 'TBool
-> Notes 'TBool -> Either AnnConvergeError (Notes 'TBool)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TBool
n1 Notes 'TBool
n2
evalOp :: proxy Xor
-> Value' instr 'TBool
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr (ArithRes Xor 'TBool 'TBool))
evalOp proxy Xor
_ (VBool Bool
i) (VBool Bool
j) = Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. b -> Either a b
Right (Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool))
-> Value' instr 'TBool
-> Either
(ArithError (Value' instr 'TBool) (Value' instr 'TBool))
(Value' instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool
i Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
`xor` Bool
j)
commutativityProof :: Maybe
$ Dict
(ArithRes Xor 'TBool 'TBool ~ ArithRes Xor 'TBool 'TBool,
ArithOp Xor 'TBool 'TBool)
commutativityProof = Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool)
-> Maybe (Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool))
forall a. a -> Maybe a
Just Dict ('TBool ~ 'TBool, ArithOp Xor 'TBool 'TBool)
forall (a :: Constraint). a => Dict a
Dict
instance ArithOp Lsl 'TNat 'TNat where
type ArithRes Lsl 'TNat 'TNat = 'TNat
convergeArith :: proxy Lsl
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Lsl 'TNat 'TNat))
convergeArith proxy Lsl
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Lsl
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Lsl 'TNat 'TNat))
evalOp proxy Lsl
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TNat
m@(VNat Natural
j) =
if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
256
then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ ShiftArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TNat
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
forall n m. ShiftArithErrorType -> n -> m -> ArithError n m
ShiftArithError ShiftArithErrorType
LslOverflow Value' instr 'TNat
n Value' instr 'TNat
m
else Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
j))
instance ArithOp Lsr 'TNat 'TNat where
type ArithRes Lsr 'TNat 'TNat = 'TNat
convergeArith :: proxy Lsr
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Lsr 'TNat 'TNat))
convergeArith proxy Lsr
_ Notes 'TNat
n1 Notes 'TNat
n2 = Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
evalOp :: proxy Lsr
-> Value' instr 'TNat
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr (ArithRes Lsr 'TNat 'TNat))
evalOp proxy Lsr
_ n :: Value' instr 'TNat
n@(VNat Natural
i) m :: Value' instr 'TNat
m@(VNat Natural
j) =
if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
256
then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. a -> Either a b
Left (ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ ShiftArithErrorType
-> Value' instr 'TNat
-> Value' instr 'TNat
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
forall n m. ShiftArithErrorType -> n -> m -> ArithError n m
ShiftArithError ShiftArithErrorType
LsrUnderflow Value' instr 'TNat
n Value' instr 'TNat
m
else Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. b -> Either a b
Right (Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat))
-> Value' instr 'TNat
-> Either
(ArithError (Value' instr 'TNat) (Value' instr 'TNat))
(Value' instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shift (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) (-(Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
j)))
instance UnaryArithOp Not 'TInt where
type UnaryArithRes Not 'TInt = 'TInt
evalUnaryArithOp :: proxy Not
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Not 'TInt)
evalUnaryArithOp proxy Not
_ (VInt Integer
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
i)
instance UnaryArithOp Not 'TNat where
type UnaryArithRes Not 'TNat = 'TInt
evalUnaryArithOp :: proxy Not
-> Value' instr 'TNat -> Value' instr (UnaryArithRes Not 'TNat)
evalUnaryArithOp proxy Not
_ (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer
forall a. Bits a => a -> a
complement (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i)
instance UnaryArithOp Not 'TBool where
type UnaryArithRes Not 'TBool = 'TBool
evalUnaryArithOp :: proxy Not
-> Value' instr 'TBool -> Value' instr (UnaryArithRes Not 'TBool)
evalUnaryArithOp proxy Not
_ (VBool Bool
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Bool
not Bool
i)
compareOp :: Comparable t => Value' i t -> Value' i t -> Integer
compareOp :: Value' i t -> Value' i t -> Integer
compareOp Value' i t
a Value' i t
b =
Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Ordering -> Int
forall a. Enum a => a -> Int
fromEnum (Value' i t -> Value' i t -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Value' i t
a Value' i t
b) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
instance UnaryArithOp Eq' 'TInt where
type UnaryArithRes Eq' 'TInt = 'TBool
evalUnaryArithOp :: proxy Eq'
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Eq' 'TInt)
evalUnaryArithOp proxy Eq'
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
instance UnaryArithOp Neq 'TInt where
type UnaryArithRes Neq 'TInt = 'TBool
evalUnaryArithOp :: proxy Neq
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Neq 'TInt)
evalUnaryArithOp proxy Neq
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
instance UnaryArithOp Lt 'TInt where
type UnaryArithRes Lt 'TInt = 'TBool
evalUnaryArithOp :: proxy Lt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Lt 'TInt)
evalUnaryArithOp proxy Lt
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
instance UnaryArithOp Gt 'TInt where
type UnaryArithRes Gt 'TInt = 'TBool
evalUnaryArithOp :: proxy Gt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Gt 'TInt)
evalUnaryArithOp proxy Gt
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0)
instance UnaryArithOp Le 'TInt where
type UnaryArithRes Le 'TInt = 'TBool
evalUnaryArithOp :: proxy Le
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Le 'TInt)
evalUnaryArithOp proxy Le
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0)
instance UnaryArithOp Ge 'TInt where
type UnaryArithRes Ge 'TInt = 'TBool
evalUnaryArithOp :: proxy Ge
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Ge 'TInt)
evalUnaryArithOp proxy Ge
_ (VInt Integer
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0)
instance ToIntArithOp 'TNat where
evalToIntOp :: Value' instr 'TNat -> Value' instr 'TInt
evalToIntOp (VNat Natural
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i)
instance ToIntArithOp 'TBls12381Fr where
evalToIntOp :: Value' instr 'TBls12381Fr -> Value' instr 'TInt
evalToIntOp (VBls12381Fr Bls12381Fr
i) = Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Bls12381Fr -> Integer
forall a. Integral a => a -> Integer
toInteger Bls12381Fr
i)
instance Buildable ShiftArithErrorType where
build :: ShiftArithErrorType -> Builder
build = \case
ShiftArithErrorType
LslOverflow -> Builder
"lsl overflow"
ShiftArithErrorType
LsrUnderflow -> Builder
"lsr underflow"
instance Buildable MutezArithErrorType where
build :: MutezArithErrorType -> Builder
build = \case
MutezArithErrorType
AddOverflow -> Builder
"add overflow"
MutezArithErrorType
MulOverflow -> Builder
"mul overflow"
MutezArithErrorType
SubUnderflow -> Builder
"sub underflow"
instance (Show n, Show m) => Buildable (ArithError n m) where
build :: ArithError n m -> Builder
build (MutezArithError MutezArithErrorType
errType n
n m
m) = Builder
"Mutez "
Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> MutezArithErrorType -> Builder
forall p. Buildable p => p -> Builder
build MutezArithErrorType
errType Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" with " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> n -> Builder
forall b a. (Show a, IsString b) => a -> b
show n
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
", " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> m -> Builder
forall b a. (Show a, IsString b) => a -> b
show m
m
build (ShiftArithError ShiftArithErrorType
errType n
n m
m) =
ShiftArithErrorType -> Builder
forall p. Buildable p => p -> Builder
build ShiftArithErrorType
errType Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" with " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> n -> Builder
forall b a. (Show a, IsString b) => a -> b
show n
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
", " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> m -> Builder
forall b a. (Show a, IsString b) => a -> b
show m
m