{-# 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 Plutarch.DataRepr (PDataFields)
import Plutarch.Enum (
  PCountable (psuccessor),
  PEnumerable (ppredecessor),
 )
import Plutarch.Internal.Lift (DeriveDataPLiftable)
import Plutarch.Prelude hiding (psingleton, pto)
import PlutusLedgerApi.V3 qualified as Plutus

-- | @since 2.0.0
newtype PInterval (a :: S -> Type) (s :: S)
  = PInterval
      ( Term
          s
          ( PDataRecord
              '[ "from" ':= PLowerBound a
               , "to" ':= 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
      (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
    , -- | @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 (PDataRecord (PFields (PInterval a))))
-> PDataFields (PInterval a)
forall (s :: S).
Term s (PInterval a)
-> Term s (PDataRecord (PFields (PInterval a)))
forall (a :: S -> Type).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
forall (a :: S -> Type) (s :: S).
Term s (PInterval a)
-> Term s (PDataRecord (PFields (PInterval a)))
$cptoFields :: forall (a :: S -> Type) (s :: S).
Term s (PInterval a)
-> Term s (PDataRecord (PFields (PInterval a)))
ptoFields :: forall (s :: S).
Term s (PInterval a)
-> Term s (PDataRecord (PFields (PInterval a)))
PDataFields
    , -- | @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 (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 (PInterval a) -> Term s (PInterval a) -> Term s PBool
$c#== :: forall (a :: S -> Type) (s :: S).
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
      PEq (PInterval a)
PEq (PInterval a) =>
(forall (s :: S).
 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)
-> (forall (s :: S).
    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)
-> PPartialOrd (PInterval a)
forall (s :: S).
Term s (PInterval a) -> Term s (PInterval a) -> Term s PBool
forall (a :: S -> Type).
(PIsData a, PEnumerable a) =>
PEq (PInterval a)
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).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd 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
$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
$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
$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
PPartialOrd
    , -- | @since 2.0.0
      PPartialOrd (PInterval a)
PPartialOrd (PInterval a) =>
(forall (s :: S).
 Term s (PInterval a)
 -> Term s (PInterval a) -> Term s (PInterval a))
-> (forall (s :: S).
    Term s (PInterval a)
    -> Term s (PInterval a) -> Term s (PInterval a))
-> POrd (PInterval a)
forall (s :: S).
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
forall (a :: S -> Type).
(PIsData a, PEnumerable a) =>
PPartialOrd (PInterval a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
forall (t :: S -> Type).
PPartialOrd t =>
(forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t) -> POrd t
$cpmax :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
pmax :: forall (s :: S).
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
$cpmin :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
pmin :: forall (s :: S).
Term s (PInterval a)
-> Term s (PInterval a) -> Term s (PInterval a)
POrd
    , -- | @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
    )

-- | @since 2.0.0
instance DerivePlutusType (PInterval a) where
  type DPTStrat _ = PlutusTypeData

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

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PInterval a)

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PAsData (PInterval a))

-- | @since 2.0.0
newtype PLowerBound (a :: S -> Type) (s :: S)
  = PLowerBound
      ( Term
          s
          ( PDataRecord
              '[ "_0" ':= PExtended a
               , "_1" ':= 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
      (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
    , -- | @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).
 Term s (PLowerBound a)
 -> Term s (PDataRecord (PFields (PLowerBound a))))
-> PDataFields (PLowerBound a)
forall (s :: S).
Term s (PLowerBound a)
-> Term s (PDataRecord (PFields (PLowerBound a)))
forall (a :: S -> Type).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a)
-> Term s (PDataRecord (PFields (PLowerBound a)))
$cptoFields :: forall (a :: S -> Type) (s :: S).
Term s (PLowerBound a)
-> Term s (PDataRecord (PFields (PLowerBound a)))
ptoFields :: forall (s :: S).
Term s (PLowerBound a)
-> Term s (PDataRecord (PFields (PLowerBound a)))
PDataFields
    , -- | @since 2.0.0
      PPartialOrd (PLowerBound a)
PPartialOrd (PLowerBound a) =>
(forall (s :: S).
 Term s (PLowerBound a)
 -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> (forall (s :: S).
    Term s (PLowerBound a)
    -> Term s (PLowerBound a) -> Term s (PLowerBound a))
-> POrd (PLowerBound a)
forall (s :: S).
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (a :: S -> Type).
(PIsData a, PCountable a) =>
PPartialOrd (PLowerBound a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
forall (t :: S -> Type).
PPartialOrd t =>
(forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t) -> POrd t
$cpmax :: forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
pmax :: forall (s :: S).
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
$cpmin :: forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
pmin :: forall (s :: S).
Term s (PLowerBound a)
-> Term s (PLowerBound a) -> Term s (PLowerBound a)
POrd
    , -- | @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 via
  DeriveDataPLiftable (PLowerBound a) (Plutus.LowerBound (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PLowerBound a)

-- | @since WIP
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 WIP
instance (PIsData a, PCountable a) => PPartialOrd (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).
PPartialOrd 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).
PPartialOrd 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
instance DerivePlutusType (PLowerBound a) where
  type DPTStrat _ = PlutusTypeData

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PLowerBound a)

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PAsData (PLowerBound a))

-- | @since 2.0.0
newtype PUpperBound (a :: S -> Type) (s :: S)
  = PUpperBound
      ( Term
          s
          ( PDataRecord
              '[ "_0" ':= PExtended a
               , "_1" ':= 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
      (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
    , -- | @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).
 Term s (PUpperBound a)
 -> Term s (PDataRecord (PFields (PUpperBound a))))
-> PDataFields (PUpperBound a)
forall (s :: S).
Term s (PUpperBound a)
-> Term s (PDataRecord (PFields (PUpperBound a)))
forall (a :: S -> Type).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
forall (a :: S -> Type) (s :: S).
Term s (PUpperBound a)
-> Term s (PDataRecord (PFields (PUpperBound a)))
$cptoFields :: forall (a :: S -> Type) (s :: S).
Term s (PUpperBound a)
-> Term s (PDataRecord (PFields (PUpperBound a)))
ptoFields :: forall (s :: S).
Term s (PUpperBound a)
-> Term s (PDataRecord (PFields (PUpperBound a)))
PDataFields
    , -- | @since 2.0.0
      PPartialOrd (PUpperBound a)
PPartialOrd (PUpperBound a) =>
(forall (s :: S).
 Term s (PUpperBound a)
 -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> (forall (s :: S).
    Term s (PUpperBound a)
    -> Term s (PUpperBound a) -> Term s (PUpperBound a))
-> POrd (PUpperBound a)
forall (s :: S).
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (a :: S -> Type).
(PIsData a, PEnumerable a) =>
PPartialOrd (PUpperBound a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
forall (t :: S -> Type).
PPartialOrd t =>
(forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t) -> POrd t
$cpmax :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
pmax :: forall (s :: S).
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
$cpmin :: forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
pmin :: forall (s :: S).
Term s (PUpperBound a)
-> Term s (PUpperBound a) -> Term s (PUpperBound a)
POrd
    , -- | @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 via
  DeriveDataPLiftable (PUpperBound a) (Plutus.UpperBound (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PUpperBound a)

-- | @since WIP
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 WIP
instance (PIsData a, PEnumerable a) => PPartialOrd (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).
PPartialOrd 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).
PPartialOrd 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
instance DerivePlutusType (PUpperBound a) where
  type DPTStrat _ = PlutusTypeData

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PUpperBound a)

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PAsData (PUpperBound a))

-- | @since 2.0.0
data PExtended (a :: S -> Type) (s :: S)
  = PNegInf (Term s (PDataRecord '[]))
  | PFinite (Term s (PDataRecord '["_0" ':= a]))
  | PPosInf (Term s (PDataRecord '[]))
  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
      (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
    , -- | @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
      PEq (PExtended a)
PEq (PExtended a) =>
(forall (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)
-> (forall (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)
-> PPartialOrd (PExtended a)
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type). (POrd a, PIsData a) => PEq (PExtended a)
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type).
PEq t =>
(forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> (forall (s :: S). Term s t -> Term s t -> Term s PBool)
-> PPartialOrd t
$c#<= :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
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
$c#< :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
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
$c#>= :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
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
$c#> :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
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
PPartialOrd
    , -- | @since 2.0.0
      PPartialOrd (PExtended a)
PPartialOrd (PExtended a) =>
(forall (s :: S).
 Term s (PExtended a)
 -> Term s (PExtended a) -> Term s (PExtended a))
-> (forall (s :: S).
    Term s (PExtended a)
    -> Term s (PExtended a) -> Term s (PExtended a))
-> POrd (PExtended a)
forall (s :: S).
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
forall (a :: S -> Type).
(POrd a, PIsData a) =>
PPartialOrd (PExtended a)
forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
forall (t :: S -> Type).
PPartialOrd t =>
(forall (s :: S). Term s t -> Term s t -> Term s t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t) -> POrd t
$cpmax :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
pmax :: forall (s :: S).
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
$cpmin :: forall (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
pmin :: forall (s :: S).
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
POrd
    , -- | @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 via
  DeriveDataPLiftable (PExtended a) (Plutus.Extended (AsHaskell a))
  instance
    (Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PExtended a)

-- | @since 2.0.0
instance DerivePlutusType (PExtended a) where
  type DPTStrat _ = PlutusTypeData

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PExtended a)

-- | @since 3.1.0
instance PTryFrom PData a => PTryFrom PData (PAsData (PExtended a))

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

@since WIP
-}
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 WIP
-}
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
  HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpacked <- ((HRec
    '[ '("from", Term s (PAsData (PLowerBound a))),
       '("to", Term s (PAsData (PUpperBound a)))]
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("from", Term s (PAsData (PLowerBound a))),
        '("to", Term s (PAsData (PUpperBound a)))]
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      s
      (HRec
         '[ '("from", Term s (PAsData (PLowerBound a))),
            '("to", Term s (PAsData (PUpperBound a)))]))
-> ((HRec
       '[ '("from", Term s (PAsData (PLowerBound a))),
          '("to", Term s (PAsData (PUpperBound a)))]
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
i
  let lowerBound :: Term s (PLowerBound a)
lowerBound = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpacked
  let upperBound :: Term s (PUpperBound a)
upperBound = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpacked
  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 (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#> Term s (PExtended a)
inclusiveUpperBound

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

@since WIP
-}
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
  HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PExtended a))
 -> Term s (PExtended a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PExtended a))
  -> Term s (PExtended a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PExtended a))
    -> Term s (PExtended a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (PLowerBound a)
lb
  let extended :: Term s (PExtended a)
extended = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked
  let closure :: Term s PBool
closure = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked
  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 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 (PDataRecord '["_0" ':= a])
t -> forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0"] Term s (PDataRecord '["_0" ':= a])
t ((HRec
    (BoundTerms
       (PFields (PDataRecord '["_0" ':= a]))
       (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
       s)
  -> Term s (PExtended a))
 -> Term s (PExtended a))
-> (HRec
      (BoundTerms
         (PFields (PDataRecord '["_0" ':= a]))
         (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
         s)
    -> Term s (PExtended a))
-> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ \HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= a]))
     (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
     s)
unpackedT ->
            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))
-> (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a])
-> Term s (PExtended a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> Term s (PExtended a))
-> Term s (PDataRecord '["_0" ':= a]) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# 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 :--> 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
# forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec '[ '("_0", Term s (PAsData a))]
HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= a]))
     (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
     s)
unpackedT) Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
          -- We have an infinity, who cares
          PExtended a s
_ -> Term s (PExtended a)
extended
      )

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

@since WIP
-}
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
  HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PExtended a))
 -> Term s (PExtended a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PExtended a))
  -> Term s (PExtended a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PExtended a))
    -> Term s (PExtended a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (PUpperBound a)
ub
  let extended :: Term s (PExtended a)
extended = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked
  let closure :: Term s PBool
closure = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
unpacked
  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 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 (PDataRecord '["_0" ':= a])
t -> forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0"] Term s (PDataRecord '["_0" ':= a])
t ((HRec
    (BoundTerms
       (PFields (PDataRecord '["_0" ':= a]))
       (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
       s)
  -> Term s (PExtended a))
 -> Term s (PExtended a))
-> (HRec
      (BoundTerms
         (PFields (PDataRecord '["_0" ':= a]))
         (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
         s)
    -> Term s (PExtended a))
-> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ \HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= a]))
     (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
     s)
unpackedT ->
            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))
-> (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a])
-> Term s (PExtended a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> Term s (PExtended a))
-> Term s (PDataRecord '["_0" ':= a]) -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# 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 :--> 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
# forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec '[ '("_0", Term s (PAsData a))]
HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= a]))
     (Bindings (PFields (PDataRecord '["_0" ':= a])) '["_0"])
     s)
unpackedT) Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
          -- 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 WIP
-}
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
  HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpackedI1 <- ((HRec
    '[ '("from", Term s (PAsData (PLowerBound a))),
       '("to", Term s (PAsData (PUpperBound a)))]
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("from", Term s (PAsData (PLowerBound a))),
        '("to", Term s (PAsData (PUpperBound a)))]
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      s
      (HRec
         '[ '("from", Term s (PAsData (PLowerBound a))),
            '("to", Term s (PAsData (PUpperBound a)))]))
-> ((HRec
       '[ '("from", Term s (PAsData (PLowerBound a))),
          '("to", Term s (PAsData (PUpperBound a)))]
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
i1
  HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
unpackedI2 <- ((HRec
    (BoundTerms
       (PFields (PInterval a))
       (Bindings (PFields (PInterval a)) '["from", "to"])
       s)
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     (BoundTerms
        (PFields (PInterval a))
        (Bindings (PFields (PInterval a)) '["from", "to"])
        s)
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      s
      (HRec
         (BoundTerms
            (PFields (PInterval a))
            (Bindings (PFields (PInterval a)) '["from", "to"])
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PInterval a))
          (Bindings (PFields (PInterval a)) '["from", "to"])
          s)
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
i2
  let l1 :: Term s (PLowerBound a)
l1 = Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a))
-> Term s (PAsData (PLowerBound a)) -> Term s (PLowerBound a)
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpackedI1
  let l2 :: Term s (PLowerBound a)
l2 = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
unpackedI2
  let u1 :: Term s (PUpperBound a)
u1 = Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a))
-> Term s (PAsData (PUpperBound a)) -> Term s (PUpperBound a)
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
unpackedI1
  let u2 :: Term s (PUpperBound a)
u2 = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
unpackedI2
  -- 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 (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> 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 (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> 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).
PPartialOrd 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).
PPartialOrd 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 (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0" Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= 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 Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil) ((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 (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0" Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
        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 (PDataRecord '[]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '[]) -> PExtended a s
PPosInf Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
     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 -> Term s (PExtended a))
-> PExtended a s -> Term s (PExtended a)
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord '[]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '[]) -> PExtended a s
PNegInf Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
        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 (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0" Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
a Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
     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
    HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x <- ((HRec
    '[ '("from", Term s (PAsData (PLowerBound a))),
       '("to", Term s (PAsData (PUpperBound a)))]
  -> Term s (PInterval a))
 -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("from", Term s (PAsData (PLowerBound a))),
        '("to", Term s (PAsData (PUpperBound a)))]
   -> Term s (PInterval a))
  -> Term s (PInterval a))
 -> TermCont
      s
      (HRec
         '[ '("from", Term s (PAsData (PLowerBound a))),
            '("to", Term s (PAsData (PUpperBound a)))]))
-> ((HRec
       '[ '("from", Term s (PAsData (PLowerBound a))),
          '("to", Term s (PAsData (PUpperBound a)))]
     -> Term s (PInterval a))
    -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
x'
    HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
y <- ((HRec
    (BoundTerms
       (PFields (PInterval a))
       (Bindings (PFields (PInterval a)) '["from", "to"])
       s)
  -> Term s (PInterval a))
 -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     (BoundTerms
        (PFields (PInterval a))
        (Bindings (PFields (PInterval a)) '["from", "to"])
        s)
   -> Term s (PInterval a))
  -> Term s (PInterval a))
 -> TermCont
      s
      (HRec
         (BoundTerms
            (PFields (PInterval a))
            (Bindings (PFields (PInterval a)) '["from", "to"])
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PInterval a))
          (Bindings (PFields (PInterval a)) '["from", "to"])
          s)
     -> Term s (PInterval a))
    -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
y'
    let lowerX :: Term s (PLowerBound a)
lowerX = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x
    let upperX :: Term s (PUpperBound a)
upperX = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x
    let lowerY :: Term s (PLowerBound a)
lowerY = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
y
    let upperY :: Term s (PUpperBound a)
upperY = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
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
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
-> Term s (PAsData (PLowerBound a))
-> Term s (PAsData (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) -> Term s (PAsData (PLowerBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower Term s (PAsData (PUpperBound a) :--> PInterval a)
-> Term s (PAsData (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) -> Term s (PAsData (PUpperBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata 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
    HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x <- ((HRec
    '[ '("from", Term s (PAsData (PLowerBound a))),
       '("to", Term s (PAsData (PUpperBound a)))]
  -> Term s (PInterval a))
 -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("from", Term s (PAsData (PLowerBound a))),
        '("to", Term s (PAsData (PUpperBound a)))]
   -> Term s (PInterval a))
  -> Term s (PInterval a))
 -> TermCont
      s
      (HRec
         '[ '("from", Term s (PAsData (PLowerBound a))),
            '("to", Term s (PAsData (PUpperBound a)))]))
-> ((HRec
       '[ '("from", Term s (PAsData (PLowerBound a))),
          '("to", Term s (PAsData (PUpperBound a)))]
     -> Term s (PInterval a))
    -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        '[ '("from", Term s (PAsData (PLowerBound a))),
           '("to", Term s (PAsData (PUpperBound a)))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
x'
    HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
y <- ((HRec
    (BoundTerms
       (PFields (PInterval a))
       (Bindings (PFields (PInterval a)) '["from", "to"])
       s)
  -> Term s (PInterval a))
 -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     (BoundTerms
        (PFields (PInterval a))
        (Bindings (PFields (PInterval a)) '["from", "to"])
        s)
   -> Term s (PInterval a))
  -> Term s (PInterval a))
 -> TermCont
      s
      (HRec
         (BoundTerms
            (PFields (PInterval a))
            (Bindings (PFields (PInterval a)) '["from", "to"])
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PInterval a))
          (Bindings (PFields (PInterval a)) '["from", "to"])
          s)
     -> Term s (PInterval a))
    -> Term s (PInterval a))
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PInterval a))
           (Bindings (PFields (PInterval a)) '["from", "to"])
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["from", "to"] Term s (PInterval a)
y'
    let lowerX :: Term s (PLowerBound a)
lowerX = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x
    let upperX :: Term s (PUpperBound a)
upperX = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  '[ '("from", Term s (PAsData (PLowerBound a))),
     '("to", Term s (PAsData (PUpperBound a)))]
x
    let lowerY :: Term s (PLowerBound a)
lowerY = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"from" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
y
    let upperY :: Term s (PUpperBound a)
upperY = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"to" HRec
  (BoundTerms
     (PFields (PInterval a))
     (Bindings (PFields (PInterval a)) '["from", "to"])
     s)
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
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
-> Term s (PAsData (PLowerBound a))
-> Term s (PAsData (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) -> Term s (PAsData (PLowerBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower Term s (PAsData (PUpperBound a) :--> PInterval a)
-> Term s (PAsData (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) -> Term s (PAsData (PUpperBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata 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 ->
    let lower :: Term s (PLowerBound a)
lower = forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"from" Term s (PInterval a :--> PLowerBound a)
-> Term s (PInterval 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 (PInterval a)
y
     in Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
pbefore' Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
-> Term s a
-> Term
     s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool] :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
a Term
  s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool] :--> PBool)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PLowerBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lower)

{- | @'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 ->
    let upper :: Term s (PUpperBound a)
upper = forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"to" Term s (PInterval a :--> PUpperBound a)
-> Term s (PInterval 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 (PInterval a)
y
     in Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
pafter' Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
-> Term s a
-> Term
     s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool] :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
a Term
  s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool] :--> PBool)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PUpperBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
upper)

{- | @'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 (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0" Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= 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 Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
        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 (PDataRecord '["_0" ':= a]) -> PExtended a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
PFinite (Term s (PDataRecord '["_0" ':= a]) -> PExtended a s)
-> Term s (PDataRecord '["_0" ':= a]) -> PExtended a s
forall a b. (a -> b) -> a -> b
$ forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0" Term
  s (PAsData a :--> (PDataRecord '[] :--> PDataRecord '["_0" ':= a]))
-> Term s (PAsData a)
-> Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
y Term s (PDataRecord '[] :--> PDataRecord '["_0" ':= a])
-> Term s (PDataRecord '[]) -> Term s (PDataRecord '["_0" ':= a])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord '[])
forall (s :: S). Term s (PDataRecord '[])
pdnil
     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 = Bool -> Term s (PAsData PBool)
forall (p :: S -> Type) h (s :: S).
(ToData h, AsHaskell p ~ h) =>
h -> Term s (PAsData p)
pconstantData Bool
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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PUpperBound a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PUpperBound a s
PUpperBound (Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> PUpperBound a s)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PUpperBound a s
forall a b. (a -> b) -> a -> b
$
              forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0"
                # pdata end
                #$ pdcons @"_1"
                # closure
                # pdnil
        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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PLowerBound a s
forall (a :: S -> Type) (s :: S).
Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PLowerBound a s
PLowerBound (Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> PLowerBound a s)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> PLowerBound a s
forall a b. (a -> b) -> a -> b
$
              forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons @"_0"
                # pdata start
                #$ pdcons @"_1"
                # closure
                # pdnil
     in Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
forall (a :: S -> Type) (s :: S).
Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
pinterval' Term
  s
  (PAsData (PLowerBound a)
   :--> (PAsData (PUpperBound a) :--> PInterval a))
-> Term s (PAsData (PLowerBound a))
-> Term s (PAsData (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) -> Term s (PAsData (PLowerBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PLowerBound a)
lower Term s (PAsData (PUpperBound a) :--> PInterval a)
-> Term s (PAsData (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) -> Term s (PAsData (PUpperBound a))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PUpperBound a)
upper

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

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
  PNegInf Term s (PDataRecord '[])
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
  PPosInf Term s (PDataRecord '[])
_ -> 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 (PDataRecord '["_0" ':= 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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" Term s (PDataRecord '["_0" ':= a] :--> a)
-> Term s (PDataRecord '["_0" ':= 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 (PDataRecord '["_0" ':= a])
r

lToE ::
  forall (a :: S -> Type) (s :: S).
  Term s (PLowerBound a :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE :: forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE = ClosedTerm
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term
     s
     (PLowerBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PLowerBound a
    :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term
      s
      (PLowerBound a
       :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> ClosedTerm
     (PLowerBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term
     s
     (PLowerBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall a b. (a -> b) -> a -> b
$ (Term s (PLowerBound a)
 -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s
     (PLowerBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= 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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s (c :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
plam ((Term s (PLowerBound a)
  -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
 -> Term
      s
      (PLowerBound a
       :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> (Term s (PLowerBound a)
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s
     (PLowerBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall a b. (a -> b) -> a -> b
$ \Term s (PLowerBound a)
x -> Term s (PLowerBound a)
-> (PLowerBound a s
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= 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 (PLowerBound a)
x (\(PLowerBound Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
a) -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
a)

uToE ::
  forall (a :: S -> Type) (s :: S).
  Term s (PUpperBound a :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE :: forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE = ClosedTerm
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term
     s
     (PUpperBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PUpperBound a
    :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term
      s
      (PUpperBound a
       :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> ClosedTerm
     (PUpperBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term
     s
     (PUpperBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall a b. (a -> b) -> a -> b
$ (Term s (PUpperBound a)
 -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s
     (PUpperBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= 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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s (c :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
plam ((Term s (PUpperBound a)
  -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
 -> Term
      s
      (PUpperBound a
       :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> (Term s (PUpperBound a)
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term
     s
     (PUpperBound a
      :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall a b. (a -> b) -> a -> b
$ \Term s (PUpperBound a)
x -> Term s (PUpperBound a)
-> (PUpperBound a s
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= 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 (PUpperBound a)
x (\(PUpperBound Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
a) -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
a)

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 (PDataRecord '["_0" ':= 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 a
b <- ((Term s a -> Term s PBool) -> Term s PBool)
-> TermCont s (Term s a)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((Term s a -> Term s PBool) -> Term s PBool)
 -> TermCont s (Term s a))
-> ((Term s a -> Term s PBool) -> Term s PBool)
-> TermCont s (Term s a)
forall a b. (a -> b) -> a -> b
$ Term s a -> (Term s a -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s a -> (Term s a -> Term s PBool) -> Term s PBool)
-> Term s a -> (Term s a -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" Term s (PDataRecord '["_0" ':= a] :--> a)
-> Term s (PDataRecord '["_0" ':= 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 (PDataRecord '["_0" ':= a])
r
    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 a
b
  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
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PLowerBound a))
 -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PLowerBound a))
  -> Term s (PLowerBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PLowerBound a))
    -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PLowerBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
x')
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PLowerBound a))
 -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PLowerBound a))
  -> Term s (PLowerBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PLowerBound a))
    -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PLowerBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
y')
    let xt :: Term s (PAsData (PExtended a))
xt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    let yt :: Term s (PAsData (PExtended a))
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y
    let xc :: Term s PBool
xc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 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
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PLowerBound a))
 -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PLowerBound a))
  -> Term s (PLowerBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PLowerBound a))
    -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PLowerBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
x')
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PLowerBound a))
 -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PLowerBound a))
  -> Term s (PLowerBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PLowerBound a))
    -> Term s (PLowerBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
lToE Term
  s
  (PLowerBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PLowerBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
y')
    let xt :: Term s (PAsData (PExtended a))
xt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    let yt :: Term s (PAsData (PExtended a))
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y
    let xc :: Term s PBool
xc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 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
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PUpperBound a))
 -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PUpperBound a))
  -> Term s (PUpperBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PUpperBound a))
    -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PUpperBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
x')
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PUpperBound a))
 -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PUpperBound a))
  -> Term s (PUpperBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PUpperBound a))
    -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PUpperBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
y')
    let xt :: Term s (PAsData (PExtended a))
xt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    let yt :: Term s (PAsData (PExtended a))
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y
    let xc :: Term s PBool
xc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 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
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PUpperBound a))
 -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PUpperBound a))
  -> Term s (PUpperBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PUpperBound a))
    -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PUpperBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
x')
    HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y <- ((HRec
    '[ '("_0", Term s (PAsData (PExtended a))),
       '("_1", Term s (PAsData PBool))]
  -> Term s (PUpperBound a))
 -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     '[ '("_0", Term s (PAsData (PExtended a))),
        '("_1", Term s (PAsData PBool))]
   -> Term s (PUpperBound a))
  -> Term s (PUpperBound a))
 -> TermCont
      s
      (HRec
         '[ '("_0", Term s (PAsData (PExtended a))),
            '("_1", Term s (PAsData PBool))]))
-> ((HRec
       '[ '("_0", Term s (PAsData (PExtended a))),
          '("_1", Term s (PAsData PBool))]
     -> Term s (PUpperBound a))
    -> Term s (PUpperBound a))
-> TermCont
     s
     (HRec
        '[ '("_0", Term s (PAsData (PExtended a))),
           '("_1", Term s (PAsData PBool))])
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] (Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (a :: S -> Type) (s :: S).
Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
uToE Term
  s
  (PUpperBound a
   :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
-> Term s (PUpperBound a)
-> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
y')
    let xt :: Term s (PAsData (PExtended a))
xt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    let yt :: Term s (PAsData (PExtended a))
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
y
    let xc :: Term s PBool
xc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  '[ '("_0", Term s (PAsData (PExtended a))),
     '("_1", Term s (PAsData PBool))]
x
    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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData (PExtended a)) -> Term s (PExtended a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (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 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 < endpoint
pbefore' ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    ( a
        :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
        :--> PBool
    )
pbefore' :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
pbefore' = ClosedTerm
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (a
    :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
          :--> PBool))
 -> Term
      s
      (a
       :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
             :--> PBool)))
-> ClosedTerm
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s a
 -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term s PBool)
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> 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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term s PBool)
-> Term
     s
     (c
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
plam ((Term s a
  -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
  -> Term s PBool)
 -> Term
      s
      (a
       :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
             :--> PBool)))
-> (Term s a
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
    -> Term s PBool)
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
y' -> 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
    HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y <- ((HRec
    (BoundTerms
       (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
       (Bindings
          (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
          '["_0", "_1"])
       s)
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           (Bindings
              (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
              '["_0", "_1"])
           s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     (BoundTerms
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        (Bindings
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           '["_0", "_1"])
        s)
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      s
      (HRec
         (BoundTerms
            (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
            (Bindings
               (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
               '["_0", "_1"])
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
          (Bindings
             (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
             '["_0", "_1"])
          s)
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           (Bindings
              (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
              '["_0", "_1"])
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
y'
    let yt :: Term s (PExtended a)
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y
    let yc :: Term s PBool
yc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y
    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 PBool
yc
        (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)
yt (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)
yt (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))

-- value > endpoint
pafter' ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, POrd a) =>
  Term
    s
    ( a
        :--> PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
        :--> PBool
    )
pafter' :: forall (a :: S -> Type) (s :: S).
(PIsData a, POrd a) =>
Term
  s
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
pafter' = ClosedTerm
  (a
   :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
         :--> PBool))
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (a
    :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
          :--> PBool))
 -> Term
      s
      (a
       :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
             :--> PBool)))
-> ClosedTerm
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s a
 -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term s PBool)
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> 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 (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
 -> Term s PBool)
-> Term
     s
     (c
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
plam ((Term s a
  -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
  -> Term s PBool)
 -> Term
      s
      (a
       :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
             :--> PBool)))
-> (Term s a
    -> Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
    -> Term s PBool)
-> Term
     s
     (a
      :--> (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]
            :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
a Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
y' -> 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
    HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y <- ((HRec
    (BoundTerms
       (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
       (Bindings
          (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
          '["_0", "_1"])
       s)
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           (Bindings
              (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
              '["_0", "_1"])
           s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont (((HRec
     (BoundTerms
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        (Bindings
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           '["_0", "_1"])
        s)
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      s
      (HRec
         (BoundTerms
            (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
            (Bindings
               (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
               '["_0", "_1"])
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
          (Bindings
             (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
             '["_0", "_1"])
          s)
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     s
     (HRec
        (BoundTerms
           (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
           (Bindings
              (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
              '["_0", "_1"])
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["_0", "_1"] Term s (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool])
y'
    let yt :: Term s (PExtended a)
yt = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_0" HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y
    let yc :: Term s PBool
yc = forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"_1" HRec
  (BoundTerms
     (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
     (Bindings
        (PFields (PDataRecord '["_0" ':= PExtended a, "_1" ':= PBool]))
        '["_0", "_1"])
     s)
y
    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 PBool
yc
        (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)
yt (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)
yt (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))

-- 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
  PNegInf Term s (PDataRecord '[])
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  PPosInf Term s (PDataRecord '[])
_ -> 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 (PDataRecord '["_0" ':= a])
r ->
    let y :: Term s a
y = forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p, as ~ PFields p, n ~ PLabelIndex name as,
 KnownNat n, a ~ PUnLabel (IndexList n as), PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" Term s (PDataRecord '["_0" ':= a] :--> a)
-> Term s (PDataRecord '["_0" ':= 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 (PDataRecord '["_0" ':= a])
r
     in Term s a
y Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
x