@@ -0,0 +1,187 @@
5+||| Numbers strictly less than some bound. The name comes from "finite sets".
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
12+ FS : Fin k -> Fin (S k)
14+instance Uninhabited (Fin Z) where
15+ uninhabited FZ impossible
16+ uninhabited (FS f) impossible
18+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
19+FSInjective left _ Refl = Refl
21+instance Eq (Fin n) where
23+ (==) (FS k) (FS k') = k == k'
26+||| There are no elements of `Fin Z`
27+FinZAbsurd : Fin Z -> Void
28+FinZAbsurd FZ impossible
31+FinZElim x = void (FinZAbsurd x)
33+||| Convert a Fin to a Nat
34+finToNat : Fin n -> Nat
36+finToNat (FS k) = S (finToNat k)
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))
46+instance Cast (Fin n) Nat where
49+||| Convert a Fin to an Integer
50+finToInteger : Fin n -> Integer
52+finToInteger (FS k) = 1 + finToInteger k
54+instance Cast (Fin n) Integer where
55+ cast x = finToInteger x
57+||| Weaken the bound on a Fin by 1
58+weaken : Fin n -> Fin (S n)
60+weaken (FS k) = FS (weaken k)
62+||| Weaken the bound on a Fin by some amount
63+weakenN : (n : Nat) -> Fin m -> Fin (m + n)
65+weakenN n (FS f) = FS (weakenN n f)
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)
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)
81+shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
83+||| The largest element of some Fin type
86+last {n=S _} = FS last
88+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
89+FSinjective Refl = Refl
91+instance Ord (Fin n) where
93+ compare FZ (FS _) = LT
94+ compare (FS _) FZ = GT
95+ compare (FS x) (FS y) = compare x y
97+instance MinBound (Fin (S n)) where
100+instance MaxBound (Fin (S n)) where
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')
109+||| Substract two Fins, keeping the bound of the minuend
110+(-) : Fin n -> Fin m -> Fin n
113+(FS f) - (FS f') = weaken $ f - f'
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')
122+-- Construct a Fin from an integer literal which must fit in the given Fin
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')
129+natToFin _ _ = Nothing
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
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) ->
140+ prf : (IsJust (integerToFin x n))} ->
142+fromInteger {n} x {prf} with (integerToFin x n)
143+ fromInteger {n} x {prf = ItIsJust} | Just y = y
145+%language ErrorReflection
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"
155+ , TextPart "is less than"
159+finFromIntegerErrors _ = Nothing
161+%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
163+instance Enum (Fin (S n)) where
165+ pred (FS n) = weaken n
166+ succ n = case strengthen (FS n) of
170+ fromNat {n=n} m = case natToFin m (S n) of
174+--------------------------------------------------------------------------------
176+--------------------------------------------------------------------------------
178+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
179+FZNotFS Refl impossible
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