module Std.Fin

import Std.Foundation

-- Bounded indices (Language Platform PRD §28.2 Numerics, LP-801).
--
-- `StdFin n` is a natural strictly below `n`, carried in the TYPE. An index
-- that cannot exist cannot be built, so an out-of-range access is not a
-- runtime error to handle: it is a program the checker rejects. The bound is
-- erased, so nothing here costs anything at runtime.

family StdFin : Type 0
index erased stdFinBound : Nat
constructor StdFinZero
field erased stdFinZeroBound : Nat
result (succ stdFinZeroBound)
constructor StdFinNext
field erased stdFinNextBound : Nat
recursive unrestricted stdFinNextPredecessor
recursive-index stdFinNextBound
result (succ stdFinNextBound)
end-family

-- The index as an ordinary natural.
def stdFinToNatural =
  (lambda erased bound : Nat .
    (lambda unrestricted index : (family StdFin bound) .
      (eliminate StdFin
        (lambda erased motiveBound : Nat .
          (lambda unrestricted value : (family StdFin motiveBound) . Nat))
        index
        (branch StdFinZero zeroBound . zero)
        (branch StdFinNext nextBound predecessor induction . (succ induction)))))

-- The smallest index of a non-empty range.
def stdFinFirst =
  (lambda erased bound : Nat .
    (constructor StdFin StdFinZero bound))

-- The next index up, in a range one larger.
def stdFinNextOf =
  (lambda erased bound : Nat .
    (lambda unrestricted index : (family StdFin bound) .
      (constructor StdFin StdFinNext bound index)))

-- Is this the first index?
def stdFinIsFirst =
  (lambda erased bound : Nat .
    (lambda unrestricted index : (family StdFin bound) .
      (eliminate StdFin
        (lambda erased motiveBound : Nat .
          (lambda unrestricted value : (family StdFin motiveBound) . (family StdBool)))
        index
        (branch StdFinZero zeroBound . (constructor StdBool StdTrue))
        (branch StdFinNext nextBound predecessor induction . (constructor StdBool StdFalse)))))