0 | ||| This module provides several ways to safely index into an
  1 | ||| array of known size. All conversions between different index
  2 | ||| types are optimized away by the compiler, because they are
  3 | ||| all of the same structure during code generation: An encoding
  4 | ||| of natural numbers which the Idris compiler converts to a
  5 | ||| native integer representation.
  6 | |||
  7 | ||| The main type for indexing into an array of size `n` is `Fin n`,
  8 | ||| representing a natural number strictly smaller than `n`.
  9 | |||
 10 | ||| As an alternative, we can use a natural number `k` directly, together
 11 | ||| with a proof of type `LT k n`, showing that `k` is strictly smaller
 12 | ||| than `n`. Such numbers can be converted directly to `Fin n` by means
 13 | ||| of function `Data.Nat.natToFinLT`. This way of indexing is very
 14 | ||| useful for iterating over the whole array from then end: We start
 15 | ||| with `n` itself together with an erased proof of type `LTE n n`, which
 16 | ||| can be generated automatically. By pattern matching on the current
 17 | ||| position, we can safely access all positions in the array until
 18 | ||| we arrive at 0. See the implementation of `foldr` (a private
 19 | ||| function called `foldrI`) in module `Data.Array.Indexed` for an
 20 | ||| example how this is used.
 21 | |||
 22 | ||| It is only slightly harder to iterate over an array from the
 23 | ||| front. This is where data type `Ix m n` comes into play: It's
 24 | ||| another way of saying that `m <= n` holds, but it works in
 25 | ||| the oposite direction than `LTE`: It's zero constructor `IZ` proofs
 26 | ||| that `n <= n` for all `n`, while its successor constructor
 27 | ||| proofs that from `S k <= n` follows `k <= n`. This means, that
 28 | ||| for a given `k`, a values of type `Ix k n` corresponds to the
 29 | ||| values `n - k`. This allows us to recurse over a natural number
 30 | ||| while keeping an auto-implicit proof of type `Ix k n`, and use
 31 | ||| this proof for indexing into the array.
 32 | ||| See the implementation of `foldl` (a private
 33 | ||| function called `foldlI`) in module `Data.Array.Indexed` for an
 34 | ||| example how this is used.
 35 | module Data.Array.Index
 36 |
 37 | import Control.Order
 38 | import Data.So
 39 | import Decidable.Equality
 40 | import public Data.DPair
 41 | import public Data.Fin
 42 | import public Data.Maybe0
 43 | import public Data.Nat
 44 |
 45 | %default total
 46 |
 47 | export
 48 | 0 ltLemma : (0 k,m,n : Nat) -> k + S m === n -> LT k n
 49 | ltLemma 0     m (S m) Refl = %search
 50 | ltLemma (S k) m (S n) prf  = LTESucc $ ltLemma k m n (injective prf)
 51 | ltLemma (S k) m 0     prf  = absurd prf
 52 |
 53 | export
 54 | 0 lteLemma : (0 k,m,n : Nat) -> k + m === n -> LTE k n
 55 | lteLemma 0     m m     Refl = %search
 56 | lteLemma (S k) m (S n) prf  = LTESucc $ lteLemma k m n (injective prf)
 57 | lteLemma (S k) m 0     prf  = absurd prf
 58 |
 59 | export
 60 | 0 lteSuccPlus : (k : Nat) -> LTE (S k) (k + S m)
 61 | lteSuccPlus 0     = LTESucc LTEZero
 62 | lteSuccPlus (S k) = LTESucc $ lteSuccPlus k
 63 |
 64 | ||| Generates the list of all `Fin n` in linear type.
 65 | |||
 66 | ||| This is a lot faster than `Data.Fin.allFins`, which runs in quadratic
 67 | ||| time.
 68 | export
 69 | allFinsFast : (n : Nat) -> List (Fin n)
 70 | allFinsFast 0 = []
 71 | allFinsFast (S n) = go [] last
 72 |   where
 73 |     go : List (Fin $ S n) -> Fin (S n) -> List (Fin $ S n)
 74 |     go xs FZ     = FZ :: xs
 75 |     go xs (FS x) = go (FS x :: xs) (assert_smaller (FS x) $ weaken x)
 76 |
 77 | --------------------------------------------------------------------------------
 78 | --          Suffix
 79 | --------------------------------------------------------------------------------
 80 |
 81 | public export
 82 | data Suffix : (xs,ys : List a) -> Type where
 83 |   Same   : Suffix xs xs
 84 |   Uncons : Suffix (x::xs) ys -> Suffix xs ys
 85 |
 86 | public export
 87 | suffixToNat : Suffix xs ys -> Nat
 88 | suffixToNat Same       = 0
 89 | suffixToNat (Uncons x) = S $ suffixToNat x
 90 |
 91 | export
 92 | 0 suffixLemma : (s : Suffix xs ys) -> suffixToNat s + length xs === length ys
 93 | suffixLemma Same       = Refl
 94 | suffixLemma (Uncons x) = trans (plusSuccRightSucc _ _) $ suffixLemma x
 95 |
 96 | export
 97 | 0 suffixLT : (s : Suffix (x::xs) ys) -> LT (suffixToNat s) (length ys)
 98 | suffixLT s = ltLemma _ _ _ $ suffixLemma s
 99 |
100 | public export
101 | suffixToFin : Suffix (x::xs) ys -> Fin (length ys)
102 | suffixToFin x = natToFinLT (suffixToNat x) @{suffixLT x}
103 |
104 | --------------------------------------------------------------------------------
105 | --          Ix
106 | --------------------------------------------------------------------------------
107 |
108 | ||| A data type for safely indexing into an array from the
109 | ||| front during in a fuction recursing on natural number `m`.
110 | |||
111 | ||| This is another way to proof that `m <= n`.
112 | public export
113 | data Ix : (m,n : Nat) -> Type where
114 |   IZ : Ix n n
115 |   IS : Ix (S m) n -> Ix m n
116 |
117 | ||| O(1) conversion from `Ix m n` to `Nat`. The result equals `n - m`.
118 | public export
119 | ixToNat : Ix m n -> Nat
120 | ixToNat IZ     = 0
121 | ixToNat (IS n) = S $ ixToNat n
122 |
123 | ||| If `m <= n` then `S m <= S n`.
124 | public export
125 | succIx : Ix m n -> Ix (S m) (S n)
126 | succIx IZ     = IZ
127 | succIx (IS x) = IS (succIx x)
128 |
129 | ||| If `m <= n` then `o+m <= o+n`.
130 | public export
131 | plusIx : Ix m n -> Ix (o + m) (o + n)
132 | plusIx IZ     = IZ
133 | plusIx (IS x) = IS $ rewrite plusSuccRightSucc o m in plusIx x
134 |
135 | ||| If `m <= n` then `m+o <= n*o`.
136 | public export
137 | symPlusIx : Ix m n -> Ix (m+o) (n+o)
138 | symPlusIx x =
139 |   rewrite plusCommutative m o in
140 |   rewrite plusCommutative n o in plusIx x
141 |
142 | ||| Convert a natural number to the corresponding `Ix 0 n`
143 | ||| so that `n === ixToNat (natToIx n)` as shown in
144 | ||| `ixLemma`.
145 | public export
146 | natToIx : (n : Nat) -> Ix 0 n
147 | natToIx 0     = IZ
148 | natToIx (S k) = IS $ succIx (natToIx k)
149 |
150 | public export
151 | offset : (0 n : Nat) -> (o : Nat) -> Ix n (o+n)
152 | offset n o = symPlusIx {o = n} $ natToIx o
153 |
154 | ||| Convert a natural number to the corresponding `Ix 1 (S n)`,
155 | ||| the largest value strictly smaller than `S n`.
156 | |||
157 | ||| This is similar to `Data.Fin.last`.
158 | public export
159 | natToIx1 : (n : Nat) -> Ix 1 (S n)
160 | natToIx1 n = case natToIx (S n) of
161 |   IS x => x
162 |
163 | ||| Proof that for an index `x` of type `Ix m n` `ixToNat x` equals `n - m`.
164 | export
165 | 0 ixLemma : (x : Ix m n) -> ixToNat x + m === n
166 | ixLemma IZ     = Refl
167 | ixLemma (IS v) = trans (plusSuccRightSucc _ _) $ ixLemma v
168 |
169 | ||| Proof an `Ix (S m) n` corresponds to a natural number
170 | ||| strictly smaller than `n` and can therefore be used as an index
171 | ||| into an array of size `n`.
172 | export
173 | 0 ixLT : (x : Ix (S m) n) -> LT (ixToNat x) n
174 | ixLT s = ltLemma _ _ _ $ ixLemma s
175 |
176 | ||| Proof an `Ix m n` corresponds to a natural number
177 | ||| smaller than or equal to `n
178 | export
179 | 0 ixLTE : (x : Ix m n) -> LTE (ixToNat x) n
180 | ixLTE s = lteLemma _ _ _ $ ixLemma s
181 |
182 | ||| From lemma `ixLT` follows, that we can convert an `Ix (S m) n` to
183 | ||| a `Fin n` corresponding to the same natural numbers. All conversions
184 | ||| involved are optimized away by the identity optimizer during code
185 | ||| generation.
186 | public export
187 | ixToFin : Ix (S m) n -> Fin n
188 | ixToFin x = natToFinLT (ixToNat x) @{ixLT x}
189 |
190 | --------------------------------------------------------------------------------
191 | --          Sublength
192 | --------------------------------------------------------------------------------
193 |
194 | export
195 | 0 finToNatLT : (x : Fin n) -> LT (finToNat x) n
196 | finToNatLT FZ     = %search
197 | finToNatLT (FS x) = LTESucc $ finToNatLT x
198 |
199 | ||| This type is used to cut off a portion of
200 | ||| a `ByteString`. It must be no larger than the number
201 | ||| of elements in the ByteString
202 | public export
203 | 0 SubLength : Nat -> Type
204 | SubLength n = Subset Nat (`LTE` n)
205 |
206 | export %inline
207 | sublength : (k : Nat) -> (0 lte : LTE k n) => SubLength n
208 | sublength k = Element k lte
209 |
210 | export %inline
211 | fromFin : Fin n -> SubLength n
212 | fromFin x = Element (finToNat x) (lteSuccLeft $ finToNatLT x)
213 |
214 | export %inline
215 | fromIx : Ix m n -> SubLength n
216 | fromIx x = Element (ixToNat x) (ixLTE x)
217 |
218 | --------------------------------------------------------------------------------
219 | --          Hints
220 | --------------------------------------------------------------------------------
221 |
222 | export %hint
223 | 0 refl : LTE n n
224 | refl = reflexive
225 |
226 | export %hint
227 | 0 lsl : (p : LTE (S m) n) => LTE m n
228 | lsl = lteSuccLeft p
229 |
230 | --------------------------------------------------------------------------------
231 | --          Proofs
232 | --------------------------------------------------------------------------------
233 |
234 | export
235 | 0 lteOpReflectsLTE : (m,n : Nat) -> (m <= n) === True -> LTE m n
236 | lteOpReflectsLTE 0     (S k) prf = LTEZero
237 | lteOpReflectsLTE (S k) (S j) prf = LTESucc (lteOpReflectsLTE k j prf)
238 | lteOpReflectsLTE 0 0         prf = LTEZero
239 | lteOpReflectsLTE (S k) Z     prf impossible
240 |
241 | export
242 | 0 ltOpReflectsLT : (m,n : Nat) -> (m < n) === True -> LT m n
243 | ltOpReflectsLT 0     (S k) prf = LTESucc LTEZero
244 | ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
245 | ltOpReflectsLT Z Z         prf impossible
246 | ltOpReflectsLT (S k) Z     prf impossible
247 |
248 | export
249 | 0 eqOpReflectsEquals : (m,n : Nat) -> (m == n) === True -> m === n
250 | eqOpReflectsEquals 0     0     prf = Refl
251 | eqOpReflectsEquals (S k) (S j) prf = cong S $ eqOpReflectsEquals k j prf
252 | eqOpReflectsEquals Z     (S k) prf impossible
253 | eqOpReflectsEquals (S k) Z     prf impossible
254 |
255 | --------------------------------------------------------------------------------
256 | --          Proofs
257 | --------------------------------------------------------------------------------
258 |
259 | export
260 | tryLT : {n : _} -> (k : Nat) -> Maybe0 (LT k n)
261 | tryLT k with (k < n) proof eq
262 |   _ | True  = Just0 $ ltOpReflectsLT k n eq
263 |   _ | False = Nothing0
264 |
265 | export
266 | tryLTE : {n : _} -> (k : Nat) -> Maybe0 (LTE k n)
267 | tryLTE 0     = Just0 %search
268 | tryLTE (S k) = tryLT k
269 |
270 | ||| Tries to convert a natural number to a `Fin k`.
271 | export
272 | tryNatToFin : {k : _} -> Nat -> Maybe (Fin k)
273 | tryNatToFin n with (n < k) proof eq
274 |   _ | True  = Just $ natToFinLT n @{ltOpReflectsLT n k eq}
275 |   _ | False = Nothing
276 |
277 | ||| Tries to convert a `Fin n` to a `Fin k`.
278 | export %inline
279 | tryFinToFin : {k : _} -> Fin n -> Maybe (Fin k)
280 | tryFinToFin = tryNatToFin . finToNat
281 |
282 | export
283 | 0 minusLTE : (k,m : Nat) -> LTE (k `minus` m) k
284 | minusLTE 0     m     = LTEZero
285 | minusLTE (S k) 0     = reflexive
286 | minusLTE (S k) (S j) = lteSuccRight $ minusLTE k j
287 |
288 | export
289 | 0 minusFinLT : (n : Nat) -> (x : Fin n) -> LT (n `minus` S (finToNat x)) n
290 | minusFinLT (S k) FZ = LTESucc (minusLTE k 0)
291 | minusFinLT (S k) (FS x) = LTESucc (minusLTE k _)
292 |
293 | export
294 | 0 minusLT : (x,m,n : Nat) -> LT x (n `minus` m) -> LT (x+m) n
295 | minusLT x _     0     y = absurd y
296 | minusLT x 0     (S k) y = rewrite plusZeroRightNeutral x in y
297 | minusLT x (S k) (S j) y =
298 |   let p1 := minusLT x k j y
299 |    in LTESucc (rewrite sym (plusSuccRightSucc x k) in p1)
300 |
301 | export
302 | inc : {m : _} -> Fin (n `minus` m) -> Fin n
303 | inc x =
304 |   let 0 p1 := finToNatLT x
305 |    in natToFinLT (finToNat x + m) @{minusLT _ _ _ p1}
306 |
307 | export
308 | 0 ltAddLeft : LT k n -> LT k (m+n)
309 | ltAddLeft {m = 0}   lt = lt
310 | ltAddLeft {m = S x} lt = lteSuccRight $ ltAddLeft lt
311 |
312 | export
313 | 0 lteAddLeft : (n : Nat) -> LTE n (m+n)
314 | lteAddLeft n = rewrite plusCommutative m n in lteAddRight n
315 |
316 | --------------------------------------------------------------------------------
317 | --          Lemma (Drop)
318 | --------------------------------------------------------------------------------
319 |
320 | export
321 | 0 plusMinus : (m,n : Nat) -> LTE m n -> m + (n `minus` m) === n
322 | plusMinus 0 0         _           = Refl
323 | plusMinus 0 (S k)     x           = Refl
324 | plusMinus (S k) (S j) (LTESucc p) = cong S $ plusMinus k j p
325 | plusMinus (S k) Z     x impossible
326 |
327 | export
328 | 0 eqLTE : (m,n : Nat) -> m === n -> LTE m n
329 | eqLTE 0     0     Refl = LTEZero
330 | eqLTE (S k) (S k) Refl = LTESucc $ eqLTE k k Refl
331 |
332 | export
333 | 0 dropLemma : (k,n : Nat) -> LTE (plus (minus n (minus n k)) (minus n k)) n
334 | dropLemma k n =
335 |   let p1 := minusLTE n k
336 |       p2 := plusMinus _ _ p1
337 |       p3 := trans (plusCommutative _ _) p2
338 |    in eqLTE _ _ p3
339 |
340 | export
341 | 0 plusMinusLTE : (m,n : Nat) -> LTE m n -> LTE (m + (n `minus` m)) n
342 | plusMinusLTE m n lte = eqLTE _ _ $ plusMinus m n lte
343 |
344 | export
345 | 0 plusMinus0 : (m,n,x : Nat) -> n === 0 -> LTE m x -> LTE (m + n) x
346 | plusMinus0 m 0 x Refl lte = rewrite plusZeroRightNeutral m in lte
347 |
348 | export
349 | 0 minusGTE : (m,n : Nat) -> GTE m n -> (n `minus` m) === 0
350 | minusGTE m 0         x           = Refl
351 | minusGTE 0 (S k)     x           = absurd x
352 | minusGTE (S j) (S k) (LTESucc x) = minusGTE j k x
353 |
354 | export
355 | 0 plusMinusBothLTE : (m,n : Nat) -> LTE m x -> LTE n x -> LTE (m + (n `minus` m)) x
356 | plusMinusBothLTE m n ltm ltn =
357 |   case decEq m n of
358 |     Yes prf => plusMinus0 m _ x (minusGTE m n $ rewrite prf in refl) ltm
359 |     No contra => case connex {rel = LTE} contra of
360 |       Left y  => transitive (plusMinusLTE m n y) ltn
361 |       Right y => plusMinus0 m _ x (minusGTE m n y) ltm
362 |
363 | --------------------------------------------------------------------------------
364 | --          Relations
365 | --------------------------------------------------------------------------------
366 |
367 | ||| `Suffix` is a reflexive and transitive relation.
368 | |||
369 | ||| Performance: This is integer addition at runtime.
370 | public export
371 | trans : Ix k m -> Ix m n -> Ix k n
372 | trans IZ y     = y
373 | trans (IS x) t = IS $ trans x t
374 |
375 | %inline
376 | transp : Ix k m -> Ix m n -> Ix k n
377 | transp x y =  believe_me (ixToNat x + ixToNat y)
378 |
379 | %transform "ixTransPlus" Index.trans = Index.transp
380 |
381 | ||| `Ix` is a reflexive relation on natural numbers.
382 | public export %inline
383 | Reflexive Nat Ix where
384 |   reflexive = IZ
385 |
386 | ||| `Ix` is a transitive relation on natural numbers.
387 | public export %inline
388 | Transitive Nat Ix where
389 |   transitive = trans
390 |
391 | --------------------------------------------------------------------------------
392 | --          Fixed-precision integers
393 | --------------------------------------------------------------------------------
394 |
395 | export
396 | 0 castBits8LT : (x : Bits8) -> LT (cast x) 256
397 | castBits8LT x =
398 |   case choose (cast {to = Nat} x < 256) of
399 |     Left oh => Data.Nat.ltOpReflectsLT _ _ oh
400 |     _       => assert_total $ idris_crash "Bits8 value >= 256"
401 |
402 | ||| Every `Bits8` value can be safely cast to a `Fin 256`.
403 | export %inline
404 | bits8ToFin : Bits8 -> Fin 256
405 | bits8ToFin x = natToFinLT (cast x) @{castBits8LT x}
406 |