Whether to include boundary in Range

Default range, inclusive in both boundaries.

Range inclusive in lower boundary, but exclusive in upper boundary.

Range exclusive in lower boundary, but inclusive in upper boundary.

Range exclusive in both boundaries.

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.

Information about the range check failure

Helper class for RangeBoundaryInclusion.

Helper class for the Range types that encapsulates common features.

Helper class to check if a range is empty. Gives up when both boundaries are exclusive.

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]

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.

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]

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]

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]

Convert a Range to a pair of (lower, upper)

>>> mkRangeForSafe_ # fromRange_ -$ #start :! (123 :: Integer) ::: #length :! (456 :: Natural)
(123,579)

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]

Get a range's lower bound

Get a range's upper bound.

Get the lower bound of a Range

>>> mkRange_ # rangeLower_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer)
123

Get the upper bound of a Range

>>> mkRange_ # rangeUpper_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer)
456

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]

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

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]

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

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_.

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"' ...
...

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
...

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
...

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
...

Construct OnRangeAssertFailure that performs the same action on both overflow and underflow

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 ::: ()
()

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 ::: ()
()

Value-level representation as Bool