Data.Vec.Functional operations and properties

CHANGELOG.md

@@ -148,12 +148,18 @@ New modules
   ```agda
   Function.Properties.Inverse
   Function.Properties.Equivalence
+  ```
 
 * Indexed nullary relations/sets:
   ```
   Relation.Nullary.Indexed
   ```
 
+* Properties for functional vectors:
+  ```
+  Data.Vec.Functional.Properties
+  ```
+
 * Generic printf
   ```
   Text.Format.Generic
@@ -388,6 +394,36 @@ Other minor additions
   _⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
   ```
 
+* Added new functions to `Data.Fin.Base`:
+  ```agda
+  quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
+  opposite : ∀ {n} → Fin n → Fin n
+  ```
+
+* Added new proofs to `Data.Fin.Properties`:
+  ```agda
+  splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
+  splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
+  ```
+
+* Added new functions to `Data.Vec.Functional`:
+  ```agda
+  length : ∀ {n} → Vector A n → ℕ
+  insert : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
+  updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
+  _++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
+  concat : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
+  _>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
+  unzipWith : ∀ {n} → (A → B × C) → Vector A n → Vector B n × Vector C n
+  unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
+  take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
+  drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
+  reverse : ∀ {n} → Vector A n → Vector A n
+  init : ∀ {n} → Vector A (suc n) → Vector A n
+  last : ∀ {n} → Vector A (suc n) → A
+  transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
+  ```
+
 Refactorings
 ------------
 

src/Data/Fin/Base.agda

@@ -15,6 +15,7 @@ module Data.Fin.Base where
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
 open import Data.Nat.Properties.Core using (≤-pred)
+open import Data.Product as Product using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (id; _∘_; _on_)
 open import Level using () renaming (zero to ℓ₀)
@@ -130,6 +131,14 @@ splitAt zero    i       = inj₂ i
 splitAt (suc m) zero    = inj₁ zero
 splitAt (suc m) (suc i) = Sum.map suc id (splitAt m i)
 
+-- quotRem k "i" = "i % k" , "i / k"
+-- This is dual to group from Data.Vec.
+
+quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
+quotRem {suc n} k i with splitAt k i
+... | inj₁ j = j , zero
+... | inj₂ j = Product.map₂ suc (quotRem {n} k j)
+
 ------------------------------------------------------------------------
 -- Operations
 
@@ -195,6 +204,12 @@ pred : ∀ {n} → Fin n → Fin n
 pred zero    = zero
 pred (suc i) = inject₁ i
 
+-- opposite "i" = "n - i" (i.e. the additive inverse).
+
+opposite : ∀ {n} → Fin n → Fin n
+opposite {suc n} zero    = fromℕ n
+opposite {suc n} (suc i) = inject₁ (opposite i)
+
 -- The function f(i,j) = if j>i then j-1 else j
 -- This is a variant of the thick function from Conor
 -- McBride's "First-order unification by structural recursion".

src/Data/Fin/Properties.agda

@@ -19,7 +19,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Unit using (tt)
 open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁; uncurry; <_,_>)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr)
 open import Function.Base using (_∘_; id; _$_)
 open import Function.Equivalence using (_⇔_; equivalence)
@@ -436,6 +436,17 @@ inject+-raise-splitAt (suc m) n (suc i) = begin
   suc i                                                        ∎
   where open ≡-Reasoning
 
+-- splitAt "m" "i" ≡ inj₁ "i" if i < m
+
+splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
+splitAt-< (suc m) zero    _         = refl
+splitAt-< (suc m) (suc i) (s≤s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
+
+-- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
+
+splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
+splitAt-≥ zero    i       _         = refl
+splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m i i≥m)
 
 ------------------------------------------------------------------------
 -- lift

src/Data/Vec/Functional.agda

@@ -15,17 +15,18 @@
 
 module Data.Vec.Functional where
 
-open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
+open import Data.Fin.Base
 open import Data.List.Base as L using (List)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)
 open import Function
 open import Level using (Level)
 
 infixr 5 _∷_ _++_
 infixl 4 _⊛_
+infixl 1 _>>=_
 
 private
   variable
@@ -56,7 +57,7 @@ fromList : ∀ (xs : List A) → Vector A (L.length xs)
 fromList = L.lookup
 
 ------------------------------------------------------------------------
--- Construction and deconstruction
+-- Basic operations
 
 [] : Vector A zero
 [] ()
@@ -65,6 +66,9 @@ _∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
 (x ∷ xs) zero    = x
 (x ∷ xs) (suc i) = xs i
 
+length : ∀ {n} → Vector A n → ℕ
+length {n = n} _ = n
+
 head : ∀ {n} → Vector A (suc n) → A
 head xs = xs zero
 
@@ -77,18 +81,33 @@ uncons xs = head xs , tail xs
 replicate : ∀ {n} → A → Vector A n
 replicate = const
 
+insert : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
+insert {n = n}     xs zero    v zero    = v
+insert {n = n}     xs zero    v (suc j) = xs j
+insert {n = suc n} xs (suc i) v zero    = head xs
+insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j
+
 remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
 remove i t = t ∘ punchIn i
 
+updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
+updateAt {n = suc n} zero    f xs zero    = f (head xs)
+updateAt {n = suc n} zero    f xs (suc j) = xs (suc j)
+updateAt {n = suc n} (suc i) f xs zero    = head xs
+updateAt {n = suc n} (suc i) f xs (suc j) = updateAt i f (tail xs) j
+
 ------------------------------------------------------------------------
 -- Transformations
 
 map : (A → B) → ∀ {n} → Vector A n → Vector B n
 map f xs = f ∘ xs
 
-_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
+_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
 _++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)
 
+concat : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
+concat {m = m} xss i = uncurry (flip xss) (quotRem m i)
+
 foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
 foldr f z {n = zero}  xs = z
 foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))
@@ -103,8 +122,35 @@ rearrange r xs = xs ∘ r
 _⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
 _⊛_ = _ˢ_
 
+_>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
+xs >>= f = concat (map f xs)
+
 zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
 zipWith f xs ys i = f (xs i) (ys i)
 
+unzipWith : ∀ {n} → (A → B × C) → Vector A n → Vector B n × Vector C n
+unzipWith f xs = proj₁ ∘ f ∘ xs , proj₂ ∘ f ∘ xs
+
 zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
 zip = zipWith _,_
+
+unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
+unzip = unzipWith id
+
+take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
+take _ {n = n} xs = xs ∘ inject+ n
+
+drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
+drop m xs = xs ∘ raise m
+
+reverse : ∀ {n} → Vector A n → Vector A n
+reverse xs = xs ∘ opposite
+
+init : ∀ {n} → Vector A (suc n) → Vector A n
+init xs = xs ∘ inject₁
+
+last : ∀ {n} → Vector A (suc n) → A
+last {n = n} xs = xs (fromℕ n)
+
+transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
+transpose = flip