Std.Fin

1module Std.Fin
2
3import Std.Foundation
4
5-- Bounded indices (Language Platform PRD §28.2 Numerics, LP-801).
6--
7-- `StdFin n` is a natural strictly below `n`, carried in the TYPE. An index
8-- that cannot exist cannot be built, so an out-of-range access is not a
9-- runtime error to handle: it is a program the checker rejects. The bound is
10-- erased, so nothing here costs anything at runtime.
11
12family StdFin : Type 0
13index erased stdFinBound : Nat
14constructor StdFinZero
15field erased stdFinZeroBound : Nat
16result (succ stdFinZeroBound)
17constructor StdFinNext
18field erased stdFinNextBound : Nat
19recursive unrestricted stdFinNextPredecessor
20recursive-index stdFinNextBound
21result (succ stdFinNextBound)
22end-family
23
24-- The index as an ordinary natural.
25def stdFinToNatural =
26  (lambda erased bound : Nat .
27    (lambda unrestricted index : (family StdFin bound) .
28      (eliminate StdFin
29        (lambda erased motiveBound : Nat .
30          (lambda unrestricted value : (family StdFin motiveBound) . Nat))
31        index
32        (branch StdFinZero zeroBound . zero)
33        (branch StdFinNext nextBound predecessor induction . (succ induction)))))
34
35-- The smallest index of a non-empty range.
36def stdFinFirst =
37  (lambda erased bound : Nat .
38    (constructor StdFin StdFinZero bound))
39
40-- The next index up, in a range one larger.
41def stdFinNextOf =
42  (lambda erased bound : Nat .
43    (lambda unrestricted index : (family StdFin bound) .
44      (constructor StdFin StdFinNext bound index)))
45
46-- Is this the first index?
47def stdFinIsFirst =
48  (lambda erased bound : Nat .
49    (lambda unrestricted index : (family StdFin bound) .
50      (eliminate StdFin
51        (lambda erased motiveBound : Nat .
52          (lambda unrestricted value : (family StdFin motiveBound) . (family StdBool)))
53        index
54        (branch StdFinZero zeroBound . (constructor StdBool StdTrue))
55        (branch StdFinNext nextBound predecessor induction . (constructor StdBool StdFalse)))))