git.iko.soy/Idris-dev
on fbb201c help sign in
Idris-dev/libs/base/Data/Fin.idr
219 lines 6.9 kB history raw
1module Data.Fin
3%default total
4%access public
6||| Numbers strictly less than some bound. The name comes from "finite sets".
7|||
8||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
9||| exceedingly inefficient at run time.
10||| @ n the upper bound
11data Fin : (n : Nat) -> Type where
12 FZ : Fin (S k)
13 FS : Fin k -> Fin (S k)
15instance Uninhabited (Fin Z) where
16 uninhabited FZ impossible
17 uninhabited (FS f) impossible
19FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n
20FSInjective left _ Refl = Refl
22instance Eq (Fin n) where
23 (==) FZ FZ = True
24 (==) (FS k) (FS k') = k == k'
25 (==) _ _ = False
27||| There are no elements of `Fin Z`
28FinZAbsurd : Fin Z -> Void
29FinZAbsurd FZ impossible
31FinZElim : Fin Z -> a
32FinZElim x = void (FinZAbsurd x)
34||| Convert a Fin to a Nat
35finToNat : Fin n -> Nat
36finToNat FZ = Z
37finToNat (FS k) = S (finToNat k)
39||| `finToNat` is injective
40finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
41finToNatInjective FZ FZ Refl = Refl
42finToNatInjective (FS m) FZ Refl impossible
43finToNatInjective FZ (FS n) Refl impossible
44finToNatInjective (FS m) (FS n) prf =
45 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
47instance Cast (Fin n) Nat where
48 cast x = finToNat x
50||| Convert a Fin to an Integer
51finToInteger : Fin n -> Integer
52finToInteger FZ = 0
53finToInteger (FS k) = 1 + finToInteger k
55instance Cast (Fin n) Integer where
56 cast x = finToInteger x
58||| Weaken the bound on a Fin by 1
59weaken : Fin n -> Fin (S n)
60weaken FZ = FZ
61weaken (FS k) = FS (weaken k)
63||| Weaken the bound on a Fin by some amount
64weakenN : (n : Nat) -> Fin m -> Fin (m + n)
65weakenN n FZ = FZ
66weakenN n (FS f) = FS (weakenN n f)
68||| Attempt to tighten the bound on a Fin.
69||| Return `Left` if the bound could not be tightened, or `Right` if it could.
70strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
71strengthen {n = S k} FZ = Right FZ
72strengthen {n = S k} (FS i) with (strengthen i)
73 strengthen (FS k) | Left x = Left (FS x)
74 strengthen (FS k) | Right x = Right (FS x)
75strengthen f = Left f
77||| Add some natural number to a Fin, extending the bound accordingly
78||| @ n the previous bound
79||| @ m the number to increase the Fin by
80shift : (m : Nat) -> Fin n -> Fin (m + n)
81shift Z f = f
82shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)
84||| The largest element of some Fin type
85last : Fin (S n)
86last {n=Z} = FZ
87last {n=S _} = FS last
89total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
90FSinjective Refl = Refl
92instance Ord (Fin n) where
93 compare FZ FZ = EQ
94 compare FZ (FS _) = LT
95 compare (FS _) FZ = GT
96 compare (FS x) (FS y) = compare x y
98instance MinBound (Fin (S n)) where
99 minBound = FZ
101instance MaxBound (Fin (S n)) where
102 maxBound = last
105||| Add two Fins, extending the bound
106(+) : Fin n -> Fin m -> Fin (n + m)
107(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
108(+) (FS f) f' = FS (f + f')
110||| Substract two Fins, keeping the bound of the minuend
111(-) : Fin n -> Fin m -> Fin n
112FZ - _ = FZ
113f - FZ = f
114(FS f) - (FS f') = weaken $ f - f'
116||| Multiply two Fins, extending the bound
117(*) : Fin n -> Fin m -> Fin (n * m)
118(*) {n=Z} f f' = FinZElim f
119(*) {m=Z} f f' = FinZElim f'
120(*) {n=S n} {m=S m} FZ f' = FZ
121(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')
123-- Construct a Fin from an integer literal which must fit in the given Fin
125natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
126natToFin Z (S j) = Just FZ
127natToFin (S k) (S j) with (natToFin k j)
128 | Just k' = Just (FS k')
129 | Nothing = Nothing
130natToFin _ _ = Nothing
132||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
133||| @n The upper bound of the Fin
134integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
135integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
136integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
138||| Allow overloading of Integer literals for Fin.
139||| @ x the Integer that the user typed
140||| @ prf an automatically-constructed proof that `x` is in bounds
141fromInteger : (x : Integer) ->
142 {default ItIsJust
143 prf : (IsJust (integerToFin x n))} ->
144 Fin n
145fromInteger {n} x {prf} with (integerToFin x n)
146 fromInteger {n} x {prf = ItIsJust} | Just y = y
148%language ErrorReflection
150||| Attempt to convert a reflected (fromInteger n) to a Nat
151total private
152getNat' : TT -> Maybe TT
153getNat' `(fromInteger ~(TConst (BI c)) : Nat) = Just $ quote (the Nat (fromInteger c))
154getNat' _ = Nothing
156||| Attempt to convert a reflected (fromInteger n) to a Nat. Return
157||| the original term on failure.
158total private
159getNat : TT -> TT
160getNat tm = maybe tm id $ getNat' tm
162total private
163mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
164mkFinIntegerErr lit finSize subErr
165 = Just [ TextPart "When using", TermPart lit
166 , TextPart "as a literal for a"
167 , TermPart `(Fin ~(getNat finSize))
168 , SubReport subErr
169 ]
170total
171finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
172finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
173 = mkFinIntegerErr (TConst c) m
174 [ TermPart (TConst c)
175 , TextPart "is not strictly less than"
176 , TermPart (getNat m)
177 ]
178finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
179 = mkFinIntegerErr (P Bound n t) m
180 [ TextPart "Could not show that", TermPart (P Bound n t)
181 , TextPart "is less than", TermPart (getNat m)
182 , TextPart "because", TermPart (P Bound n t)
183 , TextPart "is a bound variable instead of a constant"
184 , TermPart `(Integer : Type)
185 ]
186finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
187 = mkFinIntegerErr n m
188 [ TextPart "Could not show that" , TermPart n
189 , TextPart "is less than" , TermPart (getNat m)
190 ]
191finFromIntegerErrors _ = Nothing
193%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
195instance Enum (Fin (S n)) where
196 pred FZ = FZ
197 pred (FS n) = weaken n
198 succ n = case strengthen (FS n) of
199 Left _ => last
200 Right k => k
201 toNat n = cast n
202 fromNat {n=n} m = case natToFin m (S n) of
203 Just k => k
204 Nothing => last
206--------------------------------------------------------------------------------
207-- DecEq
208--------------------------------------------------------------------------------
210total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
211FZNotFS Refl impossible
213instance DecEq (Fin n) where
214 decEq FZ FZ = Yes Refl
215 decEq FZ (FS f) = No FZNotFS
216 decEq (FS f) FZ = No $ negEqSym FZNotFS
217 decEq (FS f) (FS f') with (decEq f f')
218 | Yes p = Yes $ cong p
219 | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h