git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/base/Data/Fin.idr
217 lines 6.8 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
132integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
133integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
134integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
136||| Allow overloading of Integer literals for Fin.
137||| @ x the Integer that the user typed
138||| @ prf an automatically-constructed proof that `x` is in bounds
139fromInteger : (x : Integer) ->
140 {default ItIsJust
141 prf : (IsJust (integerToFin x n))} ->
142 Fin n
143fromInteger {n} x {prf} with (integerToFin x n)
144 fromInteger {n} x {prf = ItIsJust} | Just y = y
146%language ErrorReflection
148||| Attempt to convert a reflected (fromInteger n) to a Nat
149total private
150getNat' : TT -> Maybe TT
151getNat' `(fromInteger ~(TConst (BI c)) : Nat) = Just $ quote (the Nat (fromInteger c))
152getNat' _ = Nothing
154||| Attempt to convert a reflected (fromInteger n) to a Nat. Return
155||| the original term on failure.
156total private
157getNat : TT -> TT
158getNat tm = maybe tm id $ getNat' tm
160total private
161mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
162mkFinIntegerErr lit finSize subErr
163 = Just [ TextPart "When using", TermPart lit
164 , TextPart "as a literal for a"
165 , TermPart `(Fin ~(getNat finSize))
166 , SubReport subErr
167 ]
168total
169finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
170finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
171 = mkFinIntegerErr (TConst c) m
172 [ TermPart (TConst c)
173 , TextPart "is not strictly less than"
174 , TermPart (getNat m)
175 ]
176finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
177 = mkFinIntegerErr (P Bound n t) m
178 [ TextPart "Could not show that", TermPart (P Bound n t)
179 , TextPart "is less than", TermPart (getNat m)
180 , TextPart "because", TermPart (P Bound n t)
181 , TextPart "is a bound variable instead of a constant"
182 , TermPart `(Integer : Type)
183 ]
184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
185 = mkFinIntegerErr n m
186 [ TextPart "Could not show that" , TermPart n
187 , TextPart "is less than" , TermPart (getNat m)
188 ]
189finFromIntegerErrors _ = Nothing
191%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
193instance Enum (Fin (S n)) where
194 pred FZ = FZ
195 pred (FS n) = weaken n
196 succ n = case strengthen (FS n) of
197 Left _ => last
198 Right k => k
199 toNat n = cast n
200 fromNat {n=n} m = case natToFin m (S n) of
201 Just k => k
202 Nothing => last
204--------------------------------------------------------------------------------
205-- DecEq
206--------------------------------------------------------------------------------
208total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
209FZNotFS Refl impossible
211instance DecEq (Fin n) where
212 decEq FZ FZ = Yes Refl
213 decEq FZ (FS f) = No FZNotFS
214 decEq (FS f) FZ = No $ negEqSym FZNotFS
215 decEq (FS f) (FS f') with (decEq f f')
216 | Yes p = Yes $ cong p
217 | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h