module Plutarch.Internal.Ord (
  POrd (..),
  (#>),
  (#>=),
) where

import Data.Kind (Type)
import Plutarch.Builtin.Bool (
  PBool,
  pand',
  pfalse,
  pif',
  por',
  ptrue,
 )
import Plutarch.Builtin.ByteString (
  PByte,
  PByteString,
  PEndianness,
  PLogicOpSemantics,
 )
import Plutarch.Builtin.Integer (
  PInteger,
  pleInteger,
  pltInteger,
 )
import Plutarch.Builtin.Unit (PUnit)
import Plutarch.Internal.Eq (PEq)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PlutusType (PInner)
import Plutarch.Internal.Term (
  S,
  Term,
  plet,
  punsafeBuiltin,
  (#),
 )
import PlutusCore qualified as PLC

{- | Total ordering relation.

= Laws

'#<=' must form a total order. More precisely:

1. @x #<= x@ @=@ @pcon PTrue@ (reflexivity)
2. @(y #< x) #|| (z #< y) #|| (x #<= z)@ @=@ @pcon PTrue@ (transitivity)
3. @(x #<= y) #|| (y #<= x)@ @=@ @pcon PTrue@ (totality)

Furthermore, '#<' must be an equivalent strict total order to '#<=':

4. @x #< x@ @=@ @pcon PFalse@ (irreflexivity)
5. @(y #<= x) #|| (z #<= y) #|| (x #< z)@ @=@ @pcon PTrue@ (transitivity)
6. @(x #< y) #|| (y #< x) #|| (x #== z)@ @=@ @pcon PTrue@ (trichotomy)
7. @x #<= y@ @=@ @(x #< y) #|| (x #== y)@ (strict equivalence)

If you define 'pmax' or 'pmin', ensure the following also hold:

8. @pmax # x # y@ @=@ @pmax # y # x@ (commutativity, also for @pmin)
9. @pmax # x #$ pmax y z@ @=@ @pmax # (pmax # x # y) # z@ (associativity,
    also for @pmin)
10. @pmax # x #$ pmin # y # z@ @=@ @pmin # (pmax # x # y) # (pmax # x # z)@
    ('pmax' distributes over 'pmin', also equivalent for 'pmin')
11. @pmin x y@ @=@ @pif' (x #<= y) x y@
12. @pmax x y@ @=@ @pif' (x #<= y) y x@

Laws 8-12 hold if you use the defaults provided by this type class.

@since WIP
-}
class PEq t => POrd t where
  -- | @since WIP
  {-# INLINEABLE (#<=) #-}
  (#<=) :: Term s t -> Term s t -> Term s PBool
  default (#<=) :: POrd (PInner t) => Term s t -> Term s t -> Term s PBool
  Term s t
x #<= Term s t
y = Term s t -> Term s (PInner t)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
x Term s (PInner t) -> Term s (PInner t) -> Term s PBool
forall (s :: S).
Term s (PInner t) -> Term s (PInner t) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s t -> Term s (PInner t)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
y

  -- | @since WIP
  {-# INLINEABLE (#<) #-}
  (#<) :: Term s t -> Term s t -> Term s PBool
  default (#<) :: POrd (PInner t) => Term s t -> Term s t -> Term s PBool
  Term s t
x #< Term s t
y = Term s t -> Term s (PInner t)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
x Term s (PInner t) -> Term s (PInner t) -> Term s PBool
forall (s :: S).
Term s (PInner t) -> Term s (PInner t) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s t -> Term s (PInner t)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
y

  -- | @since WIP
  {-# INLINEABLE pmax #-}
  pmax :: forall (s :: S). Term s t -> Term s t -> Term s t
  pmax Term s t
x Term s t
y = Term s (PBool :--> (t :--> (t :--> t)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (t :--> (t :--> t)))
-> Term s PBool -> Term s (t :--> (t :--> t))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s t
x Term s t -> Term s t -> Term s PBool
forall (s :: S). Term s t -> Term s t -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s t
y) Term s (t :--> (t :--> t)) -> Term s t -> Term s (t :--> t)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
y Term s (t :--> t) -> Term s t -> Term s t
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
x

  -- | @since WIP
  {-# INLINEABLE pmin #-}
  pmin :: forall (s :: S). Term s t -> Term s t -> Term s t
  pmin Term s t
x Term s t
y = Term s (PBool :--> (t :--> (t :--> t)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (t :--> (t :--> t)))
-> Term s PBool -> Term s (t :--> (t :--> t))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s t
x Term s t -> Term s t -> Term s PBool
forall (s :: S). Term s t -> Term s t -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s t
y) Term s (t :--> (t :--> t)) -> Term s t -> Term s (t :--> t)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
x Term s (t :--> t) -> Term s t -> Term s t
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
y

infix 4 #<=
infix 4 #<

-- | @since WIP
(#>) ::
  forall (a :: S -> Type) (s :: S).
  POrd a =>
  Term s a ->
  Term s a ->
  Term s PBool
Term s a
x #> :: forall (a :: PType) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s a
y = Term s a
y Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
x

infix 4 #>

-- | @since WIP
(#>=) ::
  forall (a :: S -> Type) (s :: S).
  POrd a =>
  Term s a ->
  Term s a ->
  Term s PBool
Term s a
x #>= :: forall (a :: PType) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#>= Term s a
y = Term s a
y Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
x

infix 4 #>=

instance POrd PBool where
  {-# INLINEABLE (#<) #-}
  Term s PBool
x #< :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#< Term s PBool
y = Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
-> Term s PBool -> Term s (PBool :--> (PBool :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PBool :--> (PBool :--> PBool))
-> Term s PBool -> Term s (PBool :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y
  {-# INLINEABLE (#<=) #-}
  Term s PBool
x #<= :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#<= Term s PBool
y = Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
-> Term s PBool -> Term s (PBool :--> (PBool :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PBool :--> (PBool :--> PBool))
-> Term s PBool -> Term s (PBool :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  {-# INLINEABLE pmin #-}
  pmin :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
pmin Term s PBool
x Term s PBool
y = Term s (PBool :--> (PBool :--> PBool))
forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
pand' Term s (PBool :--> (PBool :--> PBool))
-> Term s PBool -> Term s (PBool :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y
  {-# INLINEABLE pmax #-}
  pmax :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
pmax Term s PBool
x Term s PBool
y = Term s (PBool :--> (PBool :--> PBool))
forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
por' Term s (PBool :--> (PBool :--> PBool))
-> Term s PBool -> Term s (PBool :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y

instance POrd PInteger where
  {-# INLINEABLE (#<=) #-}
  Term s PInteger
x #<= :: forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
#<= Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PBool))
pleInteger Term s (PInteger :--> (PInteger :--> PBool))
-> Term s PInteger -> Term s (PInteger :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PBool) -> Term s PInteger -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
  {-# INLINEABLE (#<) #-}
  Term s PInteger
x #< :: forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
#< Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PBool))
pltInteger Term s (PInteger :--> (PInteger :--> PBool))
-> Term s PInteger -> Term s (PInteger :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PBool) -> Term s PInteger -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y

-- | @since WIP
instance POrd PByteString where
  {-# INLINEABLE (#<=) #-}
  Term s PByteString
x #<= :: forall (s :: S).
Term s PByteString -> Term s PByteString -> Term s PBool
#<= Term s PByteString
y = DefaultFun -> Term s (PByteString :--> (PByteString :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanEqualsByteString Term s (PByteString :--> (PByteString :--> PBool))
-> Term s PByteString -> Term s (PByteString :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
x Term s (PByteString :--> PBool)
-> Term s PByteString -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
y
  {-# INLINEABLE (#<) #-}
  Term s PByteString
x #< :: forall (s :: S).
Term s PByteString -> Term s PByteString -> Term s PBool
#< Term s PByteString
y = DefaultFun -> Term s (PByteString :--> (PByteString :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanByteString Term s (PByteString :--> (PByteString :--> PBool))
-> Term s PByteString -> Term s (PByteString :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
x Term s (PByteString :--> PBool)
-> Term s PByteString -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
y

-- | @since WIP
instance POrd PByte where
  {-# INLINEABLE (#<=) #-}
  Term s PByte
x #<= :: forall (s :: S). Term s PByte -> Term s PByte -> Term s PBool
#<= Term s PByte
y = DefaultFun -> Term s (PByte :--> (PByte :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanEqualsInteger Term s (PByte :--> (PByte :--> PBool))
-> Term s PByte -> Term s (PByte :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
x Term s (PByte :--> PBool) -> Term s PByte -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
y
  {-# INLINEABLE (#<) #-}
  Term s PByte
x #< :: forall (s :: S). Term s PByte -> Term s PByte -> Term s PBool
#< Term s PByte
y = DefaultFun -> Term s (PByte :--> (PByte :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanInteger Term s (PByte :--> (PByte :--> PBool))
-> Term s PByte -> Term s (PByte :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
x Term s (PByte :--> PBool) -> Term s PByte -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
y

deriving anyclass instance POrd PLogicOpSemantics

-- | @since WIP
instance POrd PUnit where
  {-# INLINEABLE (#<=) #-}
  Term s PUnit
x #<= :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PBool
#<= Term s PUnit
y = Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PBool) -> Term s PBool)
-> (Term s PUnit -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \Term s PUnit
_ -> Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
y ((Term s PUnit -> Term s PBool) -> Term s PBool)
-> (Term s PUnit -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PUnit -> Term s PBool
forall a b. a -> b -> a
const Term s PBool
forall (s :: S). Term s PBool
ptrue
  {-# INLINEABLE (#<) #-}
  Term s PUnit
x #< :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PBool
#< Term s PUnit
y = Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PBool) -> Term s PBool)
-> (Term s PUnit -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \Term s PUnit
_ -> Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
y ((Term s PUnit -> Term s PBool) -> Term s PBool)
-> (Term s PUnit -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PUnit -> Term s PBool
forall a b. a -> b -> a
const Term s PBool
forall (s :: S). Term s PBool
pfalse
  {-# INLINEABLE pmax #-}
  pmax :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PUnit
pmax Term s PUnit
x Term s PUnit
y = Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ \Term s PUnit
_ -> Term s PUnit -> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
y ((Term s PUnit -> Term s PUnit) -> Term s PUnit)
-> (Term s PUnit -> Term s PUnit) -> Term s PUnit
forall a b. (a -> b) -> a -> b
$ Term s PUnit -> Term s PUnit -> Term s PUnit
forall a b. a -> b -> a
const Term s PUnit
x
  {-# INLINEABLE pmin #-}
  pmin :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PUnit
pmin = Term s PUnit -> Term s PUnit -> Term s PUnit
forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PUnit
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s t
pmax

-- | @since WIP
deriving anyclass instance POrd PEndianness