-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, containing some boilerplate for support of
-- arithmetic operations in Michelson language.

module Michelson.Typed.Arith
  ( ArithOp (..)
  , UnaryArithOp (..)
  , ArithError (..)
  , ShiftArithErrorType (..)
  , MutezArithErrorType (..)
  , Add
  , Sub
  , Mul
  , Abs
  , Neg
  , Or
  , And
  , Xor
  , Not
  , Lsl
  , Lsr
  , Compare
  , Eq'
  , Neq
  , Lt
  , Gt
  , Le
  , Ge
  , compareOp
  ) where

import Data.Bits (complement, shift, (.&.), (.|.))
import Data.Constraint (Dict(..))
import Data.Singletons (Sing, SingI(..))
import Fmt (Buildable(build))

import Michelson.Typed.Annotation (AnnConvergeError, Notes(..), converge, convergeAnns, starNotes)
import Michelson.Typed.Sing (SingT(..))
import Michelson.Typed.T (T(..))
import Michelson.Typed.Value (Comparability(..), Comparable, Value'(..), checkComparability)
import Tezos.Core (addMutez, mulMutez, subMutez, timestampFromSeconds, timestampToSeconds)

-- | Class for binary arithmetic operation.
--
-- Takes binary operation marker as @op@ parameter,
-- types of left operand @n@ and right operand @m@.
class ArithOp aop (n :: T) (m :: T) where

  -- | Type family @ArithRes@ denotes the type resulting from
  -- computing operation @op@ from operands of types @n@ and @m@.
  --
  -- For instance, adding integer to natural produces integer,
  -- which is reflected in following instance of type family:
  -- @ArithRes Add CNat CInt = CInt@.
  type ArithRes aop n m :: T

  -- | Converge the notes of given operands.
  convergeArith
    :: proxy aop
    -> Notes n
    -> Notes m
    -> Either AnnConvergeError (Notes (ArithRes aop n m))

  -- | Evaluate arithmetic operation on given operands.
  evalOp
    :: proxy aop
    -> Value' instr n
    -> Value' instr m
    -> Either (ArithError (Value' instr n) (Value' instr m)) (Value' instr (ArithRes aop n m))

  -- | An operation can marked as commutative, it does not affect its
  -- runtime behavior, but enables certain optimization in the optimizer.
  -- We conservatively consider operations non-commutative by default.
  --
  -- Note that there is one unusual case: @AND@ works with @int : nat@
  -- but not with @nat : int@. That's how it's specified in Michelson.
  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

-- | Denotes the error type occurred in the arithmetic shift operation.
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

-- | Denotes the error type occurred in the arithmetic operation involving mutez.
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

-- | Represents an arithmetic error of the operation.
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)

-- | Marker data type for add operation.
class UnaryArithOp aop (n :: T) where
  type UnaryArithRes aop n :: T
  evalUnaryArithOp :: proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)

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 _ _ n2 :: 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 _ (VNat i :: Natural
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TNat 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TNat '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 _ n1 :: Notes 'TInt
n1 _ = 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 _ (VInt i :: Integer
i) (VNat j :: Natural
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Add 'TInt 'TNat)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TInt 'TNat))
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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Add 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Add 'TNat '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 _ n1 :: Notes 'TInt
n1 n2 :: 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 _ (VInt i :: Integer
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TInt 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TInt '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 _ n1 :: Notes 'TTimestamp
n1 _ = 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 _ (VTimestamp i :: Timestamp
i) (VInt j :: Integer
j) =
    Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TTimestamp 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
      (Value' instr (ArithRes Add 'TTimestamp 'TInt)))
-> Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Add 'TTimestamp 'TInt))
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 _ _ n2 :: 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 _ (VInt i :: Integer
i) (VTimestamp j :: Timestamp
j) =
    Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Add 'TInt 'TTimestamp))
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
      (Value' instr (ArithRes Add 'TInt 'TTimestamp)))
-> Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Add 'TInt '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 _ n1 :: Notes 'TMutez
n1 n2 :: 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 _ n :: Value' instr 'TMutez
n@(VMutez i :: Mutez
i) m :: Value' instr 'TMutez
m@(VMutez j :: 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 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 _ _ n2 :: 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 _ (VNat i :: Natural
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TNat 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TNat '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 _ n1 :: Notes 'TInt
n1 _ = 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 _ (VInt i :: Integer
i) (VNat j :: Natural
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Sub 'TInt 'TNat)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TInt 'TNat))
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
  -- | Subtraction between @Nat@ and @Nat@ does not retain annotation.
  convergeArith :: proxy Sub
-> Notes 'TNat
-> Notes 'TNat
-> Either AnnConvergeError (Notes (ArithRes Sub 'TNat 'TNat))
convergeArith _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Sub 'TNat 'TNat)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Sub 'TNat 'TNat))
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 _ n1 :: Notes 'TInt
n1 n2 :: 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 _ (VInt i :: Integer
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TInt 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TInt '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 _ n1 :: Notes 'TTimestamp
n1 _ = 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 _ (VTimestamp i :: Timestamp
i) (VInt j :: Integer
j) =
    Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TTimestamp 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TTimestamp
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
      (Value' instr (ArithRes Sub 'TTimestamp 'TInt)))
-> Value' instr 'TTimestamp
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt))
     (Value' instr (ArithRes Sub 'TTimestamp 'TInt))
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 _ (NTTimestamp a :: TypeAnn
a) (NTTimestamp b :: 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 _ (VTimestamp i :: Timestamp
i) (VTimestamp j :: Timestamp
j) =
    Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
      (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TTimestamp) (Value' instr 'TTimestamp))
     (Value' instr (ArithRes Sub 'TTimestamp 'TTimestamp))
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 _ n1 :: Notes 'TMutez
n1 n2 :: 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 _ n :: Value' instr 'TMutez
n@(VMutez i :: Mutez
i) m :: Value' instr 'TMutez
m@(VMutez j :: 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 _ _ n2 :: 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 _ (VNat i :: Natural
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TNat 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
      (Value' instr (ArithRes Mul 'TNat 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TNat '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 _ n1 :: Notes 'TInt
n1 _ = 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 _ (VInt i :: Integer
i) (VNat j :: Natural
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes Mul 'TInt 'TNat)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TInt 'TNat))
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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Mul 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Mul 'TNat '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 _ n1 :: Notes 'TInt
n1 n2 :: 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 _ (VInt i :: Integer
i) (VInt j :: Integer
j) = Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TInt 'TInt))
forall a b. b -> Either a b
Right (Value' instr 'TInt
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
      (Value' instr (ArithRes Mul 'TInt 'TInt)))
-> Value' instr 'TInt
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TInt))
     (Value' instr (ArithRes Mul 'TInt '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 _ _ n2 :: 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 _ n :: Value' instr 'TNat
n@(VNat i :: Natural
i) m :: Value' instr 'TMutez
m@(VMutez j :: 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 _ n1 :: Notes 'TMutez
n1 _ = 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 _ n :: Value' instr 'TMutez
n@(VMutez i :: Mutez
i) m :: Value' instr 'TNat
m@(VNat j :: 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 UnaryArithOp Abs 'TInt where
  type UnaryArithRes Abs 'TInt = 'TNat
  evalUnaryArithOp :: proxy Abs
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Abs 'TInt)
evalUnaryArithOp _ (VInt i :: 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 _ (VInt i :: 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 _ (VNat i :: 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 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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Or 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Or 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Or 'TNat '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 _ n1 :: Notes 'TBool
n1 n2 :: 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 _ (VBool i :: Bool
i) (VBool j :: Bool
j) = Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Or 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr 'TBool
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes Or 'TBool 'TBool)))
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Or 'TBool '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 _ _ n2 :: 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 _ (VInt i :: Integer
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TInt 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
      (Value' instr (ArithRes And 'TInt 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TInt) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TInt '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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes And 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes And 'TNat '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 _ n1 :: Notes 'TBool
n1 n2 :: 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 _ (VBool i :: Bool
i) (VBool j :: Bool
j) = Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes And 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr 'TBool
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes And 'TBool 'TBool)))
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes And 'TBool '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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ (VNat i :: Natural
i) (VNat j :: Natural
j) = Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Xor 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Xor 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Xor 'TNat '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 _ n1 :: Notes 'TBool
n1 n2 :: 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 _ (VBool i :: Bool
i) (VBool j :: Bool
j) = Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Xor 'TBool 'TBool))
forall a b. b -> Either a b
Right (Value' instr 'TBool
 -> Either
      (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
      (Value' instr (ArithRes Xor 'TBool 'TBool)))
-> Value' instr 'TBool
-> Either
     (ArithError (Value' instr 'TBool) (Value' instr 'TBool))
     (Value' instr (ArithRes Xor 'TBool '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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ n :: Value' instr 'TNat
n@(VNat i :: Natural
i) m :: Value' instr 'TNat
m@(VNat j :: Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> 256
    then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat '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 (ArithRes Lsl 'TNat 'TNat)))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat '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 (ArithRes Lsl 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsl 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsl 'TNat '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 _ n1 :: Notes 'TNat
n1 n2 :: 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 _ n :: Value' instr 'TNat
n@(VNat i :: Natural
i) m :: Value' instr 'TNat
m@(VNat j :: Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> 256
    then ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat '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 (ArithRes Lsr 'TNat 'TNat)))
-> ArithError (Value' instr 'TNat) (Value' instr 'TNat)
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat '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 (ArithRes Lsr 'TNat 'TNat))
forall a b. b -> Either a b
Right (Value' instr 'TNat
 -> Either
      (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
      (Value' instr (ArithRes Lsr 'TNat 'TNat)))
-> Value' instr 'TNat
-> Either
     (ArithError (Value' instr 'TNat) (Value' instr 'TNat))
     (Value' instr (ArithRes Lsr 'TNat '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 _ (VInt i :: 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 _ (VNat i :: 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 _ (VBool i :: Bool
i) = Bool -> Value' instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Bool
not Bool
i)

compareOp :: forall t i. (Comparable t, SingI t) => Value' i t -> Value' i t -> Integer
compareOp :: Value' i t -> Value' i t -> Integer
compareOp a' :: Value' i t
a' b' :: Value' i t
b' = case (Sing t
forall k (a :: k). SingI a => Sing a
sing :: Sing t, Value' i t
a', Value' i t
b') of
  (STInt, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STNat, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STString, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STBytes, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STMutez, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STBool, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STKeyHash, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STTimestamp, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STAddress, i :: Value' i t
i, j :: Value' i t
j) -> 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
i Value' i t
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
  (STPair l :: Sing a
l m :: Sing b
m, VPair (a :: Value' i l
a, b :: Value' i r
b), VPair (c :: Value' i l
c, d :: Value' i r
d)) ->
    case Sing a -> Comparability a
forall (t :: T). Sing t -> Comparability t
checkComparability Sing a
l of
      CanBeCompared ->
        case Value' i l -> Value' i l -> Integer
forall (t :: T) (i :: [T] -> [T] -> *).
(Comparable t, SingI t) =>
Value' i t -> Value' i t -> Integer
compareOp Value' i l
a Value' i l
Value' i l
c of
          0  -> case Sing b -> Comparability b
forall (t :: T). Sing t -> Comparability t
checkComparability Sing b
m of
            CanBeCompared -> Value' i r -> Value' i r -> Integer
forall (t :: T) (i :: [T] -> [T] -> *).
(Comparable t, SingI t) =>
Value' i t -> Value' i t -> Integer
compareOp Value' i r
b Value' i r
Value' i r
d
          r' :: Integer
r' -> Integer
r'

instance UnaryArithOp Eq' 'TInt where
  type UnaryArithRes Eq' 'TInt = 'TBool
  evalUnaryArithOp :: proxy Eq'
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Eq' 'TInt)
evalUnaryArithOp _ (VInt i :: 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
== 0)

instance UnaryArithOp Neq 'TInt where
  type UnaryArithRes Neq 'TInt = 'TBool
  evalUnaryArithOp :: proxy Neq
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Neq 'TInt)
evalUnaryArithOp _ (VInt i :: 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
/= 0)


instance UnaryArithOp Lt 'TInt where
  type UnaryArithRes Lt 'TInt = 'TBool
  evalUnaryArithOp :: proxy Lt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Lt 'TInt)
evalUnaryArithOp _ (VInt i :: 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
< 0)

instance UnaryArithOp Gt 'TInt where
  type UnaryArithRes Gt 'TInt = 'TBool
  evalUnaryArithOp :: proxy Gt
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Gt 'TInt)
evalUnaryArithOp _ (VInt i :: 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
> 0)

instance UnaryArithOp Le 'TInt where
  type UnaryArithRes Le 'TInt = 'TBool
  evalUnaryArithOp :: proxy Le
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Le 'TInt)
evalUnaryArithOp _ (VInt i :: 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
<= 0)

instance UnaryArithOp Ge 'TInt where
  type UnaryArithRes Ge 'TInt = 'TBool
  evalUnaryArithOp :: proxy Ge
-> Value' instr 'TInt -> Value' instr (UnaryArithRes Ge 'TInt)
evalUnaryArithOp _ (VInt i :: 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
>= 0)


instance Buildable ShiftArithErrorType where
  build :: ShiftArithErrorType -> Builder
build = \case
    LslOverflow -> "lsl overflow"
    LsrUnderflow -> "lsr underflow"

instance Buildable MutezArithErrorType where
  build :: MutezArithErrorType -> Builder
build = \case
    AddOverflow -> "add overflow"
    MulOverflow -> "mul overflow"
    SubUnderflow -> "sub underflow"

instance (Show n, Show m) => Buildable (ArithError n m) where
  build :: ArithError n m -> Builder
build (MutezArithError errType :: MutezArithErrorType
errType n :: n
n m :: m
m) = "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
<> " 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
forall a. Semigroup a => a -> a -> a
<> m -> Builder
forall b a. (Show a, IsString b) => a -> b
show m
m
  build (ShiftArithError errType :: ShiftArithErrorType
errType n :: n
n m :: m
m) =
    ShiftArithErrorType -> Builder
forall p. Buildable p => p -> Builder
build ShiftArithErrorType
errType Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> " 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
forall a. Semigroup a => a -> a -> a
<> m -> Builder
forall b a. (Show a, IsString b) => a -> b
show m
m