@@ -0,0 +1,187 @@
1+module Data.Fin
2+
3+%default total
4+
5+||| Numbers strictly less than some bound. The name comes from "finite sets".
6+|||
7+||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
8+||| exceedingly inefficient at run time.
9+||| @ n the upper bound
10+data Fin : (n : Nat) -> Type where
11+ FZ : Fin (S k)
12+ FS : Fin k -> Fin (S k)
13+
14+instance Uninhabited (Fin Z) where
15+ uninhabited FZ impossible
16+ uninhabited (FS f) impossible
17+
18+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
19+FSInjective left _ Refl = Refl
20+
21+instance Eq (Fin n) where
22+ (==) FZ FZ = True
23+ (==) (FS k) (FS k') = k == k'
24+ (==) _ _ = False
25+
26+||| There are no elements of `Fin Z`
27+FinZAbsurd : Fin Z -> Void
28+FinZAbsurd FZ impossible
29+
30+FinZElim : Fin Z -> a
31+FinZElim x = void (FinZAbsurd x)
32+
33+||| Convert a Fin to a Nat
34+finToNat : Fin n -> Nat
35+finToNat FZ = Z
36+finToNat (FS k) = S (finToNat k)
37+
38+||| `finToNat` is injective
39+finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
40+finToNatInjective FZ FZ Refl = Refl
41+finToNatInjective (FS m) FZ Refl impossible
42+finToNatInjective FZ (FS n) Refl impossible
43+finToNatInjective (FS m) (FS n) prf =
44+ cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
45+
46+instance Cast (Fin n) Nat where
47+ cast x = finToNat x
48+
49+||| Convert a Fin to an Integer
50+finToInteger : Fin n -> Integer
51+finToInteger FZ = 0
52+finToInteger (FS k) = 1 + finToInteger k
53+
54+instance Cast (Fin n) Integer where
55+ cast x = finToInteger x
56+
57+||| Weaken the bound on a Fin by 1
58+weaken : Fin n -> Fin (S n)
59+weaken FZ = FZ
60+weaken (FS k) = FS (weaken k)
61+
62+||| Weaken the bound on a Fin by some amount
63+weakenN : (n : Nat) -> Fin m -> Fin (m + n)
64+weakenN n FZ = FZ
65+weakenN n (FS f) = FS (weakenN n f)
66+
67+||| Attempt to tighten the bound on a Fin.
68+||| Return `Left` if the bound could not be tightened, or `Right` if it could.
69+strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
70+strengthen {n = S k} FZ = Right FZ
71+strengthen {n = S k} (FS i) with (strengthen i)
72+ strengthen (FS k) | Left x = Left (FS x)
73+ strengthen (FS k) | Right x = Right (FS x)
74+strengthen f = Left f
75+
76+||| Add some natural number to a Fin, extending the bound accordingly
77+||| @ n the previous bound
78+||| @ m the number to increase the Fin by
79+shift : (m : Nat) -> Fin n -> Fin (m + n)
80+shift Z f = f
81+shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
82+
83+||| The largest element of some Fin type
84+last : Fin (S n)
85+last {n=Z} = FZ
86+last {n=S _} = FS last
87+
88+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
89+FSinjective Refl = Refl
90+
91+instance Ord (Fin n) where
92+ compare FZ FZ = EQ
93+ compare FZ (FS _) = LT
94+ compare (FS _) FZ = GT
95+ compare (FS x) (FS y) = compare x y
96+
97+instance MinBound (Fin (S n)) where
98+ minBound = FZ
99+
100+instance MaxBound (Fin (S n)) where
101+ maxBound = last
102+
103+
104+||| Add two Fins, extending the bound
105+(+) : Fin n -> Fin m -> Fin (n + m)
106+(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
107+(+) (FS f) f' = FS (f + f')
108+
109+||| Substract two Fins, keeping the bound of the minuend
110+(-) : Fin n -> Fin m -> Fin n
111+FZ - _ = FZ
112+f - FZ = f
113+(FS f) - (FS f') = weaken $ f - f'
114+
115+||| Multiply two Fins, extending the bound
116+(*) : Fin n -> Fin m -> Fin (n * m)
117+(*) {n=Z} f f' = FinZElim f
118+(*) {m=Z} f f' = FinZElim f'
119+(*) {n=S n} {m=S m} FZ f' = FZ
120+(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')
121+
122+-- Construct a Fin from an integer literal which must fit in the given Fin
123+
124+natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
125+natToFin Z (S j) = Just FZ
126+natToFin (S k) (S j) with (natToFin k j)
127+ | Just k' = Just (FS k')
128+ | Nothing = Nothing
129+natToFin _ _ = Nothing
130+
131+integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
132+integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
133+integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
134+
135+||| Allow overloading of Integer literals for Fin.
136+||| @ x the Integer that the user typed
137+||| @ prf an automatically-constructed proof that `x` is in bounds
138+fromInteger : (x : Integer) ->
139+ {default ItIsJust
140+ prf : (IsJust (integerToFin x n))} ->
141+ Fin n
142+fromInteger {n} x {prf} with (integerToFin x n)
143+ fromInteger {n} x {prf = ItIsJust} | Just y = y
144+
145+%language ErrorReflection
146+
147+total
148+finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
149+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
150+ = Just [ TextPart "When using", TermPart n
151+ , TextPart "as a literal for a"
152+ , TermPart `(Fin ~m)
153+ , SubReport [ TextPart "Could not show that"
154+ , TermPart n
155+ , TextPart "is less than"
156+ , TermPart m
157+ ]
158+ ]
159+finFromIntegerErrors _ = Nothing
160+
161+%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
162+
163+instance Enum (Fin (S n)) where
164+ pred FZ = FZ
165+ pred (FS n) = weaken n
166+ succ n = case strengthen (FS n) of
167+ Left _ => last
168+ Right k => k
169+ toNat n = cast n
170+ fromNat {n=n} m = case natToFin m (S n) of
171+ Just k => k
172+ Nothing => last
173+
174+--------------------------------------------------------------------------------
175+-- DecEq
176+--------------------------------------------------------------------------------
177+
178+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
179+FZNotFS Refl impossible
180+
181+instance DecEq (Fin n) where
182+ decEq FZ FZ = Yes Refl
183+ decEq FZ (FS f) = No FZNotFS
184+ decEq (FS f) FZ = No $ negEqSym FZNotFS
185+ decEq (FS f) (FS f') with (decEq f f')
186+ | Yes p = Yes $ cong p
187+ | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h