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