-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Type families from "Morley.Michelson.Typed.Arith" lifted to Haskell types.
module Lorentz.Arith
  ( ArithOpHs (..)
  , DefArithOp (..)
  , UnaryArithOpHs (..)
  , DefUnaryArithOp (..)
  , ToIntegerArithOpHs (..)
  ) where

import Prelude hiding (natVal)

import Lorentz.Base
import Lorentz.Value
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Instr qualified as M

-- | Lifted 'ArithOp'.
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)

-- | Helper typeclass that provides default definition of 'evalArithOpHs'.
class DefArithOp aop where
  defEvalOpHs
    :: ( ArithOp aop n m
       , r ~ ArithRes aop n m
       )
    => M.Instr (n : m : s) (r : s)

-- | Lifted 'UnaryArithOp'.
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)
       )
    => 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) =>
Instr (n : s) (r : s)
forall {k} (aop :: k) (n :: T) (r :: T) (s :: [T]).
(DefUnaryArithOp aop, UnaryArithOp aop n,
 r ~ UnaryArithRes aop n) =>
Instr (n : s) (r : s)
defUnaryArithOpHs @aop)

-- | Helper typeclass that provides default definition of 'evalUnaryArithOpHs'.
class DefUnaryArithOp aop where
  defUnaryArithOpHs
    :: ( UnaryArithOp aop n
       , r ~ UnaryArithRes 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 (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

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
  defUnaryArithOpHs :: forall (n :: T) (r :: T) (s :: [T]).
(UnaryArithOp Not n, r ~ UnaryArithRes 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),
 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) =>
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) =>
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) =>
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) =>
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) =>
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) =>
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) =>
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) =>
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 ~ Natural) => ArithOpHs And Integer Natural r
instance (r ~ Natural) => ArithOpHs And Natural Natural r
instance (r ~ Bool) => ArithOpHs And Bool Bool r

instance (r ~ Natural) => ArithOpHs Xor Natural Natural r
instance (r ~ Bool) => ArithOpHs Xor Bool Bool r

instance (r ~ Natural) => ArithOpHs Lsl Natural Natural r where

instance (r ~ Natural) => ArithOpHs Lsr Natural 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 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 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 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 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 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 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 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