------------------------------------------------------------------------ -- The Agda standard library -- -- Vectors, basic types and operations ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Vec.Base where open import Data.Bool.Base using (Bool; true; false; if_then_else_) open import Data.Nat.Base open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List) open import Data.Product.Base as Product using (∃; ∃₂; _×_; _,_; proj₁; proj₂) open import Data.These.Base as These using (These; this; that; these) open import Function.Base using (const; _∘′_; id; _∘_; _$_) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong) open import Relation.Nullary.Decidable.Core using (does; T?) open import Relation.Unary using (Pred; Decidable) private variable a b c p : Level A : Set a B : Set b C : Set c m n : ℕ ------------------------------------------------------------------------ -- Types infixr 5 _∷_ data Vec (A : Set a) : ℕ → Set a where [] : Vec A zero _∷_ : ∀ (x : A) (xs : Vec A n) → Vec A (suc n) infix 4 _[_]=_ data _[_]=_ {A : Set a} : Vec A n → Fin n → A → Set a where here : ∀ {x} {xs : Vec A n} → x ∷ xs [ zero ]= x there : ∀ {i} {x y} {xs : Vec A n} (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x ------------------------------------------------------------------------ -- Basic operations length : Vec A n → ℕ length {n = n} _ = n head : Vec A (1 + n) → A head (x ∷ xs) = x tail : Vec A (1 + n) → Vec A n tail (x ∷ xs) = xs lookup : Vec A n → Fin n → A lookup (x ∷ xs) zero = x lookup (x ∷ xs) (suc i) = lookup xs i iterate : (A → A) → A → ∀ n → Vec A n iterate s z zero = [] iterate s z (suc n) = z ∷ iterate s (s z) n insertAt : Vec A n → Fin (suc n) → A → Vec A (suc n) insertAt xs zero v = v ∷ xs insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v removeAt : Vec A (suc n) → Fin (suc n) → Vec A n removeAt (x ∷ xs) zero = xs removeAt (x ∷ xs@(_ ∷ _)) (suc i) = x ∷ removeAt xs i updateAt : Vec A n → Fin n → (A → A) → Vec A n updateAt (x ∷ xs) zero f = f x ∷ xs updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f -- xs [ i ]%= f modifies the i-th element of xs according to f infixl 6 _[_]%=_ _[_]≔_ _[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n xs [ i ]%= f = updateAt xs i f -- xs [ i ]≔ y overwrites the i-th element of xs with y _[_]≔_ : Vec A n → Fin n → A → Vec A n xs [ i ]≔ y = xs [ i ]%= const y ------------------------------------------------------------------------ -- Operations for transforming vectors -- See README.Data.Vec.Relation.Binary.Equality.Cast for the reasoning -- system of `cast`-ed equality. cast : .(eq : m ≡ n) → Vec A m → Vec A n cast {n = zero} eq [] = [] cast {n = suc _} eq (x ∷ xs) = x ∷ cast (cong pred eq) xs map : (A → B) → Vec A n → Vec B n map f [] = [] map f (x ∷ xs) = f x ∷ map f xs -- Concatenation. infixr 5 _++_ _++_ : Vec A m → Vec A n → Vec A (m + n) [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) concat : Vec (Vec A m) n → Vec A (n * m) concat [] = [] concat (xs ∷ xss) = xs ++ concat xss -- Align, Restrict, and Zip. alignWith : (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n) alignWith f [] bs = map (f ∘′ that) bs alignWith f as@(_ ∷ _) [] = map (f ∘′ this) as alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ alignWith f as bs restrictWith : (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n) restrictWith f [] bs = [] restrictWith f (_ ∷ _) [] = [] restrictWith f (a ∷ as) (b ∷ bs) = f a b ∷ restrictWith f as bs zipWith : (A → B → C) → Vec A n → Vec B n → Vec C n zipWith f [] [] = [] zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys unzipWith : (A → B × C) → Vec A n → Vec B n × Vec C n unzipWith f [] = [] , [] unzipWith f (a ∷ as) = Product.zip _∷_ _∷_ (f a) (unzipWith f as) align : Vec A m → Vec B n → Vec (These A B) (m ⊔ n) align = alignWith id restrict : Vec A m → Vec B n → Vec (A × B) (m ⊓ n) restrict = restrictWith _,_ zip : Vec A n → Vec B n → Vec (A × B) n zip = zipWith _,_ unzip : Vec (A × B) n → Vec A n × Vec B n unzip = unzipWith id -- Interleaving. infixr 5 _⋎_ _⋎_ : Vec A m → Vec A n → Vec A (m +⋎ n) [] ⋎ ys = ys (x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs) -- Pointwise application infixl 4 _⊛_ _⊛_ : Vec (A → B) n → Vec A n → Vec B n [] ⊛ [] = [] (f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs) -- Multiplication module CartesianBind where infixl 1 _>>=_ _>>=_ : Vec A m → (A → Vec B n) → Vec B (m * n) xs >>= f = concat (map f xs) infixl 4 _⊛*_ _⊛*_ : Vec (A → B) m → Vec A n → Vec B (m * n) fs ⊛* xs = fs CartesianBind.>>= λ f → map f xs allPairs : Vec A m → Vec B n → Vec (A × B) (m * n) allPairs xs ys = map _,_ xs ⊛* ys -- Diagonal diagonal : Vec (Vec A n) n → Vec A n diagonal [] = [] diagonal (xs ∷ xss) = head xs ∷ diagonal (map tail xss) module DiagonalBind where infixl 1 _>>=_ _>>=_ : Vec A n → (A → Vec B n) → Vec B n xs >>= f = diagonal (map f xs) ------------------------------------------------------------------------ -- Operations for reducing vectors -- Dependent folds module _ (A : Set a) (B : ℕ → Set b) where FoldrOp = ∀ {n} → A → B n → B (suc n) FoldlOp = ∀ {n} → B n → A → B (suc n) foldr : ∀ (B : ℕ → Set b) → FoldrOp A B → B zero → Vec A n → B n foldr B _⊕_ e [] = e foldr B _⊕_ e (x ∷ xs) = x ⊕ foldr B _⊕_ e xs foldl : ∀ (B : ℕ → Set b) → FoldlOp A B → B zero → Vec A n → B n foldl B _⊕_ e [] = e foldl B _⊕_ e (x ∷ xs) = foldl (B ∘ suc) _⊕_ (e ⊕ x) xs -- Non-dependent folds foldr′ : (A → B → B) → B → Vec A n → B foldr′ _⊕_ = foldr _ _⊕_ foldl′ : (B → A → B) → B → Vec A n → B foldl′ _⊕_ = foldl _ _⊕_ -- Non-empty folds foldr₁ : (A → A → A) → Vec A (suc n) → A foldr₁ _⊕_ (x ∷ []) = x foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys) foldl₁ : (A → A → A) → Vec A (suc n) → A foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs -- Special folds sum : Vec ℕ n → ℕ sum = foldr _ _+_ 0 count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ count P? [] = zero count P? (x ∷ xs) = if does (P? x) then suc else id $ count P? xs countᵇ : (A → Bool) → Vec A n → ℕ countᵇ p = count (T? ∘ p) ------------------------------------------------------------------------ -- Operations for building vectors [_] : A → Vec A 1 [ x ] = x ∷ [] replicate : (n : ℕ) → A → Vec A n replicate zero x = [] replicate (suc n) x = x ∷ replicate n x tabulate : (Fin n → A) → Vec A n tabulate {n = zero} f = [] tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc) allFin : ∀ n → Vec (Fin n) n allFin _ = tabulate id ------------------------------------------------------------------------ -- Operations for dividing vectors splitAt : ∀ m {n} (xs : Vec A (m + n)) → ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs splitAt zero xs = [] , xs , refl splitAt (suc m) (x ∷ xs) = let ys , zs , eq = splitAt m xs in x ∷ ys , zs , cong (x ∷_) eq take : ∀ m {n} → Vec A (m + n) → Vec A m take m xs = proj₁ (splitAt m xs) drop : ∀ m {n} → Vec A (m + n) → Vec A n drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) group (suc n) k xs = let ys , zs , eq-split = splitAt k xs in let zss , eq-group = group n k zs in (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group) split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋ split [] = ([] , []) split (x ∷ []) = (x ∷ [] , []) split (x ∷ y ∷ xs) = Product.map (x ∷_) (y ∷_) (split xs) uncons : Vec A (suc n) → A × Vec A n uncons (x ∷ xs) = x , xs ------------------------------------------------------------------------ -- Operations involving ≤ -- Take the first 'm' elements of a vector. truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m truncate {m = zero} _ _ = [] truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) -- Pad out a vector with extra elements. padRight : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n padRight z≤n a xs = replicate _ a padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs ------------------------------------------------------------------------ -- Operations for converting between lists toList : Vec A n → List A toList [] = List.[] toList (x ∷ xs) = List._∷_ x (toList xs) fromList : (xs : List A) → Vec A (List.length xs) fromList List.[] = [] fromList (List._∷_ x xs) = x ∷ fromList xs ------------------------------------------------------------------------ -- Operations for reversing vectors -- snoc infixl 5 _∷ʳ_ _∷ʳ_ : Vec A n → A → Vec A (suc n) [] ∷ʳ y = [ y ] (x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y) -- vanilla reverse reverse : Vec A n → Vec A n reverse = foldl (Vec _) (λ rev x → x ∷ rev) [] -- reverse-append infix 5 _ʳ++_ _ʳ++_ : Vec A m → Vec A n → Vec A (m + n) xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs -- init and last initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y initLast {n = zero} (x ∷ []) = [] , x , refl initLast {n = suc n} (x ∷ xs) = let ys , y , eq = initLast xs in x ∷ ys , y , cong (x ∷_) eq init : Vec A (1 + n) → Vec A n init xs = proj₁ (initLast xs) last : Vec A (1 + n) → A last xs = proj₁ (proj₂ (initLast xs)) ------------------------------------------------------------------------ -- Other operations transpose : Vec (Vec A n) m → Vec (Vec A m) n transpose {n = n} [] = replicate n [] transpose {n = n} (as ∷ ass) = ((replicate n _∷_) ⊛ as) ⊛ transpose ass ------------------------------------------------------------------------ -- DEPRECATED ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 remove = removeAt {-# WARNING_ON_USAGE remove "Warning: remove was deprecated in v2.0. Please use removeAt instead." #-} insert = insertAt {-# WARNING_ON_USAGE insert "Warning: insert was deprecated in v2.0. Please use insertAt instead." #-}