{-# OPTIONS_GHC -Wno-orphans #-}
module Plutarch.LedgerApi.Interval (
PInterval (..),
PLowerBound (..),
PUpperBound (..),
PExtended (..),
psingleton,
pfrom,
pto,
palways,
pinterval,
pinclusiveLowerBound,
pinclusiveUpperBound,
pmember,
pcontains,
pbefore,
pafter,
pisEmpty,
phull,
pintersection,
) where
import Data.Kind (Type)
import GHC.Generics (Generic)
import GHC.Records (getField)
import Plutarch.Prelude hiding (psingleton, pto)
import PlutusLedgerApi.V3 qualified as Plutus
newtype PInterval (a :: S -> Type) (s :: S)
= PInterval
( Term
s
( PDataRecord
'[ "from" ':= PLowerBound a
, "to" ':= PUpperBound a
]
)
)
deriving stock
(
(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
(
(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
,
(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
,
(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
,
(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
,
(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
)
instance DerivePlutusType (PInterval a) where
type DPTStrat _ = PlutusTypeData
deriving via
DeriveDataPLiftable (PInterval a) (Plutus.Interval (AsHaskell a))
instance
(Plutus.FromData (AsHaskell a), Plutus.ToData (AsHaskell a)) => PLiftable (PInterval a)
instance PTryFrom PData a => PTryFrom PData (PInterval a)
instance PTryFrom PData a => PTryFrom PData (PAsData (PInterval a))
newtype PLowerBound (a :: S -> Type) (s :: S)
= PLowerBound
( Term
s
( PDataRecord
'[ "_0" ':= PExtended a
, "_1" ':= PBool
]
)
)
deriving stock
(
(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
(
(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
,
(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
,
(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
,
(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)
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)
instance (PIsData a, PCountable a) => POrd (PLowerBound a) where
{-# INLINEABLE (#<=) #-}
Term s (PLowerBound a)
lb1 #<= :: forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
#<= Term s (PLowerBound a)
lb2 = (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb2)
{-# INLINEABLE (#<) #-}
Term s (PLowerBound a)
lb1 #< :: forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
#< Term s (PLowerBound a)
lb2 = (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< (Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
lb2)
instance DerivePlutusType (PLowerBound a) where
type DPTStrat _ = PlutusTypeData
instance PTryFrom PData a => PTryFrom PData (PLowerBound a)
instance PTryFrom PData a => PTryFrom PData (PAsData (PLowerBound a))
newtype PUpperBound (a :: S -> Type) (s :: S)
= PUpperBound
( Term
s
( PDataRecord
'[ "_0" ':= PExtended a
, "_1" ':= PBool
]
)
)
deriving stock
(
(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
(
(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
,
(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
,
(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
,
(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)
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)
instance (PIsData a, PEnumerable a) => POrd (PUpperBound a) where
{-# INLINEABLE (#<=) #-}
Term s (PUpperBound a)
ub1 #<= :: forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
#<= Term s (PUpperBound a)
ub2 = (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub2)
{-# INLINEABLE (#<) #-}
Term s (PUpperBound a)
ub1 #< :: forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
#< Term s (PUpperBound a)
ub2 = (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub1) Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (s :: S).
Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< (Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
ub2)
instance DerivePlutusType (PUpperBound a) where
type DPTStrat _ = PlutusTypeData
instance PTryFrom PData a => PTryFrom PData (PUpperBound a)
instance PTryFrom PData a => PTryFrom PData (PAsData (PUpperBound a))
data PExtended (a :: S -> Type) (s :: S)
= PNegInf (Term s (PDataRecord '[]))
| PFinite (Term s (PDataRecord '["_0" ':= a]))
| PPosInf (Term s (PDataRecord '[]))
deriving stock
(
(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
(
(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
,
(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
,
(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
,
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 (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 PBool
forall (s :: S).
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
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 t)
-> (forall (s :: S). Term s t -> Term s t -> Term s t)
-> POrd t
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 (a :: S -> Type) (s :: S).
(POrd a, PIsData a) =>
Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PExtended a)
$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
$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
,
(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)
instance DerivePlutusType (PExtended a) where
type DPTStrat _ = PlutusTypeData
instance PTryFrom PData a => PTryFrom PData (PExtended a)
instance PTryFrom PData a => PTryFrom PData (PAsData (PExtended a))
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)
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 (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
inclusiveUpperBound
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
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
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
PExtended a s
_ -> Term s (PExtended a)
extended
)
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
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
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
PExtended a s
_ -> Term s (PExtended a)
extended
)
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
let ilb2 :: Term s (PExtended a)
ilb2 = Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
l2
let iub2 :: Term s (PExtended a)
iub2 = Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
u2
Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s (PExtended a)
ilb2 Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
iub2)
(PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue)
( TermCont s (Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PBool) -> Term s PBool)
-> TermCont s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
let ilb1 :: Term s (PExtended a)
ilb1 = Term s (PLowerBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PCountable a) =>
Term s (PLowerBound a :--> PExtended a)
pinclusiveLowerBound Term s (PLowerBound a :--> PExtended a)
-> Term s (PLowerBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PLowerBound a)
l1
let iub1 :: Term s (PExtended a)
iub1 = Term s (PUpperBound a :--> PExtended a)
forall (a :: S -> Type) (s :: S).
(PIsData a, PEnumerable a) =>
Term s (PUpperBound a :--> PExtended a)
pinclusiveUpperBound Term s (PUpperBound a :--> PExtended a)
-> Term s (PUpperBound a) -> Term s (PExtended a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUpperBound a)
u1
Term s PBool -> TermCont s (Term s PBool)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont s (Term s PBool))
-> Term s PBool -> TermCont s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s (PExtended a)
ilb1 Term s (PExtended a) -> Term s (PExtended a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s a -> Term s a -> Term s PBool
#> Term s (PExtended a)
iub1)
(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)
((Term s (PLowerBound a)
l1 Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
forall (s :: S).
Term s (PLowerBound a) -> Term s (PLowerBound a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PLowerBound a)
l2) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (PUpperBound a)
u2 Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
forall (s :: S).
Term s (PUpperBound a) -> Term s (PUpperBound a) -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PUpperBound a)
u1))
)
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
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
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
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 ::
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 ::
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
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)
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 ::
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
pclosedInterval ::
forall (a :: S -> Type) (s :: S).
Term
s
( PExtended a
:--> PExtended a
:--> PInterval a
)
pclosedInterval :: forall (a :: S -> Type) (s :: S).
Term s (PExtended a :--> (PExtended a :--> PInterval a))
pclosedInterval = ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a)))
-> ClosedTerm (PExtended a :--> (PExtended a :--> PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$
(Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (c :--> (PExtended a :--> PInterval a))
plam ((Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a)))
-> (Term s (PExtended a)
-> Term s (PExtended a) -> Term s (PInterval a))
-> Term s (PExtended a :--> (PExtended a :--> PInterval a))
forall a b. (a -> b) -> a -> b
$ \Term s (PExtended a)
start Term s (PExtended a)
end ->
let closure :: Term s (PAsData PBool)
closure = forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @(PAsData PBool) Bool
AsHaskell (PAsData PBool)
True
upper :: Term s (PUpperBound a)
upper =
PUpperBound a s -> Term s (PUpperBound a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PUpperBound a s -> Term s (PUpperBound a))
-> PUpperBound a s -> Term s (PUpperBound a)
forall a b. (a -> b) -> a -> b
$
Term s (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
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).
POrd 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).
POrd 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).
POrd 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).
POrd 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).
POrd 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).
POrd 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).
POrd 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).
POrd 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).
POrd 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'))
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))
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))
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
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
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).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s a
x