
  0 | {--
  1 | Copyright (C) 2021  Joel Berkeley
  2 | 
  3 | This program is free software: you can redistribute it and/or modify
  4 | it under the terms of the GNU Affero General Public License as published
  5 | by the Free Software Foundation, either version 3 of the License, or
  6 | (at your option) any later version.
  7 | 
  8 | This program is distributed in the hope that it will be useful,
  9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
 10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 11 | GNU Affero General Public License for more details.
 12 | 
 13 | You should have received a copy of the GNU Affero General Public License
 14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
 15 | --}
 16 | ||| Vect definitions.
 17 | module Spidr.Data.Vect
 18 | 
 19 | import public Data.Vect
 20 | 
 21 | ||| All numbers from `0` to `n - 1` inclusive, in increasing order.
 22 | |||
 23 | ||| @n The (exclusive) limit of the range.
 24 | export
 25 | range : (n : Nat) -> Vect n Nat
 26 | range Z = []
 27 | range (S n) = snoc (range n) n
 28 | 
 29 | ||| Enumerate entries in a vector with their indices. For example, `enumerate [5, 7, 9]`
 30 | ||| is `[(0, 5), (1, 7), (2, 9)]`.
 31 | export
 32 | enumerate : Vect n a -> Vect n (Nat, a)
 33 | enumerate xs =
 34 |   let lengthOK = lengthCorrect xs
 35 |     in rewrite sym lengthOK in zip (range (length xs)) (rewrite lengthOK in xs)
 36 | 
 37 | public export
 38 | functorIdentity : forall a . (xs : Vect n a) -> map Prelude.id xs = xs
 39 | functorIdentity [] = Refl
 40 | functorIdentity (x :: xs) = cong2 (::) Refl (functorIdentity xs)
 41 |