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 Data.So
 38 | import public Data.DPair
 39 | import public Data.Fin
 40 | import public Data.Maybe0
 41 | import public Data.Nat
 42 |
 43 | %default total
 44 |
 45 | export
 46 | 0 ltLemma : (0 k,m,n : Nat) -> k + S m === n -> LT k n
 47 | ltLemma 0     m (S m) Refl = %search
 48 | ltLemma (S k) m (S n) prf  = LTESucc $ ltLemma k m n (injective prf)
 49 | ltLemma (S k) m 0     prf  = absurd prf
 50 |
 51 | export
 52 | 0 lteLemma : (0 k,m,n : Nat) -> k + m === n -> LTE k n
 53 | lteLemma 0     m m     Refl = %search
 54 | lteLemma (S k) m (S n) prf  = LTESucc $ lteLemma k m n (injective prf)
 55 | lteLemma (S k) m 0     prf  = absurd prf
 56 |
 57 | export
 58 | 0 lteSuccPlus : (k : Nat) -> LTE (S k) (k + S m)
 59 | lteSuccPlus 0     = LTESucc LTEZero
 60 | lteSuccPlus (S k) = LTESucc $ lteSuccPlus k
 61 |
 62 | ||| Generates the list of all `Fin n` in linear type.
 63 | |||
 64 | ||| This is a lot faster than `Data.Fin.allFins`, which runs in quadratic
 65 | ||| time.
 66 | export
 67 | allFinsFast : (n : Nat) -> List (Fin n)
 68 | allFinsFast 0 = []
 69 | allFinsFast (S n) = go [] last
 70 |   where
 71 |     go : List (Fin $ S n) -> Fin (S n) -> List (Fin $ S n)
 72 |     go xs FZ     = FZ :: xs
 73 |     go xs (FS x) = go (FS x :: xs) (assert_smaller (FS x) $ weaken x)
 74 |
 75 | --------------------------------------------------------------------------------
 76 | --          Suffix
 77 | --------------------------------------------------------------------------------
 78 |
 79 | public export
 80 | data Suffix : (xs,ys : List a) -> Type where
 81 |   Same   : Suffix xs xs
 82 |   Uncons : Suffix (x::xs) ys -> Suffix xs ys
 83 |
 84 | public export
 85 | suffixToNat : Suffix xs ys -> Nat
 86 | suffixToNat Same       = 0
 87 | suffixToNat (Uncons x) = S $ suffixToNat x
 88 |
 89 | export
 90 | 0 suffixLemma : (s : Suffix xs ys) -> suffixToNat s + length xs === length ys
 91 | suffixLemma Same       = Refl
 92 | suffixLemma (Uncons x) = trans (plusSuccRightSucc _ _) $ suffixLemma x
 93 |
 94 | export
 95 | 0 suffixLT : (s : Suffix (x::xs) ys) -> LT (suffixToNat s) (length ys)
 96 | suffixLT s = ltLemma _ _ _ $ suffixLemma s
 97 |
 98 | public export
 99 | suffixToFin : Suffix (x::xs) ys -> Fin (length ys)
100 | suffixToFin x = natToFinLT (suffixToNat x) @{suffixLT x}
101 |
102 | --------------------------------------------------------------------------------
103 | --          Ix
104 | --------------------------------------------------------------------------------
105 |
106 | ||| A data type for safely indexing into an array from the
107 | ||| front during in a fuction recursing on natural number `m`.
108 | |||
109 | ||| This is another way to proof that `m <= n`.
110 | public export
111 | data Ix : (m,n : Nat) -> Type where
112 |   IZ : Ix n n
113 |   IS : Ix (S m) n -> Ix m n
114 |
115 | ||| O(1) conversion from `Ix m n` to `Nat`. The result equals `n - m`.
116 | public export
117 | ixToNat : Ix m n -> Nat
118 | ixToNat IZ     = 0
119 | ixToNat (IS n) = S $ ixToNat n
120 |
121 | ||| If `m <= n` then `S m <= S n`.
122 | public export
123 | succIx : Ix m n -> Ix (S m) (S n)
124 | succIx IZ     = IZ
125 | succIx (IS x) = IS (succIx x)
126 |
127 | ||| Convert a natural number to the corresponding `Ix 0 n`
128 | ||| so that `n === ixToNat (natToIx n)` as shown in
129 | ||| `ixLemma`.
130 | public export
131 | natToIx : (n : Nat) -> Ix 0 n
132 | natToIx 0     = IZ
133 | natToIx (S k) = IS $ succIx (natToIx k)
134 |
135 | ||| Convert a natural number to the corresponding `Ix 1 (S n)`,
136 | ||| the largest value strictly smaller than `S n`.
137 | |||
138 | ||| This is similar to `Data.Fin.last`.
139 | public export
140 | natToIx1 : (n : Nat) -> Ix 1 (S n)
141 | natToIx1 n = case natToIx (S n) of
142 |   IS x => x
143 |
144 | ||| Proof that for an index `x` of type `Ix m n` `ixToNat x` equals `n - m`.
145 | export
146 | 0 ixLemma : (x : Ix m n) -> ixToNat x + m === n
147 | ixLemma IZ     = Refl
148 | ixLemma (IS v) = trans (plusSuccRightSucc _ _) $ ixLemma v
149 |
150 | ||| Proof an `Ix (S m) n` corresponds to a natural number
151 | ||| strictly smaller than `n` and can therefore be used as an index
152 | ||| into an array of size `n`.
153 | export
154 | 0 ixLT : (x : Ix (S m) n) -> LT (ixToNat x) n
155 | ixLT s = ltLemma _ _ _ $ ixLemma s
156 |
157 | ||| Proof an `Ix m n` corresponds to a natural number
158 | ||| smaller than or equal to `n
159 | export
160 | 0 ixLTE : (x : Ix m n) -> LTE (ixToNat x) n
161 | ixLTE s = lteLemma _ _ _ $ ixLemma s
162 |
163 | ||| From lemma `ixLT` follows, that we can convert an `Ix (S m) n` to
164 | ||| a `Fin n` corresponding to the same natural numbers. All conversions
165 | ||| involved are optimized away by the identity optimizer during code
166 | ||| generation.
167 | public export
168 | ixToFin : Ix (S m) n -> Fin n
169 | ixToFin x = natToFinLT (ixToNat x) @{ixLT x}
170 |
171 | --------------------------------------------------------------------------------
172 | --          Sublength
173 | --------------------------------------------------------------------------------
174 |
175 | export
176 | 0 finToNatLT : (x : Fin n) -> LT (finToNat x) n
177 | finToNatLT FZ     = %search
178 | finToNatLT (FS x) = LTESucc $ finToNatLT x
179 |
180 | ||| This type is used to cut off a portion of
181 | ||| a `ByteString`. It must be no larger than the number
182 | ||| of elements in the ByteString
183 | public export
184 | 0 SubLength : Nat -> Type
185 | SubLength n = Subset Nat (`LTE` n)
186 |
187 | export %inline
188 | sublength : (k : Nat) -> (0 lte : LTE k n) => SubLength n
189 | sublength k = Element k lte
190 |
191 | export %inline
192 | fromFin : Fin n -> SubLength n
193 | fromFin x = Element (finToNat x) (lteSuccLeft $ finToNatLT x)
194 |
195 | export %inline
196 | fromIx : Ix m n -> SubLength n
197 | fromIx x = Element (ixToNat x) (ixLTE x)
198 |
199 | --------------------------------------------------------------------------------
200 | --          Hints
201 | --------------------------------------------------------------------------------
202 |
203 | export %hint
204 | 0 refl : LTE n n
205 | refl = reflexive
206 |
207 | export %hint
208 | 0 lsl : (p : LTE (S m) n) => LTE m n
209 | lsl = lteSuccLeft p
210 |
211 | --------------------------------------------------------------------------------
212 | --          Proofs
213 | --------------------------------------------------------------------------------
214 |
215 | export
216 | 0 lteOpReflectsLTE : (m,n : Nat) -> (m <= n) === True -> LTE m n
217 | lteOpReflectsLTE 0     (S k) prf = LTEZero
218 | lteOpReflectsLTE (S k) (S j) prf = LTESucc (lteOpReflectsLTE k j prf)
219 | lteOpReflectsLTE 0 0         prf = LTEZero
220 | lteOpReflectsLTE (S k) Z     prf impossible
221 |
222 | export
223 | 0 ltOpReflectsLT : (m,n : Nat) -> (m < n) === True -> LT m n
224 | ltOpReflectsLT 0     (S k) prf = LTESucc LTEZero
225 | ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
226 | ltOpReflectsLT Z Z         prf impossible
227 | ltOpReflectsLT (S k) Z     prf impossible
228 |
229 | export
230 | 0 eqOpReflectsEquals : (m,n : Nat) -> (m == n) === True -> m === n
231 | eqOpReflectsEquals 0     0     prf = Refl
232 | eqOpReflectsEquals (S k) (S j) prf = cong S $ eqOpReflectsEquals k j prf
233 | eqOpReflectsEquals Z     (S k) prf impossible
234 | eqOpReflectsEquals (S k) Z     prf impossible
235 |
236 | --------------------------------------------------------------------------------
237 | --          Proofs
238 | --------------------------------------------------------------------------------
239 |
240 | export
241 | tryLT : {n : _} -> (k : Nat) -> Maybe0 (LT k n)
242 | tryLT k with (k < n) proof eq
243 |   _ | True  = Just0 $ ltOpReflectsLT k n eq
244 |   _ | False = Nothing0
245 |
246 | export
247 | tryLTE : {n : _} -> (k : Nat) -> Maybe0 (LTE k n)
248 | tryLTE 0     = Just0 %search
249 | tryLTE (S k) = tryLT k
250 |
251 | ||| Tries to convert a natural number to a `Fin k`.
252 | export
253 | tryNatToFin : {k : _} -> Nat -> Maybe (Fin k)
254 | tryNatToFin n with (n < k) proof eq
255 |   _ | True  = Just $ natToFinLT n @{ltOpReflectsLT n k eq}
256 |   _ | False = Nothing
257 |
258 | ||| Tries to convert a `Fin n` to a `Fin k`.
259 | export %inline
260 | tryFinToFin : {k : _} -> Fin n -> Maybe (Fin k)
261 | tryFinToFin = tryNatToFin . finToNat
262 |
263 | export
264 | 0 minusLTE : (k,m : Nat) -> LTE (k `minus` m) k
265 | minusLTE 0     m     = LTEZero
266 | minusLTE (S k) 0     = reflexive
267 | minusLTE (S k) (S j) = lteSuccRight $ minusLTE k j
268 |
269 | export
270 | 0 minusFinLT : (n : Nat) -> (x : Fin n) -> LT (n `minus` S (finToNat x)) n
271 | minusFinLT (S k) FZ = LTESucc (minusLTE k 0)
272 | minusFinLT (S k) (FS x) = LTESucc (minusLTE k _)
273 |
274 | export
275 | 0 minusLT : (x,m,n : Nat) -> LT x (n `minus` m) -> LT (x+m) n
276 | minusLT x _     0     y = absurd y
277 | minusLT x 0     (S k) y = rewrite plusZeroRightNeutral x in y
278 | minusLT x (S k) (S j) y =
279 |   let p1 := minusLT x k j y
280 |    in LTESucc (rewrite sym (plusSuccRightSucc x k) in p1)
281 |
282 | export
283 | inc : {m : _} -> Fin (n `minus` m) -> Fin n
284 | inc x =
285 |   let 0 p1 := finToNatLT x
286 |    in natToFinLT (finToNat x + m) @{minusLT _ _ _ p1}
287 |
288 | export
289 | 0 ltAddLeft : LT k n -> LT k (m+n)
290 | ltAddLeft {m = 0}   lt = lt
291 | ltAddLeft {m = S x} lt = lteSuccRight $ ltAddLeft lt
292 |
293 | export
294 | 0 lteAddLeft : (n : Nat) -> LTE n (m+n)
295 | lteAddLeft n = rewrite plusCommutative m n in lteAddRight n
296 |
297 | --------------------------------------------------------------------------------
298 | --          Lemma (Drop)
299 | --------------------------------------------------------------------------------
300 |
301 | export
302 | 0 plusMinus : (m,n : Nat) -> LTE m n -> m + (n `minus` m) === n
303 | plusMinus 0 0         _           = Refl
304 | plusMinus 0 (S k)     x           = Refl
305 | plusMinus (S k) (S j) (LTESucc p) = cong S $ plusMinus k j p
306 | plusMinus (S k) Z     x impossible
307 |
308 | export
309 | 0 eqLTE : (m,n : Nat) -> m === n -> LTE m n
310 | eqLTE 0     0     Refl = LTEZero
311 | eqLTE (S k) (S k) Refl = LTESucc $ eqLTE k k Refl
312 |
313 | export
314 | 0 dropLemma : (k,n : Nat) -> LTE (plus (minus n (minus n k)) (minus n k)) n
315 | dropLemma k n =
316 |   let p1 := minusLTE n k
317 |       p2 := plusMinus _ _ p1
318 |       p3 := trans (plusCommutative _ _) p2
319 |    in eqLTE _ _ p3
320 |
321 | export
322 | 0 plusMinusLTE : (m,n : Nat) -> LTE m n -> LTE (m + (n `minus` m)) n
323 | plusMinusLTE m n lte = eqLTE _ _ $ plusMinus m n lte
324 |
325 | --------------------------------------------------------------------------------
326 | --          Relations
327 | --------------------------------------------------------------------------------
328 |
329 | ||| `Suffix` is a reflexive and transitive relation.
330 | |||
331 | ||| Performance: This is integer addition at runtime.
332 | public export
333 | trans : Ix k m -> Ix m n -> Ix k n
334 | trans IZ y     = y
335 | trans (IS x) t = IS $ trans x t
336 |
337 | %inline
338 | transp : Ix k m -> Ix m n -> Ix k n
339 | transp x y =  believe_me (ixToNat x + ixToNat y)
340 |
341 | %transform "ixTransPlus" Index.trans = Index.transp
342 |
343 | ||| `Ix` is a reflexive relation on natural numbers.
344 | public export %inline
345 | Reflexive Nat Ix where
346 |   reflexive = IZ
347 |
348 | ||| `Ix` is a transitive relation on natural numbers.
349 | public export %inline
350 | Transitive Nat Ix where
351 |   transitive = trans
352 |
353 | --------------------------------------------------------------------------------
354 | --          Fixed-precision integers
355 | --------------------------------------------------------------------------------
356 |
357 | export
358 | 0 castBits8LT : (x : Bits8) -> LT (cast x) 256
359 | castBits8LT x =
360 |   case choose (cast {to = Nat} x < 256) of
361 |     Left oh => Data.Nat.ltOpReflectsLT _ _ oh
362 |     _       => assert_total $ idris_crash "Bits8 value >= 256"
363 |
364 | ||| Every `Bits8` value can be safely cast to a `Fin 256`.
365 | export %inline
366 | bits8ToFin : Bits8 -> Fin 256
367 | bits8ToFin x = natToFinLT (cast x) @{castBits8LT x}
368 |