Data.Array.Index

(source)

This module provides several ways to safely index into an
array of known size. All conversions between different index
types are optimized away by the compiler, because they are
all of the same structure during code generation: An encoding
of natural numbers which the Idris compiler converts to a
native integer representation.

The main type for indexing into an array of size `n` is `Fin n`,
representing a natural number strictly smaller than `n`.

As an alternative, we can use a natural number `k` directly, together
with a proof of type `LT k n`, showing that `k` is strictly smaller
than `n`. Such numbers can be converted directly to `Fin n` by means
of function `Data.Nat.natToFinLT`. This way of indexing is very
useful for iterating over the whole array from then end: We start
with `n` itself together with an erased proof of type `LTE n n`, which
can be generated automatically. By pattern matching on the current
position, we can safely access all positions in the array until
we arrive at 0. See the implementation of `foldr` (a private
function called `foldrI`) in module `Data.Array.Indexed` for an
example how this is used.

It is only slightly harder to iterate over an array from the
front. This is where data type `Ix m n` comes into play: It's
another way of saying that `m <= n` holds, but it works in
the oposite direction than `LTE`: It's zero constructor `IZ` proofs
that `n <= n` for all `n`, while its successor constructor
proofs that from `S k <= n` follows `k <= n`. This means, that
for a given `k`, a values of type `Ix k n` corresponds to the
values `n - k`. This allows us to recurse over a natural number
while keeping an auto-implicit proof of type `Ix k n`, and use
this proof for indexing into the array.
See the implementation of `foldl` (a private
function called `foldlI`) in module `Data.Array.Indexed` for an
example how this is used.

Reexports

import public Data.DPair
import public Data.Fin
import public Data.Maybe0
import public Data.Nat

Definitions

0 ltLemma : (0 k : Nat) -> (0 m : Nat) -> (0 n : Nat) -> k + S m = n -> LT k n

Totality: total
Visibility: export

0 lteLemma : (0 k : Nat) -> (0 m : Nat) -> (0 n : Nat) -> k + m = n -> LTE k n

Totality: total
Visibility: export

0 lteSuccPlus : (k : Nat) -> LTE (S k) (k + S m)

Totality: total
Visibility: export

data Suffix : List a -> List a -> Type

Totality: total
Visibility: public export
Constructors:

Same : Suffix xs xs
Uncons : Suffix (x :: xs) ys -> Suffix xs ys

suffixToNat : Suffix xs ys -> Nat

Totality: total
Visibility: public export

0 suffixLemma : (s : Suffix xs ys) -> suffixToNat s + length xs = length ys

Totality: total
Visibility: export

0 suffixLT : (s : Suffix (x :: xs) ys) -> LT (suffixToNat s) (length ys)

Totality: total
Visibility: export

suffixToFin : Suffix (x :: xs) ys -> Fin (length ys)

Totality: total
Visibility: public export

data Ix : Nat -> Nat -> Type

  A data type for safely indexing into an array from the
  front during in a fuction recursing on natural number `m`.
  
  This is another way to proof that `m <= n`.

Totality: total
Visibility: public export
Constructors:

IZ : Ix n n
IS : Ix (S m) n -> Ix m n

Hints:

Reflexive Nat Ix
Transitive Nat Ix

ixToNat : Ix m n -> Nat

  O(1) conversion from `Ix m n` to `Nat`. The result equals `n - m`.

Totality: total
Visibility: public export

succIx : Ix m n -> Ix (S m) (S n)

  If `m <= n` then `S m <= S n`.

Totality: total
Visibility: public export

natToIx : (n : Nat) -> Ix 0 n

  Convert a natural number to the corresponding `Ix 0 n`
  so that `n === ixToNat (natToIx n)` as shown in
  `ixLemma`.

Totality: total
Visibility: public export

natToIx1 : (n : Nat) -> Ix 1 (S n)

  Convert a natural number to the corresponding `Ix 1 (S n)`,
  the largest value strictly smaller than `S n`.
  
  This is similar to `Data.Fin.last`.

Totality: total
Visibility: public export

0 ixLemma : (x : Ix m n) -> ixToNat x + m = n

  Proof that for an index `x` of type `Ix m n` `ixToNat x` equals `n - m`.

Totality: total
Visibility: export

0 ixLT : (x : Ix (S m) n) -> LT (ixToNat x) n

  Proof an `Ix (S m) n` corresponds to a natural number
  strictly smaller than `n` and can therefore be used as an index
  into an array of size `n`.

Totality: total
Visibility: export

0 ixLTE : (x : Ix m n) -> LTE (ixToNat x) n

  Proof an `Ix m n` corresponds to a natural number
  smaller than or equal to `n

Totality: total
Visibility: export

ixToFin : Ix (S m) n -> Fin n

  From lemma `ixLT` follows, that we can convert an `Ix (S m) n` to
  a `Fin n` corresponding to the same natural numbers. All conversions
  involved are optimized away by the identity optimizer during code
  generation.

Totality: total
Visibility: public export

0 finToNatLT : (x : Fin n) -> LT (finToNat x) n

Totality: total
Visibility: export

0 SubLength : Nat -> Type

  This type is used to cut off a portion of
  a `ByteString`. It must be no larger than the number
  of elements in the ByteString

Totality: total
Visibility: public export

sublength : (k : Nat) -> {auto 0 _ : LTE k n} -> SubLength n

Totality: total
Visibility: export

fromFin : Fin n -> SubLength n

Totality: total
Visibility: export

fromIx : Ix m n -> SubLength n

Totality: total
Visibility: export

0 refl : LTE n n

Totality: total
Visibility: export

0 lsl : LTE (S m) n => LTE m n

Totality: total
Visibility: export

0 lteOpReflectsLTE : (m : Nat) -> (n : Nat) -> m <= n = True -> LTE m n

Totality: total
Visibility: export

0 ltOpReflectsLT : (m : Nat) -> (n : Nat) -> m < n = True -> LT m n

Totality: total
Visibility: export

0 eqOpReflectsEquals : (m : Nat) -> (n : Nat) -> m == n = True -> m = n

Totality: total
Visibility: export

tryLT : (k : Nat) -> Maybe0 (LT k n)

Totality: total
Visibility: export

tryLTE : (k : Nat) -> Maybe0 (LTE k n)

Totality: total
Visibility: export

tryNatToFin : Nat -> Maybe (Fin k)

  Tries to convert a natural number to a `Fin k`.

Totality: total
Visibility: export

tryFinToFin : Fin n -> Maybe (Fin k)

  Tries to convert a `Fin n` to a `Fin k`.

Totality: total
Visibility: export

0 minusLTE : (k : Nat) -> (m : Nat) -> LTE (minus k m) k

Totality: total
Visibility: export

0 minusFinLT : (n : Nat) -> (x : Fin n) -> LT (minus n (S (finToNat x))) n

Totality: total
Visibility: export

0 minusLT : (x : Nat) -> (m : Nat) -> (n : Nat) -> LT x (minus n m) -> LT (x + m) n

Totality: total
Visibility: export

inc : Fin (minus n m) -> Fin n

Totality: total
Visibility: export

0 ltAddLeft : LT k n -> LT k (m + n)

Totality: total
Visibility: export

0 lteAddLeft : (n : Nat) -> LTE n (m + n)

Totality: total
Visibility: export

0 plusMinus : (m : Nat) -> (n : Nat) -> LTE m n -> m + minus n m = n

Totality: total
Visibility: export

0 eqLTE : (m : Nat) -> (n : Nat) -> m = n -> LTE m n

Totality: total
Visibility: export

0 dropLemma : (k : Nat) -> (n : Nat) -> LTE (plus (minus n (minus n k)) (minus n k)) n

Totality: total
Visibility: export

0 plusMinusLTE : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (m + minus n m) n

Totality: total
Visibility: export

trans : Ix k m -> Ix m n -> Ix k n

  `Suffix` is a reflexive and transitive relation.
  
  Performance: This is integer addition at runtime.

Totality: total
Visibility: public export

0 castBits8LT : (x : Bits8) -> LT (cast x) 256

Totality: total
Visibility: export

bits8ToFin : Bits8 -> Fin 256

  Every `Bits8` value can be safely cast to a `Fin 256`.

Totality: total
Visibility: export