{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE NoImplicitPrelude    #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns         #-}

{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
{-# OPTIONS_GHC -fno-specialise #-}
{-# OPTIONS_GHC -fno-ignore-interface-pragmas #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}

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

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

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.Blueprint.TH (makeIsDataSchemaIndexed)
import PlutusTx.Eq as PlutusTx
import PlutusTx.IsData (makeIsDataIndexed)
import PlutusTx.Lift (makeLift)
import PlutusTx.Ord as PlutusTx
import PlutusTx.Prelude

-- 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.
-}
data Interval a = Interval { forall a. Interval a -> LowerBound a
ivFrom :: LowerBound a, forall a. Interval a -> UpperBound a
ivTo :: UpperBound a }
    deriving stock (Int -> Interval a -> ShowS
[Interval a] -> ShowS
Interval a -> String
(Int -> Interval a -> ShowS)
-> (Interval a -> String)
-> ([Interval a] -> ShowS)
-> Show (Interval a)
forall a. Show a => Int -> Interval a -> ShowS
forall a. Show a => [Interval a] -> ShowS
forall a. Show a => Interval a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Interval a -> ShowS
showsPrec :: Int -> Interval a -> ShowS
$cshow :: forall a. Show a => Interval a -> String
show :: Interval a -> String
$cshowList :: forall a. Show a => [Interval a] -> ShowS
showList :: [Interval a] -> ShowS
Haskell.Show, (forall x. Interval a -> Rep (Interval a) x)
-> (forall x. Rep (Interval a) x -> Interval a)
-> Generic (Interval a)
forall x. Rep (Interval a) x -> Interval a
forall x. Interval a -> Rep (Interval a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Interval a) x -> Interval a
forall a x. Interval a -> Rep (Interval a) x
$cfrom :: forall a x. Interval a -> Rep (Interval a) x
from :: forall x. Interval a -> Rep (Interval a) x
$cto :: forall a x. Rep (Interval a) x -> Interval a
to :: forall x. Rep (Interval a) x -> Interval a
Generic)
    deriving anyclass (Interval a -> ()
(Interval a -> ()) -> NFData (Interval a)
forall a. NFData a => Interval a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => Interval a -> ()
rnf :: Interval a -> ()
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
          ]
      )

instance Functor Interval where
  fmap :: forall a b. (a -> b) -> Interval a -> Interval b
fmap a -> b
f (Interval LowerBound a
fromA UpperBound a
toA) = LowerBound b -> UpperBound b -> Interval b
forall a. LowerBound a -> UpperBound a -> Interval a
Interval (a -> b
f (a -> b) -> LowerBound a -> LowerBound b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LowerBound a
fromA) (a -> b
f (a -> b) -> UpperBound a -> UpperBound b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpperBound a
toA)

instance Pretty 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 a ann. Pretty a => a -> Doc ann
forall ann. LowerBound 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 a ann. Pretty a => a -> Doc ann
forall ann. UpperBound a -> Doc ann
pretty UpperBound a
h

-- | A set extended with a positive and negative infinity.
data Extended a = NegInf | Finite a | PosInf
    deriving stock (Int -> Extended a -> ShowS
[Extended a] -> ShowS
Extended a -> String
(Int -> Extended a -> ShowS)
-> (Extended a -> String)
-> ([Extended a] -> ShowS)
-> Show (Extended a)
forall a. Show a => Int -> Extended a -> ShowS
forall a. Show a => [Extended a] -> ShowS
forall a. Show a => Extended a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Extended a -> ShowS
showsPrec :: Int -> Extended a -> ShowS
$cshow :: forall a. Show a => Extended a -> String
show :: Extended a -> String
$cshowList :: forall a. Show a => [Extended a] -> ShowS
showList :: [Extended a] -> ShowS
Haskell.Show, (forall x. Extended a -> Rep (Extended a) x)
-> (forall x. Rep (Extended a) x -> Extended a)
-> Generic (Extended a)
forall x. Rep (Extended a) x -> Extended a
forall x. Extended a -> Rep (Extended a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Extended a) x -> Extended a
forall a x. Extended a -> Rep (Extended a) x
$cfrom :: forall a x. Extended a -> Rep (Extended a) x
from :: forall x. Extended a -> Rep (Extended a) x
$cto :: forall a x. Rep (Extended a) x -> Extended a
to :: forall x. Rep (Extended a) x -> Extended a
Generic)
    deriving anyclass (Extended a -> ()
(Extended a -> ()) -> NFData (Extended a)
forall a. NFData a => Extended a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => Extended a -> ()
rnf :: Extended a -> ()
NFData)

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

instance Functor Extended where
  fmap :: forall a b. (a -> b) -> Extended a -> Extended b
fmap a -> b
_ Extended a
NegInf     = Extended b
forall a. Extended a
NegInf
  fmap a -> b
f (Finite a
a) = b -> Extended b
forall a. a -> Extended a
Finite (a -> b
f a
a)
  fmap a -> b
_ Extended a
PosInf     = Extended b
forall a. Extended a
PosInf

instance Pretty 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

-- See Note [Enumerable Intervals]
-- | Whether a bound is inclusive or not.
type Closure = Bool

-- | The upper bound of an interval.
data UpperBound a = UpperBound (Extended a) Closure
    deriving stock (Int -> UpperBound a -> ShowS
[UpperBound a] -> ShowS
UpperBound a -> String
(Int -> UpperBound a -> ShowS)
-> (UpperBound a -> String)
-> ([UpperBound a] -> ShowS)
-> Show (UpperBound a)
forall a. Show a => Int -> UpperBound a -> ShowS
forall a. Show a => [UpperBound a] -> ShowS
forall a. Show a => UpperBound a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> UpperBound a -> ShowS
showsPrec :: Int -> UpperBound a -> ShowS
$cshow :: forall a. Show a => UpperBound a -> String
show :: UpperBound a -> String
$cshowList :: forall a. Show a => [UpperBound a] -> ShowS
showList :: [UpperBound a] -> ShowS
Haskell.Show, (forall x. UpperBound a -> Rep (UpperBound a) x)
-> (forall x. Rep (UpperBound a) x -> UpperBound a)
-> Generic (UpperBound a)
forall x. Rep (UpperBound a) x -> UpperBound a
forall x. UpperBound a -> Rep (UpperBound a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (UpperBound a) x -> UpperBound a
forall a x. UpperBound a -> Rep (UpperBound a) x
$cfrom :: forall a x. UpperBound a -> Rep (UpperBound a) x
from :: forall x. UpperBound a -> Rep (UpperBound a) x
$cto :: forall a x. Rep (UpperBound a) x -> UpperBound a
to :: forall x. Rep (UpperBound a) x -> UpperBound a
Generic)
    deriving anyclass (UpperBound a -> ()
(UpperBound a -> ()) -> NFData (UpperBound a)
forall a. NFData a => UpperBound a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => UpperBound a -> ()
rnf :: UpperBound a -> ()
NFData)

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 => UpperBound a -> Extended a
-- already inclusive
inclusiveUpperBound :: forall a. Enum 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. 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

instance Functor UpperBound where
  fmap :: forall a b. (a -> b) -> UpperBound a -> UpperBound b
fmap a -> b
f (UpperBound Extended a
e Closure
c) = Extended b -> Closure -> UpperBound b
forall a. Extended a -> Closure -> UpperBound a
UpperBound (a -> b
f (a -> b) -> Extended a -> Extended b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Extended a
e) Closure
c

instance Pretty 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 a ann. Pretty a => a -> Doc ann
forall ann. Extended 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 a ann. Pretty a => a -> Doc ann
forall ann. Extended 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
")"

-- | The lower bound of an interval.
data LowerBound a = LowerBound (Extended a) Closure
    deriving stock (Int -> LowerBound a -> ShowS
[LowerBound a] -> ShowS
LowerBound a -> String
(Int -> LowerBound a -> ShowS)
-> (LowerBound a -> String)
-> ([LowerBound a] -> ShowS)
-> Show (LowerBound a)
forall a. Show a => Int -> LowerBound a -> ShowS
forall a. Show a => [LowerBound a] -> ShowS
forall a. Show a => LowerBound a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> LowerBound a -> ShowS
showsPrec :: Int -> LowerBound a -> ShowS
$cshow :: forall a. Show a => LowerBound a -> String
show :: LowerBound a -> String
$cshowList :: forall a. Show a => [LowerBound a] -> ShowS
showList :: [LowerBound a] -> ShowS
Haskell.Show, (forall x. LowerBound a -> Rep (LowerBound a) x)
-> (forall x. Rep (LowerBound a) x -> LowerBound a)
-> Generic (LowerBound a)
forall x. Rep (LowerBound a) x -> LowerBound a
forall x. LowerBound a -> Rep (LowerBound a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LowerBound a) x -> LowerBound a
forall a x. LowerBound a -> Rep (LowerBound a) x
$cfrom :: forall a x. LowerBound a -> Rep (LowerBound a) x
from :: forall x. LowerBound a -> Rep (LowerBound a) x
$cto :: forall a x. Rep (LowerBound a) x -> LowerBound a
to :: forall x. Rep (LowerBound a) x -> LowerBound a
Generic)
    deriving anyclass (LowerBound a -> ()
(LowerBound a -> ()) -> NFData (LowerBound a)
forall a. NFData a => LowerBound a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => LowerBound a -> ()
rnf :: LowerBound a -> ()
NFData)

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 => LowerBound a -> Extended a
-- already inclusive
inclusiveLowerBound :: forall a. Enum 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. 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

instance Functor LowerBound where
  fmap :: forall a b. (a -> b) -> LowerBound a -> LowerBound b
fmap a -> b
f (LowerBound Extended a
e Closure
c) = Extended b -> Closure -> LowerBound b
forall a. Extended a -> Closure -> LowerBound a
LowerBound (a -> b
f (a -> b) -> Extended a -> Extended b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Extended a
e) Closure
c

instance Pretty 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 a ann. Pretty a => a -> Doc ann
forall ann. Extended 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 a ann. Pretty a => a -> Doc ann
forall ann. Extended a -> Doc ann
pretty Extended a
a

instance Eq a => Eq (Extended a) where
    {-# INLINABLE (==) #-}
    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 => 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 => Ord (Extended a) where
    {-# INLINABLE 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 => 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) => Eq (UpperBound a) where
    {-# INLINABLE (==) #-}
    UpperBound a
b1 == :: UpperBound a -> UpperBound a -> Closure
== UpperBound a
b2 = UpperBound a -> Extended a
forall a. Enum 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 => UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b2

instance (Enum a, Eq 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) => Ord (UpperBound a) where
    {-# INLINABLE compare #-}
    UpperBound a
b1 compare :: UpperBound a -> UpperBound a -> Ordering
`compare` UpperBound a
b2 = UpperBound a -> Extended a
forall a. Enum 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 => UpperBound a -> Extended a
inclusiveUpperBound UpperBound a
b2

instance (Enum a, Ord 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) => Eq (LowerBound a) where
    {-# INLINABLE (==) #-}
    LowerBound a
b1 == :: LowerBound a -> LowerBound a -> Closure
== LowerBound a
b2 = LowerBound a -> Extended a
forall a. Enum 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 => LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b2

instance (Enum a, Eq 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) => Ord (LowerBound a) where
    {-# INLINABLE compare #-}
    LowerBound a
b1 compare :: LowerBound a -> LowerBound a -> Ordering
`compare` LowerBound a
b2 = LowerBound a -> Extended a
forall a. Enum 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 => LowerBound a -> Extended a
inclusiveLowerBound LowerBound a
b2

instance (Enum a, Ord 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 :: a -> UpperBound a
strictUpperBound :: forall a. a -> UpperBound a
strictUpperBound a
a = Extended a -> Closure -> UpperBound a
forall a. Extended a -> Closure -> UpperBound a
UpperBound (a -> Extended a
forall a. a -> Extended a
Finite a
a) Closure
False
{-# INLINABLE strictUpperBound #-}

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

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

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

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

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

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

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

-- See Note [Enumerable Intervals]
instance (Enum a, Ord a) => Eq (Interval a) where
    {-# INLINABLE (==) #-}
    -- 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) => Interval a -> Closure
isEmpty Interval a
iv1 Closure -> Closure -> Closure
&& Interval a -> Closure
forall a. (Enum a, Ord 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) => Haskell.Eq (Interval a) where
    {-# INLINABLE (==) #-}
    == :: 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 :: a -> a -> Interval a
interval :: forall a. a -> a -> Interval a
interval a
s a
s' = LowerBound a -> UpperBound a -> Interval a
forall a. LowerBound a -> UpperBound a -> Interval a
Interval (a -> LowerBound a
forall a. a -> LowerBound a
lowerBound a
s) (a -> UpperBound a
forall a. a -> UpperBound a
upperBound a
s')
{-# INLINABLE 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 :: a -> Interval a
singleton :: forall a. a -> Interval a
singleton a
s = a -> a -> Interval a
forall a. a -> a -> Interval a
interval a
s a
s
{-# INLINABLE singleton #-}

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

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

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

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

-- | Check whether a value is in an interval.
member :: (Enum a, Ord a) => a -> Interval a -> Bool
member :: forall a. (Enum a, Ord 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) => Interval a -> Interval a -> Closure
`contains` a -> Interval a
forall a. a -> Interval a
singleton a
a
{-# INLINABLE 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) => Interval a -> Interval a -> Bool
overlaps :: forall a. (Enum a, Ord 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) => Interval a -> Closure
isEmpty (Interval a
l Interval a -> Interval a -> Interval a
forall a. (Enum a, Ord a) => Interval a -> Interval a -> Interval a
`intersection` Interval a
r)
{-# INLINABLE overlaps #-}

-- | 'intersection a b' is the largest interval that is contained in 'a' and in
--   'b', if it exists.
intersection :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a
intersection :: forall a. (Enum a, Ord 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. 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)
{-# INLINABLE intersection #-}

-- | 'hull a b' is the smallest interval containing 'a' and 'b'.
hull :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a
hull :: forall a. (Enum a, Ord 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. 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)
{-# INLINABLE 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) => Interval a -> Interval a -> Bool
-- Everything contains the empty interval
contains :: forall a. (Enum a, Ord a) => Interval a -> Interval a -> Closure
contains Interval a
_ Interval a
i2 | Interval a -> Closure
forall a. (Enum a, Ord 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) => 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
{-# INLINABLE contains #-}

{- | Check if an 'Interval' is empty. -}
isEmpty :: (Enum a, Ord a) => Interval a -> Bool
isEmpty :: forall a. (Enum a, Ord a) => Interval a -> Closure
isEmpty (Interval LowerBound a
lb UpperBound a
ub) = case LowerBound a -> Extended a
forall a. Enum 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 => 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
{-# INLINABLE isEmpty #-}

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

-- | Check if a value is later than the end of an 'Interval'.
after :: (Enum a , Ord a) => a -> Interval a -> Bool
after :: forall a. (Enum a, Ord a) => a -> Interval a -> Closure
after a
h (Interval LowerBound a
_ UpperBound a
t) = a -> UpperBound a
forall a. a -> UpperBound a
upperBound a
h UpperBound a -> UpperBound a -> Closure
forall a. Ord a => a -> a -> Closure
> UpperBound a
t
{-# INLINABLE 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 --------------------------------------------------------------------------------------

$(makeIsDataSchemaIndexed ''Extended [('NegInf, 0), ('Finite, 1), ('PosInf, 2)])
$(makeIsDataIndexed ''UpperBound [('UpperBound, 0)])
$(makeIsDataIndexed ''LowerBound [('LowerBound, 0)])
$(makeIsDataIndexed ''Interval [('Interval, 0)])

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