
   0 | module IotaTime.Interval
   1 | 
   2 | import public Data.So
   3 | import public IotaTime.Duration
   4 | import public IotaTime.Instant
   5 | import Derive.Prelude
   6 | 
   7 | %language ElabReflection
   8 | 
   9 | %default total
  10 | 
  11 | ||| A half-open interval `[start, end)` on the global timeline.
  12 | export
  13 | record IntervalRep where
  14 |   constructor MkInterval
  15 |   storedStart : Instant
  16 |   storedEnd : Instant
  17 |   0 valid : So
  18 |     (toNanosecondsSinceEpoch storedStart <= toNanosecondsSinceEpoch storedEnd)
  19 | 
  20 | public export
  21 | Interval : Type
  22 | Interval = IntervalRep
  23 | 
  24 | ||| Decide whether two instants are ordered as a valid interval.
  25 | public export
  26 | isValidInterval : Instant -> Instant -> Bool
  27 | isValidInterval start end =
  28 |   toNanosecondsSinceEpoch start <= toNanosecondsSinceEpoch end
  29 | 
  30 | ||| Construct a statically validated half-open interval from nanosecond counts
  31 | ||| relative to the library epoch.
  32 | public export
  33 | interval : (startNanoseconds, endNanoseconds : Integer) ->
  34 |            {auto 0 valid : So (startNanoseconds <= endNanoseconds)} -> Interval
  35 | interval startNanoseconds endNanoseconds = MkInterval
  36 |   (fromNanosecondsSinceEpoch startNanoseconds)
  37 |   (fromNanosecondsSinceEpoch endNanoseconds)
  38 |   (rewrite instantNanosecondsRoundTrip startNanoseconds in
  39 |    rewrite instantNanosecondsRoundTrip endNanoseconds in valid)
  40 | 
  41 | checkedInterval : (start, end : Instant) ->
  42 |                   {auto 0 valid : So (isValidInterval start end)} -> Interval
  43 | checkedInterval start end = MkInterval start end valid
  44 | 
  45 | public export
  46 | data IntervalError = ReversedInterval Instant Instant
  47 | 
  48 | ||| Validate arbitrary endpoints learned at runtime.
  49 | public export
  50 | refineInterval : (start, end : Instant) -> Either IntervalError Interval
  51 | refineInterval start end =
  52 |   case choose (isValidInterval start end) of
  53 |     Left valid => Right (checkedInterval start end @{valid})
  54 |     Right _ => Left (ReversedInterval start end)
  55 | 
  56 | public export
  57 | start : Interval -> Instant
  58 | start (MkInterval value _ _) = value
  59 | 
  60 | public export
  61 | end : Interval -> Instant
  62 | end (MkInterval _ value _) = value
  63 | 
  64 | ||| Every interval carries erased evidence that its endpoints are ordered.
  65 | public export
  66 | 0 intervalIsValid : (value : Interval) ->
  67 |   So (isValidInterval (start value) (end value))
  68 | intervalIsValid (MkInterval _ _ valid) = valid
  69 | 
  70 | ||| Test membership in the half-open interval `[start, end)`.
  71 | public export
  72 | contains : Interval -> Instant -> Bool
  73 | contains value instant = start value <= instant && instant < end value
  74 | 
  75 | ||| Whether the interval contains no instants.
  76 | public export
  77 | isEmpty : Interval -> Bool
  78 | isEmpty value =
  79 |   toNanosecondsSinceEpoch (start value) ==
  80 |   toNanosecondsSinceEpoch (end value)
  81 | 
  82 | ||| Whether two half-open intervals share at least one instant.
  83 | public export
  84 | overlaps : Interval -> Interval -> Bool
  85 | overlaps left right = not (isEmpty left) && not (isEmpty right) &&
  86 |   toNanosecondsSinceEpoch (start left) <
  87 |     toNanosecondsSinceEpoch (end right) &&
  88 |   toNanosecondsSinceEpoch (start right) <
  89 |     toNanosecondsSinceEpoch (end left)
  90 | 
  91 | ||| Whether two non-overlapping intervals touch at one endpoint.
  92 | public export
  93 | isAdjacent : Interval -> Interval -> Bool
  94 | isAdjacent left right =
  95 |   toNanosecondsSinceEpoch (end left) ==
  96 |     toNanosecondsSinceEpoch (start right) ||
  97 |   toNanosecondsSinceEpoch (end right) ==
  98 |     toNanosecondsSinceEpoch (start left)
  99 | 
 100 | ||| The later start bound selected for an intersection.
 101 | public export
 102 | intersectionStart : Interval -> Interval -> Instant
 103 | intersectionStart left right = max (start left) (start right)
 104 | 
 105 | ||| The earlier end bound selected for an intersection.
 106 | public export
 107 | intersectionEnd : Interval -> Interval -> Instant
 108 | intersectionEnd left right = min (end left) (end right)
 109 | 
 110 | ||| Whether two intervals have a valid, non-empty intersection.
 111 | public export
 112 | hasNonEmptyIntersection : Interval -> Interval -> Bool
 113 | hasNonEmptyIntersection left right =
 114 |   isValidInterval (intersectionStart left right) (intersectionEnd left right) &&
 115 |   toNanosecondsSinceEpoch (intersectionStart left right) <
 116 |     toNanosecondsSinceEpoch (intersectionEnd left right)
 117 | 
 118 | 0 andLeft : (left, right : Bool) -> So (left && right) -> So left
 119 | andLeft True True Oh = Oh
 120 | 
 121 | 0 andRight : (left, right : Bool) -> So (left && right) -> So right
 122 | andRight True True Oh = Oh
 123 | 
 124 | ||| Return the non-empty intersection when its existence is statically known.
 125 | public export
 126 | intersection : (left, right : Interval) ->
 127 |                {auto 0 intersects : So
 128 |                  (hasNonEmptyIntersection left right)} ->
 129 |                Interval
 130 | intersection left right @{intersects} = MkInterval
 131 |   (intersectionStart left right)
 132 |   (intersectionEnd left right)
 133 |   (andLeft
 134 |     (isValidInterval
 135 |       (intersectionStart left right) (intersectionEnd left right))
 136 |     (toNanosecondsSinceEpoch (intersectionStart left right) <
 137 |       toNanosecondsSinceEpoch (intersectionEnd left right))
 138 |     intersects)
 139 | 
 140 | public export
 141 | data IntersectionError = NoNonEmptyIntersection
 142 | 
 143 | ||| Return the non-empty intersection of intervals learned at runtime.
 144 | public export
 145 | refineIntersection : (left, right : Interval) ->
 146 |                      Either IntersectionError Interval
 147 | refineIntersection left right =
 148 |   case choose (hasNonEmptyIntersection left right) of
 149 |     Left intersects => Right (intersection left right @{intersects})
 150 |     Right _ => Left NoNonEmptyIntersection
 151 | 
 152 | ||| The start bound selected for a connected union.
 153 | public export
 154 | unionStart : Interval -> Interval -> Instant
 155 | unionStart left right =
 156 |   if isEmpty left then start right
 157 |   else if isEmpty right then start left
 158 |   else if toNanosecondsSinceEpoch (start left) <=
 159 |       toNanosecondsSinceEpoch (start right)
 160 |     then start left
 161 |     else start right
 162 | 
 163 | ||| The end bound selected for a connected union.
 164 | public export
 165 | unionEnd : Interval -> Interval -> Instant
 166 | unionEnd left right =
 167 |   if isEmpty left then end right
 168 |   else if isEmpty right then end left
 169 |   else if toNanosecondsSinceEpoch (end left) >=
 170 |       toNanosecondsSinceEpoch (end right)
 171 |     then end left
 172 |     else end right
 173 | 
 174 | ||| Whether the union of two intervals is connected.
 175 | connectedRelationship : Interval -> Interval -> Bool
 176 | connectedRelationship left right =
 177 |   isEmpty left || isEmpty right || overlaps left right || isAdjacent left right
 178 | 
 179 | public export
 180 | isConnected : Interval -> Interval -> Bool
 181 | isConnected left right = connectedRelationship left right &&
 182 |   isValidInterval (unionStart left right) (unionEnd left right)
 183 | 
 184 | ||| Return the smallest interval containing both inputs when their union is
 185 | ||| statically known to be connected. Empty intervals are absorbed by the
 186 | ||| other input.
 187 | public export
 188 | union : (left, right : Interval) ->
 189 |         {auto 0 connected : So (isConnected left right)} ->
 190 |         Interval
 191 | union left right @{connected} = MkInterval
 192 |   (unionStart left right)
 193 |   (unionEnd left right)
 194 |   (andRight
 195 |     (connectedRelationship left right)
 196 |     (isValidInterval (unionStart left right) (unionEnd left right))
 197 |     connected)
 198 | 
 199 | public export
 200 | data UnionError = DisconnectedIntervals
 201 | 
 202 | ||| Return the connected union of intervals learned at runtime.
 203 | public export
 204 | refineUnion : (left, right : Interval) -> Either UnionError Interval
 205 | refineUnion left right = case choose (isConnected left right) of
 206 |   Left connected => Right (union left right @{connected})
 207 |   Right _ => Left DisconnectedIntervals
 208 | 
 209 | ||| Return the nonnegative fixed duration between the endpoints.
 210 | public export
 211 | duration : Interval -> Duration
 212 | duration value = difference (end value) (start value)
 213 | 
 214 | %runElab derive `{IntervalRep} [Eq, Ord]
 215 | 
 216 | public export
 217 | Show IntervalRep where
 218 |   show value = "interval " ++ show (start value) ++ " " ++ show (end value)
 219 | 
 220 | ||| A half-open timeline interval whose start, end, or both may be unbounded.
 221 | ||| `Nothing` denotes negative infinity for the start and positive infinity for
 222 | ||| the end.
 223 | ||| Decide whether optional endpoints are ordered as a valid interval.
 224 | public export
 225 | isValidUnboundedInterval : Maybe Instant -> Maybe Instant -> Bool
 226 | isValidUnboundedInterval (Just start) (Just end) =
 227 |   isValidInterval start end
 228 | isValidUnboundedInterval _ _ = True
 229 | 
 230 | public export
 231 | isValidUnboundedNanosecondInterval : Maybe Integer -> Maybe Integer -> Bool
 232 | isValidUnboundedNanosecondInterval (Just start) (Just end) = start <= end
 233 | isValidUnboundedNanosecondInterval _ _ = True
 234 | 
 235 | export
 236 | record UnboundedIntervalRep where
 237 |   constructor MkUnboundedInterval
 238 |   storedUnboundedStart : Maybe Instant
 239 |   storedUnboundedEnd : Maybe Instant
 240 |   0 valid : So
 241 |     (isValidUnboundedInterval storedUnboundedStart storedUnboundedEnd)
 242 | 
 243 | public export
 244 | UnboundedInterval : Type
 245 | UnboundedInterval = UnboundedIntervalRep
 246 | 
 247 | ||| Construct a statically validated interval with optional endpoints.
 248 | public export
 249 | unboundedInterval : (startNanoseconds, endNanoseconds : Maybe Integer) ->
 250 |                     {auto 0 valid : So (isValidUnboundedNanosecondInterval
 251 |                       startNanoseconds endNanoseconds)} ->
 252 |                     UnboundedInterval
 253 | unboundedInterval Nothing Nothing = MkUnboundedInterval Nothing Nothing Oh
 254 | unboundedInterval Nothing (Just end) = MkUnboundedInterval Nothing
 255 |   (Just (fromNanosecondsSinceEpoch end)) Oh
 256 | unboundedInterval (Just start) Nothing = MkUnboundedInterval
 257 |   (Just (fromNanosecondsSinceEpoch start)) Nothing Oh
 258 | unboundedInterval (Just start) (Just end) @{valid} = MkUnboundedInterval
 259 |   (Just (fromNanosecondsSinceEpoch start))
 260 |   (Just (fromNanosecondsSinceEpoch end))
 261 |   (rewrite instantNanosecondsRoundTrip start in
 262 |    rewrite instantNanosecondsRoundTrip end in valid)
 263 | 
 264 | ||| Validate optional endpoints learned at runtime.
 265 | public export
 266 | refineUnboundedInterval : (start, end : Maybe Instant) ->
 267 |                           Either IntervalError UnboundedInterval
 268 | refineUnboundedInterval (Just start) (Just end) =
 269 |   case choose (isValidUnboundedInterval (Just start) (Just end)) of
 270 |     Left valid => Right (MkUnboundedInterval (Just start) (Just end) valid)
 271 |     Right _ => Left (ReversedInterval start end)
 272 | refineUnboundedInterval Nothing Nothing =
 273 |   Right (MkUnboundedInterval Nothing Nothing Oh)
 274 | refineUnboundedInterval Nothing (Just end) =
 275 |   Right (MkUnboundedInterval Nothing (Just end) Oh)
 276 | refineUnboundedInterval (Just start) Nothing =
 277 |   Right (MkUnboundedInterval (Just start) Nothing Oh)
 278 | 
 279 | public export
 280 | unboundedStart : UnboundedInterval -> Maybe Instant
 281 | unboundedStart (MkUnboundedInterval value _ _) = value
 282 | 
 283 | public export
 284 | unboundedEnd : UnboundedInterval -> Maybe Instant
 285 | unboundedEnd (MkUnboundedInterval _ value _) = value
 286 | 
 287 | ||| Every unbounded interval carries erased evidence that its finite endpoints
 288 | ||| are ordered.
 289 | public export
 290 | 0 unboundedIntervalIsValid : (value : UnboundedInterval) ->
 291 |   So (isValidUnboundedInterval
 292 |     (unboundedStart value) (unboundedEnd value))
 293 | unboundedIntervalIsValid (MkUnboundedInterval _ _ valid) = valid
 294 | 
 295 | ||| Treat a bounded interval as an interval with two finite bounds.
 296 | public export
 297 | toUnboundedInterval : Interval -> UnboundedInterval
 298 | toUnboundedInterval value = MkUnboundedInterval (Just (start value))
 299 |   (Just (end value)) (intervalIsValid value)
 300 | 
 301 | ||| Recover a bounded interval only when both endpoints are finite.
 302 | public export
 303 | toBoundedInterval : UnboundedInterval -> Maybe Interval
 304 | toBoundedInterval
 305 |   (MkUnboundedInterval (Just start) (Just end) valid) =
 306 |     Just (MkInterval start end valid)
 307 | toBoundedInterval _ = Nothing
 308 | 
 309 | ||| Test membership using half-open endpoint semantics at every finite bound.
 310 | public export
 311 | unboundedContains : UnboundedInterval -> Instant -> Bool
 312 | unboundedContains value instant =
 313 |   case (unboundedStart value, unboundedEnd value) of
 314 |     (Nothing, Nothing) => True
 315 |     (Nothing, Just end) => instant < end
 316 |     (Just start, Nothing) => start <= instant
 317 |     (Just start, Just end) => start <= instant && instant < end
 318 | 
 319 | ||| Whether the interval contains no instants.
 320 | public export
 321 | unboundedIsEmpty : UnboundedInterval -> Bool
 322 | unboundedIsEmpty (MkUnboundedInterval (Just start) (Just end) _) =
 323 |   toNanosecondsSinceEpoch start == toNanosecondsSinceEpoch end
 324 | unboundedIsEmpty _ = False
 325 | 
 326 | ||| Whether an optional end lies after an optional start, treating `Nothing`
 327 | ||| as the appropriate infinity.
 328 | public export
 329 | unboundedEndAfterStart : Maybe Instant -> Maybe Instant -> Bool
 330 | unboundedEndAfterStart Nothing _ = True
 331 | unboundedEndAfterStart _ Nothing = True
 332 | unboundedEndAfterStart (Just end) (Just start) =
 333 |   toNanosecondsSinceEpoch start < toNanosecondsSinceEpoch end
 334 | 
 335 | ||| Whether two unbounded intervals share at least one instant.
 336 | public export
 337 | unboundedOverlaps : UnboundedInterval -> UnboundedInterval -> Bool
 338 | unboundedOverlaps left right =
 339 |   not (unboundedIsEmpty left) && not (unboundedIsEmpty right) &&
 340 |   unboundedEndAfterStart (unboundedEnd left) (unboundedStart right) &&
 341 |   unboundedEndAfterStart (unboundedEnd right) (unboundedStart left)
 342 | 
 343 | ||| Whether two optional bounds are finite and equal.
 344 | public export
 345 | finiteUnboundedBoundsEqual : Maybe Instant -> Maybe Instant -> Bool
 346 | finiteUnboundedBoundsEqual (Just left) (Just right) =
 347 |   toNanosecondsSinceEpoch left == toNanosecondsSinceEpoch right
 348 | finiteUnboundedBoundsEqual _ _ = False
 349 | 
 350 | ||| Whether two non-overlapping intervals touch at one finite endpoint.
 351 | public export
 352 | unboundedIsAdjacent : UnboundedInterval -> UnboundedInterval -> Bool
 353 | unboundedIsAdjacent left right =
 354 |   finiteUnboundedBoundsEqual (unboundedEnd left) (unboundedStart right) ||
 355 |   finiteUnboundedBoundsEqual (unboundedEnd right) (unboundedStart left)
 356 | 
 357 | laterStart : Maybe Instant -> Maybe Instant -> Maybe Instant
 358 | laterStart Nothing right = right
 359 | laterStart left Nothing = left
 360 | laterStart (Just left) (Just right) = Just
 361 |   (if toNanosecondsSinceEpoch left >= toNanosecondsSinceEpoch right
 362 |     then left else right)
 363 | 
 364 | earlierEnd : Maybe Instant -> Maybe Instant -> Maybe Instant
 365 | earlierEnd Nothing right = right
 366 | earlierEnd left Nothing = left
 367 | earlierEnd (Just left) (Just right) = Just
 368 |   (if toNanosecondsSinceEpoch left <= toNanosecondsSinceEpoch right
 369 |     then left else right)
 370 | 
 371 | earlierStart : Maybe Instant -> Maybe Instant -> Maybe Instant
 372 | earlierStart Nothing _ = Nothing
 373 | earlierStart _ Nothing = Nothing
 374 | earlierStart (Just left) (Just right) = Just
 375 |   (if toNanosecondsSinceEpoch left <= toNanosecondsSinceEpoch right
 376 |     then left else right)
 377 | 
 378 | laterEnd : Maybe Instant -> Maybe Instant -> Maybe Instant
 379 | laterEnd Nothing _ = Nothing
 380 | laterEnd _ Nothing = Nothing
 381 | laterEnd (Just left) (Just right) = Just
 382 |   (if toNanosecondsSinceEpoch left >= toNanosecondsSinceEpoch right
 383 |     then left else right)
 384 | 
 385 | ||| The later optional start bound selected for an intersection.
 386 | public export
 387 | unboundedIntersectionStart : UnboundedInterval -> UnboundedInterval ->
 388 |                              Maybe Instant
 389 | unboundedIntersectionStart left right =
 390 |   laterStart (unboundedStart left) (unboundedStart right)
 391 | 
 392 | ||| The earlier optional end bound selected for an intersection.
 393 | public export
 394 | unboundedIntersectionEnd : UnboundedInterval -> UnboundedInterval ->
 395 |                            Maybe Instant
 396 | unboundedIntersectionEnd left right =
 397 |   earlierEnd (unboundedEnd left) (unboundedEnd right)
 398 | 
 399 | ||| Whether two unbounded intervals have a valid, non-empty intersection.
 400 | public export
 401 | hasNonEmptyUnboundedIntersection : UnboundedInterval ->
 402 |                                    UnboundedInterval -> Bool
 403 | hasNonEmptyUnboundedIntersection left right =
 404 |   isValidUnboundedInterval
 405 |     (unboundedIntersectionStart left right)
 406 |     (unboundedIntersectionEnd left right) &&
 407 |   unboundedOverlaps left right
 408 | 
 409 | ||| Return the non-empty intersection when its existence is statically known.
 410 | public export
 411 | unboundedIntersection : (left, right : UnboundedInterval) ->
 412 |   {auto 0 intersects : So
 413 |     (hasNonEmptyUnboundedIntersection left right)} ->
 414 |   UnboundedInterval
 415 | unboundedIntersection left right @{intersects} = MkUnboundedInterval
 416 |   (unboundedIntersectionStart left right)
 417 |   (unboundedIntersectionEnd left right)
 418 |   (andLeft
 419 |     (isValidUnboundedInterval
 420 |       (unboundedIntersectionStart left right)
 421 |       (unboundedIntersectionEnd left right))
 422 |     (unboundedOverlaps left right)
 423 |     intersects)
 424 | 
 425 | ||| Return the non-empty intersection of unbounded intervals learned at
 426 | ||| runtime.
 427 | public export
 428 | refineUnboundedIntersection : (left, right : UnboundedInterval) ->
 429 |   Either IntersectionError UnboundedInterval
 430 | refineUnboundedIntersection left right =
 431 |   case choose (hasNonEmptyUnboundedIntersection left right) of
 432 |     Left intersects =>
 433 |       Right (unboundedIntersection left right @{intersects})
 434 |     Right _ => Left NoNonEmptyIntersection
 435 | 
 436 | ||| The optional start bound selected for a connected union.
 437 | public export
 438 | unboundedUnionStart : UnboundedInterval -> UnboundedInterval -> Maybe Instant
 439 | unboundedUnionStart left right =
 440 |   if unboundedIsEmpty left then unboundedStart right
 441 |   else if unboundedIsEmpty right then unboundedStart left
 442 |   else earlierStart (unboundedStart left) (unboundedStart right)
 443 | 
 444 | ||| The optional end bound selected for a connected union.
 445 | public export
 446 | unboundedUnionEnd : UnboundedInterval -> UnboundedInterval -> Maybe Instant
 447 | unboundedUnionEnd left right =
 448 |   if unboundedIsEmpty left then unboundedEnd right
 449 |   else if unboundedIsEmpty right then unboundedEnd left
 450 |   else laterEnd (unboundedEnd left) (unboundedEnd right)
 451 | 
 452 | ||| Whether the union of two unbounded intervals is connected.
 453 | unboundedConnectedRelationship : UnboundedInterval ->
 454 |                                  UnboundedInterval -> Bool
 455 | unboundedConnectedRelationship left right =
 456 |   unboundedIsEmpty left || unboundedIsEmpty right ||
 457 |   unboundedOverlaps left right || unboundedIsAdjacent left right
 458 | 
 459 | public export
 460 | unboundedIsConnected : UnboundedInterval -> UnboundedInterval -> Bool
 461 | unboundedIsConnected left right = unboundedConnectedRelationship left right &&
 462 |   isValidUnboundedInterval
 463 |     (unboundedUnionStart left right) (unboundedUnionEnd left right)
 464 | 
 465 | ||| Return the smallest interval containing both inputs when their union is
 466 | ||| statically known to be connected. Empty intervals are absorbed by the
 467 | ||| other input.
 468 | public export
 469 | unboundedUnion : (left, right : UnboundedInterval) ->
 470 |   {auto 0 connected : So (unboundedIsConnected left right)} ->
 471 |   UnboundedInterval
 472 | unboundedUnion left right @{connected} = MkUnboundedInterval
 473 |   (unboundedUnionStart left right)
 474 |   (unboundedUnionEnd left right)
 475 |   (andRight
 476 |     (unboundedConnectedRelationship left right)
 477 |     (isValidUnboundedInterval
 478 |       (unboundedUnionStart left right) (unboundedUnionEnd left right))
 479 |     connected)
 480 | 
 481 | ||| Return the connected union of unbounded intervals learned at runtime.
 482 | public export
 483 | refineUnboundedUnion : (left, right : UnboundedInterval) ->
 484 |   Either UnionError UnboundedInterval
 485 | refineUnboundedUnion left right =
 486 |   case choose (unboundedIsConnected left right) of
 487 |     Left connected => Right (unboundedUnion left right @{connected})
 488 |     Right _ => Left DisconnectedIntervals
 489 | 
 490 | ||| Return the duration when both endpoints are finite.
 491 | public export
 492 | unboundedDuration : UnboundedInterval -> Maybe Duration
 493 | unboundedDuration (MkUnboundedInterval (Just start) (Just end) _) =
 494 |   Just (difference end start)
 495 | unboundedDuration _ = Nothing
 496 | 
 497 | public export
 498 | Eq UnboundedIntervalRep where
 499 |   left == right = unboundedStart left == unboundedStart right &&
 500 |     unboundedEnd left == unboundedEnd right
 501 | 
 502 | compareStarts : Maybe Instant -> Maybe Instant -> Ordering
 503 | compareStarts Nothing Nothing = EQ
 504 | compareStarts Nothing (Just _) = LT
 505 | compareStarts (Just _) Nothing = GT
 506 | compareStarts (Just left) (Just right) = compare left right
 507 | 
 508 | compareEnds : Maybe Instant -> Maybe Instant -> Ordering
 509 | compareEnds Nothing Nothing = EQ
 510 | compareEnds Nothing (Just _) = GT
 511 | compareEnds (Just _) Nothing = LT
 512 | compareEnds (Just left) (Just right) = compare left right
 513 | 
 514 | public export
 515 | Ord UnboundedIntervalRep where
 516 |   compare left right = case compareStarts
 517 |     (unboundedStart left) (unboundedStart right) of
 518 |       EQ => compareEnds (unboundedEnd left) (unboundedEnd right)
 519 |       result => result
 520 | 
 521 | public export
 522 | Show UnboundedIntervalRep where
 523 |   show value = "unboundedInterval " ++ show (unboundedStart value) ++ " " ++
 524 |     show (unboundedEnd value)