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

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

import GHC.TypeLits hiding (Div)
import Prelude hiding (natVal)

import Lorentz.Base
import Lorentz.Value
import Morley.Michelson.Typed.Arith
import qualified Morley.Michelson.Typed.Instr 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 (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 (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 (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
M.INT

instance DefArithOp Add where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
M.ADD
instance DefArithOp Sub where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
Instr (n : m : s) (ArithRes Sub n m : s)
M.SUB
instance DefArithOp Mul where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
M.MUL
instance DefArithOp And where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp And n m =>
Instr (n : m : s) (ArithRes And n m : s)
M.AND
instance DefArithOp Or where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Or n m =>
Instr (n : m : s) (ArithRes Or n m : s)
M.OR
instance DefArithOp Xor where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Xor n m =>
Instr (n : m : s) (ArithRes Xor n m : s)
M.XOR
instance DefArithOp Lsl where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Lsl n m =>
Instr (n : m : s) (ArithRes Lsl n m : s)
M.LSL
instance DefArithOp Lsr where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Lsr n m =>
Instr (n : m : s) (ArithRes Lsr n m : s)
M.LSR
instance DefArithOp EDiv where
  defEvalOpHs :: Instr (n : m : s) (r : s)
defEvalOpHs = Instr (n : m : s) (r : s)
forall (n :: T) (m :: T) (s :: [T]).
ArithOp EDiv n m =>
Instr (n : m : s) (ArithRes EDiv n m : s)
M.EDIV
instance DefUnaryArithOp Not where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Not n =>
Instr (n : s) (UnaryArithRes Not n : s)
M.NOT
instance DefUnaryArithOp Abs where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Abs n =>
Instr (n : s) (UnaryArithRes Abs n : s)
M.ABS
instance DefUnaryArithOp Eq' where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
M.EQ
instance DefUnaryArithOp Neq where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Neq n =>
Instr (n : s) (UnaryArithRes Neq n : s)
M.NEQ
instance DefUnaryArithOp Lt where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Lt n =>
Instr (n : s) (UnaryArithRes Lt n : s)
M.LT
instance DefUnaryArithOp Le where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Le n =>
Instr (n : s) (UnaryArithRes Le n : s)
M.LE
instance DefUnaryArithOp Gt where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Gt n =>
Instr (n : s) (UnaryArithRes Gt n : s)
M.GT
instance DefUnaryArithOp Ge where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Ge n =>
Instr (n : s) (UnaryArithRes Ge n : s)
M.GE
instance DefUnaryArithOp Neg where
  defUnaryArithOpHs :: Instr (n : s) (r : s)
defUnaryArithOpHs = Instr (n : s) (r : s)
forall (n :: T) (s :: [T]).
UnaryArithOp Neg n =>
Instr (n : s) (UnaryArithRes Neg n : s)
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 ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Add Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add Natural (Fixed p) r

instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) Integer r
instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Add Integer (NFixed p) r
instance (r ~ (NFixed p)) => ArithOpHs Add Natural (NFixed p) r

instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) (Fixed p) 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 ~ Mutez) => ArithOpHs Sub Mutez Mutez r

instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (Fixed p) r

instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (NFixed p) r

instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) 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 :: (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 (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
M.MUL)
instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381Fr Bls12381G2 r where
  evalArithOpHs :: (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 (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
M.MUL)

instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))
instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r

instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))
instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))
instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r
instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r
instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r

instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))
instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))

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 (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r
instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsr (NFixed (BinBase a)) 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 UnaryArithOpHs Neg (Fixed p) where
  type UnaryArithResHs Neg (Fixed p) = (Fixed p)
instance UnaryArithOpHs Neg (NFixed p) where
  type UnaryArithResHs Neg (NFixed p) = (Fixed p)


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 :: (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 n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
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 :: (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 n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
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 :: (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 n (s :: [*]).
UnaryArithOpHs Lt n =>
(n : s) :-> (UnaryArithResHs Lt n : s)
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 :: (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 n (s :: [*]).
UnaryArithOpHs Gt n =>
(n : s) :-> (UnaryArithResHs Gt n : s)
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 :: (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 n (s :: [*]).
UnaryArithOpHs Le n =>
(n : s) :-> (UnaryArithResHs Le n : s)
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 :: (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 n (s :: [*]).
UnaryArithOpHs Ge n =>
(n : s) :-> (UnaryArithResHs Ge n : s)
forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Ge

instance ToIntegerArithOpHs Natural
instance ToIntegerArithOpHs (NFixed a)
instance ToIntegerArithOpHs Bls12381Fr