module vector where open import bool open import eq open import list open import list-to-string open import nat open import nat-thms open import product open import string ---------------------------------------------------------------------- -- datatypes ---------------------------------------------------------------------- data 𝕍 {β„“} (A : Set β„“) : β„• β†’ Set β„“ where [] : 𝕍 A 0 _::_ : {n : β„•} β†’ A β†’ 𝕍 A n β†’ 𝕍 A (suc n) vector = 𝕍 ---------------------------------------------------------------------- -- syntax ---------------------------------------------------------------------- infixr 6 _::_ _++𝕍_ ---------------------------------------------------------------------- -- operations ---------------------------------------------------------------------- [_]𝕍 : βˆ€ {β„“} {A : Set β„“} β†’ A β†’ 𝕍 A 1 [ x ]𝕍 = x :: [] _++𝕍_ : βˆ€ {β„“} {A : Set β„“}{n m : β„•} β†’ 𝕍 A n β†’ 𝕍 A m β†’ 𝕍 A (n + m) [] ++𝕍 ys = ys (x :: xs) ++𝕍 ys = x :: xs ++𝕍 ys head𝕍 : βˆ€ {β„“} {A : Set β„“}{n : β„•} β†’ 𝕍 A (suc n) β†’ A head𝕍 (x :: _) = x tail𝕍 : βˆ€ {β„“} {A : Set β„“}{n : β„•} β†’ 𝕍 A n β†’ 𝕍 A (pred n) tail𝕍 [] = [] tail𝕍 (_ :: xs) = xs map𝕍 : βˆ€ {β„“ β„“'} {A : Set β„“} {B : Set β„“'}{n : β„•} β†’ (A β†’ B) β†’ 𝕍 A n β†’ 𝕍 B n map𝕍 f [] = [] map𝕍 f (x :: xs) = f x :: map𝕍 f xs concat𝕍 : βˆ€{β„“}{A : Set β„“}{n m : β„•} β†’ 𝕍 (𝕍 A n) m β†’ 𝕍 A (m * n) concat𝕍 [] = [] concat𝕍 (x :: xs) = x ++𝕍 (concat𝕍 xs) nth𝕍 : βˆ€ {β„“} {A : Set β„“}{m : β„•} β†’ (n : β„•) β†’ n < m ≑ tt β†’ 𝕍 A m β†’ A nth𝕍 0 _ (x :: _) = x nth𝕍 (suc n) p (_ :: xs) = nth𝕍 n p xs nth𝕍 (suc n) () [] nth𝕍 0 () [] member𝕍 : βˆ€{β„“}{A : Set β„“}{n : β„•}(eq : A β†’ A β†’ 𝔹)(a : A)(l : 𝕍 A n) β†’ 𝔹 member𝕍 eq a [] = ff member𝕍 eq a (x :: l) = if (eq a x) then tt else (member𝕍 eq a l) repeat𝕍 : βˆ€ {β„“} {A : Set β„“} β†’ (a : A)(n : β„•) β†’ 𝕍 A n repeat𝕍 a 0 = [] repeat𝕍 a (suc n) = a :: (repeat𝕍 a n) foldl𝕍 : βˆ€{β„“ β„“'}{A : Set β„“}{B : Set β„“'} β†’ B β†’ (B β†’ A β†’ B) β†’ {n : β„•} β†’ 𝕍 A n β†’ 𝕍 B n foldl𝕍 b _f_ [] = [] foldl𝕍 b _f_ (x :: xs) = let r = (b f x) in r :: (foldl𝕍 r _f_ xs) zipWith𝕍 : βˆ€ {β„“ β„“' β„“''} {A : Set β„“}{B : Set β„“'}{C : Set β„“''} β†’ (A β†’ B β†’ C) β†’ {n : β„•} β†’ 𝕍 A n β†’ 𝕍 B n β†’ 𝕍 C n zipWith𝕍 f [] [] = [] zipWith𝕍 _f_ (x :: xs) (y :: ys) = (x f y) :: (zipWith𝕍 _f_ xs ys) -- helper function for all𝕍 allh𝕍 : βˆ€ {β„“} {A : Set β„“}{n : β„•}(p : β„• β†’ A β†’ 𝔹) β†’ 𝕍 A n β†’ β„• β†’ 𝔹 allh𝕍 p [] n = tt allh𝕍 p (x :: xs) n = p n x && allh𝕍 p xs (suc n) -- given a predicate p which takes in an index and the element of -- the given 𝕍 at that index, return tt iff the predicate -- returns true for all indices (and their elements). all𝕍 : βˆ€ {β„“} {A : Set β„“}{n : β„•}(p : β„• β†’ A β†’ 𝔹) β†’ 𝕍 A n β†’ 𝔹 all𝕍 p v = allh𝕍 p v 0 𝕍-to-𝕃 : βˆ€ {β„“} {A : Set β„“}{n : β„•} β†’ 𝕍 A n β†’ 𝕃 A 𝕍-to-𝕃 [] = [] 𝕍-to-𝕃 (x :: xs) = x :: (𝕍-to-𝕃 xs) 𝕃-to-𝕍 : βˆ€ {β„“} {A : Set β„“} β†’ 𝕃 A β†’ Ξ£ β„• (Ξ» n β†’ 𝕍 A n) 𝕃-to-𝕍 [] = (0 , []) 𝕃-to-𝕍 (x :: xs) with 𝕃-to-𝕍 xs ... | (n , v) = (suc n , x :: v) {- turn the given 𝕍 into a string by calling f on each element, and separating the elements with the given separator string -} 𝕍-to-string : βˆ€ {β„“} {A : Set β„“}{n : β„•} β†’ (f : A β†’ string) β†’ (separator : string) β†’ 𝕍 A n β†’ string 𝕍-to-string f sep v = 𝕃-to-string f sep (𝕍-to-𝕃 v)