{-# OPTIONS_GHC -Wno-orphans #-}

{- | This module is meant to be imported qualified, as some of its identifiers
clash with the Plutarch prelude, as well as other parts of the Plutarch API.
-}
module Plutarch.LedgerApi.Interval (
  -- * Types
  PInterval (..),
  PLowerBound (..),
  PUpperBound (..),
  PExtended (..),

  -- * Functions

  -- ** Creation
  psingleton,
  pfrom,
  pto,
  palways,
  pinterval,
  pinclusiveLowerBound,
  pinclusiveUpperBound,

  -- ** Queries
  pmember,
  pcontains,
  pbefore,
  pafter,
  pisEmpty,

  -- ** Transformation
  phull,
  pintersection,
) where

import Data.Kind (Type)
import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Plutarch.Prelude hiding (psingleton, pto)
import PlutusLedgerApi.V3 qualified as Plutus

-- | @since 2.0.0
data PInterval (a :: S -> Type) (s :: S) = PInterval
  { forall (a :: S -> Type) (s :: S).
PInterval a s -> Term s (PLowerBound a)
pinteral'from :: Term s (PLowerBound a)
  , forall (a :: S -> Type) (s :: S).
PInterval a s -> Term s (PUpperBound a)
pinteral'to :: Term s (PUpperBound a)
  }
  deriving stock
    ( -- | @since 2.0.0
      (forall x. PInterval a s -> Rep (PInterval a s) x)
-> (forall x. Rep (PInterval a s) x -> PInterval a s)
-> Generic (PInterval a s)
forall x. Rep (PInterval a s) x -> PInterval a s
forall x. PInterval a s -> Rep (PInterval a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x.
Rep (PInterval a s) x -> PInterval a s
forall (a :: S -> Type) (s :: S) x.
PInterval a s -> Rep (PInterval a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PInterval a s -> Rep (PInterval a s) x
from :: forall x. PInterval a s -> Rep (PInterval a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PInterval a s) x -> PInterval a s
to :: forall x. Rep (PInterval a s) x -> PInterval a s
Generic
    )
  deriving anyclass
    ( -- | @since 2.0.0
      All SListI (Code (PInterval a s))
All SListI (Code (PInterval a s)) =>
(PInterval a s -> Rep (PInterval a s))
-> (Rep (PInterval a s) -> PInterval a s)
-> Generic (PInterval a s)
Rep (PInterval a s) -> PInterval a s
PInterval a s -> Rep (PInterval a s)
forall a.
All SListI (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S). All SListI (Code (PInterval a s))
forall (a :: S -> Type) (s :: S).
Rep (PInterval a s) -> PInterval a s
forall (a :: S -> Type) (s :: S).
PInterval a s -> Rep (PInterval a s)
$cfrom :: forall (a :: S -> Type) (s :: S).
PInterval a s -> Rep (PInterval a s)
from :: PInterval a s -> Rep (PInterval a s)
$cto :: forall (a :: S -> Type) (s :: S).
Rep (PInterval a s) -> PInterval a s
to :: Rep (PInterval a s) -> PInterval a s
SOP.Generic
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PAsData (PInterval a)) -> Term s (PInterval a))
-> (forall (s :: S). Term s (PInterval a) -> Term s PData)
-> PIsData (PInterval a)
forall (s :: S).
Term s (PAsData (PInterval a)) -> Term s (PInterval a)
forall (s :: S). Term s (PInterval a) -> Term s PData
forall (a :: S -> Type).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
forall (a :: S -> Type) (s :: S).
Term s (PAsData (PInterval a)) -> Term s (PInterval a)
forall (a :: S -> Type) (s :: S).
Term s (PInterval a) -> Term s PData
$cpfromDataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PAsData (PInterval a)) -> Term s (PInterval a)
pfromDataImpl :: forall (s :: S).
Term s (PAsData (PInterval a)) -> Term s (PInterval a)
$cpdataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PInterval a) -> Term s PData
pdataImpl :: forall (s :: S). Term s (PInterval a) -> Term s PData
PIsData
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool)
-> PEq (PInterval a)
forall (s :: S).
Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool
#== :: forall (s :: S).
Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool
PEq
    , -- | @since 2.0.0
      (forall (s :: S). Bool -> Term s (PInterval a) -> Term s PString)
-> PShow (PInterval a)
forall (s :: S). Bool -> Term s (PInterval a) -> Term s PString
forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PInterval a) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PInterval a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PInterval a) -> Term s PString
PShow
    )
  deriving
    ( -- | @since 3.3.0
      (forall (s :: S). PInterval a s -> Term s (PInner (PInterval a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PInterval a))
    -> (PInterval a s -> Term s b) -> Term s b)
-> PlutusType (PInterval a)
forall (s :: S). PInterval a s -> Term s (PInner (PInterval a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PInterval a))
-> (PInterval a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PInterval a s -> Term s (PInner (PInterval a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PInterval a))
-> (PInterval a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PInterval a s -> Term s (PInner (PInterval a))
pcon' :: forall (s :: S). PInterval a s -> Term s (PInner (PInterval a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PInterval a))
-> (PInterval a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PInterval a))
-> (PInterval a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveAsDataStruct (PInterval a))

-- | @since 3.3.0
deriving via
  DeriveDataPLiftable (PInterval a) (Plutus.Interval (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PInterval a)

-- | @since 2.0.0
data PLowerBound (a :: S -> Type) (s :: S)
  = PLowerBound (Term s (PExtended a)) (Term s (PAsData PBool))
  deriving stock
    ( -- | @since 2.0.0
      (forall x. PLowerBound a s -> Rep (PLowerBound a s) x)
-> (forall x. Rep (PLowerBound a s) x -> PLowerBound a s)
-> Generic (PLowerBound a s)
forall x. Rep (PLowerBound a s) x -> PLowerBound a s
forall x. PLowerBound a s -> Rep (PLowerBound a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x.
Rep (PLowerBound a s) x -> PLowerBound a s
forall (a :: S -> Type) (s :: S) x.
PLowerBound a s -> Rep (PLowerBound a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PLowerBound a s -> Rep (PLowerBound a s) x
from :: forall x. PLowerBound a s -> Rep (PLowerBound a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PLowerBound a s) x -> PLowerBound a s
to :: forall x. Rep (PLowerBound a s) x -> PLowerBound a s
Generic
    )
  deriving anyclass
    ( -- | @since 2.0.0
      All SListI (Code (PLowerBound a s))
All SListI (Code (PLowerBound a s)) =>
(PLowerBound a s -> Rep (PLowerBound a s))
-> (Rep (PLowerBound a s) -> PLowerBound a s)
-> Generic (PLowerBound a s)
Rep (PLowerBound a s) -> PLowerBound a s
PLowerBound a s -> Rep (PLowerBound a s)
forall a.
All SListI (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S).
All SListI (Code (PLowerBound a s))
forall (a :: S -> Type) (s :: S).
Rep (PLowerBound a s) -> PLowerBound a s
forall (a :: S -> Type) (s :: S).
PLowerBound a s -> Rep (PLowerBound a s)
$cfrom :: forall (a :: S -> Type) (s :: S).
PLowerBound a s -> Rep (PLowerBound a s)
from :: PLowerBound a s -> Rep (PLowerBound a s)
$cto :: forall (a :: S -> Type) (s :: S).
Rep (PLowerBound a s) -> PLowerBound a s
to :: Rep (PLowerBound a s) -> PLowerBound a s
SOP.Generic
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a))
-> (forall (s :: S). Term s (PLowerBound a) -> Term s PData)
-> PIsData (PLowerBound a)
forall (s :: S).
Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
forall (s :: S). Term s (PLowerBound a) -> Term s PData
forall (a :: S -> Type).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
forall (a :: S -> Type) (s :: S).
Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a) -> Term s PData
$cpfromDataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
pfromDataImpl :: forall (s :: S).
Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
$cpdataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a) -> Term s PData
pdataImpl :: forall (s :: S). Term s (PLowerBound a) -> Term s PData
PIsData
    , -- | @since 2.0.0
      (forall (s :: S). Bool -> Term s (PLowerBound a) -> Term s PString)
-> PShow (PLowerBound a)
forall (s :: S). Bool -> Term s (PLowerBound a) -> Term s PString
forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PLowerBound a) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PLowerBound a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PLowerBound a) -> Term s PString
PShow
    )
  deriving
    ( -- | @since 3.3.0
      (forall (s :: S).
 PLowerBound a s -> Term s (PInner (PLowerBound a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PLowerBound a))
    -> (PLowerBound a s -> Term s b) -> Term s b)
-> PlutusType (PLowerBound a)
forall (s :: S). PLowerBound a s -> Term s (PInner (PLowerBound a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PLowerBound a))
-> (PLowerBound a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PLowerBound a s -> Term s (PInner (PLowerBound a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PLowerBound a))
-> (PLowerBound a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PLowerBound a s -> Term s (PInner (PLowerBound a))
pcon' :: forall (s :: S). PLowerBound a s -> Term s (PInner (PLowerBound a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PLowerBound a))
-> (PLowerBound a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PLowerBound a))
-> (PLowerBound a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveAsDataStruct (PLowerBound a))

deriving via
  DeriveDataPLiftable (PLowerBound a) (Plutus.LowerBound (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PLowerBound a)

-- | @since 3.3.0
instance (PIsData a, PCountable a) => PEq (PLowerBound a) where
  {-# INLINEABLE (#==) #-}
  Term s (PLowerBound a)
lb1 #== :: forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
#== Term s (PLowerBound a)
lb2 = (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb2)

-- | @since 3.3.0
instance (PIsData a, PCountable a) => POrd (PLowerBound a) where
  {-# INLINEABLE (#<=) #-}
  Term s (PLowerBound a)
lb1 #<= :: forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
#<= Term s (PLowerBound a)
lb2 = (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb2)
  {-# INLINEABLE (#<) #-}
  Term s (PLowerBound a)
lb1 #< :: forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
#< Term s (PLowerBound a)
lb2 = (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb2)

-- | @since 2.0.0
data PUpperBound (a :: S -> Type) (s :: S)
  = PUpperBound (Term s (PExtended a)) (Term s (PAsData PBool))
  deriving stock
    ( -- | @since 2.0.0
      (forall x. PUpperBound a s -> Rep (PUpperBound a s) x)
-> (forall x. Rep (PUpperBound a s) x -> PUpperBound a s)
-> Generic (PUpperBound a s)
forall x. Rep (PUpperBound a s) x -> PUpperBound a s
forall x. PUpperBound a s -> Rep (PUpperBound a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x.
Rep (PUpperBound a s) x -> PUpperBound a s
forall (a :: S -> Type) (s :: S) x.
PUpperBound a s -> Rep (PUpperBound a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PUpperBound a s -> Rep (PUpperBound a s) x
from :: forall x. PUpperBound a s -> Rep (PUpperBound a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PUpperBound a s) x -> PUpperBound a s
to :: forall x. Rep (PUpperBound a s) x -> PUpperBound a s
Generic
    )
  deriving anyclass
    ( -- | @since 2.0.0
      All SListI (Code (PUpperBound a s))
All SListI (Code (PUpperBound a s)) =>
(PUpperBound a s -> Rep (PUpperBound a s))
-> (Rep (PUpperBound a s) -> PUpperBound a s)
-> Generic (PUpperBound a s)
Rep (PUpperBound a s) -> PUpperBound a s
PUpperBound a s -> Rep (PUpperBound a s)
forall a.
All SListI (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S).
All SListI (Code (PUpperBound a s))
forall (a :: S -> Type) (s :: S).
Rep (PUpperBound a s) -> PUpperBound a s
forall (a :: S -> Type) (s :: S).
PUpperBound a s -> Rep (PUpperBound a s)
$cfrom :: forall (a :: S -> Type) (s :: S).
PUpperBound a s -> Rep (PUpperBound a s)
from :: PUpperBound a s -> Rep (PUpperBound a s)
$cto :: forall (a :: S -> Type) (s :: S).
Rep (PUpperBound a s) -> PUpperBound a s
to :: Rep (PUpperBound a s) -> PUpperBound a s
SOP.Generic
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a))
-> (forall (s :: S). Term s (PUpperBound a) -> Term s PData)
-> PIsData (PUpperBound a)
forall (s :: S).
Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
forall (s :: S). Term s (PUpperBound a) -> Term s PData
forall (a :: S -> Type).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
forall (a :: S -> Type) (s :: S).
Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
Term s (PUpperBound a) -> Term s PData
$cpfromDataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
pfromDataImpl :: forall (s :: S).
Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
$cpdataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PUpperBound a) -> Term s PData
pdataImpl :: forall (s :: S). Term s (PUpperBound a) -> Term s PData
PIsData
    , -- | @since 2.0.0
      (forall (s :: S). Bool -> Term s (PUpperBound a) -> Term s PString)
-> PShow (PUpperBound a)
forall (s :: S). Bool -> Term s (PUpperBound a) -> Term s PString
forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PUpperBound a) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PUpperBound a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PUpperBound a) -> Term s PString
PShow
    )
  deriving
    ( -- | @since 3.3.0
      (forall (s :: S).
 PUpperBound a s -> Term s (PInner (PUpperBound a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PUpperBound a))
    -> (PUpperBound a s -> Term s b) -> Term s b)
-> PlutusType (PUpperBound a)
forall (s :: S). PUpperBound a s -> Term s (PInner (PUpperBound a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PUpperBound a))
-> (PUpperBound a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PUpperBound a s -> Term s (PInner (PUpperBound a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PUpperBound a))
-> (PUpperBound a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PUpperBound a s -> Term s (PInner (PUpperBound a))
pcon' :: forall (s :: S). PUpperBound a s -> Term s (PInner (PUpperBound a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PUpperBound a))
-> (PUpperBound a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PUpperBound a))
-> (PUpperBound a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveAsDataStruct (PUpperBound a))

deriving via
  DeriveDataPLiftable (PUpperBound a) (Plutus.UpperBound (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PUpperBound a)

-- | @since 3.3.0
instance (PIsData a, PEnumerable a) => PEq (PUpperBound a) where
  {-# INLINEABLE (#==) #-}
  Term s (PUpperBound a)
ub1 #== :: forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
#== Term s (PUpperBound a)
ub2 = (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub2)

-- | @since 3.3.0
instance (PIsData a, PEnumerable a) => POrd (PUpperBound a) where
  {-# INLINEABLE (#<=) #-}
  Term s (PUpperBound a)
ub1 #<= :: forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
#<= Term s (PUpperBound a)
ub2 = (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub2)
  {-# INLINEABLE (#<) #-}
  Term s (PUpperBound a)
ub1 #< :: forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
#< Term s (PUpperBound a)
ub2 = (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub2)

-- | @since 2.0.0
data PExtended (a :: S -> Type) (s :: S)
  = PNegInf
  | PFinite (Term s (PAsData a))
  | PPosInf
  deriving stock
    ( -- | @since 2.0.0
      (forall x. PExtended a s -> Rep (PExtended a s) x)
-> (forall x. Rep (PExtended a s) x -> PExtended a s)
-> Generic (PExtended a s)
forall x. Rep (PExtended a s) x -> PExtended a s
forall x. PExtended a s -> Rep (PExtended a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x.
Rep (PExtended a s) x -> PExtended a s
forall (a :: S -> Type) (s :: S) x.
PExtended a s -> Rep (PExtended a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PExtended a s -> Rep (PExtended a s) x
from :: forall x. PExtended a s -> Rep (PExtended a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PExtended a s) x -> PExtended a s
to :: forall x. Rep (PExtended a s) x -> PExtended a s
Generic
    )
  deriving anyclass
    ( -- | @since 2.0.0
      All SListI (Code (PExtended a s))
All SListI (Code (PExtended a s)) =>
(PExtended a s -> Rep (PExtended a s))
-> (Rep (PExtended a s) -> PExtended a s)
-> Generic (PExtended a s)
Rep (PExtended a s) -> PExtended a s
PExtended a s -> Rep (PExtended a s)
forall a.
All SListI (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S). All SListI (Code (PExtended a s))
forall (a :: S -> Type) (s :: S).
Rep (PExtended a s) -> PExtended a s
forall (a :: S -> Type) (s :: S).
PExtended a s -> Rep (PExtended a s)
$cfrom :: forall (a :: S -> Type) (s :: S).
PExtended a s -> Rep (PExtended a s)
from :: PExtended a s -> Rep (PExtended a s)
$cto :: forall (a :: S -> Type) (s :: S).
Rep (PExtended a s) -> PExtended a s
to :: Rep (PExtended a s) -> PExtended a s
SOP.Generic
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PAsData (PExtended a)) -> Term s (PExtended a))
-> (forall (s :: S). Term s (PExtended a) -> Term s PData)
-> PIsData (PExtended a)
forall (s :: S).
Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (s :: S). Term s (PExtended a) -> Term s PData
forall (a :: S -> Type).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
forall (a :: S -> Type) (s :: S).
Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s PData
$cpfromDataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PAsData (PExtended a)) -> Term s (PExtended a)
pfromDataImpl :: forall (s :: S).
Term s (PAsData (PExtended a)) -> Term s (PExtended a)
$cpdataImpl :: forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s PData
pdataImpl :: forall (s :: S). Term s (PExtended a) -> Term s PData
PIsData
    , -- | @since 2.0.0
      (forall (s :: S).
 Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
-> PEq (PExtended a)
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
$c#== :: forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
#== :: forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
PEq
    , -- | @since 2.0.0
      (forall (s :: S). Bool -> Term s (PExtended a) -> Term s PString)
-> PShow (PExtended a)
forall (s :: S). Bool -> Term s (PExtended a) -> Term s PString
forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PExtended a) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PExtended a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PExtended a) -> Term s PString
PShow
    )
  deriving
    ( -- | @since 3.3.0
      (forall (s :: S). PExtended a s -> Term s (PInner (PExtended a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PExtended a))
    -> (PExtended a s -> Term s b) -> Term s b)
-> PlutusType (PExtended a)
forall (s :: S). PExtended a s -> Term s (PInner (PExtended a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PExtended a))
-> (PExtended a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PExtended a s -> Term s (PInner (PExtended a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PExtended a))
-> (PExtended a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PExtended a s -> Term s (PInner (PExtended a))
pcon' :: forall (s :: S). PExtended a s -> Term s (PInner (PExtended a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PExtended a))
-> (PExtended a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PExtended a))
-> (PExtended a s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveAsDataStruct (PExtended a))

deriving via
  DeriveDataPLiftable (PExtended a) (Plutus.Extended (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PExtended a)

-- phoistAcyclic is used because comparators generates very large code.
instance (POrd a, PIsData a) => POrd (PExtended a) where
  Term s (PExtended a)
x #<= :: forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
#<= Term s (PExtended a)
y = Term s (PExtended a :--> (PExtended a :--> PBool))
forall {s :: S}. Term s (PExtended a :--> (PExtended a :--> PBool))
f Term s (PExtended a :--> (PExtended a :--> PBool))
-> Term s (PExtended a) -> Term s (PExtended a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
x Term s (PExtended a :--> PBool)
-> Term s (PExtended a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
y
    where
      f :: Term s (PExtended a :--> (PExtended a :--> PBool))
f = (forall {s :: S}.
 Term s (PExtended a :--> (PExtended a :--> PBool)))
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall {s :: S}.
  Term s (PExtended a :--> (PExtended a :--> PBool)))
 -> Term s (PExtended a :--> (PExtended a :--> PBool)))
-> (forall {s :: S}.
    Term s (PExtended a :--> (PExtended a :--> PBool)))
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a b. (a -> b) -> a -> b
$
        (Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a) -> Term s PBool)
-> Term s (c :--> (PExtended a :--> PBool))
plam ((Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
 -> Term s (PExtended a :--> (PExtended a :--> PBool)))
-> (Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
a Term s (PExtended a)
b ->
          Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
a ((PExtended a s -> Term s PBool) -> Term s PBool)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \PExtended a s
a' ->
            Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
b ((PExtended a s -> Term s PBool) -> Term s PBool)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \PExtended a s
b' ->
              case (PExtended a s
a', PExtended a s
b') of
                (PExtended a s
PNegInf, PExtended a s
PNegInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
PNegInf, PExtended a s
_) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
_, PExtended a s
PNegInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PExtended a s
PPosInf, PExtended a s
PPosInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
_, PExtended a s
PPosInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
PPosInf, PExtended a s
_) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PFinite Term s (PAsData a)
l, PFinite Term s (PAsData a)
r) -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
l Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
r

  Term s (PExtended a)
x #< :: forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
#< Term s (PExtended a)
y = Term s (PExtended a :--> (PExtended a :--> PBool))
forall {s :: S}. Term s (PExtended a :--> (PExtended a :--> PBool))
f Term s (PExtended a :--> (PExtended a :--> PBool))
-> Term s (PExtended a) -> Term s (PExtended a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
x Term s (PExtended a :--> PBool)
-> Term s (PExtended a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
y
    where
      f :: Term s (PExtended a :--> (PExtended a :--> PBool))
f = (forall {s :: S}.
 Term s (PExtended a :--> (PExtended a :--> PBool)))
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall {s :: S}.
  Term s (PExtended a :--> (PExtended a :--> PBool)))
 -> Term s (PExtended a :--> (PExtended a :--> PBool)))
-> (forall {s :: S}.
    Term s (PExtended a :--> (PExtended a :--> PBool)))
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a b. (a -> b) -> a -> b
$
        (Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a) -> Term s PBool)
-> Term s (c :--> (PExtended a :--> PBool))
plam ((Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
 -> Term s (PExtended a :--> (PExtended a :--> PBool)))
-> (Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool)
-> Term s (PExtended a :--> (PExtended a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
a Term s (PExtended a)
b ->
          Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
a ((PExtended a s -> Term s PBool) -> Term s PBool)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \PExtended a s
a' ->
            Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
b ((PExtended a s -> Term s PBool) -> Term s PBool)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \PExtended a s
b' ->
              case (PExtended a s
a', PExtended a s
b') of
                (PExtended a s
PNegInf, PExtended a s
PNegInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PExtended a s
PNegInf, PExtended a s
_) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
_, PExtended a s
PNegInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PExtended a s
PPosInf, PExtended a s
PPosInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PExtended a s
_, PExtended a s
PPosInf) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
                (PExtended a s
PPosInf, PExtended a s
_) -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
                (PFinite Term s (PAsData a)
l, PFinite Term s (PAsData a)
r) -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
l Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
r

{- | Check if a value is inside the given interval.

@since 3.3.0
-}
pmember ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PEnumerable a) =>
  Term
    s
    ( PAsData a
        :--> PInterval a
        :--> PBool
    )
pmember :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PAsData a :--> (PInterval a :--> PBool))
pmember = ClosedTerm (PAsData a :--> (PInterval a :--> PBool))
-> Term s (PAsData a :--> (PInterval a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> (PInterval a :--> PBool))
 -> Term s (PAsData a :--> (PInterval a :--> PBool)))
-> ClosedTerm (PAsData a :--> (PInterval a :--> PBool))
-> Term s (PAsData a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData a) -> Term s (PInterval a) -> Term s PBool)
-> Term s (PAsData a :--> (PInterval a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s PBool)
-> Term s (c :--> (PInterval a :--> PBool))
plam ((Term s (PAsData a) -> Term s (PInterval a) -> Term s PBool)
 -> Term s (PAsData a :--> (PInterval a :--> PBool)))
-> (Term s (PAsData a) -> Term s (PInterval a) -> Term s PBool)
-> Term s (PAsData a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
x Term s (PInterval a)
i -> Term s (PInterval a :--> (PInterval a :--> PBool))
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a :--> (PInterval a :--> PBool))
pcontains Term s (PInterval a :--> (PInterval a :--> PBool))
-> Term s (PInterval a) -> Term s (PInterval a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInterval a)
i Term s (PInterval a :--> PBool)
-> Term s (PInterval a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PAsData a :--> PInterval a)
forall (a :: S -> Type) (s :: S).
Term s (PAsData a :--> PInterval a)
psingleton Term s (PAsData a :--> PInterval a)
-> Term s (PAsData a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
x)

{- | Check if a 'PInterval' is empty.

@since 3.3.0
-}
pisEmpty ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PEnumerable a) =>
  Term s (PInterval a :--> PBool)
pisEmpty :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a :--> PBool)
pisEmpty = ClosedTerm (PInterval a :--> PBool)
-> Term s (PInterval a :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInterval a :--> PBool)
 -> Term s (PInterval a :--> PBool))
-> ClosedTerm (PInterval a :--> PBool)
-> Term s (PInterval a :--> PBool)
forall a b. (a -> b) -> a -> b
$ (Term s (PInterval a) -> Term s PBool)
-> Term s (PInterval a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PBool) -> Term s (c :--> PBool)
plam ((Term s (PInterval a) -> Term s PBool)
 -> Term s (PInterval a :--> PBool))
-> (Term s (PInterval a) -> Term s PBool)
-> Term s (PInterval a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
i -> TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
  PInterval Term s (PLowerBound a)
lowerBound Term s (PUpperBound a)
upperBound <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
i
  let inclusiveLowerBound :: Term s (PExtended a)
inclusiveLowerBound = Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerBound
  let inclusiveUpperBound :: Term s (PExtended a)
inclusiveUpperBound = Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperBound
  Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PExtended a)
inclusiveLowerBound Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
inclusiveUpperBound

{- | Turn a 'PLowerBound' into a single inclusive bounding value.

@since 3.3.0
-}
pinclusiveLowerBound ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PCountable a) =>
  Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound :: forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound = ClosedTerm (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PLowerBound a :--> PExtended a)
 -> Term s (PLowerBound a :--> PExtended a))
-> ClosedTerm (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a :--> PExtended a)
forall a b. (a -> b) -> a -> b
$ (Term s (PLowerBound a) -> Term s (PExtended a))
-> Term s (PLowerBound a :--> PExtended a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a)) -> Term s (c :--> PExtended a)
plam ((Term s (PLowerBound a) -> Term s (PExtended a))
 -> Term s (PLowerBound a :--> PExtended a))
-> (Term s (PLowerBound a) -> Term s (PExtended a))
-> Term s (PLowerBound a :--> PExtended a)
forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
lb -> TermCont s (Term s (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PExtended a)) -> Term s (PExtended a))
-> TermCont s (Term s (PExtended a)) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ do
  PLowerBound Term s (PExtended a)
extended Term s (PAsData PBool)
closure <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
lb
  Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PExtended a) -> TermCont s (Term s (PExtended a)))
-> Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall a b. (a -> b) -> a -> b
$
    Term s PBool
-> Term s (PExtended a)
-> Term s (PExtended a)
-> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
closure)
      -- We are already closed
      Term s (PExtended a)
extended
      ( Term s (PExtended a)
-> (PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
extended ((PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a))
-> (PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ \case
          -- Open at a finite value, get its successor
          PFinite Term s (PAsData a)
t -> PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite (Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s a -> Term s (PAsData a)) -> Term s a -> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t)
          -- We have an infinity, who cares
          PExtended a s
_ -> Term s (PExtended a)
extended
      )

{- | Turn a 'PUpperBound' into a single inclusive bounding value.

@since 3.3.0
-}
pinclusiveUpperBound ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PEnumerable a) =>
  Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound = ClosedTerm (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PUpperBound a :--> PExtended a)
 -> Term s (PUpperBound a :--> PExtended a))
-> ClosedTerm (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a :--> PExtended a)
forall a b. (a -> b) -> a -> b
$ (Term s (PUpperBound a) -> Term s (PExtended a))
-> Term s (PUpperBound a :--> PExtended a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a)) -> Term s (c :--> PExtended a)
plam ((Term s (PUpperBound a) -> Term s (PExtended a))
 -> Term s (PUpperBound a :--> PExtended a))
-> (Term s (PUpperBound a) -> Term s (PExtended a))
-> Term s (PUpperBound a :--> PExtended a)
forall a b. (a -> b) -> a -> b
$ \Term s (PUpperBound a)
ub -> TermCont s (Term s (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PExtended a)) -> Term s (PExtended a))
-> TermCont s (Term s (PExtended a)) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ do
  PUpperBound Term s (PExtended a)
extended Term s (PAsData PBool)
closure <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
ub
  Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PExtended a) -> TermCont s (Term s (PExtended a)))
-> Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall a b. (a -> b) -> a -> b
$
    Term s PBool
-> Term s (PExtended a)
-> Term s (PExtended a)
-> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
closure)
      -- We are already closed
      Term s (PExtended a)
extended
      ( Term s (PExtended a)
-> (PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
extended ((PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a))
-> (PExtended a s -> Term s (PExtended a)) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ \case
          -- Open at a finite value, get its predecessor
          PFinite Term s (PAsData a)
t ->
            PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite (Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s a -> Term s (PAsData a)) -> Term s a -> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t)
          -- We have an infinity, who cares
          PExtended a s
_ -> Term s (PExtended a)
extended
      )

{- | @'pcontains' # i1 # i2@ is true if @i2@ is entirely contained in @i1@: more
specifically, if for any @s@, if @'pmember' # s # i2@, then @'pmember' # s #
i1@.

@since 3.3.0
-}
pcontains ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PEnumerable a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PBool
    )
pcontains :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a :--> (PInterval a :--> PBool))
pcontains = ClosedTerm (PInterval a :--> (PInterval a :--> PBool))
-> Term s (PInterval a :--> (PInterval a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInterval a :--> (PInterval a :--> PBool))
 -> Term s (PInterval a :--> (PInterval a :--> PBool)))
-> ClosedTerm (PInterval a :--> (PInterval a :--> PBool))
-> Term s (PInterval a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool)
-> Term s (PInterval a :--> (PInterval a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s PBool)
-> Term s (c :--> (PInterval a :--> PBool))
plam ((Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool)
 -> Term s (PInterval a :--> (PInterval a :--> PBool)))
-> (Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool)
-> Term s (PInterval a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
i1 Term s (PInterval a)
i2 -> TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
  PInterval Term s (PLowerBound a)
l1' Term s (PUpperBound a)
u1' <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
i1
  PInterval Term s (PLowerBound a)
l2' Term s (PUpperBound a)
u2' <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
i2
  Term s (PLowerBound a)
l1 <- Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PLowerBound a)
l1'
  Term s (PUpperBound a)
u1 <- Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PUpperBound a)
u1'
  Term s (PLowerBound a)
l2 <- Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PLowerBound a)
l2'
  Term s (PUpperBound a)
u2 <- Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PUpperBound a)
u2'
  -- Note: This manually inlines `pisEmpty` to avoid redundant unpacking.
  let ilb2 :: Term s (PExtended a)
ilb2 = Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
l2
  let iub2 :: Term s (PExtended a)
iub2 = Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
u2
  Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
    Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s (PExtended a)
ilb2 Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
iub2)
      -- i2 is empty, so therefore it must be contained in i1
      (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue)
      ( TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
          let ilb1 :: Term s (PExtended a)
ilb1 = Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
l1
          let iub1 :: Term s (PExtended a)
iub1 = Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
u1
          Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
            Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (Term s (PExtended a)
ilb1 Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
iub1)
              -- i1 is empty, so therefore it cannot contain
              -- anything
              (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)
              -- Neither interval is empty, so compare bounds
              ((Term s (PLowerBound a)
l1 Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PLowerBound a)
l2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (PUpperBound a)
u2 Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PUpperBound a)
u1))
      )

{- | Given @x@, create the interval @[x, x]@.

@since 2.1.1
-}
psingleton ::
  forall (a :: S -> Type) (s :: S).
  Term s (PAsData a :--> PInterval a)
psingleton :: forall (a :: S -> Type) (s :: S).
Term s (PAsData a :--> PInterval a)
psingleton = ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> PInterval a)
 -> Term s (PAsData a :--> PInterval a))
-> ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a)) -> Term s (c :--> PInterval a)
plam ((Term s (PAsData a) -> Term s (PInterval a))
 -> Term s (PAsData a :--> PInterval a))
-> (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
x ->
    Term s (PExtended a)
-> (Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite Term s (PAsData a)
x) ((Term s (PExtended a) -> Term s (PInterval a))
 -> Term s (PInterval a))
-> (Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PInterval a)
forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
start ->
      Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval Term s (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a) -> Term s (PExtended a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start Term s (PExtended a :--> PInterval a)
-> Term s (PExtended a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start

{- | Given @x@, create the interval @[x, +infty)@

@since 2.1.1
-}
pfrom ::
  forall (a :: S -> Type) (s :: S).
  Term s (PAsData a :--> PInterval a)
pfrom :: forall (a :: S -> Type) (s :: S).
Term s (PAsData a :--> PInterval a)
pfrom = ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> PInterval a)
 -> Term s (PAsData a :--> PInterval a))
-> ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a)) -> Term s (c :--> PInterval a)
plam ((Term s (PAsData a) -> Term s (PInterval a))
 -> Term s (PAsData a :--> PInterval a))
-> (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a ->
    let start :: Term s (PExtended a)
start = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite Term s (PAsData a)
a
        end :: Term s (PExtended a)
end = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PExtended a s
forall (a :: S -> Type) (s :: S). PExtended a s
PPosInf
     in Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval Term s (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a) -> Term s (PExtended a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start Term s (PExtended a :--> PInterval a)
-> Term s (PExtended a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
forall {s :: S} {a :: S -> Type}. Term s (PExtended a)
end

{- | Given @x@, create the interval @(-infty, x]@.

@since 2.1.1
-}
pto ::
  forall (a :: S -> Type) (s :: S).
  Term s (PAsData a :--> PInterval a)
pto :: forall (a :: S -> Type) (s :: S).
Term s (PAsData a :--> PInterval a)
pto = ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> PInterval a)
 -> Term s (PAsData a :--> PInterval a))
-> ClosedTerm (PAsData a :--> PInterval a)
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a)) -> Term s (c :--> PInterval a)
plam ((Term s (PAsData a) -> Term s (PInterval a))
 -> Term s (PAsData a :--> PInterval a))
-> (Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> PInterval a)
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
a ->
    let start :: Term s (PExtended a)
start = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PExtended a s
forall (a :: S -> Type) (s :: S). PExtended a s
PNegInf
        end :: Term s (PExtended a)
end = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite Term s (PAsData a)
a
     in Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval Term s (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a) -> Term s (PExtended a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
forall {s :: S} {a :: S -> Type}. Term s (PExtended a)
start Term s (PExtended a :--> PInterval a)
-> Term s (PExtended a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
end

-- TODO: Rename this, as this name is too specific to slots.

{- | Create the interval @(-infty, +infty)@.

@since 2.1.1
-}
palways ::
  forall (a :: S -> Type) (s :: S).
  (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) =>
  Term s (PInterval a)
palways :: forall (a :: S -> Type) (s :: S).
(FromData (AsHaskell a), ToData (AsHaskell a)) =>
Term s (PInterval a)
palways = AsHaskell (PInterval a) -> Term s (PInterval a)
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell (PInterval a)
Interval (AsHaskell a)
forall a. Interval a
Plutus.always

{- | @'phull' i1 i2@ gives the smallest interval that contains both @i1@ and
@i2@.

@since 2.1.1
-}
phull ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PInterval a
    )
phull :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PInterval a))
phull = ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
 -> Term s (PInterval a :--> (PInterval a :--> PInterval a)))
-> ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PInterval a)
 -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (c :--> (PInterval a :--> PInterval a))
plam ((Term s (PInterval a)
  -> Term s (PInterval a) -> Term s (PInterval a))
 -> Term s (PInterval a :--> (PInterval a :--> PInterval a)))
-> (Term s (PInterval a)
    -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
x' Term s (PInterval a)
y' -> TermCont s (Term s (PInterval a)) -> Term s (PInterval a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PInterval a)) -> Term s (PInterval a))
-> TermCont s (Term s (PInterval a)) -> Term s (PInterval a)
forall a b. (a -> b) -> a -> b
$ do
    PInterval Term s (PLowerBound a)
lowerX Term s (PUpperBound a)
upperX <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
x'
    PInterval Term s (PLowerBound a)
lowerY Term s (PUpperBound a)
upperY <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
y'
    let lower :: Term s (PLowerBound a)
lower = Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
minLower Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a)
-> Term s (PLowerBound a :--> PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerX Term s (PLowerBound a :--> PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerY
    let upper :: Term s (PUpperBound a)
upper = Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
maxUpper Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a)
-> Term s (PUpperBound a :--> PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperX Term s (PUpperBound a :--> PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperY
    Term s (PInterval a) -> TermCont s (Term s (PInterval a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PInterval a) -> TermCont s (Term s (PInterval a)))
-> Term s (PInterval a) -> TermCont s (Term s (PInterval a))
forall a b. (a -> b) -> a -> b
$ Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
pinterval' Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
-> Term s (PLowerBound a)
-> Term s (PUpperBound a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lower Term s (PUpperBound a :--> PInterval a)
-> Term s (PUpperBound a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upper

{- | @'pintersection' i1 i2@ gives the largest interval that is contained in
both @i1@ and @i2@.

@since 2.1.1
-}
pintersection ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term
    s
    ( PInterval a
        :--> PInterval a
        :--> PInterval a
    )
pintersection :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PInterval a :--> (PInterval a :--> PInterval a))
pintersection = ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
 -> Term s (PInterval a :--> (PInterval a :--> PInterval a)))
-> ClosedTerm (PInterval a :--> (PInterval a :--> PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PInterval a)
 -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (c :--> (PInterval a :--> PInterval a))
plam ((Term s (PInterval a)
  -> Term s (PInterval a) -> Term s (PInterval a))
 -> Term s (PInterval a :--> (PInterval a :--> PInterval a)))
-> (Term s (PInterval a)
    -> Term s (PInterval a) -> Term s (PInterval a))
-> Term s (PInterval a :--> (PInterval a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PInterval a)
x' Term s (PInterval a)
y' -> TermCont s (Term s (PInterval a)) -> Term s (PInterval a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PInterval a)) -> Term s (PInterval a))
-> TermCont s (Term s (PInterval a)) -> Term s (PInterval a)
forall a b. (a -> b) -> a -> b
$ do
    PInterval Term s (PLowerBound a)
lowerX Term s (PUpperBound a)
upperX <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
x'
    PInterval Term s (PLowerBound a)
lowerY Term s (PUpperBound a)
upperY <- Term s (PInterval a) -> TermCont s (PInterval a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PInterval a)
y'
    let lower :: Term s (PLowerBound a)
lower = Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
maxLower Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a)
-> Term s (PLowerBound a :--> PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerX Term s (PLowerBound a :--> PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lowerY
    let upper :: Term s (PUpperBound a)
upper = Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
minUpper Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a)
-> Term s (PUpperBound a :--> PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperX Term s (PUpperBound a :--> PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upperY
    Term s (PInterval a) -> TermCont s (Term s (PInterval a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PInterval a) -> TermCont s (Term s (PInterval a)))
-> Term s (PInterval a) -> TermCont s (Term s (PInterval a))
forall a b. (a -> b) -> a -> b
$ Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
pinterval' Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
-> Term s (PLowerBound a)
-> Term s (PUpperBound a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lower Term s (PUpperBound a :--> PInterval a)
-> Term s (PUpperBound a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upper

{- | @'before' x i@ is true if @x@ is earlier than the start of @i@.

@since 2.1.1
-}
pbefore ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term
    s
    ( a
        :--> PInterval a
        :--> PBool
    )
pbefore :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (a :--> (PInterval a :--> PBool))
pbefore = ClosedTerm (a :--> (PInterval a :--> PBool))
-> Term s (a :--> (PInterval a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PInterval a :--> PBool))
 -> Term s (a :--> (PInterval a :--> PBool)))
-> ClosedTerm (a :--> (PInterval a :--> PBool))
-> Term s (a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s a -> Term s (PInterval a) -> Term s PBool)
-> Term s (a :--> (PInterval a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s PBool)
-> Term s (c :--> (PInterval a :--> PBool))
plam ((Term s a -> Term s (PInterval a) -> Term s PBool)
 -> Term s (a :--> (PInterval a :--> PBool)))
-> (Term s a -> Term s (PInterval a) -> Term s PBool)
-> Term s (a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PInterval a)
y ->
    Term s (PInterval a)
-> (PInterval a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInterval a)
y ((PInterval a s -> Term s PBool) -> Term s PBool)
-> (PInterval a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PInterval Term s (PLowerBound a)
lower Term s (PUpperBound a)
_) -> TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
      PLowerBound Term s (PExtended a)
t Term s (PAsData PBool)
c <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
lower
      Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
        Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
c)
          (Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
t (Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
a))
          (Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
t (Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
leqE' Term s a
a))

{- | @'after' x u@ is true if @x@ is later than the end of @i@.

@since 2.1.1
-}
pafter ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term
    s
    ( a
        :--> PInterval a
        :--> PBool
    )
pafter :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (a :--> (PInterval a :--> PBool))
pafter = ClosedTerm (a :--> (PInterval a :--> PBool))
-> Term s (a :--> (PInterval a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PInterval a :--> PBool))
 -> Term s (a :--> (PInterval a :--> PBool)))
-> ClosedTerm (a :--> (PInterval a :--> PBool))
-> Term s (a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s a -> Term s (PInterval a) -> Term s PBool)
-> Term s (a :--> (PInterval a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PInterval a) -> Term s PBool)
-> Term s (c :--> (PInterval a :--> PBool))
plam ((Term s a -> Term s (PInterval a) -> Term s PBool)
 -> Term s (a :--> (PInterval a :--> PBool)))
-> (Term s a -> Term s (PInterval a) -> Term s PBool)
-> Term s (a :--> (PInterval a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PInterval a)
y ->
    Term s (PInterval a)
-> (PInterval a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInterval a)
y ((PInterval a s -> Term s PBool) -> Term s PBool)
-> (PInterval a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PInterval Term s (PLowerBound a)
_ Term s (PUpperBound a)
upper) -> TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
      PUpperBound Term s (PExtended a)
t Term s (PAsData PBool)
c <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
upper
      Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
        Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
c)
          (Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
t (Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
a))
          (Term s (PExtended a)
-> (PExtended a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PExtended a)
t (Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
geqE' Term s a
a))

{- | @'pinterval' x y@ creates the interval @[x, y]@.

@since 2.1.1
-}
pinterval ::
  forall (a :: S -> Type) (s :: S).
  Term
    s
    ( PAsData a
        :--> PAsData a
        :--> PInterval a
    )
pinterval :: forall (a :: S -> Type) (s :: S).
Term s (PAsData a :--> (PAsData a :--> PInterval a))
pinterval = ClosedTerm (PAsData a :--> (PAsData a :--> PInterval a))
-> Term s (PAsData a :--> (PAsData a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> (PAsData a :--> PInterval a))
 -> Term s (PAsData a :--> (PAsData a :--> PInterval a)))
-> ClosedTerm (PAsData a :--> (PAsData a :--> PInterval a))
-> Term s (PAsData a :--> (PAsData a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PAsData a) -> Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> (PAsData a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PAsData a) -> Term s (PInterval a))
-> Term s (c :--> (PAsData a :--> PInterval a))
plam ((Term s (PAsData a) -> Term s (PAsData a) -> Term s (PInterval a))
 -> Term s (PAsData a :--> (PAsData a :--> PInterval a)))
-> (Term s (PAsData a)
    -> Term s (PAsData a) -> Term s (PInterval a))
-> Term s (PAsData a :--> (PAsData a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
x Term s (PAsData a)
y ->
    let start :: Term s (PExtended a)
start = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite Term s (PAsData a)
x
        end :: Term s (PExtended a)
end = PExtended a s -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PExtended a s -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PExtended a s
PFinite Term s (PAsData a)
y
     in Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval Term s (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a) -> Term s (PExtended a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
start Term s (PExtended a :--> PInterval a)
-> Term s (PExtended a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PExtended a)
end

-- Helpers

-- closed interval from PExtended
pclosedInterval ::
  forall (a :: S -> Type) (s :: S).
  Term
    s
    ( PExtended a
        :--> PExtended a
        :--> PInterval a
    )
pclosedInterval :: forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval = ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
 -> Term s (PExtended a :--> (PExtended a :--> PInterval a)))
-> ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PExtended a)
 -> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (c :--> (PExtended a :--> PInterval a))
plam ((Term s (PExtended a)
  -> Term s (PExtended a) -> Term s (PInterval a))
 -> Term s (PExtended a :--> (PExtended a :--> PInterval a)))
-> (Term s (PExtended a)
    -> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
start Term s (PExtended a)
end ->
    let closure :: Term s (PAsData PBool)
closure = forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @(PAsData PBool) Bool
AsHaskell (PAsData PBool)
True
        upper :: Term s (PUpperBound a)
upper = PUpperBound a s -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PUpperBound a s -> Term s (PUpperBound a))
-> PUpperBound a s -> Term s (PUpperBound a)
forall a b. (a -> b) -> a -> b
$ Term s (PExtended a) -> Term s (PAsData PBool) -> PUpperBound a s
forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s (PAsData PBool) -> PUpperBound a s
PUpperBound Term s (PExtended a)
end Term s (PAsData PBool)
forall {s :: S}. Term s (PAsData PBool)
closure
        lower :: Term s (PLowerBound a)
lower = PLowerBound a s -> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PLowerBound a s -> Term s (PLowerBound a))
-> PLowerBound a s -> Term s (PLowerBound a)
forall a b. (a -> b) -> a -> b
$ Term s (PExtended a) -> Term s (PAsData PBool) -> PLowerBound a s
forall (a :: S -> Type) (s :: S).
Term s (PExtended a) -> Term s (PAsData PBool) -> PLowerBound a s
PLowerBound Term s (PExtended a)
start Term s (PAsData PBool)
forall {s :: S}. Term s (PAsData PBool)
closure
     in Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
pinterval' Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
-> Term s (PLowerBound a)
-> Term s (PUpperBound a :--> PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lower Term s (PUpperBound a :--> PInterval a)
-> Term s (PUpperBound a) -> Term s (PInterval a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upper

--  interval from upper and lower
pinterval' ::
  forall (a :: S -> Type) (s :: S).
  Term
    s
    ( PLowerBound a
        :--> PUpperBound a
        :--> PInterval a
    )
pinterval' :: forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
pinterval' = ClosedTerm (PLowerBound a :--> (PUpperBound a :--> PInterval a))
-> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PLowerBound a :--> (PUpperBound a :--> PInterval a))
 -> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a)))
-> ClosedTerm (PLowerBound a :--> (PUpperBound a :--> PInterval a))
-> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PLowerBound a)
 -> Term s (PUpperBound a) -> Term s (PInterval a))
-> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PUpperBound a) -> Term s (PInterval a))
-> Term s (c :--> (PUpperBound a :--> PInterval a))
plam ((Term s (PLowerBound a)
  -> Term s (PUpperBound a) -> Term s (PInterval a))
 -> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a)))
-> (Term s (PLowerBound a)
    -> Term s (PUpperBound a) -> Term s (PInterval a))
-> Term s (PLowerBound a :--> (PUpperBound a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
lower Term s (PUpperBound a)
upper ->
    PInterval a s -> Term s (PInterval a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInterval a s -> Term s (PInterval a))
-> PInterval a s -> Term s (PInterval a)
forall a b. (a -> b) -> a -> b
$
      Term s (PLowerBound a) -> Term s (PUpperBound a) -> PInterval a s
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a) -> Term s (PUpperBound a) -> PInterval a s
PInterval Term s (PLowerBound a)
lower Term s (PUpperBound a)
upper

ltE' ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
ltE' :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
x = \case
  PExtended a s
PNegInf -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
  PExtended a s
PPosInf -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  PFinite Term s (PAsData a)
r -> Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
r

eqE' ::
  forall (a :: S -> Type) (s :: S).
  (PEq a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
eqE' :: forall (a :: S -> Type) (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 (PAsData a)
r -> TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s a
a Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
r
  PExtended a s
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False

minLower ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    (PLowerBound a :--> PLowerBound a :--> PLowerBound a)
minLower :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
minLower = ClosedTerm (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
 -> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> ClosedTerm
     (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PLowerBound a)
 -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (c :--> (PLowerBound a :--> PLowerBound a))
plam ((Term s (PLowerBound a)
  -> Term s (PLowerBound a) -> Term s (PLowerBound a))
 -> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> (Term s (PLowerBound a)
    -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
x' Term s (PLowerBound a)
y' -> TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a))
-> TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a)
forall a b. (a -> b) -> a -> b
$ do
    PLowerBound Term s (PExtended a)
xt' Term s (PAsData PBool)
xc <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
x'
    PLowerBound Term s (PExtended a)
yt' Term s (PAsData PBool)
_ <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
y'
    Term s (PExtended a)
xt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
xt'
    Term s (PExtended a)
yt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
yt'

    Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a)))
-> Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall a b. (a -> b) -> a -> b
$
      Term s PBool
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PExtended a)
xt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
yt)
        Term s (PLowerBound a)
x'
        (Term s PBool
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PExtended a)
yt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
xt) Term s (PLowerBound a)
y' (Term
  s
  (PBool
   :--> (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
  s
  (PBool
   :--> (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> Term s PBool
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
xc Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a)
-> Term s (PLowerBound a :--> PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
x' Term s (PLowerBound a :--> PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
y'))

maxLower ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    (PLowerBound a :--> PLowerBound a :--> PLowerBound a)
maxLower :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
maxLower = ClosedTerm (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
 -> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> ClosedTerm
     (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PLowerBound a)
 -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (c :--> (PLowerBound a :--> PLowerBound a))
plam ((Term s (PLowerBound a)
  -> Term s (PLowerBound a) -> Term s (PLowerBound a))
 -> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> (Term s (PLowerBound a)
    -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
x' Term s (PLowerBound a)
y' -> TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a))
-> TermCont s (Term s (PLowerBound a)) -> Term s (PLowerBound a)
forall a b. (a -> b) -> a -> b
$ do
    PLowerBound Term s (PExtended a)
xt' Term s (PAsData PBool)
xc <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
x'
    PLowerBound Term s (PExtended a)
yt' Term s (PAsData PBool)
_ <- Term s (PLowerBound a) -> TermCont s (PLowerBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PLowerBound a)
y'
    Term s (PExtended a)
xt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
xt'
    Term s (PExtended a)
yt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
yt'

    Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a)))
-> Term s (PLowerBound a) -> TermCont s (Term s (PLowerBound a))
forall a b. (a -> b) -> a -> b
$
      Term s PBool
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PExtended a)
xt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
yt)
        Term s (PLowerBound a)
y'
        (Term s PBool
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
-> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PExtended a)
yt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
xt) Term s (PLowerBound a)
x' (Term
  s
  (PBool
   :--> (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
  s
  (PBool
   :--> (PLowerBound a :--> (PLowerBound a :--> PLowerBound a)))
-> Term s PBool
-> Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
xc Term s (PLowerBound a :--> (PLowerBound a :--> PLowerBound a))
-> Term s (PLowerBound a)
-> Term s (PLowerBound a :--> PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
y' Term s (PLowerBound a :--> PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
x'))

minUpper ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    (PUpperBound a :--> PUpperBound a :--> PUpperBound a)
minUpper :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
minUpper = ClosedTerm (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
 -> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> ClosedTerm
     (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PUpperBound a)
 -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (c :--> (PUpperBound a :--> PUpperBound a))
plam ((Term s (PUpperBound a)
  -> Term s (PUpperBound a) -> Term s (PUpperBound a))
 -> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> (Term s (PUpperBound a)
    -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a b. (a -> b) -> a -> b
$ \Term s (PUpperBound a)
x' Term s (PUpperBound a)
y' -> TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a))
-> TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a)
forall a b. (a -> b) -> a -> b
$ do
    PUpperBound Term s (PExtended a)
xt' Term s (PAsData PBool)
xc <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
x'
    PUpperBound Term s (PExtended a)
yt' Term s (PAsData PBool)
_ <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
y'
    Term s (PExtended a)
xt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
xt'
    Term s (PExtended a)
yt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
yt'

    Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a)))
-> Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall a b. (a -> b) -> a -> b
$
      Term s PBool
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PExtended a)
xt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
yt)
        Term s (PUpperBound a)
x'
        (Term s PBool
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PExtended a)
yt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
xt) Term s (PUpperBound a)
y' (Term
  s
  (PBool
   :--> (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
  s
  (PBool
   :--> (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> Term s PBool
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
xc Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a)
-> Term s (PUpperBound a :--> PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
y' Term s (PUpperBound a :--> PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
x'))

maxUpper ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    (PUpperBound a :--> PUpperBound a :--> PUpperBound a)
maxUpper :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
maxUpper = ClosedTerm (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
 -> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> ClosedTerm
     (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a b. (a -> b) -> a -> b
$
  (Term s (PUpperBound a)
 -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (c :--> (PUpperBound a :--> PUpperBound a))
plam ((Term s (PUpperBound a)
  -> Term s (PUpperBound a) -> Term s (PUpperBound a))
 -> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> (Term s (PUpperBound a)
    -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall a b. (a -> b) -> a -> b
$ \Term s (PUpperBound a)
x' Term s (PUpperBound a)
y' -> TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a))
-> TermCont s (Term s (PUpperBound a)) -> Term s (PUpperBound a)
forall a b. (a -> b) -> a -> b
$ do
    PUpperBound Term s (PExtended a)
xt' Term s (PAsData PBool)
xc <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
x'
    PUpperBound Term s (PExtended a)
yt' Term s (PAsData PBool)
_ <- Term s (PUpperBound a) -> TermCont s (PUpperBound a s)
forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PUpperBound a)
y'
    Term s (PExtended a)
xt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
xt'
    Term s (PExtended a)
yt <- Term s (PExtended a) -> TermCont s (Term s (PExtended a))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC Term s (PExtended a)
yt'

    Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a)))
-> Term s (PUpperBound a) -> TermCont s (Term s (PUpperBound a))
forall a b. (a -> b) -> a -> b
$
      Term s PBool
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PExtended a)
xt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
yt)
        Term s (PUpperBound a)
y'
        (Term s PBool
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
-> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PExtended a)
yt Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PExtended a)
xt) Term s (PUpperBound a)
x' (Term
  s
  (PBool
   :--> (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
  s
  (PBool
   :--> (PUpperBound a :--> (PUpperBound a :--> PUpperBound a)))
-> Term s PBool
-> Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PBool)
xc Term s (PUpperBound a :--> (PUpperBound a :--> PUpperBound a))
-> Term s (PUpperBound a)
-> Term s (PUpperBound a :--> PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
x' Term s (PUpperBound a :--> PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
y'))

-- value <= PExtended
leqE' ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
leqE' :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
leqE' Term s a
a PExtended a s
y = Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
ltE' Term s a
a PExtended a s
y Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (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 -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
geqE' :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
geqE' Term s a
a PExtended a s
y = Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
a PExtended a s
y Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s a -> PExtended a s -> Term s PBool
forall (a :: S -> Type) (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
gtE' ::
  forall (a :: S -> Type) (s :: S).
  (POrd a, PIsData a) =>
  Term s a ->
  PExtended a s ->
  Term s PBool
gtE' :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s a -> PExtended a s -> Term s PBool
gtE' Term s a
x = \case
  PExtended a s
PNegInf -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  PExtended a s
PPosInf -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
  PFinite Term s (PAsData a)
r -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
r Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
x