-- SPDX-FileCopyrightText: 2023 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE FunctionalDependencies, RoleAnnotations #-}

-- | Range type
module Lorentz.Range
  ( RangeBoundaryInclusion(..)
  , Range(..)
  , RangeIE(..)
  , RangeEI(..)
  , RangeEE(..)
  , OnRangeAssertFailure(..)
  , RangeFailureInfo(..)
  , RangeBoundary
  , NiceRange
  , CanCheckEmpty
  , mkRange
  , mkRange_
  , mkRangeFor
  , mkRangeFor_
  , mkRangeForSafe_
  , fromRange_
  , toRange_
  , rangeLower
  , rangeUpper
  , rangeLower_
  , rangeUpper_
  , inRange
  , inRange_
  , inRangeCmp
  , inRangeCmp_
  , assertInRange_
  , assertInRangeSimple_
  , isRangeEmpty
  , isRangeEmpty_
  , assertRangeNonEmpty_
  , mkOnRangeAssertFailureSimple
  , customErrorORAF
  , customErrorORAFSimple
  -- * Internals
  , isInclusive
  ) where

import Data.Coerce (coerce)
import Data.Constraint (Bottom(..))
import Data.Singletons (demote)
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Lorentz.ADT as L
import Lorentz.Annotation as L
import Lorentz.Arith as L
import Lorentz.Base as L
import Lorentz.Coercions as L
import Lorentz.Constraints.Scopes as L
import Lorentz.Doc as L
import Lorentz.Errors as L
import Lorentz.Instr as L
import Lorentz.Macro as L
import Lorentz.Value
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped (noAnn, pattern UnsafeAnnotation, typeAnnQ, unAnnotation)
import Morley.Util.Interpolate (i)
import Morley.Util.Named

{- $setup
>>> import Fmt (pretty)
>>> import Lorentz
>>> import Morley.Util.Named
-}

-- | Whether to include boundary in 'Range'
data RangeBoundaryInclusion = IncludeBoundary | ExcludeBoundary

-- | Helper class for 'RangeBoundaryInclusion'.
type RangeBoundary :: RangeBoundaryInclusion -> Constraint
class (DefaultToInclusive r, Typeable r) => RangeBoundary r where
  -- | Parentheses for the 'Buildable' instance
  rangeParens :: (Text, Text)
  -- | Haskell comparison which either includes or excludes the boundary
  inRangeComp :: Ord a => a -> a -> Bool
  -- | Lorentz comparison which either includes or excludes the boundary
  inRangeComp_ :: NiceComparable a => a : a : s :-> Bool : s
  -- | Human-readable name for the tag
  rangeName :: Text
  -- | Value-level representation as 'Bool'
  isInclusive :: Bool

instance RangeBoundary 'IncludeBoundary where
  rangeParens = ("[", "]")
  inRangeComp = (<=)
  inRangeComp_ = L.ge
  rangeName = "Inclusive"
  isInclusive = True

instance RangeBoundary 'ExcludeBoundary where
  rangeParens = ("(", ")")
  inRangeComp = (<)
  inRangeComp_ = L.gt
  rangeName = "Exclusive"
  isInclusive = False

-- | Hacky typeclass to default boundaries to 'IncludeBoundary'.
class DefaultToInclusive bound
instance DefaultToInclusive 'IncludeBoundary
instance DefaultToInclusive 'ExcludeBoundary
instance {-# incoherent #-} a ~ 'IncludeBoundary => DefaultToInclusive a

{- | The main range type. This exists as a base for other (new)types like
'Range', 'RangeEE', etc.

The zoo of 'Range' types exists mostly for the purpose of making errors less
scary:

>>> f = push (1 :: Integer, 2 :: Natural) # unpair # inRange_
...
... error:
... Couldn't match type ‘Range Natural’ with ‘Integer’
...

>>> mkRange_ @_ @_ @_ @Integer # add -$ #min :! 123 ::: #max :! 321 ::: 555
...
... error:
... No instance for (ArithOpHs
...   Morley.Michelson.Typed.Arith.Add (Range Integer) Integer ())
...
-}
type Range' :: RangeBoundaryInclusion -> RangeBoundaryInclusion -> Type -> Type
data Range' lower upper a = Range' { rangeLower' :: a, rangeUpper' :: a }
  deriving stock (Generic, Show, Eq)
  deriving anyclass IsoValue
type role Range' nominal nominal _

instance (HasAnnotation a, RangeBoundary lower, RangeBoundary upper)
  => HasAnnotation (Range' lower upper a) where
  getAnnotation f =
    let aann = getAnnotation @a f
        e :: forall x. RangeBoundary x => Text
        e | isInclusive @x = "i"
          | otherwise = "e"
        lann = UnsafeAnnotation $ "l_" <> e @lower
        uann = UnsafeAnnotation $ "u_" <> e @upper
    in T.NTPair [typeAnnQ|range|] lann uann noAnn noAnn aann aann

-- | Default range, inclusive in both boundaries.
newtype Range a = MkRangeII (Range' 'IncludeBoundary 'IncludeBoundary a)
  deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq)
  deriving anyclass IsoValue

-- | Range exclusive in both boundaries.
newtype RangeEE a = MkRangeEE (Range' 'ExcludeBoundary 'ExcludeBoundary a)
  deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq)
  deriving anyclass IsoValue

-- | Range inclusive in lower boundary, but exclusive in upper boundary.
newtype RangeIE a = MkRangeIE (Range' 'IncludeBoundary 'ExcludeBoundary a)
  deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq)
  deriving anyclass IsoValue

-- | Range exclusive in lower boundary, but inclusive in upper boundary.
newtype RangeEI a = MkRangeEI (Range' 'ExcludeBoundary 'IncludeBoundary a)
  deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq)
  deriving anyclass IsoValue

-- We have to export data constructors because otherwise Coercible complains in
-- some contexts, but those are not intended to be used by the end-users.
{-# WARNING MkRangeII, MkRangeEE, MkRangeEI, MkRangeIE
  "Avoid using data constructors directly, use mkRange instead."
  #-}

instance (TypeHasDoc a, RangeBoundary lower, RangeBoundary upper)
  => TypeHasDoc (Range' lower upper a) where
  typeDocName _ = case (isInclusive @lower, isInclusive @upper) of
    (True, True) -> "Range"
    (True, False) -> "RangeIE"
    (False, True) -> "RangeEI"
    (False, False) -> "RangeEE"
  typeDocMdDescription =
    "Signifies a range, which is " <> build (rangeName @lower) <> " wrt its lower boundary and "
    <> build (rangeName @upper) <> " wrt its upper boundary."
  typeDocMdReference pa =
    customTypeDocMdReference
      (typeDocName pa, DType pa) [DType (Proxy @a)]
  typeDocHaskellRep pa _ = Just $
    ( Just $ fromString . toString $ typeDocName pa <> " Integer"
    , [T.ConstructorRep (typeDocName pa) Nothing fields]
    )
    where
      fields = case getAnnotation @(Range' lower upper Integer) NotFollowEntrypoint of
        T.NTPair _ lower upper _ _ _ _ ->
          [ T.FieldRep (Just $ unAnnotation lower) (Just "Lower boundary") intRef
          , T.FieldRep (Just $ unAnnotation upper) (Just "Upper boundary") intRef
          ]
      intRef = SomeTypeWithDoc $ Proxy @Integer
  typeDocMichelsonRep pa =
    ( Just $ fromString . toString $ typeDocName pa <> " Integer"
    , demote @(ToT (Range' lower upper Integer))
    )

{- | Pretty-printer for Range.

>>> pretty $ mkRange 123 456
[123, 456]

>>> pretty $ mkRange @RangeEE 123 456
(123, 456)

>>> pretty $ mkRange @RangeIE 123 456
[123, 456)

>>> pretty $ mkRange @_ @'IncludeBoundary @'ExcludeBoundary 123 456
[123, 456)
-}
instance (RangeBoundary lower, RangeBoundary upper, Buildable a)
  => Buildable (Range' lower upper a) where
  build (Range' l r) = [i|#{lpar}#{l}, #{r}#{rpar}|]
    where lpar = fst $ rangeParens @lower
          rpar = snd $ rangeParens @upper

-- | Helper class for the 'Range' types that encapsulates common features.
class (RangeBoundary lower, RangeBoundary upper, ToT (range a) ~ ToT (a, a), KnownValue (range a)
  , Coercible range (Range' lower upper))
  => NiceRange range lower upper a | range -> lower upper, lower upper -> range

instance KnownValue a => NiceRange Range 'IncludeBoundary 'IncludeBoundary a
instance KnownValue a => NiceRange RangeIE 'IncludeBoundary 'ExcludeBoundary a
instance KnownValue a => NiceRange RangeEI 'ExcludeBoundary 'IncludeBoundary a
instance KnownValue a => NiceRange RangeEE 'ExcludeBoundary 'ExcludeBoundary a

-- | Get a range's lower bound
rangeLower :: forall range lower upper a. NiceRange range lower upper a => range a -> a
rangeLower = coerce $ rangeLower' @lower @upper @a

-- | Get a range's upper bound.
rangeUpper :: forall range lower upper a. NiceRange range lower upper a => range a -> a
rangeUpper = coerce $ rangeUpper' @lower @upper @a

{- | Construct a 'Range'. Bear in mind, no checks are performed, so this can
construct empty ranges.

You can control whether boundaries are included or excluded by choosing the
appropriate type out of 'Range', 'RangeIE', 'RangeEI' and 'RangeEE', either via
a type application or a type annotation. Alternatively, you can set @lower@ and
@upper@ type arguments to 'IncludeBoundary' or 'ExcludeBoundary'. If
unspecified, the default is to include both boundaries.

>>> pretty $ mkRange 123 456
[123, 456]

>>> pretty $ mkRange 123 123
[123, 123]

>>> pretty $ mkRange 123 0 -- note this range is empty!
[123, 0]

>>> pretty (mkRange 123 456 :: RangeEE Integer)
(123, 456)

>>> pretty $ mkRange @RangeIE 123 456
[123, 456)

>>> pretty $ mkRange @_ @'IncludeBoundary @'ExcludeBoundary 123 456
[123, 456)

>>> pretty $ mkRange @RangeEI 123 456
(123, 456]

>>> pretty $ mkRange @_ @'ExcludeBoundary @'IncludeBoundary 123 456
(123, 456]
-}
mkRange :: forall range lower upper a. NiceRange range lower upper a => a -> a -> range a
mkRange = coerce $ Range' @lower @upper @a

{- | Convert a 'Range' to a pair of @(lower, upper)@

>>> mkRangeForSafe_ # fromRange_ -$ #start :! (123 :: Integer) ::: #length :! (456 :: Natural)
(123,579)
-}
fromRange_ :: NiceRange range lower upper a => range a : s :-> (a, a) : s
fromRange_ = forcedCoerce_

{- | Convert a pair of @(lower, upper)@ to 'Range'. This has the potential to
construct an empty range.

>>> pretty (toRange_ -$ (123, 456) :: Range Integer)
[123, 456]

>>> pretty (toRange_ -$ (123, -100500) :: Range Integer) -- empty range
[123, -100500]
-}
toRange_ :: NiceRange range lower upper a => (a, a) : s :-> range a : s
toRange_ = forcedCoerce_

{- | Get the lower bound of a 'Range'

>>> mkRange_ # rangeLower_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer)
123
-}
rangeLower_ :: NiceRange range lower upper a => range a : s :-> a : s
rangeLower_ = fromRange_ # car

{- | Get the upper bound of a 'Range'

>>> mkRange_ # rangeUpper_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer)
456
-}
rangeUpper_ :: NiceRange range lower upper a => range a : s :-> a : s
rangeUpper_ = fromRange_ # cdr

{- | Construct a range by specifying the start and length instead of lower and
upper bounds. @lower = start@, and @upper = start + length@.

Note this can still construct empty ranges if @length@ is negative.

See 'mkRange' for the information on how to control boundary inclusion.

>>> pretty $ mkRangeFor 123 123
[123, 246]

>>> pretty $ mkRangeFor 123 (-123) -- empty range
[123, 0]
-}
mkRangeFor :: (NiceRange range lower upper a, Num a) => a -> a -> range a
mkRangeFor start len = mkRange start (start + len)

{- | The Lorentz version of 'mkRange'

>>> pretty $ mkRange_ -$ (#min :! (123 :: Integer)) ::: (#max :! (123 :: Integer))
[123, 123]

>>> pretty $ mkRange_ @RangeEE -$ (#min :! (123 :: Integer)) ::: (#max :! (123 :: Integer))
(123, 123)

Notice the latter range is empty by construction.
-}
mkRange_
  :: NiceRange range lower upper a
  => ("min" :! a) : ("max" :! a) : s :-> range a : s
mkRange_ = fromNamed #min # dip (fromNamed #max) # L.pair # toRange_

{- | The Lorentz version of 'mkRangeFor'. Note that @length@ can be of different
type from @start@.

>>> pretty $ mkRangeFor_ -$ (#start :! (123 :: Integer)) ::: (#length :! (123 :: Natural))
[123, 246]
-}
mkRangeFor_
  :: ( NiceRange range lower upper a
     , Dupable a
     , ArithOpHs T.Add a b a
     )
  => ("start" :! a) : ("length" :! b) : s :-> range a : s
mkRangeFor_
  = fromNamed #start
  # L.dup
  # L.dip
    ( L.dip (fromNamed #length)
    # L.add
    )
  # L.pair
  # toRange_

{- | A version of 'mkRangeFor_' that requires @length@ to be isomorphic to a
@nat@ and the range to be inclusive in both bounds. This guarantees that the
range is non-empty.

>>> pretty $ mkRangeForSafe_ -$ (#start :! (123 :: Integer)) ::: (#length :! (1 :: Natural))
[123, 124]
-}
mkRangeForSafe_
  :: forall a b s.
     ( Dupable a
     , ArithOpHs T.Add a b a
     , ToT b ~ 'T.TNat
     )
  => ("start" :! a) : ("length" :! b) : s :-> Range a : s
mkRangeForSafe_ = mkRangeFor_
  where
    _ = T.Dict @(ToT b ~ 'T.TNat)

{- | Check if a value is in range.

>>> let range = mkRange -2 2
>>> inRange range <$> [-4..4]
[False,False,True,True,True,True,True,False,False]
-}
inRange :: (NiceRange range lower upper a, Ord a) => range a -> a -> Bool
inRange = (== EQ) ... inRangeCmp

{- | Check if a value is in range, and return 'Ordering'. This function returns
'EQ' if the value is in range, 'LT' if it underflows, and 'GT if it overflows.

>>> inRangeCmp (mkRange -2 2) <$> [-4..4]
[LT,LT,EQ,EQ,EQ,EQ,EQ,GT,GT]

>>> inRangeCmp (mkRange @RangeIE -2 2) <$> [-4..4]
[LT,LT,EQ,EQ,EQ,EQ,GT,GT,GT]
-}
inRangeCmp
  :: forall range lower upper a. (NiceRange range lower upper a, Ord a)
  => range a -> a -> Ordering
inRangeCmp r x
  | Prelude.not $ inRangeComp @lower (rangeLower r) x = LT
  | Prelude.not $ inRangeComp @upper x (rangeUpper r) = GT
  | otherwise = EQ

{- | Lorentz version of 'inRange'.

>>> range = mkRange 0 10 :: RangeEE Integer
>>> testCode = push range # inRange_
>>> testCode -$ 123
False
>>> testCode -$ 10
False
>>> testCode -$ 0
False
>>> testCode -$ -123
False
>>> testCode -$ 1
True
>>> testCode -$ 5
True
-}
inRange_
  :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a)
  => range a : a : s :-> Bool : s
inRange_
  = fromRange_
  # L.unpair
  # L.dupN @3
  # inRangeComp_ @lower
  # L.dug @2
  # inRangeComp_ @upper
  # L.and

{- | Lorentz version of 'inRangeCmp'. Instead of 'Ordering', returns an
'Integer', @-1@ if the value underflows, @0@ if it's in range and @1@ if it
overflows.

Use 'inRange_' if you don't particularly care whether the range is under- or
overflowed.

>>> range = mkRange 0 10 :: Range Integer
>>> testCode = push range # inRangeCmp_
>>> testCode -$ 123
1
>>> testCode -$ -123
-1
>>> testCode -$ 5
0

>>> push (mkRange 0 10 :: RangeIE Integer) # inRangeCmp_ -$ 0
0
>>> push (mkRange 0 10 :: RangeIE Integer) # inRangeCmp_ -$ 10
1

>>> push (mkRange 0 10 :: RangeEI Integer) # inRangeCmp_ -$ 0
-1
>>> push (mkRange 0 10 :: RangeEI Integer) # inRangeCmp_ -$ 10
0

>>> push (mkRange 0 10 :: RangeEE Integer) # inRangeCmp_ -$ 0
-1
>>> push (mkRange 0 10 :: RangeEE Integer) # inRangeCmp_ -$ 10
1

When lower and upper boundaries are the same and at least one boundary is
exclusive, it is ambiguous whether the value on the boundary overflows or
underflows. In this case, lower boundary takes precedence if it's exclusive.

>>> push (mkRange 0 0 :: RangeIE Integer) # inRangeCmp_ -$ 0
1

>>> push (mkRange 0 0 :: RangeEI Integer) # inRangeCmp_ -$ 0
-1

>>> push (mkRange 0 0 :: RangeEE Integer) # inRangeCmp_ -$ 0
-1
-}
inRangeCmp_
  :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a)
  => range a : a : s :-> Integer : s
inRangeCmp_
  = fromRange_
  # L.unpair
  # L.dupN @3
  # inRangeComp_ @lower
  # flip if_ (L.dropN @2 # push (-1))
      (inRangeComp_ @upper
      # if_ (push 0) (push 1)
      )

{- | Assert a value is in range; throw errors if it's under- or overflowing. See
'OnRangeAssertFailure' for information on how to specify errors.

If you don't need verbose error reporting, consider using
'assertInRangeSimple_'.
-}
assertInRange_
  :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a)
  => OnRangeAssertFailure a
  -> range a : a : s :-> s
assertInRange_ OnRangeAssertFailure{..}
  = dip (toNamed #value)
  # L.dupN @2
  # L.dupN @2
  # fromRange_
  # L.unpair
  # L.dupN @3
  # fromNamed #value
  # inRangeComp_ @lower
  # if_
      ( dip (fromNamed #value)
      # inRangeComp_ @upper
      # if_ (L.dropN @2)
          ( rangeUpper_ # toNamed #boundary
          # push (isInclusive @upper)
          # mkRangeFailureInfo
          # orafOverflow
          )
      )
      ( L.dropN @2
      # rangeLower_ # toNamed #boundary
      # push (isInclusive @lower)
      # mkRangeFailureInfo
      # orafUnderflow
      )

{- | A cheaper version of 'assertInRange_' without fancy error reporting.

>>> let range = mkRange 123 456 :: Range Integer
>>> let err = failUsing [mt|failure|]
>>> assertInRangeSimple_ err -$ range ::: 123 ::: ()
()
>>> assertInRangeSimple_ err -$ range ::: 1 ::: ()
*** Exception: Reached FAILWITH instruction with '"failure"' ...
...
-}
assertInRangeSimple_
  :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a)
  => (forall s' any. s' :-> any)
  -> range a : a : s :-> s
assertInRangeSimple_ err
  = inRange_ # if_ nop err

-- | Small helper to construct 'RangeFailureInfo' in Lorentz code.
mkRangeFailureInfo
  :: forall a s. IsoValue a
  => Bool : "boundary" :! a : "value" :! a : s :-> RangeFailureInfo a : s
mkRangeFailureInfo = coerce $ constructStack @(RangeFailureInfo a) @_ @s

-- | Information about the range check failure
data RangeFailureInfo a = RangeFailureInfo
  { rfiInclusive :: Bool -- ^ Whether the boundary is inclusive or not
  , rfiBoundary :: a     -- ^ The boundary that failed to check
  , rfiValue :: a        -- ^ The value that failed to check
  } deriving stock Generic
    deriving anyclass IsoValue
    deriving TypeHasFieldNamingStrategy via T.FieldCamelCase

instance TypeHasDoc a => TypeHasDoc (RangeFailureInfo a) where
  type TypeDocFieldDescriptions (RangeFailureInfo a) =
    '[ '( "RangeFailureInfo", '( 'Nothing,
            '[ '("rfiInclusive", "Whether the boundary is inclusive or not")
            ,  '("rfiBoundary", "The boundary that failed to check")
            ,  '("rfiValue", "The value that failed to check")
            ])
        )
     ]
  typeDocMdDescription = "Information about the range check failure"
  typeDocMdReference = poly1TypeDocMdReference
  typeDocHaskellRep
    = T.haskellRepMap (typeFieldNamingStrategy @(RangeFailureInfo a))
    $ concreteTypeDocHaskellRep @(RangeFailureInfo Integer)
  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(RangeFailureInfo Integer)

{- | Specify on how to fail on range overflow or underflow in 'assertInRange_'.

This expects two always-failing Lorentz functions, one will be called on
underflow, another on overflow.

See 'customErrorORAF' for a simpler helper to use with custom Lorentz errors.

See 'mkOnRangeAssertFailureSimple' if you don't care about distinguishing
underflow and overflow.
-}
data OnRangeAssertFailure a = OnRangeAssertFailure
  { orafUnderflow :: forall s any. RangeFailureInfo a : s :-> any
  , orafOverflow :: forall s any. RangeFailureInfo a : s :-> any
  }

-- | Construct 'OnRangeAssertFailure' that performs the same action on both
-- overflow and underflow
mkOnRangeAssertFailureSimple
  :: (forall s any. RangeFailureInfo a : s :-> any)
  -> OnRangeAssertFailure a
mkOnRangeAssertFailureSimple f = OnRangeAssertFailure f f

{- | Construct 'OnRangeAssertFailure' that throws custom errors. Errors used
must be defined somewhere using @errorDocArg@ or equivalent, and must accept
'RangeFailureInfo' as the argument.

>>> :{
type RFII = RangeFailureInfo Integer
--
[errorDocArg| "overflowInt" exception "Integer range overflow" RFII |]
[errorDocArg| "underflowInt" exception "Integer range underflow" RFII |]
--
testCode :: Range Integer : Integer : s :-> s
testCode = assertInRange_ $ customErrorORAF ! #underflow #underflowInt ! #overflow #overflowInt
:}

>>> testCode -$ mkRange 0 10 ::: 123 ::: ()
*** Exception: Reached FAILWITH instruction with 'Pair "OverflowInt" (Pair True (Pair 10 123))'
...
>>> testCode -$ mkRange 0 10 ::: -1 ::: ()
*** Exception: Reached FAILWITH instruction with 'Pair "UnderflowInt" (Pair True (Pair 0 -1))'
...
>>> testCode -$ mkRange 0 10 ::: 5 ::: ()
()

-}
customErrorORAF
  :: (NiceConstant a
    , ErrorArg underflow ~ RangeFailureInfo a
    , ErrorArg overflow ~ RangeFailureInfo a
    , CustomErrorHasDoc underflow
    , CustomErrorHasDoc overflow
    )
  => ("underflow" :! Label underflow)
  -> ("overflow" :! Label overflow)
  -> OnRangeAssertFailure a
customErrorORAF (arg #underflow -> ufl) (arg #overflow -> ofl) = OnRangeAssertFailure
  { orafUnderflow = failCustom ufl
  , orafOverflow = failCustom ofl
  }

{- | A version of 'customErrorORAF' that uses the same error for both underflow
and overflow.

>>> :{
type RFII = RangeFailureInfo Integer
[errorDocArg| "rangeError" exception "Integer range check error" RFII |]
--
testCode :: Range Integer : Integer : s :-> s
testCode = assertInRange_ $ customErrorORAFSimple #rangeError
:}

>>> testCode -$ mkRange 0 10 ::: 123 ::: ()
*** Exception: Reached FAILWITH instruction with 'Pair "RangeError" (Pair True (Pair 10 123))'
...
>>> testCode -$ mkRange 0 10 ::: -1 ::: ()
*** Exception: Reached FAILWITH instruction with 'Pair "RangeError" (Pair True (Pair 0 -1))' ...
...
>>> testCode -$ mkRange 0 10 ::: 5 ::: ()
()
-}
customErrorORAFSimple
  :: (NiceConstant a
    , ErrorArg err ~ RangeFailureInfo a
    , CustomErrorHasDoc err
    )
  => Label err
  -> OnRangeAssertFailure a
customErrorORAFSimple err = mkOnRangeAssertFailureSimple $ failCustom err

{- | Check if a range is empty by construction. Note, however, this function is
not suitable for checking whether a range with both boundaries excluded is
empty, and hence will produce a type error when such a check is attempted.

>>> isRangeEmpty $ mkRange 0 1
False
>>> isRangeEmpty $ mkRange 0 0
False
>>> isRangeEmpty $ mkRange 0 -1
True

>>> isRangeEmpty $ mkRange @RangeIE 0 1
False
>>> isRangeEmpty $ mkRange @RangeIE 0 0
True
>>> isRangeEmpty $ mkRange @RangeIE 0 -1
True

>>> isRangeEmpty $ mkRange @RangeEI 0 1
False
>>> isRangeEmpty $ mkRange @RangeEI 0 0
True
>>> isRangeEmpty $ mkRange @RangeEI 0 -1
True

>>> isRangeEmpty $ mkRange @RangeEE 0 1
...
... error:
... This function can't be used to check whenter a range with both boundaries excluded is empty
...
-}
isRangeEmpty
  :: forall range lower upper a.
    (NiceRange range lower upper a, Ord a, CanCheckEmpty lower upper)
  => range a -> Bool
isRangeEmpty r = checkEmpty @lower @upper (rangeLower r) (rangeUpper r)

{- | Lorentz version of 'isRangeEmpty'. Same caveats apply.

>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1)
False
>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0)
False
>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1)
True

>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1)
False
>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0)
True
>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1)
True

>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1)
False
>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0)
True
>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1)
True

>>> mkRange_ @RangeEE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1)
...
... error:
... This function can't be used to check whenter a range with both boundaries excluded is empty
...
-}
isRangeEmpty_
  :: forall range lower upper a s.
    ( NiceRange range lower upper a
    , CanCheckEmpty lower upper
    , NiceComparable a
    )
  => range a : s :-> Bool : s
isRangeEmpty_
  = fromRange_
  # L.unpair
  # checkEmpty_ @lower @upper

-- | Helper class to check if a range is empty. Gives up when both boundaries
-- are exclusive.
class CanCheckEmpty l u where
  -- | Returns 'True' when a range is empty, 'False' otherwise.
  checkEmpty :: Ord a => a -> a -> Bool
  -- | Lorentz version of 'checkEmpty'.
  checkEmpty_ :: NiceComparable a => a : a : s :-> Bool : s
instance CanCheckEmpty 'IncludeBoundary 'IncludeBoundary where
  checkEmpty = (>)
  checkEmpty_ = L.gt
instance CanCheckEmpty 'IncludeBoundary 'ExcludeBoundary where
  checkEmpty = (>=)
  checkEmpty_ = L.ge
instance CanCheckEmpty 'ExcludeBoundary 'IncludeBoundary where
  checkEmpty = (>=)
  checkEmpty_ = L.ge
instance (Bottom, TypeError
  ('Text "This function can't be used to check whenter a \
    \range with both boundaries excluded is empty")) =>
  CanCheckEmpty 'ExcludeBoundary 'ExcludeBoundary where
  checkEmpty = no
  checkEmpty_ = no

{- | Assert a range is non-empty, run a failing function passed as the first
argument if it is. Note, however, this function is not suitable for checking
whether a range with both boundaries excluded is empty, and hence will produce a
type error when such a check is attempted.

>>> let err = push [mt|empty range|] # pair # failWith @(MText, Range Integer)
>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 1)
[0, 1]

>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 0)
[0, 0]

>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! -1)
*** Exception: Reached FAILWITH instruction with 'Pair "empty range" (Pair 0 -1)' ...
...

>>> mkRange_ @RangeEE # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 1)
...
... error:
... This function can't be used to check whenter a range with both boundaries excluded is empty
...
-}
assertRangeNonEmpty_
  :: ( NiceRange range lower upper a
     , CanCheckEmpty lower upper
     , NiceComparable a
     , Dupable (range a)
     )
  => (forall s' any. range a : s' :-> any)
  -> range a : s :-> range a : s
assertRangeNonEmpty_ err = dup # isRangeEmpty_ # if_ err nop