{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -fno-ignore-interface-pragmas #-}
{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
{-# OPTIONS_GHC -fno-specialise #-}

-- | A type for intervals and associated functions.
module PlutusLedgerApi.V1.Data.Interval
  ( Interval
  , pattern Interval
  , ivFrom
  , ivTo
  , UpperBound
  , pattern UpperBound
  , LowerBound
  , pattern LowerBound
  , Extended
  , pattern NegInf
  , pattern Finite
  , pattern PosInf
  , Closure
  , member
  , interval
  , from
  , to
  , always
  , never
  , singleton
  , hull
  , intersection
  , overlaps
  , contains
  , isEmpty
  , before
  , after
  , lowerBound
  , upperBound
  , strictLowerBound
  , strictUpperBound
  , mapInterval
  ) where

import Control.DeepSeq (NFData)
import GHC.Generics (Generic)
import Prettyprinter (Pretty (pretty), comma, (<+>))
import Prelude qualified as Haskell

import PlutusTx qualified
import PlutusTx.AsData qualified as PlutusTx
import PlutusTx.Blueprint (ConstructorSchema (..), Schema (..))
import PlutusTx.Blueprint.Class (HasBlueprintSchema (schema))
import PlutusTx.Blueprint.Definition
  ( HasBlueprintDefinition (..)
  , HasSchemaDefinition
  , Unrolled
  , definitionIdFromTypeK
  , definitionRef
  )
import PlutusTx.Blueprint.Definition.TF (Nub, type (++))
import PlutusTx.Blueprint.Schema.Annotation (SchemaInfo (..), emptySchemaInfo)
import PlutusTx.Eq as PlutusTx
import PlutusTx.Lift (makeLift)
import PlutusTx.Ord as PlutusTx
import PlutusTx.Prelude

-- See Note [Enumerable Intervals]

-- | Whether a bound is inclusive or not.
type Closure = Bool

-- | A set extended with a positive and negative infinity.
PlutusTx.asData
  [d|
    data Extended a = NegInf | Finite a | PosInf
      deriving stock (Haskell.Show, Generic)
      deriving newtype (PlutusTx.FromData, PlutusTx.UnsafeFromData, PlutusTx.ToData)
      deriving anyclass (NFData)
    |]

-- | The upper bound of an interval.
PlutusTx.asData
  [d|
    data UpperBound a = UpperBound (Extended a) Closure
      deriving stock (Haskell.Show, Generic)
      deriving newtype (PlutusTx.FromData, PlutusTx.UnsafeFromData, PlutusTx.ToData)
      deriving anyclass (NFData)
    |]

-- | The lower bound of an interval.
PlutusTx.asData
  [d|
    data LowerBound a = LowerBound (Extended a) Closure
      deriving stock (Haskell.Show, Generic)
      deriving newtype (PlutusTx.FromData, PlutusTx.UnsafeFromData, PlutusTx.ToData)
      deriving anyclass (NFData)
    |]

-- See Note [Enumerable Intervals]

{-| An interval of @a@s.

The interval may be either closed or open at either end, meaning
that the endpoints may or may not be included in the interval.

The interval can also be unbounded on either side.

The 'Eq' instance gives equality of the intervals, not structural equality.
There is no 'Ord' instance, but 'contains' gives a partial order.

Note that some of the functions on `Interval` rely on `Enum` in order to
handle non-inclusive endpoints. For this reason, it may not be safe to
use `Interval`s with non-inclusive endpoints on types whose `Enum`
instances have partial methods. -}
PlutusTx.asData
  [d|
    data Interval a = Interval {ivFrom :: LowerBound a, ivTo :: UpperBound a}
      deriving stock (Haskell.Show, Generic)
      deriving newtype (PlutusTx.FromData, PlutusTx.UnsafeFromData, PlutusTx.ToData)
      deriving anyclass (NFData)
    |]

instance HasBlueprintDefinition a => HasBlueprintDefinition (Interval a) where
  type
    Unroll (Interval a) =
      Nub (Interval a ': (Unrolled (LowerBound a) ++ Unrolled (UpperBound a)))
  definitionId :: DefinitionId
definitionId = forall k (t :: k). Typeable t => DefinitionId
definitionIdFromTypeK @_ @Interval DefinitionId -> DefinitionId -> DefinitionId
forall a. Semigroup a => a -> a -> a
Haskell.<> forall a. HasBlueprintDefinition a => DefinitionId
definitionId @a

instance
  ( HasBlueprintDefinition a
  , HasSchemaDefinition (LowerBound a) referencedTypes
  , HasSchemaDefinition (UpperBound a) referencedTypes
  )
  => HasBlueprintSchema (Interval a) referencedTypes
  where
  {-# INLINEABLE schema #-}
  schema :: Schema referencedTypes
schema =
    SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
forall (referencedTypes :: [*]).
SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
SchemaConstructor
      (Maybe String -> Maybe String -> Maybe String -> SchemaInfo
MkSchemaInfo Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)
      ( Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
forall (referencedTypes :: [*]).
Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
MkConstructorSchema
          Natural
0
          [ forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @(LowerBound a) @referencedTypes
          , forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @(UpperBound a) @referencedTypes
          ]
      )

mapInterval
  :: ( PlutusTx.ToData a1
     , PlutusTx.ToData a2
     , PlutusTx.UnsafeFromData a1
     , PlutusTx.UnsafeFromData a2
     )
  => (a1 -> a2)
  -> Interval a1
  -> Interval a2
mapInterval :: forall a1 a2.
(ToData a1, ToData a2, UnsafeFromData a1, UnsafeFromData a2) =>
(a1 -> a2) -> Interval a1 -> Interval a2
mapInterval a1 -> a2
f (Interval LowerBound a1
fromA UpperBound a1
toA) = LowerBound a2 -> UpperBound a2 -> Interval a2
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval ((a1 -> a2) -> LowerBound a1 -> LowerBound a2
forall a1 a2.
(ToData a1, ToData a2, UnsafeFromData a1, UnsafeFromData a2) =>
(a1 -> a2) -> LowerBound a1 -> LowerBound a2
mapLowerBound a1 -> a2
f LowerBound a1
fromA) ((a1 -> a2) -> UpperBound a1 -> UpperBound a2
forall a1 a2.
(ToData a1, ToData a2, UnsafeFromData a1, UnsafeFromData a2) =>
(a1 -> a2) -> UpperBound a1 -> UpperBound a2
mapUpperBound a1 -> a2
f UpperBound a1
toA)

instance (Pretty a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Pretty (Interval a) where
  pretty :: forall ann. Interval a -> Doc ann
pretty (Interval LowerBound a
l UpperBound a
h) = LowerBound a -> Doc ann
forall ann. LowerBound a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty LowerBound a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UpperBound a -> Doc ann
forall ann. UpperBound a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty UpperBound a
h

instance HasBlueprintDefinition a => HasBlueprintDefinition (Extended a) where
  type Unroll (Extended a) = Extended a ': Unrolled a
  definitionId :: DefinitionId
definitionId = forall k (t :: k). Typeable t => DefinitionId
definitionIdFromTypeK @_ @Extended DefinitionId -> DefinitionId -> DefinitionId
forall a. Semigroup a => a -> a -> a
Haskell.<> forall a. HasBlueprintDefinition a => DefinitionId
definitionId @a

mapExtended
  :: (PlutusTx.ToData t, PlutusTx.ToData a, PlutusTx.UnsafeFromData t, PlutusTx.UnsafeFromData a)
  => (t -> a) -> Extended t -> Extended a
mapExtended :: forall t a.
(ToData t, ToData a, UnsafeFromData t, UnsafeFromData a) =>
(t -> a) -> Extended t -> Extended a
mapExtended t -> a
_ Extended t
NegInf = Extended a
forall a. Extended a
NegInf
mapExtended t -> a
f (Finite t
a) = a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite (t -> a
f t
a)
mapExtended t -> a
_ Extended t
PosInf = Extended a
forall a. Extended a
PosInf

instance (Pretty a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Pretty (Extended a) where
  pretty :: forall ann. Extended a -> Doc ann
pretty Extended a
NegInf = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"-∞"
  pretty Extended a
PosInf = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"+∞"
  pretty (Finite a
a) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a

instance HasBlueprintDefinition (Extended a) => HasBlueprintDefinition (UpperBound a) where
  type Unroll (UpperBound a) = UpperBound a ': (Unrolled Closure ++ Unrolled (Extended a))
  definitionId :: DefinitionId
definitionId = forall k (t :: k). Typeable t => DefinitionId
definitionIdFromTypeK @_ @UpperBound DefinitionId -> DefinitionId -> DefinitionId
forall a. Semigroup a => a -> a -> a
Haskell.<> forall a. HasBlueprintDefinition a => DefinitionId
definitionId @(Extended a)

instance
  ( HasSchemaDefinition a referencedTypes
  , HasBlueprintDefinition a
  , HasSchemaDefinition (Extended a) referencedTypes
  , HasSchemaDefinition Closure referencedTypes
  )
  => HasBlueprintSchema (UpperBound a) referencedTypes
  where
  {-# INLINEABLE schema #-}
  schema :: Schema referencedTypes
schema =
    SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
forall (referencedTypes :: [*]).
SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
SchemaConstructor
      SchemaInfo
emptySchemaInfo {title = Just "UpperBound"}
      ( Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
forall (referencedTypes :: [*]).
Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
MkConstructorSchema
          Natural
0
          [ forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @(Extended a) @referencedTypes
          , forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @Closure @referencedTypes
          ]
      )

{-| For an enumerable type, turn an upper bound into a single inclusive
bounding value.

Since the type is enumerable, non-inclusive bounds are equivalent
to inclusive bounds on the predecessor.

See Note [Enumerable Intervals] -}
inclusiveUpperBound
  :: (Enum a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => UpperBound a -> Extended a
-- already inclusive
inclusiveUpperBound :: forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound (UpperBound Extended a
v Closure
True) = Extended a
v
-- take pred
inclusiveUpperBound (UpperBound (Finite a
x) Closure
False) = a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite (a -> Extended a) -> a -> Extended a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
pred a
x
-- an infinity: inclusive/non-inclusive makes no difference
inclusiveUpperBound (UpperBound Extended a
v Closure
False) = Extended a
v

mapUpperBound
  :: ( PlutusTx.ToData a1
     , PlutusTx.ToData a2
     , PlutusTx.UnsafeFromData a1
     , PlutusTx.UnsafeFromData a2
     )
  => (a1 -> a2) -> UpperBound a1 -> UpperBound a2
mapUpperBound :: forall a1 a2.
(ToData a1, ToData a2, UnsafeFromData a1, UnsafeFromData a2) =>
(a1 -> a2) -> UpperBound a1 -> UpperBound a2
mapUpperBound a1 -> a2
f (UpperBound Extended a1
e Closure
c) = Extended a2 -> Closure -> UpperBound a2
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound ((a1 -> a2) -> Extended a1 -> Extended a2
forall t a.
(ToData t, ToData a, UnsafeFromData t, UnsafeFromData a) =>
(t -> a) -> Extended t -> Extended a
mapExtended a1 -> a2
f Extended a1
e) Closure
c

instance (Pretty a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Pretty (UpperBound a) where
  pretty :: forall ann. UpperBound a -> Doc ann
pretty (UpperBound Extended a
PosInf Closure
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"+∞)"
  pretty (UpperBound Extended a
NegInf Closure
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"-∞)"
  pretty (UpperBound Extended a
a Closure
True) = Extended a -> Doc ann
forall ann. Extended a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Extended a
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"]"
  pretty (UpperBound Extended a
a Closure
False) = Extended a -> Doc ann
forall ann. Extended a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Extended a
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
")"

instance HasBlueprintDefinition (Extended a) => HasBlueprintDefinition (LowerBound a) where
  type Unroll (LowerBound a) = LowerBound a ': (Unrolled Closure ++ Unrolled (Extended a))
  definitionId :: DefinitionId
definitionId = forall k (t :: k). Typeable t => DefinitionId
definitionIdFromTypeK @_ @LowerBound DefinitionId -> DefinitionId -> DefinitionId
forall a. Semigroup a => a -> a -> a
Haskell.<> forall a. HasBlueprintDefinition a => DefinitionId
definitionId @(Extended a)

instance
  ( HasSchemaDefinition a referencedTypes
  , HasBlueprintDefinition a
  , HasSchemaDefinition (Extended a) referencedTypes
  , HasSchemaDefinition Closure referencedTypes
  )
  => HasBlueprintSchema (LowerBound a) referencedTypes
  where
  {-# INLINEABLE schema #-}
  schema :: Schema referencedTypes
schema =
    SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
forall (referencedTypes :: [*]).
SchemaInfo
-> ConstructorSchema referencedTypes -> Schema referencedTypes
SchemaConstructor
      SchemaInfo
emptySchemaInfo {title = Just "LowerBound"}
      ( Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
forall (referencedTypes :: [*]).
Natural
-> [Schema referencedTypes] -> ConstructorSchema referencedTypes
MkConstructorSchema
          Natural
0
          [ forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @(Extended a) @referencedTypes
          , forall t (ts :: [*]). HasBlueprintDefinition t => Schema ts
definitionRef @Closure @referencedTypes
          ]
      )

{-| For an enumerable type, turn an lower bound into a single inclusive
bounding value.

Since the type is enumerable, non-inclusive bounds are equivalent
to inclusive bounds on the successor.

See Note [Enumerable Intervals] -}
inclusiveLowerBound
  :: (Enum a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => LowerBound a -> Extended a
-- already inclusive
inclusiveLowerBound :: forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound (LowerBound Extended a
v Closure
True) = Extended a
v
-- take succ
inclusiveLowerBound (LowerBound (Finite a
x) Closure
False) = a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite (a -> Extended a) -> a -> Extended a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
succ a
x
-- an infinity: inclusive/non-inclusive makes no difference
inclusiveLowerBound (LowerBound Extended a
v Closure
False) = Extended a
v

mapLowerBound
  :: ( PlutusTx.ToData a1
     , PlutusTx.ToData a2
     , PlutusTx.UnsafeFromData a1
     , PlutusTx.UnsafeFromData a2
     )
  => (a1 -> a2) -> LowerBound a1 -> LowerBound a2
mapLowerBound :: forall a1 a2.
(ToData a1, ToData a2, UnsafeFromData a1, UnsafeFromData a2) =>
(a1 -> a2) -> LowerBound a1 -> LowerBound a2
mapLowerBound a1 -> a2
f (LowerBound Extended a1
e Closure
c) = Extended a2 -> Closure -> LowerBound a2
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound ((a1 -> a2) -> Extended a1 -> Extended a2
forall t a.
(ToData t, ToData a, UnsafeFromData t, UnsafeFromData a) =>
(t -> a) -> Extended t -> Extended a
mapExtended a1 -> a2
f Extended a1
e) Closure
c

instance (Pretty a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Pretty (LowerBound a) where
  pretty :: forall ann. LowerBound a -> Doc ann
pretty (LowerBound Extended a
PosInf Closure
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"(+∞"
  pretty (LowerBound Extended a
NegInf Closure
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"(-∞"
  pretty (LowerBound Extended a
a Closure
True) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"[" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Extended a -> Doc ann
forall ann. Extended a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Extended a
a
  pretty (LowerBound Extended a
a Closure
False) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"(" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Extended a -> Doc ann
forall ann. Extended a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Extended a
a

instance (Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Eq (Extended a) where
  {-# INLINEABLE (==) #-}
  Extended a
NegInf == :: Extended a -> Extended a -> Closure
== Extended a
NegInf = Closure
True
  Extended a
PosInf == Extended a
PosInf = Closure
True
  Finite a
l == Finite a
r = a
l a -> a -> Closure
forall a. Eq a => a -> a -> Closure
== a
r
  Extended a
_ == Extended a
_ = Closure
False

instance (Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Haskell.Eq (Extended a) where
  == :: Extended a -> Extended a -> Closure
(==) = Extended a -> Extended a -> Closure
forall a. Eq a => a -> a -> Closure
(PlutusTx.==)

instance (Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Ord (Extended a) where
  {-# INLINEABLE compare #-}
  Extended a
NegInf compare :: Extended a -> Extended a -> Ordering
`compare` Extended a
NegInf = Ordering
EQ
  Extended a
NegInf `compare` Extended a
_ = Ordering
LT
  Extended a
_ `compare` Extended a
NegInf = Ordering
GT
  Extended a
PosInf `compare` Extended a
PosInf = Ordering
EQ
  Extended a
_ `compare` Extended a
PosInf = Ordering
LT
  Extended a
PosInf `compare` Extended a
_ = Ordering
GT
  Finite a
l `compare` Finite a
r = a
l a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
r

instance (Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Haskell.Ord (Extended a) where
  compare :: Extended a -> Extended a -> Ordering
compare = Extended a -> Extended a -> Ordering
forall a. Ord a => a -> a -> Ordering
PlutusTx.compare

-- See Note [Enumerable Intervals]
instance (Enum a, Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Eq (UpperBound a) where
  {-# INLINEABLE (==) #-}
  UpperBound a
b1 == :: UpperBound a -> UpperBound a -> Closure
== UpperBound a
b2 = UpperBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b1 Extended a -> Extended a -> Closure
forall a. Eq a => a -> a -> Closure
== UpperBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b2

instance
  (Enum a, Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Haskell.Eq (UpperBound a)
  where
  == :: UpperBound a -> UpperBound a -> Closure
(==) = UpperBound a -> UpperBound a -> Closure
forall a. Eq a => a -> a -> Closure
(PlutusTx.==)

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Ord (UpperBound a)
  where
  {-# INLINEABLE compare #-}
  UpperBound a
b1 compare :: UpperBound a -> UpperBound a -> Ordering
`compare` UpperBound a
b2 = UpperBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b1 Extended a -> Extended a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` UpperBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b2

instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Haskell.Ord (UpperBound a)
  where
  compare :: UpperBound a -> UpperBound a -> Ordering
compare = UpperBound a -> UpperBound a -> Ordering
forall a. Ord a => a -> a -> Ordering
PlutusTx.compare

-- See Note [Enumerable Intervals]
instance
  (Enum a, Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Eq (LowerBound a)
  where
  {-# INLINEABLE (==) #-}
  LowerBound a
b1 == :: LowerBound a -> LowerBound a -> Closure
== LowerBound a
b2 = LowerBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b1 Extended a -> Extended a -> Closure
forall a. Eq a => a -> a -> Closure
== LowerBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b2

instance
  (Enum a, Eq a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Haskell.Eq (LowerBound a)
  where
  == :: LowerBound a -> LowerBound a -> Closure
(==) = LowerBound a -> LowerBound a -> Closure
forall a. Eq a => a -> a -> Closure
(PlutusTx.==)

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Ord (LowerBound a)
  where
  {-# INLINEABLE compare #-}
  LowerBound a
b1 compare :: LowerBound a -> LowerBound a -> Ordering
`compare` LowerBound a
b2 = LowerBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b1 Extended a -> Extended a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` LowerBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b2

instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Haskell.Ord (LowerBound a)
  where
  compare :: LowerBound a -> LowerBound a -> Ordering
compare = LowerBound a -> LowerBound a -> Ordering
forall a. Ord a => a -> a -> Ordering
PlutusTx.compare

{-| Construct a strict upper bound from a value.
The resulting bound includes all values that are (strictly) smaller than the input value. -}
strictUpperBound :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> UpperBound a
strictUpperBound :: forall a. (ToData a, UnsafeFromData a) => a -> UpperBound a
strictUpperBound a
a = Extended a -> Closure -> UpperBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound (a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite a
a) Closure
False
{-# INLINEABLE strictUpperBound #-}

{-| Construct a strict lower bound from a value.
The resulting bound includes all values that are (strictly) greater than the input value. -}
strictLowerBound :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> LowerBound a
strictLowerBound :: forall a. (ToData a, UnsafeFromData a) => a -> LowerBound a
strictLowerBound a
a = Extended a -> Closure -> LowerBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound (a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite a
a) Closure
False
{-# INLINEABLE strictLowerBound #-}

{-| Construct a lower bound from a value.
The resulting bound includes all values that are equal or greater than the input value. -}
lowerBound :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> LowerBound a
lowerBound :: forall a. (ToData a, UnsafeFromData a) => a -> LowerBound a
lowerBound a
a = Extended a -> Closure -> LowerBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound (a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite a
a) Closure
True
{-# INLINEABLE lowerBound #-}

{-|  Construct an upper bound from a value.
The resulting bound includes all values that are equal or smaller than the input value. -}
upperBound :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> UpperBound a
upperBound :: forall a. (ToData a, UnsafeFromData a) => a -> UpperBound a
upperBound a
a = Extended a -> Closure -> UpperBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound (a -> Extended a
forall a. (ToData a, UnsafeFromData a) => a -> Extended a
Finite a
a) Closure
True
{-# INLINEABLE upperBound #-}

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => JoinSemiLattice (Interval a)
  where
  {-# INLINEABLE (\/) #-}
  \/ :: Interval a -> Interval a -> Interval a
(\/) = Interval a -> Interval a -> Interval a
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Interval a
hull

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => BoundedJoinSemiLattice (Interval a)
  where
  {-# INLINEABLE bottom #-}
  bottom :: Interval a
bottom = Interval a
forall a. (ToData a, UnsafeFromData a) => Interval a
never

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => MeetSemiLattice (Interval a)
  where
  {-# INLINEABLE (/\) #-}
  /\ :: Interval a -> Interval a -> Interval a
(/\) = Interval a -> Interval a -> Interval a
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Interval a
intersection

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => BoundedMeetSemiLattice (Interval a)
  where
  {-# INLINEABLE top #-}
  top :: Interval a
top = Interval a
forall a. (ToData a, UnsafeFromData a) => Interval a
always

-- See Note [Enumerable Intervals]
instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Eq (Interval a)
  where
  {-# INLINEABLE (==) #-}
  -- Degenerate case: both the intervals are empty.
  -- There can be many empty intervals, so we check for this case
  -- explicitly
  Interval a
iv1 == :: Interval a -> Interval a -> Closure
== Interval a
iv2 | Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty Interval a
iv1 Closure -> Closure -> Closure
&& Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty Interval a
iv2 = Closure
True
  (Interval LowerBound a
lb1 UpperBound a
ub1) == (Interval LowerBound a
lb2 UpperBound a
ub2) = LowerBound a
lb1 LowerBound a -> LowerBound a -> Closure
forall a. Eq a => a -> a -> Closure
== LowerBound a
lb2 Closure -> Closure -> Closure
&& UpperBound a
ub1 UpperBound a -> UpperBound a -> Closure
forall a. Eq a => a -> a -> Closure
== UpperBound a
ub2

instance
  (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Haskell.Eq (Interval a)
  where
  {-# INLINEABLE (==) #-}
  == :: Interval a -> Interval a -> Closure
(==) = Interval a -> Interval a -> Closure
forall a. Eq a => a -> a -> Closure
(PlutusTx.==)

{-| @interval a b@ includes all values that are greater than or equal to @a@
and smaller than or equal to @b@. Therefore it includes @a@ and @b@. In math. notation: [a,b] -}
interval :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> a -> Interval a
interval :: forall a. (ToData a, UnsafeFromData a) => a -> a -> Interval a
interval a
s a
s' = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (a -> LowerBound a
forall a. (ToData a, UnsafeFromData a) => a -> LowerBound a
lowerBound a
s) (a -> UpperBound a
forall a. (ToData a, UnsafeFromData a) => a -> UpperBound a
upperBound a
s')
{-# INLINEABLE interval #-}

{-| Create an interval that includes just a single concrete point @a@,
i.e. having the same non-strict lower and upper bounds. In math.notation: [a,a] -}
singleton :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> Interval a
singleton :: forall a. (ToData a, UnsafeFromData a) => a -> Interval a
singleton a
s = a -> a -> Interval a
forall a. (ToData a, UnsafeFromData a) => a -> a -> Interval a
interval a
s a
s
{-# INLINEABLE singleton #-}

{-| @from a@ is an 'Interval' that includes all values that are
 greater than or equal to @a@. In math. notation: [a,+∞] -}
from :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> Interval a
from :: forall a. (ToData a, UnsafeFromData a) => a -> Interval a
from a
s = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (a -> LowerBound a
forall a. (ToData a, UnsafeFromData a) => a -> LowerBound a
lowerBound a
s) (Extended a -> Closure -> UpperBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound Extended a
forall a. Extended a
PosInf Closure
True)
{-# INLINEABLE from #-}

{-| @to a@ is an 'Interval' that includes all values that are
 smaller than or equal to @a@. In math. notation: [-∞,a] -}
to :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => a -> Interval a
to :: forall a. (ToData a, UnsafeFromData a) => a -> Interval a
to a
s = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (Extended a -> Closure -> LowerBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound Extended a
forall a. Extended a
NegInf Closure
True) (a -> UpperBound a
forall a. (ToData a, UnsafeFromData a) => a -> UpperBound a
upperBound a
s)
{-# INLINEABLE to #-}

-- | An 'Interval' that covers every slot. In math. notation [-∞,+∞]
always :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Interval a
always :: forall a. (ToData a, UnsafeFromData a) => Interval a
always = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (Extended a -> Closure -> LowerBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound Extended a
forall a. Extended a
NegInf Closure
True) (Extended a -> Closure -> UpperBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound Extended a
forall a. Extended a
PosInf Closure
True)
{-# INLINEABLE always #-}

{-| An 'Interval' that is empty.
There can be many empty intervals, see `isEmpty`.
The empty interval `never` is arbitrarily set to [+∞,-∞]. -}
never :: (PlutusTx.ToData a, PlutusTx.UnsafeFromData a) => Interval a
never :: forall a. (ToData a, UnsafeFromData a) => Interval a
never = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (Extended a -> Closure -> LowerBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> LowerBound a
LowerBound Extended a
forall a. Extended a
PosInf Closure
True) (Extended a -> Closure -> UpperBound a
forall a.
(ToData a, UnsafeFromData a) =>
Extended a -> Closure -> UpperBound a
UpperBound Extended a
forall a. Extended a
NegInf Closure
True)
{-# INLINEABLE never #-}

-- | Check whether a value is in an interval.
member
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => a -> Interval a -> Bool
member :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
a -> Interval a -> Closure
member a
a Interval a
i = Interval a
i Interval a -> Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Closure
`contains` a -> Interval a
forall a. (ToData a, UnsafeFromData a) => a -> Interval a
singleton a
a
{-# INLINEABLE member #-}

{-| Check whether two intervals overlap, that is, whether there is a value that
  is a member of both intervals. -}
overlaps
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Interval a -> Interval a -> Bool
overlaps :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Closure
overlaps Interval a
l Interval a
r = Closure -> Closure
not (Closure -> Closure) -> Closure -> Closure
forall a b. (a -> b) -> a -> b
$ Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty (Interval a
l Interval a -> Interval a -> Interval a
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Interval a
`intersection` Interval a
r)
{-# INLINEABLE overlaps #-}

{-| 'intersection a b' is the largest interval that is contained in 'a' and in
  'b', if it exists. -}
intersection
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Interval a -> Interval a -> Interval a
intersection :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Interval a
intersection (Interval LowerBound a
l1 UpperBound a
h1) (Interval LowerBound a
l2 UpperBound a
h2) = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (LowerBound a -> LowerBound a -> LowerBound a
forall a. Ord a => a -> a -> a
max LowerBound a
l1 LowerBound a
l2) (UpperBound a -> UpperBound a -> UpperBound a
forall a. Ord a => a -> a -> a
min UpperBound a
h1 UpperBound a
h2)
{-# INLINEABLE intersection #-}

-- | 'hull a b' is the smallest interval containing 'a' and 'b'.
hull
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Interval a -> Interval a -> Interval a
hull :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Interval a
hull (Interval LowerBound a
l1 UpperBound a
h1) (Interval LowerBound a
l2 UpperBound a
h2) = LowerBound a -> UpperBound a -> Interval a
forall a.
(ToData a, UnsafeFromData a) =>
LowerBound a -> UpperBound a -> Interval a
Interval (LowerBound a -> LowerBound a -> LowerBound a
forall a. Ord a => a -> a -> a
min LowerBound a
l1 LowerBound a
l2) (UpperBound a -> UpperBound a -> UpperBound a
forall a. Ord a => a -> a -> a
max UpperBound a
h1 UpperBound a
h2)
{-# INLINEABLE hull #-}

{-| @a `contains` b@ is true if the 'Interval' @b@ is entirely contained in
@a@. That is, @a `contains` b@ if for every entry @s@, if @member s b@ then
@member s a@. -}
contains
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Interval a -> Interval a -> Bool
-- Everything contains the empty interval
contains :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Interval a -> Closure
contains Interval a
_ Interval a
i2 | Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty Interval a
i2 = Closure
True
-- Nothing is contained in the empty interval (except the empty interval,
-- which is already handled)
contains Interval a
i1 Interval a
_ | Interval a -> Closure
forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty Interval a
i1 = Closure
False
-- Otherwise we check the endpoints. This doesn't work for empty intervals,
-- hence the cases above.
contains (Interval LowerBound a
l1 UpperBound a
h1) (Interval LowerBound a
l2 UpperBound a
h2) = LowerBound a
l1 LowerBound a -> LowerBound a -> Closure
forall a. Ord a => a -> a -> Closure
<= LowerBound a
l2 Closure -> Closure -> Closure
&& UpperBound a
h2 UpperBound a -> UpperBound a -> Closure
forall a. Ord a => a -> a -> Closure
<= UpperBound a
h1
{-# INLINEABLE contains #-}

-- | Check if an 'Interval' is empty.
isEmpty
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => Interval a -> Bool
isEmpty :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
Interval a -> Closure
isEmpty (Interval LowerBound a
lb UpperBound a
ub) = case LowerBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
lb Extended a -> Extended a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` UpperBound a -> Extended a
forall a.
(Enum a, ToData a, UnsafeFromData a) =>
UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
ub of
  -- We have at least two possible values, the lower bound and the upper bound
  Ordering
LT -> Closure
False
  -- We have one possible value, the lower bound/upper bound
  Ordering
EQ -> Closure
False
  -- We have no possible values
  Ordering
GT -> Closure
True
{-# INLINEABLE isEmpty #-}

-- | Check if a value is earlier than the beginning of an 'Interval'.
before
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => a -> Interval a -> Bool
before :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
a -> Interval a -> Closure
before a
h (Interval LowerBound a
f UpperBound a
_) = a -> LowerBound a
forall a. (ToData a, UnsafeFromData a) => a -> LowerBound a
lowerBound a
h LowerBound a -> LowerBound a -> Closure
forall a. Ord a => a -> a -> Closure
< LowerBound a
f
{-# INLINEABLE before #-}

-- | Check if a value is later than the end of an 'Interval'.
after
  :: (Enum a, Ord a, PlutusTx.ToData a, PlutusTx.UnsafeFromData a)
  => a -> Interval a -> Bool
after :: forall a.
(Enum a, Ord a, ToData a, UnsafeFromData a) =>
a -> Interval a -> Closure
after a
h (Interval LowerBound a
_ UpperBound a
t) = a -> UpperBound a
forall a. (ToData a, UnsafeFromData a) => a -> UpperBound a
upperBound a
h UpperBound a -> UpperBound a -> Closure
forall a. Ord a => a -> a -> Closure
> UpperBound a
t
{-# INLINEABLE after #-}

{- Note [Enumerable Intervals]
The 'Interval' type is set up to handle open intervals, where we have non-inclusive
bounds. These are only meaningful for orders where there do not exist (computable)
joins and meets over all elements greater or less than an element.

If those do exist, we can eliminate non-inclusive bounds in favour of inclusive bounds.
For example, in the integers, (x, y) is equivalent to [x+1, y-1], because
x+1 = sup { z | z > x} and y-1 = inf { z | z < y }.

Checking equality, containment etc. of intervals with non-inclusive bounds is
tricky. For example, to know if (x, y) is empty, we need to know if there is a
value between x and y. We don't have a typeclass for that!

In practice, most of the intervals we care about are enumerable (have 'Enum'
instances). We assume that `pred` and `succ` calculate the infima/suprema described
above, and so we can turn non-inclusive bounds into inclusive bounds, which
makes things much easier. The downside is that some of the `Enum` instances have
partial implementations, which means that, e.g. `isEmpty (False, True]` will
throw.

The upshot of this is that many functions in this module require 'Enum'.
-}

----------------------------------------------------------------------------------------------------
-- TH Splices --------------------------------------------------------------------------------------

$(makeLift ''Extended)
$(makeLift ''LowerBound)
$(makeLift ''UpperBound)
$(makeLift ''Interval)