diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c9dd0e092..7308415529 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -599,6 +599,7 @@ Non-backwards compatible changes ```agda WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _ WfRec _<_ P x = ∀ {y} → y < x → P y + ``` ### Change in the definition of `_≤″_` (issue #1919) @@ -920,7 +921,7 @@ Non-backwards compatible changes Data.Vec.Relation.Binary.Lex.NonStrict Relation.Binary.Reasoning.StrictPartialOrder Relation.Binary.Reasoning.PartialOrder - ``` + ``` ### Other @@ -1049,60 +1050,61 @@ Non-backwards compatible changes `List` module i.e. `lookup` takes its container first and the index (whose type may depend on the container value) second. This affects modules: - ``` - Codata.Guarded.Stream - Codata.Guarded.Stream.Relation.Binary.Pointwise - Codata.Musical.Colist.Base - Codata.Musical.Colist.Relation.Unary.Any.Properties - Codata.Musical.Covec - Codata.Musical.Stream - Codata.Sized.Colist - Codata.Sized.Covec - Codata.Sized.Stream - Data.Vec.Relation.Unary.All - Data.Star.Environment - Data.Star.Pointer - Data.Star.Vec - Data.Trie - Data.Trie.NonEmpty - Data.Tree.AVL - Data.Tree.AVL.Indexed - Data.Tree.AVL.Map - Data.Tree.AVL.NonEmpty - Data.Vec.Recursive - Tactic.RingSolver - Tactic.RingSolver.Core.NatSet - ``` + ``` + Codata.Guarded.Stream + Codata.Guarded.Stream.Relation.Binary.Pointwise + Codata.Musical.Colist.Base + Codata.Musical.Colist.Relation.Unary.Any.Properties + Codata.Musical.Covec + Codata.Musical.Stream + Codata.Sized.Colist + Codata.Sized.Covec + Codata.Sized.Stream + Data.Vec.Relation.Unary.All + Data.Star.Environment + Data.Star.Pointer + Data.Star.Vec + Data.Trie + Data.Trie.NonEmpty + Data.Tree.AVL + Data.Tree.AVL.Indexed + Data.Tree.AVL.Map + Data.Tree.AVL.NonEmpty + Data.Vec.Recursive + Tactic.RingSolver + Tactic.RingSolver.Core.NatSet + ``` - * Moved & renamed from `Data.Vec.Relation.Unary.All` - to `Data.Vec.Relation.Unary.All.Properties`: - ``` - lookup ↦ lookup⁺ - tabulate ↦ lookup⁻ - ``` +* Moved & renamed from `Data.Vec.Relation.Unary.All` + to `Data.Vec.Relation.Unary.All.Properties`: + ``` + lookup ↦ lookup⁺ + tabulate ↦ lookup⁻ + ``` - * Renamed in `Data.Vec.Relation.Unary.Linked.Properties` - and `Codata.Guarded.Stream.Relation.Binary.Pointwise`: - ``` - lookup ↦ lookup⁺ - ``` +* Renamed in `Data.Vec.Relation.Unary.Linked.Properties` + and `Codata.Guarded.Stream.Relation.Binary.Pointwise`: + ``` + lookup ↦ lookup⁺ + ``` - * Added the following new definitions to `Data.Vec.Relation.Unary.All`: - ``` - lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i) - lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i) - lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) - lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) - ``` +* Added the following new definitions to `Data.Vec.Relation.Unary.All`: + ``` + lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i) + lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i) + lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) + lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) + ``` - * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to - `¬¬-excluded-middle`. +* `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to + `¬¬-excluded-middle`. - * `iterate` in `Data.Vec.Base` now takes `n` (the length of `Vec`) as an - explicit argument. - ```agda - iterate : (A → A) → A → ∀ n → Vec A n - ``` +* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional` + now take the length of vector, `n`, as an explicit rather than an implicit argument. + ```agda + iterate : (A → A) → A → ∀ n → Vec A n + replicate : ∀ n → A → Vec A n + ``` Major improvements ------------------ diff --git a/src/Algebra/Properties/Monoid/Sum.agda b/src/Algebra/Properties/Monoid/Sum.agda index 2d8605a2b0..166cba4462 100644 --- a/src/Algebra/Properties/Monoid/Sum.agda +++ b/src/Algebra/Properties/Monoid/Sum.agda @@ -64,15 +64,15 @@ sum-cong-≗ : ∀ {n} → sum {n} Preserves _≗_ ⟶ _≡_ sum-cong-≗ {zero} xs≗ys = P.refl sum-cong-≗ {suc n} xs≗ys = P.cong₂ _+_ (xs≗ys zero) (sum-cong-≗ (xs≗ys ∘ suc)) -sum-replicate : ∀ n {x} → sum {n} (replicate x) ≈ n × x +sum-replicate : ∀ n {x} → sum (replicate n x) ≈ n × x sum-replicate zero = refl sum-replicate (suc n) = +-congˡ (sum-replicate n) sum-replicate-idem : ∀ {x} → _+_ IdempotentOn x → - ∀ n → .{{_ : NonZero n}} → sum {n} (replicate x) ≈ x + ∀ n → .{{_ : NonZero n}} → sum (replicate n x) ≈ x sum-replicate-idem idem n = trans (sum-replicate n) (×-idem idem n) -sum-replicate-zero : ∀ n → sum {n} (replicate 0#) ≈ 0# +sum-replicate-zero : ∀ n → sum (replicate n 0#) ≈ 0# sum-replicate-zero zero = refl sum-replicate-zero (suc n) = sum-replicate-idem (+-identityˡ 0#) (suc n) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 7e4b14b18c..8062ff34df 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -33,6 +33,10 @@ open import Relation.Nullary.Decidable using (Dec) open CommutativeMonoid M open EqReasoning setoid +private + variable + n : ℕ + ------------------------------------------------------------------------ -- Monoid expressions @@ -55,7 +59,7 @@ Env n = Vec Carrier n -- The semantics of an expression is a function from an environment to -- a value. -⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier +⟦_⟧ : Expr n → Env n → Carrier ⟦ var x ⟧ ρ = lookup ρ x ⟦ id ⟧ ρ = ε ⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ @@ -70,27 +74,27 @@ Normal n = Vec ℕ n -- The semantics of a normal form. -⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier +⟦_⟧⇓ : Normal n → Env n → Carrier ⟦ [] ⟧⇓ _ = ε -⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (λ b → a ∙ b) n +⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n ------------------------------------------------------------------------ -- Constructions on normal forms -- The empty bag. -empty : ∀{n} → Normal n -empty = replicate 0 +empty : Normal n +empty = replicate _ 0 -- A singleton bag. -sg : ∀{n} (i : Fin n) → Normal n +sg : (i : Fin n) → Normal n sg zero = 1 ∷ empty sg (suc i) = 0 ∷ sg i -- The composition of normal forms. -_•_ : ∀{n} (v w : Normal n) → Normal n +_•_ : (v w : Normal n) → Normal n [] • [] = [] (l ∷ v) • (m ∷ w) = l + m ∷ v • w @@ -99,13 +103,13 @@ _•_ : ∀{n} (v w : Normal n) → Normal n -- The empty bag stands for the unit ε. -empty-correct : ∀{n} (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε +empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε empty-correct [] = refl empty-correct (a ∷ ρ) = empty-correct ρ -- The singleton bag stands for a single variable. -sg-correct : ∀{n} (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x +sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x sg-correct zero (x ∷ ρ) = begin x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ x ∙ ε ≈⟨ identityʳ _ ⟩ @@ -114,7 +118,7 @@ sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ -- Normal form composition corresponds to the composition of the monoid. -comp-correct : ∀ {n} (v w : Normal n) (ρ : Env n) → +comp-correct : (v w : Normal n) (ρ : Env n) → ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) comp-correct [] [] ρ = sym (identityˡ _) comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ) @@ -136,14 +140,14 @@ comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ) -- A normaliser. -normalise : ∀ {n} → Expr n → Normal n +normalise : Expr n → Normal n normalise (var x) = sg x normalise id = empty normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ -- The normaliser preserves the semantics of the expression. -normalise-correct : ∀ {n} (e : Expr n) (ρ : Env n) → +normalise-correct : (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ normalise-correct (var x) ρ = sg-correct x ρ normalise-correct id ρ = empty-correct ρ @@ -171,14 +175,14 @@ open module R = Reflection infix 5 _≟_ -_≟_ : ∀ {n} (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) +_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) where open Pointwise -- We can also give a sound, but not necessarily complete, procedure -- for determining if two expressions have the same semantics. -prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) prove′ e₁ e₂ = Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂)) where diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index fdba81a838..fc65652787 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -34,6 +34,10 @@ module Algebra.Solver.IdempotentCommutativeMonoid open IdempotentCommutativeMonoid M open EqReasoning setoid +private + variable + n : ℕ + ------------------------------------------------------------------------ -- Monoid expressions @@ -71,7 +75,7 @@ Normal n = Vec Bool n -- The semantics of a normal form. -⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier +⟦_⟧⇓ : Normal n → Env n → Carrier ⟦ [] ⟧⇓ _ = ε ⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ) @@ -80,18 +84,18 @@ Normal n = Vec Bool n -- The empty set. -empty : ∀{n} → Normal n -empty = replicate false +empty : Normal n +empty = replicate _ false -- A singleton set. -sg : ∀{n} (i : Fin n) → Normal n +sg : (i : Fin n) → Normal n sg zero = true ∷ empty sg (suc i) = false ∷ sg i -- The composition of normal forms. -_•_ : ∀{n} (v w : Normal n) → Normal n +_•_ : (v w : Normal n) → Normal n [] • [] = [] (l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w @@ -100,13 +104,13 @@ _•_ : ∀{n} (v w : Normal n) → Normal n -- The empty set stands for the unit ε. -empty-correct : ∀{n} (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε +empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε empty-correct [] = refl empty-correct (a ∷ ρ) = empty-correct ρ -- The singleton set stands for a single variable. -sg-correct : ∀{n} (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x +sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x sg-correct zero (x ∷ ρ) = begin x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ x ∙ ε ≈⟨ identityʳ _ ⟩ @@ -132,7 +136,7 @@ distr a b c = begin a ∙ (b ∙ (a ∙ c)) ≈⟨ sym (assoc _ _ _) ⟩ (a ∙ b) ∙ (a ∙ c) ∎ -comp-correct : ∀ {n} (v w : Normal n) (ρ : Env n) → +comp-correct : ∀ (v w : Normal n) (ρ : Env n) → ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) comp-correct [] [] ρ = sym (identityˡ _) comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = @@ -149,14 +153,14 @@ comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = -- A normaliser. -normalise : ∀ {n} → Expr n → Normal n +normalise : Expr n → Normal n normalise (var x) = sg x normalise id = empty normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ -- The normaliser preserves the semantics of the expression. -normalise-correct : ∀ {n} (e : Expr n) (ρ : Env n) → +normalise-correct : (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ normalise-correct (var x) ρ = sg-correct x ρ normalise-correct id ρ = empty-correct ρ @@ -184,14 +188,14 @@ open module R = Reflection infix 5 _≟_ -_≟_ : ∀ {n} (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) +_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) where open Pointwise -- We can also give a sound, but not necessarily complete, procedure -- for determining if two expressions have the same semantics. -prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) prove′ e₁ e₂ = Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂)) where diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index 41b19ec947..bd41d1967e 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -80,11 +80,11 @@ lookup-repeat : ∀ n (a : A) → lookup (repeat a) n ≡ a lookup-repeat zero a = P.refl lookup-repeat (suc n) a = lookup-repeat n a -splitAt-repeat : ∀ n (a : A) → splitAt n (repeat a) ≡ (Vec.replicate a , repeat a) +splitAt-repeat : ∀ n (a : A) → splitAt n (repeat a) ≡ (Vec.replicate n a , repeat a) splitAt-repeat zero a = P.refl splitAt-repeat (suc n) a = cong (Prod.map₁ (a ∷_)) (splitAt-repeat n a) -take-repeat : ∀ n (a : A) → take n (repeat a) ≡ Vec.replicate a +take-repeat : ∀ n (a : A) → take n (repeat a) ≡ Vec.replicate n a take-repeat n a = cong proj₁ (splitAt-repeat n a) drop-repeat : ∀ n (a : A) → drop n (repeat a) ≡ repeat a @@ -115,17 +115,17 @@ zipWith-repeat : ∀ (f : A → B → C) a b → zipWith-repeat f a b .head = P.refl zipWith-repeat f a b .tail = zipWith-repeat f a b -chunksOf-repeat : ∀ n (a : A) → chunksOf n (repeat a) ≈ repeat (Vec.replicate a) +chunksOf-repeat : ∀ n (a : A) → chunksOf n (repeat a) ≈ repeat (Vec.replicate n a) chunksOf-repeat n a = begin go where open ≈-Reasoning - go : chunksOf n (repeat a) ≈∞ repeat (Vec.replicate a) + go : chunksOf n (repeat a) ≈∞ repeat (Vec.replicate n a) go .head = take-repeat n a go .tail = chunksOf n (drop n (repeat a)) ≡⟨ P.cong (chunksOf n) (drop-repeat n a) ⟩ chunksOf n (repeat a) ↺⟨ go ⟩ - repeat (Vec.replicate a) ∎ + repeat (Vec.replicate n a) ∎ ------------------------------------------------------------------------ -- Properties of map diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda index 69685e12b2..d2cf4e3205 100644 --- a/src/Codata/Sized/Stream/Properties.agda +++ b/src/Codata/Sized/Stream/Properties.agda @@ -41,11 +41,11 @@ lookup-repeat-identity : (n : ℕ) (a : A) → lookup (repeat a) n ≡ a lookup-repeat-identity zero a = P.refl lookup-repeat-identity (suc n) a = lookup-repeat-identity n a -take-repeat-identity : (n : ℕ) (a : A) → take n (repeat a) ≡ Vec.replicate a +take-repeat-identity : (n : ℕ) (a : A) → take n (repeat a) ≡ Vec.replicate n a take-repeat-identity zero a = P.refl take-repeat-identity (suc n) a = P.cong (a Vec.∷_) (take-repeat-identity n a) -splitAt-repeat-identity : (n : ℕ) (a : A) → splitAt n (repeat a) ≡ (Vec.replicate a , repeat a) +splitAt-repeat-identity : (n : ℕ) (a : A) → splitAt n (repeat a) ≡ (Vec.replicate n a , repeat a) splitAt-repeat-identity zero a = P.refl splitAt-repeat-identity (suc n) a = P.cong (Prod.map₁ (a ∷_)) (splitAt-repeat-identity n a) diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda index b3d53106ff..2e44f69762 100644 --- a/src/Data/Fin/Subset.agda +++ b/src/Data/Fin/Subset.agda @@ -43,11 +43,11 @@ Subset = Vec Side -- The empty subset ⊥ : Subset n -⊥ = replicate outside +⊥ = replicate _ outside -- The full subset ⊤ : Subset n -⊤ = replicate inside +⊤ = replicate _ inside -- A singleton subset, containing just the given element. ⁅_⁆ : Fin n → Subset n diff --git a/src/Data/String.agda b/src/Data/String.agda index 0ad40779fa..f8ca8385e4 100644 --- a/src/Data/String.agda +++ b/src/Data/String.agda @@ -23,7 +23,6 @@ open import Relation.Nullary.Decidable.Core using (does) open import Data.List.Membership.DecPropositional Char._≟_ - ------------------------------------------------------------------------ -- Re-export contents of base, and decidability of equality @@ -62,10 +61,10 @@ rectangle pads cells = Vec.zipWith (λ p c → p width c) pads cells where -- Special cases for left, center, and right alignment rectangleˡ : ∀ {n} → Char → Vec String n → Vec String n -rectangleˡ c = rectangle (Vec.replicate $ padLeft c) +rectangleˡ c = rectangle (Vec.replicate _ $ padLeft c) rectangleʳ : ∀ {n} → Char → Vec String n → Vec String n -rectangleʳ c = rectangle (Vec.replicate $ padRight c) +rectangleʳ c = rectangle (Vec.replicate _ $ padRight c) rectangleᶜ : ∀ {n} → Char → Char → Vec String n → Vec String n -rectangleᶜ cₗ cᵣ = rectangle (Vec.replicate $ padBoth cₗ cᵣ) +rectangleᶜ cₗ cᵣ = rectangle (Vec.replicate _ $ padBoth cₗ cᵣ) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index be668897cb..0f56c9fbd7 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -243,9 +243,9 @@ count P? = countᵇ (does ∘ P?) [_] : A → Vec A 1 [ x ] = x ∷ [] -replicate : A → Vec A n -replicate {n = zero} x = [] -replicate {n = suc n} x = x ∷ replicate 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 = [] @@ -295,7 +295,7 @@ 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 z≤n a xs = replicate _ a padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs ------------------------------------------------------------------------ @@ -350,8 +350,8 @@ last xs = proj₁ (proj₂ (initLast xs)) -- Other operations transpose : Vec (Vec A n) m → Vec (Vec A m) n -transpose [] = replicate [] -transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass +transpose {n = n} [] = replicate n [] +transpose {n = n} (as ∷ ass) = ((replicate n _∷_) ⊛ as) ⊛ transpose ass ------------------------------------------------------------------------ -- DEPRECATED diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda index 17b33ef7be..c857ee6642 100644 --- a/src/Data/Vec/Bounded/Base.agda +++ b/src/Data/Vec/Bounded/Base.agda @@ -49,14 +49,14 @@ fromVec v = v , ℕₚ.≤-refl padRight : ∀ {n} → A → Vec≤ A n → Vec A n padRight a (vs , m≤n) with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n) -... | less-than-or-equal refl = vs Vec.++ Vec.replicate a +... | less-than-or-equal refl = vs Vec.++ Vec.replicate _ a padLeft : ∀ {n} → A → Vec≤ A n → Vec A n padLeft a as@(vs , m≤n) with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n) ... | less-than-or-equal {k} ∣as∣+k≡n with P.trans (ℕₚ.+-comm k (Vec≤.length as)) ∣as∣+k≡n -... | refl = Vec.replicate a Vec.++ vs +... | refl = Vec.replicate k a Vec.++ vs private split : ∀ {m n} k → m + k ≡ n → ⌊ k /2⌋ + (m + ⌈ k /2⌉) ≡ n @@ -72,10 +72,10 @@ padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n padBoth aₗ aᵣ as@(vs , m≤n) with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n) ... | less-than-or-equal {k} ∣as∣+k≡n - with split k ∣as∣+k≡n -... | refl = Vec.replicate {n = ⌊ k /2⌋} aₗ + with split k ∣as∣+k≡n +... | refl = Vec.replicate ⌊ k /2⌋ aₗ Vec.++ vs - Vec.++ Vec.replicate {n = ⌈ k /2⌉} aᵣ + Vec.++ Vec.replicate ⌈ k /2⌉ aᵣ fromList : (as : List A) → Vec≤ A (List.length as) @@ -88,7 +88,7 @@ toList = Vec.toList ∘ Vec≤.vec -- Creating new Vec≤ vectors replicate : ∀ {m n} .(m≤n : m ≤ n) → A → Vec≤ A n -replicate m≤n a = Vec.replicate a , m≤n +replicate m≤n a = Vec.replicate _ a , m≤n [] : ∀ {n} → Vec≤ A n [] = Vec.[] , z≤n diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda index 3d4c1a75e7..1ff96bd03c 100644 --- a/src/Data/Vec/Effectful.agda +++ b/src/Data/Vec/Effectful.agda @@ -34,9 +34,9 @@ functor = record } applicative : RawApplicative (λ (A : Set a) → Vec A n) -applicative = record +applicative {n = n} = record { rawFunctor = functor - ; pure = replicate + ; pure = replicate n ; _<*>_ = Vec._⊛_ } diff --git a/src/Data/Vec/Effectful/Transformer.agda b/src/Data/Vec/Effectful/Transformer.agda index cf491fdb84..637ec0b2ec 100644 --- a/src/Data/Vec/Effectful/Transformer.agda +++ b/src/Data/Vec/Effectful/Transformer.agda @@ -40,7 +40,7 @@ functor M = record applicative : RawApplicative M → RawApplicative {f} (VecT n M) applicative M = record { rawFunctor = functor rawFunctor - ; pure = mkVecT ∘′ pure ∘′ Vec.replicate + ; pure = mkVecT ∘′ pure ∘′ Vec.replicate _ ; _<*>_ = λ mf ma → mkVecT (Vec.zipWith _$_ <$> runVecT mf <*> runVecT ma) } where open RawApplicative M @@ -55,6 +55,6 @@ monad {f} {g} M = record monadT : RawMonadT {f} {g} (VecT n) monadT M = record - { lift = mkVecT ∘′ (Vec.replicate <$>_) + { lift = mkVecT ∘′ (Vec.replicate _ <$>_) ; rawMonad = monad M } where open RawMonad M diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 7b217a415b..776fedee3b 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -77,8 +77,8 @@ tail xs = xs ∘ suc uncons : Vector A (suc n) → A × Vector A n uncons xs = head xs , tail xs -replicate : A → Vector A n -replicate = const +replicate : (n : ℕ) → A → Vector A n +replicate n = const insertAt : Vector A n → Fin (suc n) → A → Vector A (suc n) insertAt {n = n} xs zero v zero = v diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda index 148fcf346f..ced1999e3a 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda @@ -142,7 +142,7 @@ module _ (R : REL A B r) where module _ {R : REL A B r} {x y n} where - replicate⁺ : R x y → Pointwise R {n = n} (replicate x) (replicate y) + replicate⁺ : R x y → Pointwise R {n = n} (replicate n x) (replicate n y) replicate⁺ = const ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda index 85b5075142..be031a1070 100644 --- a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda @@ -8,6 +8,7 @@ module Data.Vec.Functional.Relation.Unary.All.Properties where +open import Data.Nat.Base using (ℕ) open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt) open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ) open import Data.Product.Base as Σ using (_×_; _,_; proj₁; proj₂; uncurry) @@ -20,80 +21,73 @@ open import Relation.Unary private variable - a b c p q r ℓ : Level - A : Set a - B : Set b - C : Set c + a p ℓ : Level + A B C : Set a + P Q R : Pred A p + m n : ℕ + x y : A + xs ys : Vector A n ------------------------------------------------------------------------ -- map -module _ {P : Pred A p} {Q : Pred B q} {f : A → B} where - - map⁺ : (∀ {x} → P x → Q (f x)) → - ∀ {n xs} → All P {n = n} xs → All Q (VF.map f xs) - map⁺ pq ps i = pq (ps i) +map⁺ : ∀ {f : A → B} → (∀ {x} → P x → Q (f x)) → + All P xs → All Q (VF.map f xs) +map⁺ pq ps i = pq (ps i) ------------------------------------------------------------------------ -- replicate -module _ {P : Pred A p} {x : A} {n} where - - replicate⁺ : P x → All P (replicate {n = n} x) - replicate⁺ = const +replicate⁺ : P x → All P (replicate n x) +replicate⁺ = const ------------------------------------------------------------------------ -- _⊛_ -module _ {P : Pred A p} {Q : Pred B q} where - - ⊛⁺ : ∀ {n} {fs : Vector (A → B) n} {xs} → - All (λ f → ∀ {x} → P x → Q (f x)) fs → All P xs → All Q (fs ⊛ xs) - ⊛⁺ pqs ps i = (pqs i) (ps i) +⊛⁺ : ∀ {fs : Vector (A → B) n} → + All (λ f → ∀ {x} → P x → Q (f x)) fs → + All P xs → All Q (fs ⊛ xs) +⊛⁺ pqs ps i = (pqs i) (ps i) ------------------------------------------------------------------------ -- zipWith -module _ {P : Pred A p} {Q : Pred B q} {R : Pred C r} where - - zipWith⁺ : ∀ {f} → (∀ {x y} → P x → Q y → R (f x y)) → ∀ {n xs ys} → - All P xs → All Q ys → All R (zipWith f {n = n} xs ys) - zipWith⁺ pqr ps qs i = pqr (ps i) (qs i) +zipWith⁺ : ∀ {f} → (∀ {x y} → P x → Q y → R (f x y)) → + All P xs → All Q ys → All R (zipWith f xs ys) +zipWith⁺ pqr ps qs i = pqr (ps i) (qs i) ------------------------------------------------------------------------ -- zip -module _ {P : Pred A p} {Q : Pred B q} {n} {xs : Vector A n} {ys} where - - zip⁺ : All P xs → All Q ys → All (P ⟨×⟩ Q) (zip xs ys) - zip⁺ ps qs i = ps i , qs i +zip⁺ : All P xs → All Q ys → All (P ⟨×⟩ Q) (zip xs ys) +zip⁺ ps qs i = ps i , qs i - zip⁻ : All (P ⟨×⟩ Q) (zip xs ys) → All P xs × All Q ys - zip⁻ pqs = proj₁ ∘ pqs , proj₂ ∘ pqs +zip⁻ : All (P ⟨×⟩ Q) (zip xs ys) → All P xs × All Q ys +zip⁻ pqs = proj₁ ∘ pqs , proj₂ ∘ pqs ------------------------------------------------------------------------ -- head -head⁺ : ∀ (P : Pred A p) {n v} → All P v → P (head {n = n} v) +head⁺ : ∀ (P : Pred A p) → All P xs → P (head xs) head⁺ P ps = ps zero ------------------------------------------------------------------------ -- tail -tail⁺ : ∀ (P : Pred A p) {n v} → All P v → All P (tail {n = n} v) -tail⁺ P ps = ps ∘ suc +tail⁺ : ∀ (P : Pred A p) → All P xs → All P (tail xs) +tail⁺ P xs = xs ∘ suc ------------------------------------------------------------------------ -- ++ -module _ (P : Pred A p) {m n} {xs : Vector A m} {ys : Vector A n} where +module _ (P : Pred A p) {xs : Vector A m} {ys : Vector A n} where ++⁺ : All P xs → All P ys → All P (xs ++ ys) ++⁺ pxs pys i with splitAt m i ... | inj₁ i′ = pxs i′ ... | inj₂ j′ = pys j′ -module _ (P : Pred A p) {m n} (xs : Vector A m) {ys : Vector A n} where +module _ (P : Pred A p) (xs : Vector A m) {ys : Vector A n} where ++⁻ˡ : All P (xs ++ ys) → All P xs ++⁻ˡ ps i with ps (i ↑ˡ n) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index c48abc6f57..27df432105 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -143,7 +143,7 @@ padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs padRight-refl a [] = refl padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) -padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate a ≡ padRight m≤n a (replicate a) +padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m≤n a (replicate m a) padRight-replicate z≤n a = refl padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a) @@ -385,7 +385,7 @@ map-id : map id ≗ id {A = Vec A n} map-id [] = refl map-id (x ∷ xs) = cong (x ∷_) (map-id xs) -map-const : ∀ (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate y +map-const : ∀ (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate n y map-const [] _ = refl map-const (_ ∷ xs) y = cong (y ∷_) (map-const xs y) @@ -569,25 +569,25 @@ module _ {f : A → A → A} where module _ {f : A → A → A} {e : A} where zipWith-identityˡ : LeftIdentity _≡_ e f → - LeftIdentity _≡_ (replicate e) (zipWith {n = n} f) + LeftIdentity _≡_ (replicate n e) (zipWith f) zipWith-identityˡ idˡ [] = refl zipWith-identityˡ idˡ (x ∷ xs) = cong₂ _∷_ (idˡ x) (zipWith-identityˡ idˡ xs) zipWith-identityʳ : RightIdentity _≡_ e f → - RightIdentity _≡_ (replicate e) (zipWith {n = n} f) + RightIdentity _≡_ (replicate n e) (zipWith f) zipWith-identityʳ idʳ [] = refl zipWith-identityʳ idʳ (x ∷ xs) = cong₂ _∷_ (idʳ x) (zipWith-identityʳ idʳ xs) zipWith-zeroˡ : LeftZero _≡_ e f → - LeftZero _≡_ (replicate e) (zipWith {n = n} f) + LeftZero _≡_ (replicate n e) (zipWith f) zipWith-zeroˡ zeˡ [] = refl zipWith-zeroˡ zeˡ (x ∷ xs) = cong₂ _∷_ (zeˡ x) (zipWith-zeroˡ zeˡ xs) zipWith-zeroʳ : RightZero _≡_ e f → - RightZero _≡_ (replicate e) (zipWith {n = n} f) + RightZero _≡_ (replicate n e) (zipWith f) zipWith-zeroʳ zeʳ [] = refl zipWith-zeroʳ zeʳ (x ∷ xs) = cong₂ _∷_ (zeʳ x) (zipWith-zeroʳ zeʳ xs) @@ -595,13 +595,13 @@ module _ {f : A → A → A} {e : A} where module _ {f : A → A → A} {e : A} {⁻¹ : A → A} where zipWith-inverseˡ : LeftInverse _≡_ e ⁻¹ f → - LeftInverse _≡_ (replicate {n = n} e) (map ⁻¹) (zipWith f) + LeftInverse _≡_ (replicate n e) (map ⁻¹) (zipWith f) zipWith-inverseˡ invˡ [] = refl zipWith-inverseˡ invˡ (x ∷ xs) = cong₂ _∷_ (invˡ x) (zipWith-inverseˡ invˡ xs) zipWith-inverseʳ : RightInverse _≡_ e ⁻¹ f → - RightInverse _≡_ (replicate {n = n} e) (map ⁻¹) (zipWith f) + RightInverse _≡_ (replicate n e) (map ⁻¹) (zipWith f) zipWith-inverseʳ invʳ [] = refl zipWith-inverseʳ invʳ (x ∷ xs) = cong₂ _∷_ (invʳ x) (zipWith-inverseʳ invʳ xs) @@ -734,7 +734,7 @@ lookup-⊛ zero (f ∷ fs) (x ∷ xs) = refl lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs map-is-⊛ : ∀ (f : A → B) (xs : Vec A n) → - map f xs ≡ (replicate f ⊛ xs) + map f xs ≡ (replicate n f ⊛ xs) map-is-⊛ f [] = refl map-is-⊛ f (x ∷ xs) = cong (_ ∷_) (map-is-⊛ f xs) @@ -744,7 +744,7 @@ map-is-⊛ f (x ∷ xs) = cong (_ ∷_) (map-is-⊛ f xs) ⊛-is-zipWith (f ∷ fs) (x ∷ xs) = cong (f x ∷_) (⊛-is-zipWith fs xs) zipWith-is-⊛ : ∀ (f : A → B → C) (xs : Vec A n) (ys : Vec B n) → - zipWith f xs ys ≡ (replicate f ⊛ xs ⊛ ys) + zipWith f xs ys ≡ (replicate n f ⊛ xs ⊛ ys) zipWith-is-⊛ f [] [] = refl zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (zipWith-is-⊛ f xs ys) @@ -1107,51 +1107,51 @@ sum-++ {ys = ys} (x ∷ xs) = begin ------------------------------------------------------------------------ -- replicate -lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate x) i ≡ x +lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate n x) i ≡ x lookup-replicate zero x = refl lookup-replicate (suc i) x = lookup-replicate i x map-replicate : ∀ (f : A → B) (x : A) n → - map f (replicate x) ≡ replicate {n = n} (f x) + map f (replicate n x) ≡ replicate n (f x) map-replicate f x zero = refl map-replicate f x (suc n) = cong (f x ∷_) (map-replicate f x n) transpose-replicate : ∀ (xs : Vec A m) → - transpose (replicate {n = n} xs) ≡ map replicate xs + transpose (replicate n xs) ≡ map (replicate n) xs transpose-replicate {n = zero} _ = sym (map-const _ []) transpose-replicate {n = suc n} xs = begin - transpose (replicate xs) ≡⟨⟩ - (replicate _∷_ ⊛ xs ⊛ transpose (replicate xs)) ≡⟨ cong₂ _⊛_ (sym (map-is-⊛ _∷_ xs)) (transpose-replicate xs) ⟩ - (map _∷_ xs ⊛ map replicate xs) ≡⟨ map-⊛ _∷_ replicate xs ⟩ - map replicate xs ∎ + transpose (replicate (suc n) xs) ≡⟨⟩ + (replicate _ _∷_ ⊛ xs ⊛ transpose (replicate _ xs)) ≡⟨ cong₂ _⊛_ (sym (map-is-⊛ _∷_ xs)) (transpose-replicate xs) ⟩ + (map _∷_ xs ⊛ map (replicate n) xs) ≡⟨ map-⊛ _∷_ (replicate n) xs ⟩ + map (replicate (suc n)) xs ∎ where open ≡-Reasoning zipWith-replicate : ∀ (_⊕_ : A → B → C) (x : A) (y : B) → - zipWith {n = n} _⊕_ (replicate x) (replicate y) ≡ replicate (x ⊕ y) + zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y) zipWith-replicate {n = zero} _⊕_ x y = refl zipWith-replicate {n = suc n} _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate _⊕_ x y) zipWith-replicate₁ : ∀ (_⊕_ : A → B → C) (x : A) (ys : Vec B n) → - zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys + zipWith _⊕_ (replicate n x) ys ≡ map (x ⊕_) ys zipWith-replicate₁ _⊕_ x [] = refl zipWith-replicate₁ _⊕_ x (y ∷ ys) = cong (x ⊕ y ∷_) (zipWith-replicate₁ _⊕_ x ys) zipWith-replicate₂ : ∀ (_⊕_ : A → B → C) (xs : Vec A n) (y : B) → - zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs + zipWith _⊕_ xs (replicate n y) ≡ map (_⊕ y) xs zipWith-replicate₂ _⊕_ [] y = refl zipWith-replicate₂ _⊕_ (x ∷ xs) y = cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y) toList-replicate : ∀ (n : ℕ) (x : A) → - toList (replicate {n = n} a) ≡ List.replicate n a + toList (replicate n a) ≡ List.replicate n a toList-replicate zero x = refl toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x) ------------------------------------------------------------------------ -- iterate -iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate x +iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate n x iterate-id x zero = refl iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n) diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index baaf4eca37..ea7d04285f 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -90,7 +90,7 @@ 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 a) +replicate n a = fromVec (Vec.replicate n a) tabulate : ∀ n → (Fin n → A) → A ^ n tabulate n f = fromVec (Vec.tabulate f) diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda index 7e2e743088..28f022454b 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda @@ -96,8 +96,8 @@ open PW public using (concat⁺; concat⁻) -- replicate replicate-shiftʳ : ∀ {m} n x (xs : Vec A m) → - replicate {n = n} x ++ (x ∷ xs) ≋ - replicate {n = 1 + n} x ++ xs + replicate n x ++ (x ∷ xs) ≋ + replicate (1 + n) x ++ xs replicate-shiftʳ zero x xs = ≋-refl replicate-shiftʳ (suc n) x xs = refl ∷ (replicate-shiftʳ n x xs)