module Lorentz.Arith
( ArithOpHs (..)
, DefArithOp (..)
, UnaryArithOpHs (..)
, DefUnaryArithOp (..)
, ToIntegerArithOpHs (..)
, ToBytesArithOpHs (..)
) where
import Prelude hiding (natVal)
import Lorentz.Base
import Lorentz.Bytes (BytesLike)
import Lorentz.Value
import Morley.Michelson.Typed (SingI, T)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Instr qualified as M
class ArithOpHs (aop :: Type) (n :: Type) (m :: Type) (r :: Type) where
evalArithOpHs :: n : m : s :-> r : s
default evalArithOpHs
:: ( DefArithOp aop
, ArithOp aop (ToT n) (ToT m)
, ToT r ~ ArithRes aop (ToT n) (ToT m)
)
=> n : m : s :-> r : s
evalArithOpHs = Instr (ToTs (n : m : s)) (ToTs (r : s)) -> (n : m : s) :-> (r : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall aop (n :: T) (m :: T) (r :: T) (s :: [T]).
(DefArithOp aop, ArithOp aop n m, r ~ ArithRes aop n m) =>
Instr (n : m : s) (r : s)
forall {k} (aop :: k) (n :: T) (m :: T) (r :: T) (s :: [T]).
(DefArithOp aop, ArithOp aop n m, r ~ ArithRes aop n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs @aop)
class DefArithOp aop where
defEvalOpHs
:: ( ArithOp aop n m
, r ~ ArithRes aop n m
)
=> M.Instr (n : m : s) (r : s)
class UnaryArithOpHs (aop :: Type) (n :: Type) where
type UnaryArithResHs aop n :: Type
evalUnaryArithOpHs :: n : s :-> UnaryArithResHs aop n : s
default evalUnaryArithOpHs
:: ( DefUnaryArithOp aop
, UnaryArithOp aop (ToT n)
, ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)
, DefUnaryArithOpExtraConstraints aop (ToT n)
)
=> n : s :-> UnaryArithResHs aop n : s
evalUnaryArithOpHs = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs aop n : s))
-> (n : s) :-> (UnaryArithResHs aop n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall aop (n :: T) (r :: T) (s :: [T]).
(DefUnaryArithOp aop, UnaryArithOp aop n, r ~ UnaryArithRes aop n,
DefUnaryArithOpExtraConstraints aop n) =>
Instr (n : s) (r : s)
forall {k} (aop :: k) (n :: T) (r :: T) (s :: [T]).
(DefUnaryArithOp aop, UnaryArithOp aop n, r ~ UnaryArithRes aop n,
DefUnaryArithOpExtraConstraints aop n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs @aop)
class DefUnaryArithOp aop where
type aop (n :: T) :: Constraint
type _ _ = ()
defUnaryArithOpHs
:: ( UnaryArithOp aop n
, r ~ UnaryArithRes aop n
, DefUnaryArithOpExtraConstraints aop n
)
=> M.Instr (n : s) (r : s)
class ToIntegerArithOpHs (n :: Type) where
evalToIntOpHs :: n : s :-> Integer : s
default evalToIntOpHs
:: (ToIntArithOp (ToT n))
=> n : s :-> Integer : s
evalToIntOpHs = Instr (ToTs (n : s)) (ToTs (Integer : s))
-> (n : s) :-> (Integer : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToT n : ToTs s) ('TInt : ToTs s)
Instr (ToTs (n : s)) (ToTs (Integer : s))
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TInt : s), ToIntArithOp n) =>
Instr inp out
M.INT
class ToBytesArithOpHs (n :: Type) where
evalToBytesOpHs :: BytesLike bs => n : s :-> bs : s
default evalToBytesOpHs
:: (ToBytesArithOp (ToT n), BytesLike bs)
=> n : s :-> bs : s
evalToBytesOpHs = Instr (ToTs (n : s)) (ToTs (bs : s)) -> (n : s) :-> (bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToT n : ToTs s) ('TBytes : ToTs s)
Instr (ToTs (n : s)) (ToTs (bs : s))
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TBytes : s), ToBytesArithOp n) =>
Instr inp out
M.BYTES
instance DefArithOp Add where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Add n m, r ~ ArithRes Add n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Add n m : s),
ArithOp Add n m) =>
Instr inp out
M.ADD
instance DefArithOp Sub where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Sub n m, r ~ ArithRes Sub n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Sub n m : s),
ArithOp Sub n m) =>
Instr inp out
M.SUB
instance DefArithOp Mul where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Mul n m, r ~ ArithRes Mul n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Mul n m : s),
ArithOp Mul n m) =>
Instr inp out
M.MUL
instance DefArithOp And where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp And n m, r ~ ArithRes And n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes And n m : s),
ArithOp And n m) =>
Instr inp out
M.AND
instance DefArithOp Or where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Or n m, r ~ ArithRes Or n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Or n m : s), ArithOp Or n m) =>
Instr inp out
M.OR
instance DefArithOp Xor where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Xor n m, r ~ ArithRes Xor n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Xor n m : s),
ArithOp Xor n m) =>
Instr inp out
M.XOR
instance DefArithOp Lsl where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Lsl n m, r ~ ArithRes Lsl n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Lsl n m : s),
ArithOp Lsl n m) =>
Instr inp out
M.LSL
instance DefArithOp Lsr where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp Lsr n m, r ~ ArithRes Lsr n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Lsr n m : s),
ArithOp Lsr n m) =>
Instr inp out
M.LSR
instance DefArithOp EDiv where
defEvalOpHs :: forall (n :: T) (m :: T) (r :: T) (s :: [T]).
(ArithOp EDiv n m, r ~ ArithRes EDiv n m) =>
Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes EDiv n m : s),
ArithOp EDiv n m) =>
Instr inp out
M.EDIV
instance DefUnaryArithOp Not where
type Not n = SingI n
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Not n, r ~ UnaryArithRes Not n,
DefUnaryArithOpExtraConstraints Not n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Not n : s), SingI n,
UnaryArithOp Not n) =>
Instr inp out
M.NOT
instance DefUnaryArithOp Abs where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Abs n, r ~ UnaryArithRes Abs n,
DefUnaryArithOpExtraConstraints Abs n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Abs n : s),
UnaryArithOp Abs n) =>
Instr inp out
M.ABS
instance DefUnaryArithOp Eq' where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Eq' n, r ~ UnaryArithRes Eq' n,
DefUnaryArithOpExtraConstraints Eq' n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
UnaryArithOp Eq' n) =>
Instr inp out
M.EQ
instance DefUnaryArithOp Neq where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Neq n, r ~ UnaryArithRes Neq n,
DefUnaryArithOpExtraConstraints Neq n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Neq n : s),
UnaryArithOp Neq n) =>
Instr inp out
M.NEQ
instance DefUnaryArithOp Lt where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Lt n, r ~ UnaryArithRes Lt n,
DefUnaryArithOpExtraConstraints Lt n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Lt n : s),
UnaryArithOp Lt n) =>
Instr inp out
M.LT
instance DefUnaryArithOp Le where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Le n, r ~ UnaryArithRes Le n,
DefUnaryArithOpExtraConstraints Le n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Le n : s),
UnaryArithOp Le n) =>
Instr inp out
M.LE
instance DefUnaryArithOp Gt where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Gt n, r ~ UnaryArithRes Gt n,
DefUnaryArithOpExtraConstraints Gt n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Gt n : s),
UnaryArithOp Gt n) =>
Instr inp out
M.GT
instance DefUnaryArithOp Ge where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Ge n, r ~ UnaryArithRes Ge n,
DefUnaryArithOpExtraConstraints Ge n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Ge n : s),
UnaryArithOp Ge n) =>
Instr inp out
M.GE
instance DefUnaryArithOp Neg where
defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Neg n, r ~ UnaryArithRes Neg n,
DefUnaryArithOpExtraConstraints Neg n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Neg n : s),
UnaryArithOp Neg n) =>
Instr inp out
M.NEG
instance (r ~ Integer) => ArithOpHs Add Natural Integer r
instance (r ~ Integer) => ArithOpHs Add Integer Natural r
instance (r ~ Natural) => ArithOpHs Add Natural Natural r
instance (r ~ Integer) => ArithOpHs Add Integer Integer r
instance (r ~ Timestamp) => ArithOpHs Add Timestamp Integer r
instance (r ~ Timestamp) => ArithOpHs Add Integer Timestamp r
instance (r ~ Mutez) => ArithOpHs Add Mutez Mutez r
instance (r ~ Bls12381Fr) => ArithOpHs Add Bls12381Fr Bls12381Fr r
instance (r ~ Bls12381G1) => ArithOpHs Add Bls12381G1 Bls12381G1 r
instance (r ~ Bls12381G2) => ArithOpHs Add Bls12381G2 Bls12381G2 r
instance (r ~ Integer) => ArithOpHs Sub Natural Integer r
instance (r ~ Integer) => ArithOpHs Sub Integer Natural r
instance (r ~ Integer) => ArithOpHs Sub Natural Natural r
instance (r ~ Integer) => ArithOpHs Sub Integer Integer r
instance (r ~ Timestamp) => ArithOpHs Sub Timestamp Integer r
instance (r ~ Integer) => ArithOpHs Sub Timestamp Timestamp r
instance (r ~ Integer) => ArithOpHs Mul Natural Integer r
instance (r ~ Integer) => ArithOpHs Mul Integer Natural r
instance (r ~ Natural) => ArithOpHs Mul Natural Natural r
instance (r ~ Integer) => ArithOpHs Mul Integer Integer r
instance (r ~ Mutez) => ArithOpHs Mul Natural Mutez r
instance (r ~ Mutez) => ArithOpHs Mul Mutez Natural r
instance (r ~ Bls12381Fr) => ArithOpHs Mul Integer Bls12381Fr r
instance (r ~ Bls12381Fr) => ArithOpHs Mul Natural Bls12381Fr r
instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Integer r
instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Natural r
instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Bls12381Fr r
instance (r ~ Bls12381G1) => ArithOpHs Mul Bls12381G1 Bls12381Fr r
instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381G2 Bls12381Fr r
instance (r ~ Bls12381G1) => ArithOpHs Mul Bls12381Fr Bls12381G1 r where
evalArithOpHs :: forall (s :: [*]). (Bls12381Fr : Bls12381G1 : s) :-> (r : s)
evalArithOpHs = Instr (ToTs (Bls12381Fr : Bls12381G1 : s)) (ToTs (r : s))
-> (Bls12381Fr : Bls12381G1 : s) :-> (r : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
('TBls12381Fr : 'TBls12381G1 : ToTs s)
('TBls12381G1 : 'TBls12381Fr : ToTs s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
M.SWAP Instr
('TBls12381Fr : 'TBls12381G1 : ToTs s)
('TBls12381G1 : 'TBls12381Fr : ToTs s)
-> Instr
('TBls12381G1 : 'TBls12381Fr : ToTs s) ('TBls12381G1 : ToTs s)
-> Instr
('TBls12381Fr : 'TBls12381G1 : ToTs s) ('TBls12381G1 : ToTs s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`M.Seq` Instr
('TBls12381G1 : 'TBls12381Fr : ToTs s) ('TBls12381G1 : ToTs s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Mul n m : s),
ArithOp Mul n m) =>
Instr inp out
M.MUL)
instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381Fr Bls12381G2 r where
evalArithOpHs :: forall (s :: [*]). (Bls12381Fr : Bls12381G2 : s) :-> (r : s)
evalArithOpHs = Instr (ToTs (Bls12381Fr : Bls12381G2 : s)) (ToTs (r : s))
-> (Bls12381Fr : Bls12381G2 : s) :-> (r : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
('TBls12381Fr : 'TBls12381G2 : ToTs s)
('TBls12381G2 : 'TBls12381Fr : ToTs s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
M.SWAP Instr
('TBls12381Fr : 'TBls12381G2 : ToTs s)
('TBls12381G2 : 'TBls12381Fr : ToTs s)
-> Instr
('TBls12381G2 : 'TBls12381Fr : ToTs s) ('TBls12381G2 : ToTs s)
-> Instr
('TBls12381Fr : 'TBls12381G2 : ToTs s) ('TBls12381G2 : ToTs s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`M.Seq` Instr
('TBls12381G2 : 'TBls12381Fr : ToTs s) ('TBls12381G2 : ToTs s)
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Mul n m : s),
ArithOp Mul n m) =>
Instr inp out
M.MUL)
instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Natural Integer r
instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Integer Natural r
instance (r ~ Maybe (Natural, Natural)) => ArithOpHs EDiv Natural Natural r
instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Integer Integer r
instance (r ~ Maybe (Natural, Mutez)) => ArithOpHs EDiv Mutez Mutez r
instance (r ~ Maybe (Mutez, Mutez)) => ArithOpHs EDiv Mutez Natural r
instance UnaryArithOpHs Neg Integer where
type UnaryArithResHs Neg Integer = Integer
instance UnaryArithOpHs Neg Natural where
type UnaryArithResHs Neg Natural = Integer
instance UnaryArithOpHs Neg Bls12381Fr where
type UnaryArithResHs Neg Bls12381Fr = Bls12381Fr
instance UnaryArithOpHs Neg Bls12381G1 where
type UnaryArithResHs Neg Bls12381G1 = Bls12381G1
instance UnaryArithOpHs Neg Bls12381G2 where
type UnaryArithResHs Neg Bls12381G2 = Bls12381G2
instance (r ~ Natural) => ArithOpHs Or Natural Natural r
instance (r ~ Bool) => ArithOpHs Or Bool Bool r
instance (r ~ ByteString) => ArithOpHs Or ByteString ByteString r
instance (r ~ Natural) => ArithOpHs And Integer Natural r
instance (r ~ Natural) => ArithOpHs And Natural Natural r
instance (r ~ Bool) => ArithOpHs And Bool Bool r
instance (r ~ ByteString) => ArithOpHs And ByteString ByteString r
instance (r ~ Natural) => ArithOpHs Xor Natural Natural r
instance (r ~ Bool) => ArithOpHs Xor Bool Bool r
instance (r ~ ByteString) => ArithOpHs Xor ByteString ByteString r
instance (r ~ Natural) => ArithOpHs Lsl Natural Natural r where
instance (r ~ ByteString) => ArithOpHs Lsl ByteString Natural r where
instance (r ~ Natural) => ArithOpHs Lsr Natural Natural r
instance (r ~ ByteString) => ArithOpHs Lsr ByteString Natural r
instance UnaryArithOpHs Abs Integer where
type UnaryArithResHs Abs Integer = Natural
instance UnaryArithOpHs Not Integer where
type UnaryArithResHs Not Integer = Integer
instance UnaryArithOpHs Not Natural where
type UnaryArithResHs Not Natural = Integer
instance UnaryArithOpHs Not Bool where
type UnaryArithResHs Not Bool = Bool
instance UnaryArithOpHs Not ByteString where
type UnaryArithResHs Not ByteString = ByteString
instance UnaryArithOpHs Eq' Integer where
type UnaryArithResHs Eq' Integer = Bool
instance UnaryArithOpHs Eq' Natural where
type UnaryArithResHs Eq' Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Eq' Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Eq'
instance UnaryArithOpHs Neq Integer where
type UnaryArithResHs Neq Integer = Bool
instance UnaryArithOpHs Neq Natural where
type UnaryArithResHs Neq Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Neq Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Neq
instance UnaryArithOpHs Lt Integer where
type UnaryArithResHs Lt Integer = Bool
instance UnaryArithOpHs Lt Natural where
type UnaryArithResHs Lt Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Lt Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Lt
instance UnaryArithOpHs Gt Integer where
type UnaryArithResHs Gt Integer = Bool
instance UnaryArithOpHs Gt Natural where
type UnaryArithResHs Gt Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Gt Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Gt
instance UnaryArithOpHs Le Integer where
type UnaryArithResHs Le Integer = Bool
instance UnaryArithOpHs Le Natural where
type UnaryArithResHs Le Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Le Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Le
instance UnaryArithOpHs Ge Integer where
type UnaryArithResHs Ge Integer = Bool
instance UnaryArithOpHs Ge Natural where
type UnaryArithResHs Ge Natural = Bool
evalUnaryArithOpHs :: forall (s :: [*]).
(Natural : s) :-> (UnaryArithResHs Ge Natural : s)
evalUnaryArithOpHs = (Natural : s) :-> (Integer : s)
forall (s :: [*]). (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs ((Natural : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (Natural : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Ge
instance ToIntegerArithOpHs Natural
instance ToIntegerArithOpHs Bls12381Fr
instance {-# overlappable #-} BytesLike bs => ToIntegerArithOpHs bs
instance ToBytesArithOpHs Natural
instance ToBytesArithOpHs Integer