Idris2Doc : IotaTime.Interval

IotaTime.Interval

(source)
Reexports
import public Data.So
import public IotaTime.Duration
import public IotaTime.Instant
Definitions
record IntervalRep : Type
  A half-open interval `[start, end)` on the global timeline.

  Totality: total
  Visibility: export
  Constructor: 
MkInterval : (storedStart : Instant) -> (storedEnd : Instant) -> (0 _ : So (toNanosecondsSinceEpoch storedStart <= toNanosecondsSinceEpoch storedEnd)) -> IntervalRep

  Projections:
  
.storedEnd : IntervalRep -> Instant
  
.storedStart : IntervalRep -> Instant
  
0 .valid : ({rec:0} : IntervalRep) -> So (toNanosecondsSinceEpoch (storedStart {rec:0}) <= toNanosecondsSinceEpoch (storedEnd {rec:0}))

  Hints:
  
Eq IntervalRep
  
Ord IntervalRep
  
Show IntervalRep
Interval : Type
  Totality: total
  Visibility: public export
isValidInterval : Instant -> Instant -> Bool
  Decide whether two instants are ordered as a valid interval.

  Totality: total
  Visibility: public export
interval : (startNanoseconds : Integer) -> (endNanoseconds : Integer) -> {auto 0 _ : So (startNanoseconds <= endNanoseconds)} -> Interval
  Construct a statically validated half-open interval from nanosecond counts
  relative to the library epoch.

  Totality: total
  Visibility: public export
data IntervalError : Type
  Totality: total
  Visibility: public export
  Constructor: 
ReversedInterval : Instant -> Instant -> IntervalError
refineInterval : Instant -> Instant -> Either IntervalError Interval
  Validate arbitrary endpoints learned at runtime.

  Totality: total
  Visibility: public export
start : Interval -> Instant
  Totality: total
  Visibility: public export
end : Interval -> Instant
  Totality: total
  Visibility: public export
0 intervalIsValid : (value : Interval) -> So (isValidInterval (start value) (end value))
  Every interval carries erased evidence that its endpoints are ordered.

  Totality: total
  Visibility: public export
contains : Interval -> Instant -> Bool
  Test membership in the half-open interval `[start, end)`.

  Totality: total
  Visibility: public export
isEmpty : Interval -> Bool
  Whether the interval contains no instants.

  Totality: total
  Visibility: public export
overlaps : Interval -> Interval -> Bool
  Whether two half-open intervals share at least one instant.

  Totality: total
  Visibility: public export
isAdjacent : Interval -> Interval -> Bool
  Whether two non-overlapping intervals touch at one endpoint.

  Totality: total
  Visibility: public export
intersectionStart : Interval -> Interval -> Instant
  The later start bound selected for an intersection.

  Totality: total
  Visibility: public export
intersectionEnd : Interval -> Interval -> Instant
  The earlier end bound selected for an intersection.

  Totality: total
  Visibility: public export
hasNonEmptyIntersection : Interval -> Interval -> Bool
  Whether two intervals have a valid, non-empty intersection.

  Totality: total
  Visibility: public export
intersection : (left : Interval) -> (right : Interval) -> {auto 0 _ : So (hasNonEmptyIntersection left right)} -> Interval
  Return the non-empty intersection when its existence is statically known.

  Totality: total
  Visibility: public export
data IntersectionError : Type
  Totality: total
  Visibility: public export
  Constructor: 
NoNonEmptyIntersection : IntersectionError
refineIntersection : Interval -> Interval -> Either IntersectionError Interval
  Return the non-empty intersection of intervals learned at runtime.

  Totality: total
  Visibility: public export
unionStart : Interval -> Interval -> Instant
  The start bound selected for a connected union.

  Totality: total
  Visibility: public export
unionEnd : Interval -> Interval -> Instant
  The end bound selected for a connected union.

  Totality: total
  Visibility: public export
isConnected : Interval -> Interval -> Bool
  Totality: total
  Visibility: public export
union : (left : Interval) -> (right : Interval) -> {auto 0 _ : So (isConnected left right)} -> Interval
  Return the smallest interval containing both inputs when their union is
  statically known to be connected. Empty intervals are absorbed by the
  other input.

  Totality: total
  Visibility: public export
data UnionError : Type
  Totality: total
  Visibility: public export
  Constructor: 
DisconnectedIntervals : UnionError
refineUnion : Interval -> Interval -> Either UnionError Interval
  Return the connected union of intervals learned at runtime.

  Totality: total
  Visibility: public export
duration : Interval -> Duration
  Return the nonnegative fixed duration between the endpoints.

  Totality: total
  Visibility: public export
isValidUnboundedInterval : Maybe Instant -> Maybe Instant -> Bool
  A half-open timeline interval whose start, end, or both may be unbounded.
  `Nothing` denotes negative infinity for the start and positive infinity for
  the end.
  Decide whether optional endpoints are ordered as a valid interval.

  Totality: total
  Visibility: public export
isValidUnboundedNanosecondInterval : Maybe Integer -> Maybe Integer -> Bool
  Totality: total
  Visibility: public export
record UnboundedIntervalRep : Type
  Totality: total
  Visibility: export
  Constructor: 
MkUnboundedInterval : (storedUnboundedStart : Maybe Instant) -> (storedUnboundedEnd : Maybe Instant) -> (0 _ : So (isValidUnboundedInterval storedUnboundedStart storedUnboundedEnd)) -> UnboundedIntervalRep

  Projections:
  
.storedUnboundedEnd : UnboundedIntervalRep -> Maybe Instant
  
.storedUnboundedStart : UnboundedIntervalRep -> Maybe Instant
  
0 .valid : ({rec:0} : UnboundedIntervalRep) -> So (isValidUnboundedInterval (storedUnboundedStart {rec:0}) (storedUnboundedEnd {rec:0}))

  Hints:
  
Eq UnboundedIntervalRep
  
Ord UnboundedIntervalRep
  
Show UnboundedIntervalRep
UnboundedInterval : Type
  Totality: total
  Visibility: public export
unboundedInterval : (startNanoseconds : Maybe Integer) -> (endNanoseconds : Maybe Integer) -> {auto 0 _ : So (isValidUnboundedNanosecondInterval startNanoseconds endNanoseconds)} -> UnboundedInterval
  Construct a statically validated interval with optional endpoints.

  Totality: total
  Visibility: public export
refineUnboundedInterval : Maybe Instant -> Maybe Instant -> Either IntervalError UnboundedInterval
  Validate optional endpoints learned at runtime.

  Totality: total
  Visibility: public export
unboundedStart : UnboundedInterval -> Maybe Instant
  Totality: total
  Visibility: public export
unboundedEnd : UnboundedInterval -> Maybe Instant
  Totality: total
  Visibility: public export
0 unboundedIntervalIsValid : (value : UnboundedInterval) -> So (isValidUnboundedInterval (unboundedStart value) (unboundedEnd value))
  Every unbounded interval carries erased evidence that its finite endpoints
  are ordered.

  Totality: total
  Visibility: public export
toUnboundedInterval : Interval -> UnboundedInterval
  Treat a bounded interval as an interval with two finite bounds.

  Totality: total
  Visibility: public export
toBoundedInterval : UnboundedInterval -> Maybe Interval
  Recover a bounded interval only when both endpoints are finite.

  Totality: total
  Visibility: public export
unboundedContains : UnboundedInterval -> Instant -> Bool
  Test membership using half-open endpoint semantics at every finite bound.

  Totality: total
  Visibility: public export
unboundedIsEmpty : UnboundedInterval -> Bool
  Whether the interval contains no instants.

  Totality: total
  Visibility: public export
unboundedEndAfterStart : Maybe Instant -> Maybe Instant -> Bool
  Whether an optional end lies after an optional start, treating `Nothing`
  as the appropriate infinity.

  Totality: total
  Visibility: public export
unboundedOverlaps : UnboundedInterval -> UnboundedInterval -> Bool
  Whether two unbounded intervals share at least one instant.

  Totality: total
  Visibility: public export
finiteUnboundedBoundsEqual : Maybe Instant -> Maybe Instant -> Bool
  Whether two optional bounds are finite and equal.

  Totality: total
  Visibility: public export
unboundedIsAdjacent : UnboundedInterval -> UnboundedInterval -> Bool
  Whether two non-overlapping intervals touch at one finite endpoint.

  Totality: total
  Visibility: public export
unboundedIntersectionStart : UnboundedInterval -> UnboundedInterval -> Maybe Instant
  The later optional start bound selected for an intersection.

  Totality: total
  Visibility: public export
unboundedIntersectionEnd : UnboundedInterval -> UnboundedInterval -> Maybe Instant
  The earlier optional end bound selected for an intersection.

  Totality: total
  Visibility: public export
hasNonEmptyUnboundedIntersection : UnboundedInterval -> UnboundedInterval -> Bool
  Whether two unbounded intervals have a valid, non-empty intersection.

  Totality: total
  Visibility: public export
unboundedIntersection : (left : UnboundedInterval) -> (right : UnboundedInterval) -> {auto 0 _ : So (hasNonEmptyUnboundedIntersection left right)} -> UnboundedInterval
  Return the non-empty intersection when its existence is statically known.

  Totality: total
  Visibility: public export
refineUnboundedIntersection : UnboundedInterval -> UnboundedInterval -> Either IntersectionError UnboundedInterval
  Return the non-empty intersection of unbounded intervals learned at
  runtime.

  Totality: total
  Visibility: public export
unboundedUnionStart : UnboundedInterval -> UnboundedInterval -> Maybe Instant
  The optional start bound selected for a connected union.

  Totality: total
  Visibility: public export
unboundedUnionEnd : UnboundedInterval -> UnboundedInterval -> Maybe Instant
  The optional end bound selected for a connected union.

  Totality: total
  Visibility: public export
unboundedIsConnected : UnboundedInterval -> UnboundedInterval -> Bool
  Totality: total
  Visibility: public export
unboundedUnion : (left : UnboundedInterval) -> (right : UnboundedInterval) -> {auto 0 _ : So (unboundedIsConnected left right)} -> UnboundedInterval
  Return the smallest interval containing both inputs when their union is
  statically known to be connected. Empty intervals are absorbed by the
  other input.

  Totality: total
  Visibility: public export
refineUnboundedUnion : UnboundedInterval -> UnboundedInterval -> Either UnionError UnboundedInterval
  Return the connected union of unbounded intervals learned at runtime.

  Totality: total
  Visibility: public export
unboundedDuration : UnboundedInterval -> Maybe Duration
  Return the duration when both endpoints are finite.

  Totality: total
  Visibility: public export