{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}

module Plutarch.Extra.Interval (
  pmember,
  pinterval,
  pfrom,
  pto,
  palways,
  pnever,
  psingleton,
  phull,
  pintersection,
  pcontains,
  pbefore,
  pafter,
) where

import Plutarch.Api.V1.Interval (
  PClosure,
  PExtended (PFinite, PNegInf, PPosInf),
  PInterval (PInterval),
  PLowerBound (PLowerBound),
  PUpperBound (PUpperBound),
 )
import Plutarch.Bool (pif')
import qualified Plutarch.Monadic as P
import Plutarch.Prelude hiding (psingleton, pto)
import qualified PlutusLedgerApi.V1.Interval as Plutus

-- check if `a` belongs to interval `i`
pmember ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( PAsData a
        :--> PInterval a
        :--> PBool
    )
pmember :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PAsData a :--> (PInterval a :--> PBool))
pmember = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a Term s (PInterval a)
i -> forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PBool))
pcontains forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInterval a)
i forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a :--> PInterval a)
psingleton forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a)

{- | create an interval that includes all values that are greater than or equal
 - to a and smaller than or equal to b
-}
pinterval ::
  forall a (s :: S).
  PIsData a =>
  Term
    s
    ( PAsData a
        :--> PAsData a
        :--> PInterval a
    )
pinterval :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a :--> (PAsData a :--> PInterval a))
pinterval = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a Term s (PAsData a)
b ->
    let start :: Term _ (PExtended a)
        start :: Term s (PExtended a)
start = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
-> PExtended a s
PFinite forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil

        end :: Term _ (PExtended a)
        end :: Term s (PExtended a)
end = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
-> PExtended a s
PFinite forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
b forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil
     in forall (a :: PType) (s :: S).
PIsData a =>
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
end

{- | create an interval that includes all values that are greater than or equal
 - to a
-}
pfrom :: forall a s. PIsData a => Term s (PAsData a :--> PInterval a)
pfrom :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a :--> PInterval a)
pfrom = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a ->
    let start :: Term _ (PExtended a)
        start :: Term s (PExtended a)
start = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
-> PExtended a s
PFinite forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil
        end :: Term _ (PExtended a)
        end :: Term w (PExtended a)
end = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term s (PDataRecord ('[] @PLabeledType)) -> PExtended a s
PPosInf forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil
     in forall (a :: PType) (s :: S).
PIsData a =>
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall {w :: S}. Term w (PExtended a)
end

{- | create an interval that includes all values that are smaller than or equal
 - to a
-}
pto :: forall a (s :: S). PIsData a => Term s (PAsData a :--> PInterval a)
pto :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a :--> PInterval a)
pto = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a ->
    let start :: Term _ (PExtended a)
        start :: Term w (PExtended a)
start = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term s (PDataRecord ('[] @PLabeledType)) -> PExtended a s
PNegInf forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil

        end :: Term _ (PExtended a)
        end :: Term s (PExtended a)
end = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
-> PExtended a s
PFinite forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil
     in forall (a :: PType) (s :: S).
PIsData a =>
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall {w :: S}. Term w (PExtended a)
start forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
end

-- | create an interval that covers every slot
palways :: forall a (s :: S). (PIsData a, PLiftData a) => Term s (PInterval a)
palways :: forall (a :: PType) (s :: S).
(PIsData a, PLiftData a) =>
Term s (PInterval a)
palways = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant forall a. Interval a
Plutus.always

-- | create an interval that is empty
pnever :: forall a (s :: S). (PIsData a, PLiftData a) => Term s (PInterval a)
pnever :: forall (a :: PType) (s :: S).
(PIsData a, PLiftData a) =>
Term s (PInterval a)
pnever = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant forall a. Interval a
Plutus.never

-- | create and interval [a, a]
psingleton :: forall a (s :: S). PIsData a => Term s (PAsData a :--> PInterval a)
psingleton :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a :--> PInterval a)
psingleton = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a ->
    forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
-> PExtended a s
PFinite forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil) forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
start ->
      forall (a :: PType) (s :: S).
PIsData a =>
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start

-- | `hull i1 i2` is the smallest interval containing `i1` and `i2`
phull ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PInterval a
    )
phull :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PInterval a))
phull = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
x' Term s (PInterval a)
y' -> P.do
    HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
x'
    HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
y'

    let lowerX :: Term s (PLowerBound a)
lowerX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.from
        upperX :: Term s (PUpperBound a)
upperX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.to
        lowerY :: Term s (PLowerBound a)
lowerY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.from
        upperY :: Term s (PUpperBound a)
upperY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.to

        lower :: Term s (PLowerBound a)
lower = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PLowerBound a s
PLowerBound forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
minP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerX) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerY)
        upper :: Term s (PUpperBound a)
upper = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PUpperBound a s
PUpperBound forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
maxP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperX) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperY)

    forall (a :: PType) (s :: S).
PIsData a =>
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PUpperBound a)
upper

-- | `intersecion i1 i2` is the largest interval contained in `i1` and `i2`
pintersection ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PInterval a
    )
pintersection :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PInterval a))
pintersection = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
x' Term s (PInterval a)
y' -> P.do
    HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
x'
    HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
y'

    let lowerX :: Term s (PLowerBound a)
lowerX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.from
        upperX :: Term s (PUpperBound a)
upperX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.to

        lowerY :: Term s (PLowerBound a)
lowerY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.from
        upperY :: Term s (PUpperBound a)
upperY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.to

        lower :: Term s (PLowerBound a)
lower = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PLowerBound a s
PLowerBound forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
maxP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerX) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerY)
        upper :: Term s (PUpperBound a)
upper = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PUpperBound a s
PUpperBound forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
minP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperX) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperY)

    forall (a :: PType) (s :: S).
PIsData a =>
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PUpperBound a)
upper

-- | pcontains # a # b is true if the interval `b` is entirely contained in `a`
pcontains ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PBool
    )
pcontains :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PBool))
pcontains = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
x' Term s (PInterval a)
y' -> P.do
    HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
x'
    HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
y'
    let lowerX :: Term s (PLowerBound a)
lowerX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.from
        upperX :: Term s (PUpperBound a)
upperX = HRec
  ((':)
     @(Symbol, Type)
     '("from", Term s (PAsData (PLowerBound a)))
     ((':)
        @(Symbol, Type)
        '("to", Term s (PAsData (PUpperBound a)))
        ('[] @(Symbol, Type))))
x.to

        lowerY :: Term s (PLowerBound a)
lowerY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.from
        upperY :: Term s (PUpperBound a)
upperY = HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings
        (PFields (PInterval a))
        ((':) @Symbol "from" ((':) @Symbol "to" ('[] @Symbol))))
     s)
y.to

    forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> PBool))
leqP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerX) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerY) forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> PBool))
leqP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperY) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperX)

-- | `a` before interval `i` is true if `a` is earlier than the start of `i`
pbefore ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( a
        :--> PInterval a
        :--> PBool
    )
pbefore :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (a :--> (PInterval a :--> PBool))
pbefore = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PInterval a)
y ->
    let lower :: Term s (PLowerBound a)
lower = forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"from" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInterval a)
y
     in forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (a :--> (EndPoint a :--> PBool))
pbefore' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lower)

-- | `a` after interval `i` is true if `a` is later than the end of `i`
pafter ::
  forall a s.
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( a
        :--> PInterval a
        :--> PBool
    )
pafter :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (a :--> (PInterval a :--> PBool))
pafter = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PInterval a)
y ->
    let upper :: Term s (PUpperBound a)
upper = forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"to" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInterval a)
y
     in forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (a :--> (EndPoint a :--> PBool))
pafter' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upper)

-- | interval from upper and lower
pinterval' ::
  forall a (s :: S).
  PIsData a =>
  Term
    s
    ( PAsData (PLowerBound a)
        :--> PAsData (PUpperBound a)
        :--> PInterval a
    )
pinterval' :: forall (a :: PType) (s :: S).
PIsData a =>
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData (PLowerBound a))
lower Term s (PAsData (PUpperBound a))
upper ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$
      forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("from" ':= PLowerBound a)
        ((':) @PLabeledType ("to" ':= PUpperBound a) ('[] @PLabeledType))))
-> PInterval a s
PInterval forall a b. (a -> b) -> a -> b
$
        forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"from"
          # lower
          #$ pdcons @"to"
          # upper
          # pdnil

-- | closed interval from PExtended
pclosedInterval ::
  forall a (s :: S).
  PIsData a =>
  Term
    s
    ( PExtended a
        :--> PExtended a
        :--> PInterval a
    )
pclosedInterval :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
start Term s (PExtended a)
end ->
    let closure :: Term _ (PAsData PClosure)
        closure :: Term w (PAsData PBool)
closure = forall (p :: PType) h (s :: S).
(ToData h, (PLifted p :: Type) ~ (h :: Type),
 (PConstanted h :: PType) ~ (p :: PType)) =>
h -> Term s (PAsData p)
pconstantData Bool
True

        upper :: Term _ (PUpperBound a)
        upper :: Term s (PUpperBound a)
upper =
          forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$
            forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PUpperBound a s
PUpperBound forall a b. (a -> b) -> a -> b
$
              forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0"
                # pdata end
                #$ pdcons @"_1"
                # closure
                # pdnil

        lower :: Term _ (PLowerBound a)
        lower :: Term s (PLowerBound a)
lower =
          forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$
            forall (a :: PType) (s :: S).
Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("_0" ':= PExtended a)
        ((':) @PLabeledType ("_1" ':= PBool) ('[] @PLabeledType))))
-> PLowerBound a s
PLowerBound forall a b. (a -> b) -> a -> b
$
              forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons @"_0"
                # pdata start
                #$ pdcons @"_1"
                # closure
                # pdnil
     in forall (a :: PType) (s :: S).
PIsData a =>
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PUpperBound a)
upper

-- | value < endpoint
pbefore' ::
  forall a (s :: S).
  (PIsData a, POrd a, PEq a) =>
  Term
    s
    ( a
        :--> EndPoint a
        :--> PBool
    )
pbefore' :: forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (a :--> (EndPoint a :--> PBool))
pbefore' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (EndPoint a)
y' -> P.do
    HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (EndPoint a)
y'
    Term s (PExtended a)
yt <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._0
    let yc :: Term s PBool
yc = HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._1

    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      Term s PBool
yc
      (forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
yt (forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
a))
      (forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
yt (forall (a :: PType) (s :: S).
(POrd a, PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
leqE' Term s a
a))

-- | value > endpoint
pafter' ::
  forall a (s :: S).
  (PIsData a, POrd a, PEq a) =>
  Term
    s
    ( a
        :--> EndPoint a
        :--> PBool
    )
pafter' :: forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (a :--> (EndPoint a :--> PBool))
pafter' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (EndPoint a)
y' -> P.do
    HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (EndPoint a)
y'
    Term s (PExtended a)
yt <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._0
    let yc :: Term s PBool
yc = HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._1

    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      Term s PBool
yc
      (forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
yt (forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
a))
      (forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
yt (forall (a :: PType) (s :: S).
(POrd a, PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
geqE' Term s a
a))

-- | (x :: Term s (EndPoint a)) <= (y :: Term s (EndPoint a))
leqP ::
  forall a (s :: S).
  (PIsData a, POrd a, PEq a) =>
  Term
    s
    ( EndPoint a
        :--> EndPoint a
        :--> PBool
    )
leqP :: forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> PBool))
leqP = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (EndPoint a)
x' Term s (EndPoint a)
y' -> P.do
    HRec
  ((':)
     @(Symbol, Type)
     '("_0", Term s (PAsData (PExtended a)))
     ((':)
        @(Symbol, Type)
        '("_1", Term s (PAsData PBool))
        ('[] @(Symbol, Type))))
x <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (EndPoint a)
x'
    HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y <- forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (EndPoint a)
y'

    Term s (PExtended a)
xt <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  ((':)
     @(Symbol, Type)
     '("_0", Term s (PAsData (PExtended a)))
     ((':)
        @(Symbol, Type)
        '("_1", Term s (PAsData PBool))
        ('[] @(Symbol, Type))))
x._0
    Term s (PExtended a)
yt <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._0

    Term s PBool
xc <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  ((':)
     @(Symbol, Type)
     '("_0", Term s (PAsData (PExtended a)))
     ((':)
        @(Symbol, Type)
        '("_1", Term s (PAsData PBool))
        ('[] @(Symbol, Type))))
x._1
    Term s PBool
yc <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields (EndPoint a))
     (Bindings
        (PFields (EndPoint a))
        ((':) @Symbol "_0" ((':) @Symbol "_1" ('[] @Symbol))))
     s)
y._1

    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PBool
xc forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s PBool
yc forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (forall (s :: S). Term s (PBool :--> PBool)
pnot forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
xc) forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (forall (s :: S). Term s (PBool :--> PBool)
pnot forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
yc))
      (forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
leqE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
xt forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
yt)
      (forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
ltE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
xt forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
yt)

minP ::
  forall a (s :: S).
  (PIsData a, POrd a, PEq a) =>
  Term
    s
    ( EndPoint a
        :--> EndPoint a
        :--> EndPoint a
    )
minP :: forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
minP = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (EndPoint a)
x Term s (EndPoint a)
y -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> PBool))
leqP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
y) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
y

maxP ::
  forall a (s :: S).
  (PIsData a, POrd a, PEq a) =>
  Term
    s
    ( EndPoint a
        :--> EndPoint a
        :--> EndPoint a
    )
maxP :: forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> EndPoint a))
maxP = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (EndPoint a)
x Term s (EndPoint a)
y -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: PType) (s :: S).
(PIsData a, POrd a, PEq a) =>
Term s (EndPoint a :--> (EndPoint a :--> PBool))
leqP forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
y) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (EndPoint a)
x

-- | (x :: Term s (PExtended a)) < (y :: Term s (PExtended b))
ltE ::
  forall a (s :: S).
  (POrd a, PIsData a) =>
  Term
    s
    ( PExtended a
        :--> PExtended a
        :--> PBool
    )
ltE :: forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
ltE = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
x Term s (PExtended a)
y -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
x (forall {w :: S}.
Term w (PExtended a) -> PExtended a w -> Term w PBool
cont Term s (PExtended a)
y)
  where
    cont :: Term _ (PExtended a) -> PExtended a _ -> Term _ PBool
    cont :: Term w (PExtended a) -> PExtended a w -> Term w PBool
cont Term w (PExtended a)
y' PExtended a w
x' = case PExtended a w
x' of
      PNegInf Term w (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
      PPosInf Term w (PDataRecord ('[] @PLabeledType))
_ -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term w (PExtended a)
y' forall (a :: PType) (s :: S). PExtended a s -> Term s PBool
isPosInf
      PFinite Term
  w
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
l -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term w (PExtended a)
y' (forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term
  w
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
l)

-- | (x :: Term s (PExtended a)) = (y :: Term s (PExtended b))
eqE ::
  forall a (s :: S).
  (PEq a, PIsData a) =>
  Term
    s
    ( PExtended a
        :--> PExtended a
        :--> PBool
    )
eqE :: forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
eqE = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
x Term s (PExtended a)
y ->
    let cont :: PExtended a s -> Term s PBool
cont PExtended a s
x' = case PExtended a s
x' of
          PNegInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
y forall (a :: PType) (s :: S). PExtended a s -> Term s PBool
isNegInf
          PPosInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
y forall (a :: PType) (s :: S). PExtended a s -> Term s PBool
isPosInf
          PFinite Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
l -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
y (forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
eqE' (forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
l))
     in forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
x PExtended a s -> Term s PBool
cont

-- | value < PExtended
ltE' ::
  forall a (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
ltE' :: forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
a PExtended a s
y' = case PExtended a s
y' of
  PNegInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False
  PPosInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  PFinite Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r -> Term s a
a forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r

-- | value > PExtended
gtE' ::
  forall a (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
gtE' :: forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
a PExtended a s
y' = case PExtended a s
y' of
  PNegInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False
  PPosInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  PFinite Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r -> P.do
    Term s a
b <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r
    Term s a
b forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
a

-- | value = PExtended
eqE' ::
  forall a (s :: S).
  (PEq a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
eqE' :: forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
eqE' Term s a
a PExtended a s
y' = case PExtended a s
y' of
  PFinite Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r -> P.do
    Term s a
b <- forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord ((':) @PLabeledType ("_0" ':= a) ('[] @PLabeledType)))
r
    Term s a
a forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
b
  PExtended a s
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

-- | value <= PExtended
leqE' ::
  forall a (s :: S).
  (POrd a, PEq a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
leqE' :: forall (a :: PType) (s :: S).
(POrd a, PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
leqE' Term s a
a PExtended a s
y = forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
a PExtended a s
y forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
eqE' Term s a
a PExtended a s
y

-- | value >= PExtended
geqE' ::
  forall a (s :: S).
  (POrd a, PEq a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
geqE' :: forall (a :: PType) (s :: S).
(POrd a, PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
geqE' Term s a
a PExtended a s
y = forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
a PExtended a s
y forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
eqE' Term s a
a PExtended a s
y

-- | (x :: Term s (PExtended a)) <= (y :: Term s (PExtended b))
leqE ::
  forall a (s :: S).
  (PEq a, POrd a, PIsData a) =>
  Term
    s
    ( PExtended a
        :--> PExtended a
        :--> PBool
    )
leqE :: forall (a :: PType) (s :: S).
(PEq a, POrd a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
leqE = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
x Term s (PExtended a)
y -> forall (a :: PType) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
ltE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
y forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| forall (a :: PType) (s :: S).
(PEq a, PIsData a) =>
Term s (PExtended a :--> (PExtended a :--> PBool))
eqE forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
y

isNegInf :: PExtended a s -> Term s PBool
isNegInf :: forall (a :: PType) (s :: S). PExtended a s -> Term s PBool
isNegInf PExtended a s
x = case PExtended a s
x of
  PNegInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  PExtended a s
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

isPosInf :: PExtended a s -> Term s PBool
isPosInf :: forall (a :: PType) (s :: S). PExtended a s -> Term s PBool
isPosInf PExtended a s
x = case PExtended a s
x of
  PPosInf Term s (PDataRecord ('[] @PLabeledType))
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  PExtended a s
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

type EndPoint a =
  PDataRecord
    '[ "_0" ':= PExtended a
     , "_1" ':= PClosure
     ]

uToE :: Term s (PUpperBound a :--> EndPoint a)
uToE :: forall (s :: S) (a :: PType).
Term s (PUpperBound a :--> EndPoint a)
uToE = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PUpperBound a)
x -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PUpperBound a)
x (\(PUpperBound Term s (EndPoint a)
a) -> Term s (EndPoint a)
a)

lToE :: Term s (PLowerBound a :--> EndPoint a)
lToE :: forall (s :: S) (a :: PType).
Term s (PLowerBound a :--> EndPoint a)
lToE = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
x -> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PLowerBound a)
x (\(PLowerBound Term s (EndPoint a)
a) -> Term s (EndPoint a)
a)