-- 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 :: (Text, Text)
rangeParens = (Text
"[", Text
"]")
  inRangeComp :: forall a. Ord a => a -> a -> Bool
inRangeComp = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  inRangeComp_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
inRangeComp_ = (a : a : s) :-> (Bool : s)
forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
L.ge
  rangeName :: Text
rangeName = Text
"Inclusive"
  isInclusive :: Bool
isInclusive = Bool
True

instance RangeBoundary 'ExcludeBoundary where
  rangeParens :: (Text, Text)
rangeParens = (Text
"(", Text
")")
  inRangeComp :: forall a. Ord a => a -> a -> Bool
inRangeComp = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  inRangeComp_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
inRangeComp_ = (a : a : s) :-> (Bool : s)
forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
L.gt
  rangeName :: Text
rangeName = Text
"Exclusive"
  isInclusive :: Bool
isInclusive = Bool
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' { forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Range' lower upper a -> a
rangeLower' :: a, forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Range' lower upper a -> a
rangeUpper' :: a }
  deriving stock ((forall x. Range' lower upper a -> Rep (Range' lower upper a) x)
-> (forall x. Rep (Range' lower upper a) x -> Range' lower upper a)
-> Generic (Range' lower upper a)
forall x. Rep (Range' lower upper a) x -> Range' lower upper a
forall x. Range' lower upper a -> Rep (Range' lower upper a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a x.
Rep (Range' lower upper a) x -> Range' lower upper a
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a x.
Range' lower upper a -> Rep (Range' lower upper a) x
$cfrom :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a x.
Range' lower upper a -> Rep (Range' lower upper a) x
from :: forall x. Range' lower upper a -> Rep (Range' lower upper a) x
$cto :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a x.
Rep (Range' lower upper a) x -> Range' lower upper a
to :: forall x. Rep (Range' lower upper a) x -> Range' lower upper a
Generic, Int -> Range' lower upper a -> ShowS
[Range' lower upper a] -> ShowS
Range' lower upper a -> String
(Int -> Range' lower upper a -> ShowS)
-> (Range' lower upper a -> String)
-> ([Range' lower upper a] -> ShowS)
-> Show (Range' lower upper a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
Int -> Range' lower upper a -> ShowS
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
[Range' lower upper a] -> ShowS
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
Range' lower upper a -> String
$cshowsPrec :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
Int -> Range' lower upper a -> ShowS
showsPrec :: Int -> Range' lower upper a -> ShowS
$cshow :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
Range' lower upper a -> String
show :: Range' lower upper a -> String
$cshowList :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Show a =>
[Range' lower upper a] -> ShowS
showList :: [Range' lower upper a] -> ShowS
Show, Range' lower upper a -> Range' lower upper a -> Bool
(Range' lower upper a -> Range' lower upper a -> Bool)
-> (Range' lower upper a -> Range' lower upper a -> Bool)
-> Eq (Range' lower upper a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Eq a =>
Range' lower upper a -> Range' lower upper a -> Bool
$c== :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Eq a =>
Range' lower upper a -> Range' lower upper a -> Bool
== :: Range' lower upper a -> Range' lower upper a -> Bool
$c/= :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Eq a =>
Range' lower upper a -> Range' lower upper a -> Bool
/= :: Range' lower upper a -> Range' lower upper a -> Bool
Eq)
  deriving anyclass WellTypedToT (Range' lower upper a)
WellTypedToT (Range' lower upper a)
-> (Range' lower upper a -> Value (ToT (Range' lower upper a)))
-> (Value (ToT (Range' lower upper a)) -> Range' lower upper a)
-> IsoValue (Range' lower upper a)
Value (ToT (Range' lower upper a)) -> Range' lower upper a
Range' lower upper a -> Value (ToT (Range' lower upper a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {lower :: RangeBoundaryInclusion}
       {upper :: RangeBoundaryInclusion} {a}.
IsoValue a =>
WellTypedToT (Range' lower upper a)
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
IsoValue a =>
Value (ToT (Range' lower upper a)) -> Range' lower upper a
forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
IsoValue a =>
Range' lower upper a -> Value (ToT (Range' lower upper a))
$ctoVal :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
IsoValue a =>
Range' lower upper a -> Value (ToT (Range' lower upper a))
toVal :: Range' lower upper a -> Value (ToT (Range' lower upper a))
$cfromVal :: forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
IsoValue a =>
Value (ToT (Range' lower upper a)) -> Range' lower upper a
fromVal :: Value (ToT (Range' lower upper a)) -> Range' lower upper a
IsoValue
type role Range' nominal nominal _

instance (HasAnnotation a, RangeBoundary lower, RangeBoundary upper)
  => HasAnnotation (Range' lower upper a) where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT (Range' lower upper a))
getAnnotation FollowEntrypointFlag
f =
    let aann :: Notes (ToT a)
aann = forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @a FollowEntrypointFlag
f
        e :: forall x. RangeBoundary x => Text
        e :: forall (x :: RangeBoundaryInclusion). RangeBoundary x => Text
e | forall (r :: RangeBoundaryInclusion). RangeBoundary r => Bool
isInclusive @x = Text
"i"
          | Bool
otherwise = Text
"e"
        lann :: Annotation FieldTag
lann = Text -> Annotation FieldTag
forall {k} (tag :: k). Text -> Annotation tag
UnsafeAnnotation (Text -> Annotation FieldTag) -> Text -> Annotation FieldTag
forall a b. (a -> b) -> a -> b
$ Text
"l_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> forall (x :: RangeBoundaryInclusion). RangeBoundary x => Text
e @lower
        uann :: Annotation FieldTag
uann = Text -> Annotation FieldTag
forall {k} (tag :: k). Text -> Annotation tag
UnsafeAnnotation (Text -> Annotation FieldTag) -> Text -> Annotation FieldTag
forall a b. (a -> b) -> a -> b
$ Text
"u_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> forall (x :: RangeBoundaryInclusion). RangeBoundary x => Text
e @upper
    in TypeAnn
-> Annotation FieldTag
-> Annotation FieldTag
-> VarAnn
-> VarAnn
-> Notes (ToT a)
-> Notes (ToT a)
-> Notes ('TPair (ToT a) (ToT a))
forall (p :: T) (q :: T).
TypeAnn
-> Annotation FieldTag
-> Annotation FieldTag
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
T.NTPair [typeAnnQ|range|] Annotation FieldTag
lann Annotation FieldTag
uann VarAnn
forall {k} (a :: k). Annotation a
noAnn VarAnn
forall {k} (a :: k). Annotation a
noAnn Notes (ToT a)
aann Notes (ToT a)
aann

-- | Default range, inclusive in both boundaries.
newtype Range a = MkRangeII (Range' 'IncludeBoundary 'IncludeBoundary a)
  deriving newtype (Typeable (Range a)
Markdown
SingI (TypeDocFieldDescriptions (Range a))
FieldDescriptionsValid
  (TypeDocFieldDescriptions (Range a)) (Range a)
Typeable (Range a)
-> SingI (TypeDocFieldDescriptions (Range a))
-> FieldDescriptionsValid
     (TypeDocFieldDescriptions (Range a)) (Range a)
-> (Proxy (Range a) -> Text)
-> Markdown
-> (Proxy (Range a) -> WithinParens -> Markdown)
-> (Proxy (Range a) -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep (Range a)
-> TypeDocMichelsonRep (Range a)
-> TypeHasDoc (Range a)
Proxy (Range a) -> [SomeDocDefinitionItem]
TypeDocMichelsonRep (Range a)
Proxy (Range a) -> Text
TypeDocHaskellRep (Range a)
Proxy (Range a) -> WithinParens -> Markdown
forall a.
Typeable a
-> SingI (TypeDocFieldDescriptions a)
-> FieldDescriptionsValid (TypeDocFieldDescriptions a) a
-> (Proxy a -> Text)
-> Markdown
-> (Proxy a -> WithinParens -> Markdown)
-> (Proxy a -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep a
-> TypeDocMichelsonRep a
-> TypeHasDoc a
forall {a}. TypeHasDoc a => Typeable (Range a)
forall a. TypeHasDoc a => Markdown
forall {a}.
TypeHasDoc a =>
SingI (TypeDocFieldDescriptions (Range a))
forall {a}.
TypeHasDoc a =>
FieldDescriptionsValid
  (TypeDocFieldDescriptions (Range a)) (Range a)
forall a.
TypeHasDoc a =>
Proxy (Range a) -> [SomeDocDefinitionItem]
forall a. TypeHasDoc a => TypeDocMichelsonRep (Range a)
forall a. TypeHasDoc a => Proxy (Range a) -> Text
forall a. TypeHasDoc a => TypeDocHaskellRep (Range a)
forall a.
TypeHasDoc a =>
Proxy (Range a) -> WithinParens -> Markdown
$ctypeDocName :: forall a. TypeHasDoc a => Proxy (Range a) -> Text
typeDocName :: Proxy (Range a) -> Text
$ctypeDocMdDescription :: forall a. TypeHasDoc a => Markdown
typeDocMdDescription :: Markdown
$ctypeDocMdReference :: forall a.
TypeHasDoc a =>
Proxy (Range a) -> WithinParens -> Markdown
typeDocMdReference :: Proxy (Range a) -> WithinParens -> Markdown
$ctypeDocDependencies :: forall a.
TypeHasDoc a =>
Proxy (Range a) -> [SomeDocDefinitionItem]
typeDocDependencies :: Proxy (Range a) -> [SomeDocDefinitionItem]
$ctypeDocHaskellRep :: forall a. TypeHasDoc a => TypeDocHaskellRep (Range a)
typeDocHaskellRep :: TypeDocHaskellRep (Range a)
$ctypeDocMichelsonRep :: forall a. TypeHasDoc a => TypeDocMichelsonRep (Range a)
typeDocMichelsonRep :: TypeDocMichelsonRep (Range a)
TypeHasDoc, (forall x. Range a -> Rep (Range a) x)
-> (forall x. Rep (Range a) x -> Range a) -> Generic (Range a)
forall x. Rep (Range a) x -> Range a
forall x. Range a -> Rep (Range a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Range a) x -> Range a
forall a x. Range a -> Rep (Range a) x
$cfrom :: forall a x. Range a -> Rep (Range a) x
from :: forall x. Range a -> Rep (Range a) x
$cto :: forall a x. Rep (Range a) x -> Range a
to :: forall x. Rep (Range a) x -> Range a
Generic, Int -> Range a -> ShowS
[Range a] -> ShowS
Range a -> String
(Int -> Range a -> ShowS)
-> (Range a -> String) -> ([Range a] -> ShowS) -> Show (Range a)
forall a. Show a => Int -> Range a -> ShowS
forall a. Show a => [Range a] -> ShowS
forall a. Show a => Range a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Range a -> ShowS
showsPrec :: Int -> Range a -> ShowS
$cshow :: forall a. Show a => Range a -> String
show :: Range a -> String
$cshowList :: forall a. Show a => [Range a] -> ShowS
showList :: [Range a] -> ShowS
Show, [Range a] -> Markdown
Range a -> Markdown
(Range a -> Markdown)
-> ([Range a] -> Markdown) -> Buildable (Range a)
forall a. Buildable a => [Range a] -> Markdown
forall a. Buildable a => Range a -> Markdown
forall a. (a -> Markdown) -> ([a] -> Markdown) -> Buildable a
$cbuild :: forall a. Buildable a => Range a -> Markdown
build :: Range a -> Markdown
$cbuildList :: forall a. Buildable a => [Range a] -> Markdown
buildList :: [Range a] -> Markdown
Buildable, Maybe AnnOptions
FollowEntrypointFlag -> Notes (ToT (Range a))
(FollowEntrypointFlag -> Notes (ToT (Range a)))
-> Maybe AnnOptions -> HasAnnotation (Range a)
forall a. HasAnnotation a => Maybe AnnOptions
forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (Range a))
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> Maybe AnnOptions -> HasAnnotation a
$cgetAnnotation :: forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (Range a))
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (Range a))
$cannOptions :: forall a. HasAnnotation a => Maybe AnnOptions
annOptions :: Maybe AnnOptions
HasAnnotation, Range a -> Range a -> Bool
(Range a -> Range a -> Bool)
-> (Range a -> Range a -> Bool) -> Eq (Range a)
forall a. Eq a => Range a -> Range a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Range a -> Range a -> Bool
== :: Range a -> Range a -> Bool
$c/= :: forall a. Eq a => Range a -> Range a -> Bool
/= :: Range a -> Range a -> Bool
Eq)
  deriving anyclass WellTypedToT (Range a)
WellTypedToT (Range a)
-> (Range a -> Value (ToT (Range a)))
-> (Value (ToT (Range a)) -> Range a)
-> IsoValue (Range a)
Value (ToT (Range a)) -> Range a
Range a -> Value (ToT (Range a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {a}. IsoValue a => WellTypedToT (Range a)
forall a. IsoValue a => Value (ToT (Range a)) -> Range a
forall a. IsoValue a => Range a -> Value (ToT (Range a))
$ctoVal :: forall a. IsoValue a => Range a -> Value (ToT (Range a))
toVal :: Range a -> Value (ToT (Range a))
$cfromVal :: forall a. IsoValue a => Value (ToT (Range a)) -> Range a
fromVal :: Value (ToT (Range a)) -> Range a
IsoValue

-- | Range exclusive in both boundaries.
newtype RangeEE a = MkRangeEE (Range' 'ExcludeBoundary 'ExcludeBoundary a)
  deriving newtype (Typeable (RangeEE a)
Markdown
SingI (TypeDocFieldDescriptions (RangeEE a))
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeEE a)) (RangeEE a)
Typeable (RangeEE a)
-> SingI (TypeDocFieldDescriptions (RangeEE a))
-> FieldDescriptionsValid
     (TypeDocFieldDescriptions (RangeEE a)) (RangeEE a)
-> (Proxy (RangeEE a) -> Text)
-> Markdown
-> (Proxy (RangeEE a) -> WithinParens -> Markdown)
-> (Proxy (RangeEE a) -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep (RangeEE a)
-> TypeDocMichelsonRep (RangeEE a)
-> TypeHasDoc (RangeEE a)
Proxy (RangeEE a) -> [SomeDocDefinitionItem]
TypeDocMichelsonRep (RangeEE a)
Proxy (RangeEE a) -> Text
TypeDocHaskellRep (RangeEE a)
Proxy (RangeEE a) -> WithinParens -> Markdown
forall a.
Typeable a
-> SingI (TypeDocFieldDescriptions a)
-> FieldDescriptionsValid (TypeDocFieldDescriptions a) a
-> (Proxy a -> Text)
-> Markdown
-> (Proxy a -> WithinParens -> Markdown)
-> (Proxy a -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep a
-> TypeDocMichelsonRep a
-> TypeHasDoc a
forall {a}. TypeHasDoc a => Typeable (RangeEE a)
forall a. TypeHasDoc a => Markdown
forall {a}.
TypeHasDoc a =>
SingI (TypeDocFieldDescriptions (RangeEE a))
forall {a}.
TypeHasDoc a =>
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeEE a)) (RangeEE a)
forall a.
TypeHasDoc a =>
Proxy (RangeEE a) -> [SomeDocDefinitionItem]
forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeEE a)
forall a. TypeHasDoc a => Proxy (RangeEE a) -> Text
forall a. TypeHasDoc a => TypeDocHaskellRep (RangeEE a)
forall a.
TypeHasDoc a =>
Proxy (RangeEE a) -> WithinParens -> Markdown
$ctypeDocName :: forall a. TypeHasDoc a => Proxy (RangeEE a) -> Text
typeDocName :: Proxy (RangeEE a) -> Text
$ctypeDocMdDescription :: forall a. TypeHasDoc a => Markdown
typeDocMdDescription :: Markdown
$ctypeDocMdReference :: forall a.
TypeHasDoc a =>
Proxy (RangeEE a) -> WithinParens -> Markdown
typeDocMdReference :: Proxy (RangeEE a) -> WithinParens -> Markdown
$ctypeDocDependencies :: forall a.
TypeHasDoc a =>
Proxy (RangeEE a) -> [SomeDocDefinitionItem]
typeDocDependencies :: Proxy (RangeEE a) -> [SomeDocDefinitionItem]
$ctypeDocHaskellRep :: forall a. TypeHasDoc a => TypeDocHaskellRep (RangeEE a)
typeDocHaskellRep :: TypeDocHaskellRep (RangeEE a)
$ctypeDocMichelsonRep :: forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeEE a)
typeDocMichelsonRep :: TypeDocMichelsonRep (RangeEE a)
TypeHasDoc, (forall x. RangeEE a -> Rep (RangeEE a) x)
-> (forall x. Rep (RangeEE a) x -> RangeEE a)
-> Generic (RangeEE a)
forall x. Rep (RangeEE a) x -> RangeEE a
forall x. RangeEE a -> Rep (RangeEE a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RangeEE a) x -> RangeEE a
forall a x. RangeEE a -> Rep (RangeEE a) x
$cfrom :: forall a x. RangeEE a -> Rep (RangeEE a) x
from :: forall x. RangeEE a -> Rep (RangeEE a) x
$cto :: forall a x. Rep (RangeEE a) x -> RangeEE a
to :: forall x. Rep (RangeEE a) x -> RangeEE a
Generic, Int -> RangeEE a -> ShowS
[RangeEE a] -> ShowS
RangeEE a -> String
(Int -> RangeEE a -> ShowS)
-> (RangeEE a -> String)
-> ([RangeEE a] -> ShowS)
-> Show (RangeEE a)
forall a. Show a => Int -> RangeEE a -> ShowS
forall a. Show a => [RangeEE a] -> ShowS
forall a. Show a => RangeEE a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RangeEE a -> ShowS
showsPrec :: Int -> RangeEE a -> ShowS
$cshow :: forall a. Show a => RangeEE a -> String
show :: RangeEE a -> String
$cshowList :: forall a. Show a => [RangeEE a] -> ShowS
showList :: [RangeEE a] -> ShowS
Show, [RangeEE a] -> Markdown
RangeEE a -> Markdown
(RangeEE a -> Markdown)
-> ([RangeEE a] -> Markdown) -> Buildable (RangeEE a)
forall a. Buildable a => [RangeEE a] -> Markdown
forall a. Buildable a => RangeEE a -> Markdown
forall a. (a -> Markdown) -> ([a] -> Markdown) -> Buildable a
$cbuild :: forall a. Buildable a => RangeEE a -> Markdown
build :: RangeEE a -> Markdown
$cbuildList :: forall a. Buildable a => [RangeEE a] -> Markdown
buildList :: [RangeEE a] -> Markdown
Buildable, Maybe AnnOptions
FollowEntrypointFlag -> Notes (ToT (RangeEE a))
(FollowEntrypointFlag -> Notes (ToT (RangeEE a)))
-> Maybe AnnOptions -> HasAnnotation (RangeEE a)
forall a. HasAnnotation a => Maybe AnnOptions
forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeEE a))
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> Maybe AnnOptions -> HasAnnotation a
$cgetAnnotation :: forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeEE a))
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (RangeEE a))
$cannOptions :: forall a. HasAnnotation a => Maybe AnnOptions
annOptions :: Maybe AnnOptions
HasAnnotation, RangeEE a -> RangeEE a -> Bool
(RangeEE a -> RangeEE a -> Bool)
-> (RangeEE a -> RangeEE a -> Bool) -> Eq (RangeEE a)
forall a. Eq a => RangeEE a -> RangeEE a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RangeEE a -> RangeEE a -> Bool
== :: RangeEE a -> RangeEE a -> Bool
$c/= :: forall a. Eq a => RangeEE a -> RangeEE a -> Bool
/= :: RangeEE a -> RangeEE a -> Bool
Eq)
  deriving anyclass WellTypedToT (RangeEE a)
WellTypedToT (RangeEE a)
-> (RangeEE a -> Value (ToT (RangeEE a)))
-> (Value (ToT (RangeEE a)) -> RangeEE a)
-> IsoValue (RangeEE a)
Value (ToT (RangeEE a)) -> RangeEE a
RangeEE a -> Value (ToT (RangeEE a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {a}. IsoValue a => WellTypedToT (RangeEE a)
forall a. IsoValue a => Value (ToT (RangeEE a)) -> RangeEE a
forall a. IsoValue a => RangeEE a -> Value (ToT (RangeEE a))
$ctoVal :: forall a. IsoValue a => RangeEE a -> Value (ToT (RangeEE a))
toVal :: RangeEE a -> Value (ToT (RangeEE a))
$cfromVal :: forall a. IsoValue a => Value (ToT (RangeEE a)) -> RangeEE a
fromVal :: Value (ToT (RangeEE a)) -> RangeEE a
IsoValue

-- | Range inclusive in lower boundary, but exclusive in upper boundary.
newtype RangeIE a = MkRangeIE (Range' 'IncludeBoundary 'ExcludeBoundary a)
  deriving newtype (Typeable (RangeIE a)
Markdown
SingI (TypeDocFieldDescriptions (RangeIE a))
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeIE a)) (RangeIE a)
Typeable (RangeIE a)
-> SingI (TypeDocFieldDescriptions (RangeIE a))
-> FieldDescriptionsValid
     (TypeDocFieldDescriptions (RangeIE a)) (RangeIE a)
-> (Proxy (RangeIE a) -> Text)
-> Markdown
-> (Proxy (RangeIE a) -> WithinParens -> Markdown)
-> (Proxy (RangeIE a) -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep (RangeIE a)
-> TypeDocMichelsonRep (RangeIE a)
-> TypeHasDoc (RangeIE a)
Proxy (RangeIE a) -> [SomeDocDefinitionItem]
TypeDocMichelsonRep (RangeIE a)
Proxy (RangeIE a) -> Text
TypeDocHaskellRep (RangeIE a)
Proxy (RangeIE a) -> WithinParens -> Markdown
forall a.
Typeable a
-> SingI (TypeDocFieldDescriptions a)
-> FieldDescriptionsValid (TypeDocFieldDescriptions a) a
-> (Proxy a -> Text)
-> Markdown
-> (Proxy a -> WithinParens -> Markdown)
-> (Proxy a -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep a
-> TypeDocMichelsonRep a
-> TypeHasDoc a
forall {a}. TypeHasDoc a => Typeable (RangeIE a)
forall a. TypeHasDoc a => Markdown
forall {a}.
TypeHasDoc a =>
SingI (TypeDocFieldDescriptions (RangeIE a))
forall {a}.
TypeHasDoc a =>
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeIE a)) (RangeIE a)
forall a.
TypeHasDoc a =>
Proxy (RangeIE a) -> [SomeDocDefinitionItem]
forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeIE a)
forall a. TypeHasDoc a => Proxy (RangeIE a) -> Text
forall a. TypeHasDoc a => TypeDocHaskellRep (RangeIE a)
forall a.
TypeHasDoc a =>
Proxy (RangeIE a) -> WithinParens -> Markdown
$ctypeDocName :: forall a. TypeHasDoc a => Proxy (RangeIE a) -> Text
typeDocName :: Proxy (RangeIE a) -> Text
$ctypeDocMdDescription :: forall a. TypeHasDoc a => Markdown
typeDocMdDescription :: Markdown
$ctypeDocMdReference :: forall a.
TypeHasDoc a =>
Proxy (RangeIE a) -> WithinParens -> Markdown
typeDocMdReference :: Proxy (RangeIE a) -> WithinParens -> Markdown
$ctypeDocDependencies :: forall a.
TypeHasDoc a =>
Proxy (RangeIE a) -> [SomeDocDefinitionItem]
typeDocDependencies :: Proxy (RangeIE a) -> [SomeDocDefinitionItem]
$ctypeDocHaskellRep :: forall a. TypeHasDoc a => TypeDocHaskellRep (RangeIE a)
typeDocHaskellRep :: TypeDocHaskellRep (RangeIE a)
$ctypeDocMichelsonRep :: forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeIE a)
typeDocMichelsonRep :: TypeDocMichelsonRep (RangeIE a)
TypeHasDoc, (forall x. RangeIE a -> Rep (RangeIE a) x)
-> (forall x. Rep (RangeIE a) x -> RangeIE a)
-> Generic (RangeIE a)
forall x. Rep (RangeIE a) x -> RangeIE a
forall x. RangeIE a -> Rep (RangeIE a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RangeIE a) x -> RangeIE a
forall a x. RangeIE a -> Rep (RangeIE a) x
$cfrom :: forall a x. RangeIE a -> Rep (RangeIE a) x
from :: forall x. RangeIE a -> Rep (RangeIE a) x
$cto :: forall a x. Rep (RangeIE a) x -> RangeIE a
to :: forall x. Rep (RangeIE a) x -> RangeIE a
Generic, Int -> RangeIE a -> ShowS
[RangeIE a] -> ShowS
RangeIE a -> String
(Int -> RangeIE a -> ShowS)
-> (RangeIE a -> String)
-> ([RangeIE a] -> ShowS)
-> Show (RangeIE a)
forall a. Show a => Int -> RangeIE a -> ShowS
forall a. Show a => [RangeIE a] -> ShowS
forall a. Show a => RangeIE a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RangeIE a -> ShowS
showsPrec :: Int -> RangeIE a -> ShowS
$cshow :: forall a. Show a => RangeIE a -> String
show :: RangeIE a -> String
$cshowList :: forall a. Show a => [RangeIE a] -> ShowS
showList :: [RangeIE a] -> ShowS
Show, [RangeIE a] -> Markdown
RangeIE a -> Markdown
(RangeIE a -> Markdown)
-> ([RangeIE a] -> Markdown) -> Buildable (RangeIE a)
forall a. Buildable a => [RangeIE a] -> Markdown
forall a. Buildable a => RangeIE a -> Markdown
forall a. (a -> Markdown) -> ([a] -> Markdown) -> Buildable a
$cbuild :: forall a. Buildable a => RangeIE a -> Markdown
build :: RangeIE a -> Markdown
$cbuildList :: forall a. Buildable a => [RangeIE a] -> Markdown
buildList :: [RangeIE a] -> Markdown
Buildable, Maybe AnnOptions
FollowEntrypointFlag -> Notes (ToT (RangeIE a))
(FollowEntrypointFlag -> Notes (ToT (RangeIE a)))
-> Maybe AnnOptions -> HasAnnotation (RangeIE a)
forall a. HasAnnotation a => Maybe AnnOptions
forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeIE a))
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> Maybe AnnOptions -> HasAnnotation a
$cgetAnnotation :: forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeIE a))
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (RangeIE a))
$cannOptions :: forall a. HasAnnotation a => Maybe AnnOptions
annOptions :: Maybe AnnOptions
HasAnnotation, RangeIE a -> RangeIE a -> Bool
(RangeIE a -> RangeIE a -> Bool)
-> (RangeIE a -> RangeIE a -> Bool) -> Eq (RangeIE a)
forall a. Eq a => RangeIE a -> RangeIE a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RangeIE a -> RangeIE a -> Bool
== :: RangeIE a -> RangeIE a -> Bool
$c/= :: forall a. Eq a => RangeIE a -> RangeIE a -> Bool
/= :: RangeIE a -> RangeIE a -> Bool
Eq)
  deriving anyclass WellTypedToT (RangeIE a)
WellTypedToT (RangeIE a)
-> (RangeIE a -> Value (ToT (RangeIE a)))
-> (Value (ToT (RangeIE a)) -> RangeIE a)
-> IsoValue (RangeIE a)
Value (ToT (RangeIE a)) -> RangeIE a
RangeIE a -> Value (ToT (RangeIE a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {a}. IsoValue a => WellTypedToT (RangeIE a)
forall a. IsoValue a => Value (ToT (RangeIE a)) -> RangeIE a
forall a. IsoValue a => RangeIE a -> Value (ToT (RangeIE a))
$ctoVal :: forall a. IsoValue a => RangeIE a -> Value (ToT (RangeIE a))
toVal :: RangeIE a -> Value (ToT (RangeIE a))
$cfromVal :: forall a. IsoValue a => Value (ToT (RangeIE a)) -> RangeIE a
fromVal :: Value (ToT (RangeIE a)) -> RangeIE a
IsoValue

-- | Range exclusive in lower boundary, but inclusive in upper boundary.
newtype RangeEI a = MkRangeEI (Range' 'ExcludeBoundary 'IncludeBoundary a)
  deriving newtype (Typeable (RangeEI a)
Markdown
SingI (TypeDocFieldDescriptions (RangeEI a))
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeEI a)) (RangeEI a)
Typeable (RangeEI a)
-> SingI (TypeDocFieldDescriptions (RangeEI a))
-> FieldDescriptionsValid
     (TypeDocFieldDescriptions (RangeEI a)) (RangeEI a)
-> (Proxy (RangeEI a) -> Text)
-> Markdown
-> (Proxy (RangeEI a) -> WithinParens -> Markdown)
-> (Proxy (RangeEI a) -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep (RangeEI a)
-> TypeDocMichelsonRep (RangeEI a)
-> TypeHasDoc (RangeEI a)
Proxy (RangeEI a) -> [SomeDocDefinitionItem]
TypeDocMichelsonRep (RangeEI a)
Proxy (RangeEI a) -> Text
TypeDocHaskellRep (RangeEI a)
Proxy (RangeEI a) -> WithinParens -> Markdown
forall a.
Typeable a
-> SingI (TypeDocFieldDescriptions a)
-> FieldDescriptionsValid (TypeDocFieldDescriptions a) a
-> (Proxy a -> Text)
-> Markdown
-> (Proxy a -> WithinParens -> Markdown)
-> (Proxy a -> [SomeDocDefinitionItem])
-> TypeDocHaskellRep a
-> TypeDocMichelsonRep a
-> TypeHasDoc a
forall {a}. TypeHasDoc a => Typeable (RangeEI a)
forall a. TypeHasDoc a => Markdown
forall {a}.
TypeHasDoc a =>
SingI (TypeDocFieldDescriptions (RangeEI a))
forall {a}.
TypeHasDoc a =>
FieldDescriptionsValid
  (TypeDocFieldDescriptions (RangeEI a)) (RangeEI a)
forall a.
TypeHasDoc a =>
Proxy (RangeEI a) -> [SomeDocDefinitionItem]
forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeEI a)
forall a. TypeHasDoc a => Proxy (RangeEI a) -> Text
forall a. TypeHasDoc a => TypeDocHaskellRep (RangeEI a)
forall a.
TypeHasDoc a =>
Proxy (RangeEI a) -> WithinParens -> Markdown
$ctypeDocName :: forall a. TypeHasDoc a => Proxy (RangeEI a) -> Text
typeDocName :: Proxy (RangeEI a) -> Text
$ctypeDocMdDescription :: forall a. TypeHasDoc a => Markdown
typeDocMdDescription :: Markdown
$ctypeDocMdReference :: forall a.
TypeHasDoc a =>
Proxy (RangeEI a) -> WithinParens -> Markdown
typeDocMdReference :: Proxy (RangeEI a) -> WithinParens -> Markdown
$ctypeDocDependencies :: forall a.
TypeHasDoc a =>
Proxy (RangeEI a) -> [SomeDocDefinitionItem]
typeDocDependencies :: Proxy (RangeEI a) -> [SomeDocDefinitionItem]
$ctypeDocHaskellRep :: forall a. TypeHasDoc a => TypeDocHaskellRep (RangeEI a)
typeDocHaskellRep :: TypeDocHaskellRep (RangeEI a)
$ctypeDocMichelsonRep :: forall a. TypeHasDoc a => TypeDocMichelsonRep (RangeEI a)
typeDocMichelsonRep :: TypeDocMichelsonRep (RangeEI a)
TypeHasDoc, (forall x. RangeEI a -> Rep (RangeEI a) x)
-> (forall x. Rep (RangeEI a) x -> RangeEI a)
-> Generic (RangeEI a)
forall x. Rep (RangeEI a) x -> RangeEI a
forall x. RangeEI a -> Rep (RangeEI a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RangeEI a) x -> RangeEI a
forall a x. RangeEI a -> Rep (RangeEI a) x
$cfrom :: forall a x. RangeEI a -> Rep (RangeEI a) x
from :: forall x. RangeEI a -> Rep (RangeEI a) x
$cto :: forall a x. Rep (RangeEI a) x -> RangeEI a
to :: forall x. Rep (RangeEI a) x -> RangeEI a
Generic, Int -> RangeEI a -> ShowS
[RangeEI a] -> ShowS
RangeEI a -> String
(Int -> RangeEI a -> ShowS)
-> (RangeEI a -> String)
-> ([RangeEI a] -> ShowS)
-> Show (RangeEI a)
forall a. Show a => Int -> RangeEI a -> ShowS
forall a. Show a => [RangeEI a] -> ShowS
forall a. Show a => RangeEI a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RangeEI a -> ShowS
showsPrec :: Int -> RangeEI a -> ShowS
$cshow :: forall a. Show a => RangeEI a -> String
show :: RangeEI a -> String
$cshowList :: forall a. Show a => [RangeEI a] -> ShowS
showList :: [RangeEI a] -> ShowS
Show, [RangeEI a] -> Markdown
RangeEI a -> Markdown
(RangeEI a -> Markdown)
-> ([RangeEI a] -> Markdown) -> Buildable (RangeEI a)
forall a. Buildable a => [RangeEI a] -> Markdown
forall a. Buildable a => RangeEI a -> Markdown
forall a. (a -> Markdown) -> ([a] -> Markdown) -> Buildable a
$cbuild :: forall a. Buildable a => RangeEI a -> Markdown
build :: RangeEI a -> Markdown
$cbuildList :: forall a. Buildable a => [RangeEI a] -> Markdown
buildList :: [RangeEI a] -> Markdown
Buildable, Maybe AnnOptions
FollowEntrypointFlag -> Notes (ToT (RangeEI a))
(FollowEntrypointFlag -> Notes (ToT (RangeEI a)))
-> Maybe AnnOptions -> HasAnnotation (RangeEI a)
forall a. HasAnnotation a => Maybe AnnOptions
forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeEI a))
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> Maybe AnnOptions -> HasAnnotation a
$cgetAnnotation :: forall a.
HasAnnotation a =>
FollowEntrypointFlag -> Notes (ToT (RangeEI a))
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (RangeEI a))
$cannOptions :: forall a. HasAnnotation a => Maybe AnnOptions
annOptions :: Maybe AnnOptions
HasAnnotation, RangeEI a -> RangeEI a -> Bool
(RangeEI a -> RangeEI a -> Bool)
-> (RangeEI a -> RangeEI a -> Bool) -> Eq (RangeEI a)
forall a. Eq a => RangeEI a -> RangeEI a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RangeEI a -> RangeEI a -> Bool
== :: RangeEI a -> RangeEI a -> Bool
$c/= :: forall a. Eq a => RangeEI a -> RangeEI a -> Bool
/= :: RangeEI a -> RangeEI a -> Bool
Eq)
  deriving anyclass WellTypedToT (RangeEI a)
WellTypedToT (RangeEI a)
-> (RangeEI a -> Value (ToT (RangeEI a)))
-> (Value (ToT (RangeEI a)) -> RangeEI a)
-> IsoValue (RangeEI a)
Value (ToT (RangeEI a)) -> RangeEI a
RangeEI a -> Value (ToT (RangeEI a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {a}. IsoValue a => WellTypedToT (RangeEI a)
forall a. IsoValue a => Value (ToT (RangeEI a)) -> RangeEI a
forall a. IsoValue a => RangeEI a -> Value (ToT (RangeEI a))
$ctoVal :: forall a. IsoValue a => RangeEI a -> Value (ToT (RangeEI a))
toVal :: RangeEI a -> Value (ToT (RangeEI a))
$cfromVal :: forall a. IsoValue a => Value (ToT (RangeEI a)) -> RangeEI a
fromVal :: Value (ToT (RangeEI a)) -> RangeEI a
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 :: Proxy (Range' lower upper a) -> Text
typeDocName Proxy (Range' lower upper a)
_ = case (forall (r :: RangeBoundaryInclusion). RangeBoundary r => Bool
isInclusive @lower, forall (r :: RangeBoundaryInclusion). RangeBoundary r => Bool
isInclusive @upper) of
    (Bool
True, Bool
True) -> Text
"Range"
    (Bool
True, Bool
False) -> Text
"RangeIE"
    (Bool
False, Bool
True) -> Text
"RangeEI"
    (Bool
False, Bool
False) -> Text
"RangeEE"
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    Markdown
"Signifies a range, which is " Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Text -> Markdown
forall a. Buildable a => a -> Markdown
build (forall (x :: RangeBoundaryInclusion). RangeBoundary x => Text
rangeName @lower) Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
" wrt its lower boundary and "
    Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Text -> Markdown
forall a. Buildable a => a -> Markdown
build (forall (x :: RangeBoundaryInclusion). RangeBoundary x => Text
rangeName @upper) Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
" wrt its upper boundary."
  typeDocMdReference :: Proxy (Range' lower upper a) -> WithinParens -> Markdown
typeDocMdReference Proxy (Range' lower upper a)
pa =
    (Text, DType) -> [DType] -> WithinParens -> Markdown
customTypeDocMdReference
      (Proxy (Range' lower upper a) -> Text
forall a. TypeHasDoc a => Proxy a -> Text
typeDocName Proxy (Range' lower upper a)
pa, Proxy (Range' lower upper a) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (Range' lower upper a)
pa) [Proxy a -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)]
  typeDocHaskellRep :: TypeDocHaskellRep (Range' lower upper a)
typeDocHaskellRep Proxy (Range' lower upper a)
pa FieldDescriptionsV
_ = (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
-> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
forall a. a -> Maybe a
Just ((Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
 -> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc))
-> (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
-> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
forall a b. (a -> b) -> a -> b
$
    ( DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just (DocTypeRepLHS -> Maybe DocTypeRepLHS)
-> DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a b. (a -> b) -> a -> b
$ String -> DocTypeRepLHS
forall a. IsString a => String -> a
fromString (String -> DocTypeRepLHS)
-> (Text -> String) -> Text -> DocTypeRepLHS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. ToString a => a -> String
toString (Text -> DocTypeRepLHS) -> Text -> DocTypeRepLHS
forall a b. (a -> b) -> a -> b
$ Proxy (Range' lower upper a) -> Text
forall a. TypeHasDoc a => Proxy a -> Text
typeDocName Proxy (Range' lower upper a)
pa Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" Integer"
    , [Text
-> Maybe Text
-> [FieldRep SomeTypeWithDoc]
-> ConstructorRep SomeTypeWithDoc
forall a. Text -> Maybe Text -> [FieldRep a] -> ConstructorRep a
T.ConstructorRep (Proxy (Range' lower upper a) -> Text
forall a. TypeHasDoc a => Proxy a -> Text
typeDocName Proxy (Range' lower upper a)
pa) Maybe Text
forall a. Maybe a
Nothing [FieldRep SomeTypeWithDoc]
fields]
    )
    where
      fields :: [FieldRep SomeTypeWithDoc]
fields = case forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @(Range' lower upper Integer) FollowEntrypointFlag
NotFollowEntrypoint of
        T.NTPair TypeAnn
_ Annotation FieldTag
lower Annotation FieldTag
upper VarAnn
_ VarAnn
_ Notes p
_ Notes q
_ ->
          [ Maybe Text
-> Maybe Text -> SomeTypeWithDoc -> FieldRep SomeTypeWithDoc
forall a. Maybe Text -> Maybe Text -> a -> FieldRep a
T.FieldRep (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Annotation FieldTag -> Text
forall {k} (tag :: k). Annotation tag -> Text
unAnnotation Annotation FieldTag
lower) (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"Lower boundary") SomeTypeWithDoc
intRef
          , Maybe Text
-> Maybe Text -> SomeTypeWithDoc -> FieldRep SomeTypeWithDoc
forall a. Maybe Text -> Maybe Text -> a -> FieldRep a
T.FieldRep (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Annotation FieldTag -> Text
forall {k} (tag :: k). Annotation tag -> Text
unAnnotation Annotation FieldTag
upper) (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"Upper boundary") SomeTypeWithDoc
intRef
          ]
      intRef :: SomeTypeWithDoc
intRef = Proxy Integer -> SomeTypeWithDoc
forall td. TypeHasDoc td => Proxy td -> SomeTypeWithDoc
SomeTypeWithDoc (Proxy Integer -> SomeTypeWithDoc)
-> Proxy Integer -> SomeTypeWithDoc
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Integer
  typeDocMichelsonRep :: TypeDocMichelsonRep (Range' lower upper a)
typeDocMichelsonRep Proxy (Range' lower upper a)
pa =
    ( DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just (DocTypeRepLHS -> Maybe DocTypeRepLHS)
-> DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a b. (a -> b) -> a -> b
$ String -> DocTypeRepLHS
forall a. IsString a => String -> a
fromString (String -> DocTypeRepLHS)
-> (Text -> String) -> Text -> DocTypeRepLHS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
forall a. ToString a => a -> String
toString (Text -> DocTypeRepLHS) -> Text -> DocTypeRepLHS
forall a b. (a -> b) -> a -> b
$ Proxy (Range' lower upper a) -> Text
forall a. TypeHasDoc a => Proxy a -> Text
typeDocName Proxy (Range' lower upper a)
pa Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" Integer"
    , forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
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' lower upper a -> Markdown
build (Range' a
l a
r) = [i|#{lpar}#{l}, #{r}#{rpar}|]
    where lpar :: Text
lpar = (Text, Text) -> Text
forall a b. (a, b) -> a
fst ((Text, Text) -> Text) -> (Text, Text) -> Text
forall a b. (a -> b) -> a -> b
$ forall (r :: RangeBoundaryInclusion).
RangeBoundary r =>
(Text, Text)
rangeParens @lower
          rpar :: Text
rpar = (Text, Text) -> Text
forall a b. (a, b) -> b
snd ((Text, Text) -> Text) -> (Text, Text) -> Text
forall a b. (a -> b) -> a -> b
$ forall (r :: RangeBoundaryInclusion).
RangeBoundary r =>
(Text, Text)
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeLower = (Range' lower upper a -> a) -> range a -> a
forall a b. Coercible a b => a -> b
coerce ((Range' lower upper a -> a) -> range a -> a)
-> (Range' lower upper a -> a) -> range a -> a
forall a b. (a -> b) -> a -> b
$ forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Range' lower upper a -> a
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeUpper = (Range' lower upper a -> a) -> range a -> a
forall a b. Coercible a b => a -> b
coerce ((Range' lower upper a -> a) -> range a -> a)
-> (Range' lower upper a -> a) -> range a -> a
forall a b. (a -> b) -> a -> b
$ forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
Range' lower upper a -> a
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
a -> a -> range a
mkRange = (a -> a -> Range' lower upper a) -> a -> a -> range a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> Range' lower upper a) -> a -> a -> range a)
-> (a -> a -> Range' lower upper a) -> a -> a -> range a
forall a b. (a -> b) -> a -> b
$ forall (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
a -> a -> Range' lower upper a
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
fromRange_ = (range a : s) :-> ((a, a) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
((a, a) : s) :-> (range a : s)
toRange_ = ((a, a) : s) :-> (range a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> (a : s)
rangeLower_ = (range a : s) :-> ((a, a) : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
fromRange_ ((range a : s) :-> ((a, a) : s))
-> (((a, a) : s) :-> (a : s)) -> (range a : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, a) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> (a : s)
rangeUpper_ = (range a : s) :-> ((a, a) : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
fromRange_ ((range a : s) :-> ((a, a) : s))
-> (((a, a) : s) :-> (a : s)) -> (range a : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, a) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
(NiceRange range lower upper a, Num a) =>
a -> a -> range a
mkRangeFor a
start a
len = a -> a -> range a
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
a -> a -> range a
mkRange a
start (a
start a -> a -> a
forall a. Num a => a -> a -> a
+ a
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(("min" :! a) : ("max" :! a) : s) :-> (range a : s)
mkRange_ = Label "min"
-> (("min" :! a) : ("max" :! a) : s) :-> (a : ("max" :! a) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "min"
#min ((("min" :! a) : ("max" :! a) : s) :-> (a : ("max" :! a) : s))
-> ((a : ("max" :! a) : s) :-> (a : a : s))
-> (("min" :! a) : ("max" :! a) : s) :-> (a : a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((("max" :! a) : s) :-> (a : s))
-> (a : ("max" :! a) : s) :-> (a : a : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Label "max" -> (("max" :! a) : s) :-> (a : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "max"
#max) ((("min" :! a) : ("max" :! a) : s) :-> (a : a : s))
-> ((a : a : s) :-> ((a, a) : s))
-> (("min" :! a) : ("max" :! a) : s) :-> ((a, a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : a : s) :-> ((a, a) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
L.pair ((("min" :! a) : ("max" :! a) : s) :-> ((a, a) : s))
-> (((a, a) : s) :-> (range a : s))
-> (("min" :! a) : ("max" :! a) : s) :-> (range a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, a) : s) :-> (range a : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
((a, a) : s) :-> (range a : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a b (s :: [*]).
(NiceRange range lower upper a, Dupable a, ArithOpHs Add a b a) =>
(("start" :! a) : ("length" :! b) : s) :-> (range a : s)
mkRangeFor_
  = Label "start"
-> (("start" :! a) : ("length" :! b) : s)
   :-> (a : ("length" :! b) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label "start"
#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_ :: forall a b (s :: [*]).
(Dupable a, ArithOpHs Add a b a, ToT b ~ 'TNat) =>
(("start" :! a) : ("length" :! b) : s) :-> (Range a : s)
mkRangeForSafe_ = (("start" :! a) : ("length" :! b) : s) :-> (Range a : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a b (s :: [*]).
(NiceRange range lower upper a, Dupable a, ArithOpHs Add a b a) =>
(("start" :! a) : ("length" :! b) : s) :-> (range a : s)
mkRangeFor_
  where
    Dict (ToT b ~ 'TNat)
_ = forall (a :: Constraint). a => Dict a
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
(NiceRange range lower upper a, Ord a) =>
range a -> a -> Bool
inRange = (Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) (Ordering -> Bool)
-> (range a -> a -> Ordering) -> range a -> a -> Bool
forall a b c. SuperComposition a b c => a -> b -> c
... range a -> a -> Ordering
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
(NiceRange range lower upper a, Ord a) =>
range a -> a -> Ordering
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
(NiceRange range lower upper a, Ord a) =>
range a -> a -> Ordering
inRangeCmp range a
r a
x
  | Bool -> Bool
forall a. Boolean a => a -> a
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ forall (r :: RangeBoundaryInclusion) a.
(RangeBoundary r, Ord a) =>
a -> a -> Bool
inRangeComp @lower (range a -> a
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeLower range a
r) a
x = Ordering
LT
  | Bool -> Bool
forall a. Boolean a => a -> a
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ forall (r :: RangeBoundaryInclusion) a.
(RangeBoundary r, Ord a) =>
a -> a -> Bool
inRangeComp @upper a
x (range a -> a
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeUpper range a
r) = Ordering
GT
  | Bool
otherwise = Ordering
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, NiceComparable a, Dupable a) =>
(range a : a : s) :-> (Bool : s)
inRange_
  = (range a : a : s) :-> ((a, a) : a : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, NiceComparable a, Dupable a) =>
(range a : a : s) :-> (Integer : s)
inRangeCmp_
  = (range a : a : s) :-> ((a, a) : a : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, NiceComparable a, Dupable a) =>
OnRangeAssertFailure a -> (range a : a : s) :-> s
assertInRange_ OnRangeAssertFailure{forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafUnderflow :: forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafOverflow :: forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafUnderflow :: forall a.
OnRangeAssertFailure a
-> forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafOverflow :: forall a.
OnRangeAssertFailure a
-> forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
..}
  = ((a : s) :-> (("value" :! a) : s))
-> (range a : a : s) :-> (range a : ("value" :! a) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Label "value" -> (a : s) :-> (("value" :! a) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "value"
#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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, NiceComparable a, Dupable a) =>
(forall (s' :: [*]) (any :: [*]). s' :-> any)
-> (range a : a : s) :-> s
assertInRangeSimple_ forall (s' :: [*]) (any :: [*]). s' :-> any
err
  = (range a : a : s) :-> (Bool : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, NiceComparable a, Dupable a) =>
(range a : a : s) :-> (Bool : s)
inRange_ ((range a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s) -> (range a : a : s) :-> s
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ s :-> s
forall (s :: [*]). s :-> s
nop s :-> s
forall (s' :: [*]) (any :: [*]). s' :-> any
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 :: forall a (s :: [*]).
IsoValue a =>
(Bool : ("boundary" :! a) : ("value" :! a) : s)
:-> (RangeFailureInfo a : s)
mkRangeFailureInfo = (('[Bool, a, a] ++ s) :-> (RangeFailureInfo a : s))
-> (Bool : ("boundary" :! a) : ("value" :! a) : s)
   :-> (RangeFailureInfo a : s)
forall a b. Coercible a b => a -> b
coerce ((('[Bool, a, a] ++ s) :-> (RangeFailureInfo a : s))
 -> (Bool : ("boundary" :! a) : ("value" :! a) : s)
    :-> (RangeFailureInfo a : s))
-> (('[Bool, a, a] ++ s) :-> (RangeFailureInfo a : s))
-> (Bool : ("boundary" :! a) : ("value" :! a) : s)
   :-> (RangeFailureInfo a : s)
forall a b. (a -> b) -> a -> b
$ forall dt (fields :: [*]) (st :: [*]).
(InstrConstructC dt, fields ~ ConstructorFieldTypes dt,
 (ToTs fields ++ ToTs st) ~ ToTs (fields ++ st)) =>
(fields ++ st) :-> (dt : st)
constructStack @(RangeFailureInfo a) @_ @s

-- | Information about the range check failure
data RangeFailureInfo a = RangeFailureInfo
  { forall a. RangeFailureInfo a -> Bool
rfiInclusive :: Bool -- ^ Whether the boundary is inclusive or not
  , forall a. RangeFailureInfo a -> a
rfiBoundary :: a     -- ^ The boundary that failed to check
  , forall a. RangeFailureInfo a -> a
rfiValue :: a        -- ^ The value that failed to check
  } deriving stock (forall x. RangeFailureInfo a -> Rep (RangeFailureInfo a) x)
-> (forall x. Rep (RangeFailureInfo a) x -> RangeFailureInfo a)
-> Generic (RangeFailureInfo a)
forall x. Rep (RangeFailureInfo a) x -> RangeFailureInfo a
forall x. RangeFailureInfo a -> Rep (RangeFailureInfo a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RangeFailureInfo a) x -> RangeFailureInfo a
forall a x. RangeFailureInfo a -> Rep (RangeFailureInfo a) x
$cfrom :: forall a x. RangeFailureInfo a -> Rep (RangeFailureInfo a) x
from :: forall x. RangeFailureInfo a -> Rep (RangeFailureInfo a) x
$cto :: forall a x. Rep (RangeFailureInfo a) x -> RangeFailureInfo a
to :: forall x. Rep (RangeFailureInfo a) x -> RangeFailureInfo a
Generic
    deriving anyclass WellTypedToT (RangeFailureInfo a)
WellTypedToT (RangeFailureInfo a)
-> (RangeFailureInfo a -> Value (ToT (RangeFailureInfo a)))
-> (Value (ToT (RangeFailureInfo a)) -> RangeFailureInfo a)
-> IsoValue (RangeFailureInfo a)
Value (ToT (RangeFailureInfo a)) -> RangeFailureInfo a
RangeFailureInfo a -> Value (ToT (RangeFailureInfo a))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {a}. IsoValue a => WellTypedToT (RangeFailureInfo a)
forall a.
IsoValue a =>
Value (ToT (RangeFailureInfo a)) -> RangeFailureInfo a
forall a.
IsoValue a =>
RangeFailureInfo a -> Value (ToT (RangeFailureInfo a))
$ctoVal :: forall a.
IsoValue a =>
RangeFailureInfo a -> Value (ToT (RangeFailureInfo a))
toVal :: RangeFailureInfo a -> Value (ToT (RangeFailureInfo a))
$cfromVal :: forall a.
IsoValue a =>
Value (ToT (RangeFailureInfo a)) -> RangeFailureInfo a
fromVal :: Value (ToT (RangeFailureInfo a)) -> RangeFailureInfo a
IsoValue
    deriving Text -> Text
(Text -> Text) -> TypeHasFieldNamingStrategy (RangeFailureInfo a)
forall a. Text -> Text
forall {k} (a :: k). (Text -> Text) -> TypeHasFieldNamingStrategy a
$ctypeFieldNamingStrategy :: forall a. Text -> Text
typeFieldNamingStrategy :: Text -> Text
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 :: Markdown
typeDocMdDescription = Markdown
"Information about the range check failure"
  typeDocMdReference :: Proxy (RangeFailureInfo a) -> WithinParens -> Markdown
typeDocMdReference = Proxy (RangeFailureInfo a) -> WithinParens -> Markdown
forall (t :: * -> *) r a.
(r ~ t a, Typeable t, Each '[TypeHasDoc] '[r, a],
 IsHomomorphic t) =>
Proxy r -> WithinParens -> Markdown
poly1TypeDocMdReference
  typeDocHaskellRep :: TypeDocHaskellRep (RangeFailureInfo a)
typeDocHaskellRep
    = (Text -> Text)
-> TypeDocHaskellRep (RangeFailureInfo a)
-> TypeDocHaskellRep (RangeFailureInfo a)
forall a.
(Text -> Text) -> TypeDocHaskellRep a -> TypeDocHaskellRep a
T.haskellRepMap (forall a. TypeHasFieldNamingStrategy a => Text -> Text
forall {k} (a :: k). TypeHasFieldNamingStrategy a => Text -> Text
typeFieldNamingStrategy @(RangeFailureInfo a))
    (TypeDocHaskellRep (RangeFailureInfo a)
 -> TypeDocHaskellRep (RangeFailureInfo a))
-> TypeDocHaskellRep (RangeFailureInfo a)
-> TypeDocHaskellRep (RangeFailureInfo a)
forall a b. (a -> b) -> a -> b
$ forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (GRep a),
 HaveCommonTypeCtor b a) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRep @(RangeFailureInfo Integer)
  typeDocMichelsonRep :: TypeDocMichelsonRep (RangeFailureInfo a)
typeDocMichelsonRep = forall a b.
(Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
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
  { forall a.
OnRangeAssertFailure a
-> forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafUnderflow :: forall s any. RangeFailureInfo a : s :-> any
  , forall a.
OnRangeAssertFailure a
-> 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 :: forall a.
(forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
mkOnRangeAssertFailureSimple forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
f = (forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
-> (forall (s :: [*]) (any :: [*]).
    (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
forall a.
(forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
-> (forall (s :: [*]) (any :: [*]).
    (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
OnRangeAssertFailure (RangeFailureInfo a : s) :-> any
forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
f (RangeFailureInfo a : s) :-> any
forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
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 :: forall a (underflow :: Symbol) (overflow :: Symbol).
(NiceConstant a, ErrorArg underflow ~ RangeFailureInfo a,
 ErrorArg overflow ~ RangeFailureInfo a,
 CustomErrorHasDoc underflow, CustomErrorHasDoc overflow) =>
("underflow" :! Label underflow)
-> ("overflow" :! Label overflow) -> OnRangeAssertFailure a
customErrorORAF (Name "underflow"
-> ("underflow" :! Label underflow) -> Label underflow
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg Name "underflow"
#underflow -> Label underflow
ufl) (Name "overflow" -> ("overflow" :! Label overflow) -> Label overflow
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg Name "overflow"
#overflow -> Label overflow
ofl) = OnRangeAssertFailure
  { orafUnderflow :: forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafUnderflow = Label underflow -> (RangeFailureInfo a : s) :-> any
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom Label underflow
ufl
  , orafOverflow :: forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any
orafOverflow = Label overflow -> (RangeFailureInfo a : s) :-> any
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom Label overflow
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 :: forall a (err :: Symbol).
(NiceConstant a, ErrorArg err ~ RangeFailureInfo a,
 CustomErrorHasDoc err) =>
Label err -> OnRangeAssertFailure a
customErrorORAFSimple Label err
err = (forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
forall a.
(forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
mkOnRangeAssertFailureSimple ((forall (s :: [*]) (any :: [*]). (RangeFailureInfo a : s) :-> any)
 -> OnRangeAssertFailure a)
-> (forall (s :: [*]) (any :: [*]).
    (RangeFailureInfo a : s) :-> any)
-> OnRangeAssertFailure a
forall a b. (a -> b) -> a -> b
$ Label err -> (RangeFailureInfo a : s) :-> any
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom Label err
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 :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
(NiceRange range lower upper a, Ord a,
 CanCheckEmpty lower upper) =>
range a -> Bool
isRangeEmpty range a
r = forall {k} {k} (l :: k) (u :: k) a.
(CanCheckEmpty l u, Ord a) =>
a -> a -> Bool
forall (l :: RangeBoundaryInclusion) (u :: RangeBoundaryInclusion)
       a.
(CanCheckEmpty l u, Ord a) =>
a -> a -> Bool
checkEmpty @lower @upper (range a -> a
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeLower range a
r) (range a -> a
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a.
NiceRange range lower upper a =>
range a -> a
rangeUpper range a
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, CanCheckEmpty lower upper,
 NiceComparable a) =>
(range a : s) :-> (Bool : s)
isRangeEmpty_
  = (range a : s) :-> ((a, a) : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
NiceRange range lower upper a =>
(range a : s) :-> ((a, a) : s)
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 :: forall a. Ord a => a -> a -> Bool
checkEmpty = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>)
  checkEmpty_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
checkEmpty_ = (a : a : s) :-> (Bool : s)
forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
L.gt
instance CanCheckEmpty 'IncludeBoundary 'ExcludeBoundary where
  checkEmpty :: forall a. Ord a => a -> a -> Bool
checkEmpty = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
  checkEmpty_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
checkEmpty_ = (a : a : s) :-> (Bool : s)
forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
L.ge
instance CanCheckEmpty 'ExcludeBoundary 'IncludeBoundary where
  checkEmpty :: forall a. Ord a => a -> a -> Bool
checkEmpty = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
  checkEmpty_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
checkEmpty_ = (a : a : s) :-> (Bool : s)
forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
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 :: forall a. Ord a => a -> a -> Bool
checkEmpty = a -> a -> Bool
forall a. Bottom => a
forall a. a
no
  checkEmpty_ :: forall a (s :: [*]). NiceComparable a => (a : a : s) :-> (Bool : s)
checkEmpty_ = (a : a : s) :-> (Bool : s)
forall a. Bottom => a
forall a. a
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_ :: forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(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_ forall (s' :: [*]) (any :: [*]). (range a : s') :-> any
err = (range a : s) :-> (range a : range a : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((range a : s) :-> (range a : range a : s))
-> ((range a : range a : s) :-> (Bool : range a : s))
-> (range a : s) :-> (Bool : range a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (range a : range a : s) :-> (Bool : range a : s)
forall (range :: * -> *) (lower :: RangeBoundaryInclusion)
       (upper :: RangeBoundaryInclusion) a (s :: [*]).
(NiceRange range lower upper a, CanCheckEmpty lower upper,
 NiceComparable a) =>
(range a : s) :-> (Bool : s)
isRangeEmpty_ ((range a : s) :-> (Bool : range a : s))
-> ((Bool : range a : s) :-> (range a : s))
-> (range a : s) :-> (range a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((range a : s) :-> (range a : s))
-> ((range a : s) :-> (range a : s))
-> (Bool : range a : s) :-> (range a : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ (range a : s) :-> (range a : s)
forall (s' :: [*]) (any :: [*]). (range a : s') :-> any
err (range a : s) :-> (range a : s)
forall (s :: [*]). s :-> s
nop