From 2d9fbc86adea7fe74505e287f50bb3bc04385d23 Mon Sep 17 00:00:00 2001 From: Github Actions Date: Mon, 12 Aug 2024 12:54:58 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib@04f9d1cc8fce10e0bd947acc2e79d937f9a6d86b=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- master/Data.Vec.Recursive.Effectful.html | 24 +- master/Data.Vec.Recursive.Properties.html | 48 ++-- master/Data.Vec.Recursive.html | 271 +++++++++++----------- 3 files changed, 171 insertions(+), 172 deletions(-) diff --git a/master/Data.Vec.Recursive.Effectful.html b/master/Data.Vec.Recursive.Effectful.html index 8aa8d76ac5..edcd9c7722 100644 --- a/master/Data.Vec.Recursive.Effectful.html +++ b/master/Data.Vec.Recursive.Effectful.html @@ -20,14 +20,14 @@ ------------------------------------------------------------------------ -- Functor and applicative -functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n) -functor n = record { _<$>_ = λ f → map f n } +functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n) +functor n = record { _<$>_ = λ f → map f n } -applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n) +applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n) applicative n = record { rawFunctor = functor n - ; pure = replicate n - ; _<*>_ = ap n + ; pure = replicate n + ; _<*>_ = ap n } ------------------------------------------------------------------------ @@ -37,27 +37,27 @@ open RawApplicative App - sequenceA : ∀ {n A} → F A ^ n → F (A ^ n) + sequenceA : ∀ {n A} → F A ^ n → F (A ^ n) sequenceA {0} _ = pure _ sequenceA {1} fa = fa sequenceA {suc (suc _)} (fa , fas) = _,_ <$> fa ⊛ sequenceA fas - mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n) - mapA f = sequenceA ∘ map f _ + mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n) + mapA f = sequenceA ∘ map f _ - forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n) + forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n) forA = flip mapA module _ {m n M} (Mon : RawMonad {m} {n} M) where private App = RawMonad.rawApplicative Mon - sequenceM : ∀ {n A} → M A ^ n → M (A ^ n) + sequenceM : ∀ {n A} → M A ^ n → M (A ^ n) sequenceM = sequenceA App - mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n) + mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n) mapM = mapA App - forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n) + forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n) forM = forA App \ No newline at end of file diff --git a/master/Data.Vec.Recursive.Properties.html b/master/Data.Vec.Recursive.Properties.html index 8d5016743b..8b08d4ce3c 100644 --- a/master/Data.Vec.Recursive.Properties.html +++ b/master/Data.Vec.Recursive.Properties.html @@ -29,33 +29,33 @@ ------------------------------------------------------------------------ -- Basic proofs -cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as +cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as cons-head-tail-identity 0 as = refl cons-head-tail-identity (suc n) as = refl -head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a +head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a head-cons-identity 0 a as = refl head-cons-identity (suc n) a as = refl -tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as +tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as tail-cons-identity 0 a as = refl tail-cons-identity (suc n) a as = refl -append-cons : ∀ m n a (xs : A ^ m) ys → - append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys) +append-cons : ∀ m n a (xs : A ^ m) ys → + append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys) append-cons 0 n a xs ys = refl append-cons (suc m) n a xs ys = refl -append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as +append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as append-splitAt-identity 0 n as = refl append-splitAt-identity (suc m) n as = begin - let x = head (m + n) as in - let (xs , ys) = splitAt m n (tail (m + n) as) in - append (suc m) n (cons m (head (m + n) as) xs) ys + let x = head (m + n) as in + let (xs , ys) = splitAt m n (tail (m + n) as) in + append (suc m) n (cons m (head (m + n) as) xs) ys ≡⟨ append-cons m n x xs ys ⟩ - cons (m + n) x (append m n xs ys) - ≡⟨ cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩ - cons (m + n) x (tail (m + n) as) + cons (m + n) x (append m n xs ys) + ≡⟨ cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩ + cons (m + n) x (tail (m + n) as) ≡⟨ cons-head-tail-identity (m + n) as ⟩ as ∎ @@ -63,30 +63,30 @@ ------------------------------------------------------------------------ -- Conversion to and from Vec -fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs +fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs fromVec∘toVec 0 _ = refl fromVec∘toVec (suc n) xs = begin - cons n (head n xs) (fromVec (toVec n (tail n xs))) - ≡⟨ cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩ - cons n (head n xs) (tail n xs) + cons n (head n xs) (fromVec (toVec n (tail n xs))) + ≡⟨ cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩ + cons n (head n xs) (tail n xs) ≡⟨ cons-head-tail-identity n xs ⟩ xs ∎ -toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs +toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs toVec∘fromVec Vec.[] = refl toVec∘fromVec {n = suc n} (x Vec.∷ xs) = begin - head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs))) - ≡⟨ cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩ - x Vec.∷ toVec n (fromVec xs) + head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs))) + ≡⟨ cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩ + x Vec.∷ toVec n (fromVec xs) ≡⟨ cong (x Vec.∷_) (toVec∘fromVec xs) ⟩ x Vec.∷ xs ∎ where - hd-prf = head-cons-identity _ x (fromVec xs) - tl-prf = tail-cons-identity _ x (fromVec xs) + hd-prf = head-cons-identity _ x (fromVec xs) + tl-prf = tail-cons-identity _ x (fromVec xs) -↔Vec : ∀ n → A ^ n ↔ Vec A n -↔Vec n = mk↔ₛ′ (toVec n) fromVec toVec∘fromVec (fromVec∘toVec n) +↔Vec : ∀ n → A ^ n ↔ Vec A n +↔Vec n = mk↔ₛ′ (toVec n) fromVec toVec∘fromVec (fromVec∘toVec n) ------------------------------------------------------------------------ -- DEPRECATED NAMES diff --git a/master/Data.Vec.Recursive.html b/master/Data.Vec.Recursive.html index a552dd4021..555fa6518b 100644 --- a/master/Data.Vec.Recursive.html +++ b/master/Data.Vec.Recursive.html @@ -29,140 +29,139 @@ open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Unit.Polymorphic.Properties using (⊤↔⊤*) open import Data.Vec.Base as Vec using (Vec; _∷_) -open import Data.Vec.N-ary using (N-ary) -open import Function.Base using (_∘′_; _∘_; id; const) -open import Function.Bundles using (_↔_; mk↔ₛ′; mk↔) -open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans) -open import Level using (Level; lift) -open import Relation.Unary using (IUniversal; Universal; _⇒_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; subst) -open import Relation.Binary.Structures using (IsEquivalence) - -private - variable - a b c p : Level - A : Set a - B : Set b - C : Set c - ------------------------------------------------------------------------- --- Types and patterns - -infix 8 _^_ -_^_ : Set a → ℕ → Set a -A ^ 0 = ⊤ -A ^ 1 = A -A ^ (suc n@(suc _)) = A × A ^ n - -pattern [] = lift tt - -infix 3 _∈[_]_ -_∈[_]_ : {A : Set a} → A → ∀ n → A ^ n → Set a -a ∈[ 0 ] as = ⊥ -a ∈[ 1 ] a′ = a ≡ a′ -a ∈[ suc n@(suc _) ] a′ , as = a ≡ a′ ⊎ a ∈[ n ] as - ------------------------------------------------------------------------- --- Basic operations - -cons : ∀ n → A → A ^ n → A ^ suc n -cons 0 a _ = a -cons (suc n) a as = a , as - -uncons : ∀ n → A ^ suc n → A × A ^ n -uncons 0 a = a , lift tt -uncons (suc n) (a , as) = a , as - -head : ∀ n → A ^ suc n → A -head n as = proj₁ (uncons n as) - -tail : ∀ n → A ^ suc n → A ^ n -tail n as = proj₂ (uncons n as) - -fromVec : ∀[ Vec A ⇒ (A ^_) ] -fromVec = Vec.foldr (_ ^_) (cons _) _ - -toVec : Π[ (A ^_) ⇒ Vec A ] -toVec 0 as = Vec.[] -toVec (suc n) as = head n as ∷ toVec n (tail n as) - -lookup : ∀ {n} → A ^ n → Fin n → A -lookup as (zero {n}) = head n as -lookup as (suc {n} k) = lookup (tail n as) k - -replicate : ∀ n → A → A ^ n -replicate n a = fromVec (Vec.replicate n a) - -tabulate : ∀ n → (Fin n → A) → A ^ n -tabulate n f = fromVec (Vec.tabulate f) - -append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n) -append 0 n xs ys = ys -append 1 n x ys = cons n x ys -append (suc m@(suc _)) n (x , xs) ys = x , append m n xs ys - -splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n -splitAt 0 n xs = [] , xs -splitAt (suc m) n xs = - let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in - cons m (head (m Nat.+ n) xs) ys , zs - ------------------------------------------------------------------------- --- Manipulating N-ary products - -map : (A → B) → ∀ n → A ^ n → B ^ n -map f 0 as = lift tt -map f 1 a = f a -map f (suc n@(suc _)) (a , as) = f a , map f n as - -ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n -ap 0 fs ts = [] -ap 1 f t = f t -ap (suc n@(suc _)) (f , fs) (t , ts) = f t , ap n fs ts - -module _ {P : ℕ → Set p} where - - foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) → - ∀ n → A ^ n → P n - foldr p0 p1 p2+ 0 as = p0 - foldr p0 p1 p2+ 1 a = p1 a - foldr p0 p1 p2+ (suc n′@(suc n)) (a , as) = p2+ n a (foldr p0 p1 p2+ n′ as) - -foldl : (P : ℕ → Set p) → - P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) → - ∀ n → A ^ n → P n -foldl P p0 p1 p2+ 0 as = p0 -foldl P p0 p1 p2+ 1 a = p1 a -foldl P p0 p1 p2+ (suc n@(suc _)) (a , as) = let p1′ = p1 a in - foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) n as - -reverse : ∀ n → A ^ n → A ^ n -reverse = foldl (_ ^_) [] id (λ n → _,_) - -zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n -zipWith f 0 as bs = [] -zipWith f 1 a b = f a b -zipWith f ((suc n@(suc _))) (a , as) (b , bs) = f a b , zipWith f n as bs - -unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n -unzipWith f 0 as = [] , [] -unzipWith f 1 a = f a -unzipWith f (suc n@(suc _)) (a , as) = Product.zip _,_ _,_ (f a) (unzipWith f n as) - -zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n -zip = zipWith _,_ - -unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n -unzip = unzipWith id - -lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n -lift↔ 0 A↔B = mk↔ₛ′ _ _ (const refl) (const refl) -lift↔ 1 A↔B = A↔B -lift↔ (suc n@(suc _)) A↔B = ×-cong A↔B (lift↔ n A↔B) - -Fin[m^n]↔Fin[m]^n : ∀ m n → Fin (m Nat.^ n) ↔ Fin m ^ n -Fin[m^n]↔Fin[m]^n m 0 = ↔-trans 1↔⊤ (↔-sym ⊤↔⊤*) -Fin[m^n]↔Fin[m]^n m 1 = subst (λ x → Fin x ↔ Fin m) - (trans (sym (+-comm m zero)) (*-comm 1 m)) ↔-refl -Fin[m^n]↔Fin[m]^n m (suc (suc n)) = ↔-trans (*↔× {m = m}) (×-cong ↔-refl (Fin[m^n]↔Fin[m]^n _ _)) +open import Function.Base using (_∘′_; _∘_; id; const) +open import Function.Bundles using (_↔_; mk↔ₛ′; mk↔) +open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans) +open import Level using (Level; lift) +open import Relation.Unary using (IUniversal; Universal; _⇒_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; subst) +open import Relation.Binary.Structures using (IsEquivalence) + +private + variable + a b c p : Level + A : Set a + B : Set b + C : Set c + +------------------------------------------------------------------------ +-- Types and patterns + +infix 8 _^_ +_^_ : Set a → ℕ → Set a +A ^ 0 = ⊤ +A ^ 1 = A +A ^ (suc n@(suc _)) = A × A ^ n + +pattern [] = lift tt + +infix 3 _∈[_]_ +_∈[_]_ : {A : Set a} → A → ∀ n → A ^ n → Set a +a ∈[ 0 ] as = ⊥ +a ∈[ 1 ] a′ = a ≡ a′ +a ∈[ suc n@(suc _) ] a′ , as = a ≡ a′ ⊎ a ∈[ n ] as + +------------------------------------------------------------------------ +-- Basic operations + +cons : ∀ n → A → A ^ n → A ^ suc n +cons 0 a _ = a +cons (suc n) a as = a , as + +uncons : ∀ n → A ^ suc n → A × A ^ n +uncons 0 a = a , lift tt +uncons (suc n) (a , as) = a , as + +head : ∀ n → A ^ suc n → A +head n as = proj₁ (uncons n as) + +tail : ∀ n → A ^ suc n → A ^ n +tail n as = proj₂ (uncons n as) + +fromVec : ∀[ Vec A ⇒ (A ^_) ] +fromVec = Vec.foldr (_ ^_) (cons _) _ + +toVec : Π[ (A ^_) ⇒ Vec A ] +toVec 0 as = Vec.[] +toVec (suc n) as = head n as ∷ toVec n (tail n as) + +lookup : ∀ {n} → A ^ n → Fin n → A +lookup as (zero {n}) = head n as +lookup as (suc {n} k) = lookup (tail n as) k + +replicate : ∀ n → A → A ^ n +replicate n a = fromVec (Vec.replicate n a) + +tabulate : ∀ n → (Fin n → A) → A ^ n +tabulate n f = fromVec (Vec.tabulate f) + +append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n) +append 0 n xs ys = ys +append 1 n x ys = cons n x ys +append (suc m@(suc _)) n (x , xs) ys = x , append m n xs ys + +splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n +splitAt 0 n xs = [] , xs +splitAt (suc m) n xs = + let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in + cons m (head (m Nat.+ n) xs) ys , zs + +------------------------------------------------------------------------ +-- Manipulating N-ary products + +map : (A → B) → ∀ n → A ^ n → B ^ n +map f 0 as = lift tt +map f 1 a = f a +map f (suc n@(suc _)) (a , as) = f a , map f n as + +ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n +ap 0 fs ts = [] +ap 1 f t = f t +ap (suc n@(suc _)) (f , fs) (t , ts) = f t , ap n fs ts + +module _ {P : ℕ → Set p} where + + foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) → + ∀ n → A ^ n → P n + foldr p0 p1 p2+ 0 as = p0 + foldr p0 p1 p2+ 1 a = p1 a + foldr p0 p1 p2+ (suc n′@(suc n)) (a , as) = p2+ n a (foldr p0 p1 p2+ n′ as) + +foldl : (P : ℕ → Set p) → + P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (suc (suc n))) → + ∀ n → A ^ n → P n +foldl P p0 p1 p2+ 0 as = p0 +foldl P p0 p1 p2+ 1 a = p1 a +foldl P p0 p1 p2+ (suc n@(suc _)) (a , as) = let p1′ = p1 a in + foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) n as + +reverse : ∀ n → A ^ n → A ^ n +reverse = foldl (_ ^_) [] id (λ n → _,_) + +zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n +zipWith f 0 as bs = [] +zipWith f 1 a b = f a b +zipWith f ((suc n@(suc _))) (a , as) (b , bs) = f a b , zipWith f n as bs + +unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n +unzipWith f 0 as = [] , [] +unzipWith f 1 a = f a +unzipWith f (suc n@(suc _)) (a , as) = Product.zip _,_ _,_ (f a) (unzipWith f n as) + +zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n +zip = zipWith _,_ + +unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n +unzip = unzipWith id + +lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n +lift↔ 0 A↔B = mk↔ₛ′ _ _ (const refl) (const refl) +lift↔ 1 A↔B = A↔B +lift↔ (suc n@(suc _)) A↔B = ×-cong A↔B (lift↔ n A↔B) + +Fin[m^n]↔Fin[m]^n : ∀ m n → Fin (m Nat.^ n) ↔ Fin m ^ n +Fin[m^n]↔Fin[m]^n m 0 = ↔-trans 1↔⊤ (↔-sym ⊤↔⊤*) +Fin[m^n]↔Fin[m]^n m 1 = subst (λ x → Fin x ↔ Fin m) + (trans (sym (+-comm m zero)) (*-comm 1 m)) ↔-refl +Fin[m^n]↔Fin[m]^n m (suc (suc n)) = ↔-trans (*↔× {m = m}) (×-cong ↔-refl (Fin[m^n]↔Fin[m]^n _ _)) \ No newline at end of file