Make size parameter on 'replicate' explicit (#2120)

Author: MatthewDaggitt

CHANGELOG.md

@@ -603,6 +603,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)
 
@@ -924,7 +925,7 @@ Non-backwards compatible changes
   Data.Vec.Relation.Binary.Lex.NonStrict
   Relation.Binary.Reasoning.StrictPartialOrder
   Relation.Binary.Reasoning.PartialOrder
-  ```
+  ```	
 
 ### Other
 
@@ -1053,60 +1054,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
 ------------------

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)
 

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

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

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