Merge pull request #52 from jonsterling/stdlib-2.0

Update to `agda-stdlib` v2.0

Author: HarrisonGrodin

.github/workflows/agda.yaml

@@ -20,7 +20,7 @@ jobs:
     strategy:
       matrix:
         agda-ref: ["v2.6.3"]
-        stdlib-ref: ["fc473ec905ab1a11a16718a7e8b628f1ab7eb435"]
+        stdlib-ref: ["v2.0"]
         ghc-ver: ["8.10.2"]
         cabal-ver: ["3.4.0.0"]
     steps:

INSTALL.md

@@ -1,8 +1,7 @@
 # Installation
 
 1. Install Agda v2.6.3 ([instructions](https://agda.readthedocs.io/en/v2.6.3/getting-started/installation.html)).
-2. Install `agda-stdlib` v2.0 ([instructions](https://github.com/agda/agda-stdlib/blob/fc473ec/notes/installation-guide.md)).
-   We have tested on commit [fc473ec](https://github.com/agda/agda-stdlib/tree/fc473ec905ab1a11a16718a7e8b628f1ab7eb435).
+2. Install `agda-stdlib` v2.0 ([instructions](https://github.com/agda/agda-stdlib/blob/v2.0/doc/installation-guide.md)).
 
 This is all that is required to play with **calf**.
 

calf.agda-lib

@@ -1,4 +1,4 @@
 name: calf
-depend: standard-library
+depend: standard-library-2.0
 include: src
 flags: --prop --guardedness

src/Algebra/Cost/Bundles.agda

@@ -4,7 +4,7 @@ module Algebra.Cost.Bundles where
 
 open import Algebra.Core
 open import Algebra.Cost.Structures
-open import Relation.Binary using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary using (Rel; Preorder; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.PropositionalEquality using (_≡_; resp₂)
 open import Level using (0ℓ)
 
@@ -21,16 +21,14 @@ record CostMonoid : Set₁ where
 
   open IsCostMonoid isCostMonoid public
 
+  ≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
+  Preorder.Carrier ≤-preorder = ℂ
+  Preorder._≈_ ≤-preorder = _≡_
+  Preorder._≲_ ≤-preorder = _≤_
+  Preorder.isPreorder ≤-preorder = isPreorder
+
   module ≤-Reasoning where
-    open import Relation.Binary.Reasoning.Base.Triple
-      isPreorder
-      ≤-trans
-      (resp₂ _≤_)
-      (λ h → h)
-      ≤-trans
-      ≤-trans
-      public
-      hiding (step-≈; step-≈˘; step-<)
+    open import Relation.Binary.Reasoning.Preorder ≤-preorder public
 
 
 record ParCostMonoid : Set₁ where
@@ -60,13 +58,11 @@ record ParCostMonoid : Set₁ where
       }
     }
 
+  ≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
+  Preorder.Carrier ≤-preorder = ℂ
+  Preorder._≈_ ≤-preorder = _≡_
+  Preorder._≲_ ≤-preorder = _≤_
+  Preorder.isPreorder ≤-preorder = isPreorder
+
   module ≤-Reasoning where
-    open import Relation.Binary.Reasoning.Base.Triple
-      isPreorder
-      ≤-trans
-      (resp₂ _≤_)
-      (λ h → h)
-      ≤-trans
-      ≤-trans
-      public
-      hiding (step-≈; step-≈˘; step-<)
+    open import Relation.Binary.Reasoning.Preorder ≤-preorder public

src/Calf/Data/IsBounded.agda

@@ -40,11 +40,11 @@ bound/bind/const {e = e} {f} c d he hf =
   let open ≤⁻-Reasoning cost in
   begin
     bind cost e (λ v → bind cost (f v) (λ _ → ret triv))
-  ≤⟨ bind-monoʳ-≤⁻ e hf ⟩
+  ≲⟨ bind-monoʳ-≤⁻ e hf ⟩
     bind cost e (λ _ → step⋆ d)
   ≡⟨⟩
     bind cost (bind cost e λ _ → ret triv) (λ _ → step⋆ d)
-  ≤⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ d) he ⟩
+  ≲⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ d) he ⟩
     bind cost (step⋆ c) (λ _ → step⋆ d)
   ≡⟨⟩
     step⋆ (c + d)
@@ -66,6 +66,6 @@ module Legacy where
       bind cost (step (F A) c' (ret a)) (λ _ → ret triv)
     ≡⟨⟩
       step⋆ c'
-    ≤⟨ step-monoˡ-≤⁻ (ret triv) c'≤c ⟩
+    ≲⟨ step-monoˡ-≤⁻ (ret triv) c'≤c ⟩
       step⋆ c
     ∎

src/Calf/Data/IsBoundedG.agda

@@ -38,9 +38,9 @@ boundg/relax {b = b} {b'} h {e = e} ib-b =
   let open ≤⁻-Reasoning cost in
   begin
     bind cost e (λ _ → ret triv)
-  ≤⟨ ib-b ⟩
+  ≲⟨ ib-b ⟩
     b
-  ≤⟨ h ⟩
+  ≲⟨ h ⟩
     b'
   ∎
 
@@ -53,7 +53,7 @@ boundg/step c {b} e h =
     bind cost (step (F _) c e) (λ _ → ret triv)
   ≡⟨⟩
     step cost c (bind cost e (λ _ → ret triv))
-  ≤⟨ step-monoʳ-≤⁻ c h ⟩
+  ≲⟨ step-monoʳ-≤⁻ c h ⟩
     step cost c b
   ∎
 
@@ -67,6 +67,6 @@ boundg/bind {e = e} {f} b hf =
     bind cost (bind (F _) e f) (λ _ → ret triv)
   ≡⟨⟩
     bind cost e (λ a → bind cost (f a) λ _ → ret triv)
-  ≤⟨ bind-monoʳ-≤⁻ e hf ⟩
+  ≲⟨ bind-monoʳ-≤⁻ e hf ⟩
     bind cost e b
   ∎

src/Calf/Directed.agda

@@ -118,16 +118,15 @@ bind-irr-monoˡ-≤⁻ e₁≤e₁' =
   bind-irr-mono-≤⁻ e₁≤e₁' ≤⁻-refl
 
 
+open import Level using (0ℓ)
+open import Relation.Binary using (Preorder)
 open import Relation.Binary.Structures
 
+≤⁻-preorder : tp⁻ → Preorder 0ℓ 0ℓ 0ℓ
+Preorder.Carrier (≤⁻-preorder X) = cmp X
+Preorder._≈_ (≤⁻-preorder X) = _≡_
+Preorder._≲_ (≤⁻-preorder X) = _≤⁻_ {X}
+Preorder.isPreorder (≤⁻-preorder X) = ≤⁻-isPreorder {X}
+
 module ≤⁻-Reasoning (X : tp⁻) where
-  open import Relation.Binary.Reasoning.Base.Triple
-    (≤⁻-isPreorder {X})
-    ≤⁻-trans
-    (resp₂ _≤⁻_)
-    (λ h → h)
-    ≤⁻-trans
-    ≤⁻-trans
-    public
-    hiding (begin-strict_; step-<; step-≈; step-≈˘)
-    renaming (step-≤ to step-≤⁻)
+  open import Relation.Binary.Reasoning.Preorder (≤⁻-preorder X) public

src/Calf/Parallel.agda

@@ -58,11 +58,11 @@ boundg/par {A₁} {A₂} {e₁} {e₂} {b₁} {b₂} ib₁ ib₂ =
   let open ≤⁻-Reasoning cost in
   begin
     bind cost (e₁ ∥ e₂) (λ _ → ret triv)
-  ≤⟨ {!   !} ⟩
+  ≲⟨ {!   !} ⟩
     bind cost ((bind cost e₁ λ _ → ret triv) ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)
-  ≤⟨ ≤⁻-mono (λ e → bind cost (e ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)) ib₁ ⟩
+  ≲⟨ ≤⁻-mono (λ e → bind cost (e ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)) ib₁ ⟩
     bind cost (b₁ ∥ (bind cost e₂ λ _ → ret triv)) (λ _ → ret triv)
-  ≤⟨ ≤⁻-mono (λ e → bind cost (b₁ ∥ e) (λ _ → ret triv)) ib₂ ⟩
+  ≲⟨ ≤⁻-mono (λ e → bind cost (b₁ ∥ e) (λ _ → ret triv)) ib₂ ⟩
     bind cost (b₁ ∥ b₂) (λ _ → ret triv)
   ∎
 

src/Calf/Step.agda

@@ -80,8 +80,8 @@ step-mono-≤⁻ {X} {c} {c'} {e} {e'} c≤c' e≤e' =
   let open ≤⁻-Reasoning X in
   begin
     step X c e
-  ≤⟨ step-monoˡ-≤⁻ e c≤c' ⟩
+  ≲⟨ step-monoˡ-≤⁻ e c≤c' ⟩
     step X c' e
-  ≤⟨ step-monoʳ-≤⁻ c' e≤e' ⟩
+  ≲⟨ step-monoʳ-≤⁻ c' e≤e' ⟩
     step X c' e'
   ∎

src/Data/Nat/PredExp2.agda

@@ -50,7 +50,7 @@ private
   ... | zero | ()
 
 pred[2^]-mono : pred[2^_] Preserves _≤_ ⟶ _≤_
-pred[2^]-mono m≤n = pred-mono (2^-mono m≤n)
+pred[2^]-mono m≤n = pred-mono-≤ (2^-mono m≤n)
   where
     2^-mono : (2 ^_) Preserves _≤_ ⟶ _≤_
     2^-mono {y = y} z≤n = lemma/1≤2^n y

src/Examples/Decalf/HigherOrderFunction.agda

@@ -42,7 +42,7 @@ module Twice where
         bind cost e λ _ →
         ret triv
       )
-    ≤⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F _) e₁ λ _ → bind (F _) e₂ λ _ → ret triv) e≤step⋆1 e≤step⋆1 ⟩
+    ≲⟨ ≤⁻-mono₂ (λ e₁ e₂ → bind (F _) e₁ λ _ → bind (F _) e₂ λ _ → ret triv) e≤step⋆1 e≤step⋆1 ⟩
       ( bind cost (step⋆ 1) λ _ →
         bind cost (step⋆ 1) λ _ →
         ret triv
@@ -79,7 +79,7 @@ module Map where
         bind cost (map f xs) λ _ →
         ret triv
       )
-    ≤⟨
+    ≲⟨
       ≤⁻-mono₂ (λ e₁ e₂ → bind cost e₁ λ _ → bind cost e₂ λ _ → ret triv)
         (f-bound x)
         (map/is-bounded f f-bound xs)
@@ -114,11 +114,11 @@ module Map where
         bind cost (map f xs) λ _ →
         ret triv
       )
-    ≤⟨ ≤⁻-mono (λ e → bind cost (f x) λ _ → e) (map/is-bounded' f f-bound xs) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind cost (f x) λ _ → e) (map/is-bounded' f f-bound xs) ⟩
       ( bind cost (f x) λ _ →
         binomial (length xs * n)
       )
-    ≤⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial (length xs * n)) (f-bound x) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial (length xs * n)) (f-bound x) ⟩
       ( bind cost (binomial n) λ _ →
         binomial (length xs * n)
       )

src/Examples/Decalf/Nondeterminism.agda

@@ -70,7 +70,7 @@ module QuickSort (M : Comparable) where
     let open ≤⁻-Reasoning cost in
     begin
       branch (F unit) (bind (F unit) (choose (x' ∷ xs)) λ _ → ret triv) (ret triv)
-    ≤⟨ ≤⁻-mono (λ e → branch (F unit) (bind (F unit) e λ _ → ret triv) (ret triv)) (choose/is-bounded x' xs) ⟩
+    ≲⟨ ≤⁻-mono (λ e → branch (F unit) (bind (F unit) e λ _ → ret triv) (ret triv)) (choose/is-bounded x' xs) ⟩
       branch (F unit) (ret triv) (ret triv)
     ≡⟨ branch/idem ⟩
       ret triv
@@ -128,7 +128,7 @@ module QuickSort (M : Comparable) where
         bind (F unit) (x ≤? pivot) λ _ →
         ret triv
       )
-    ≤⟨
+    ≲⟨
       ( ≤⁻-mono
           {Π (Σ⁺ (list A) λ l₁ → Σ⁺ (list A) λ l₂ → meta⁺ (All (_≤ pivot) l₁) ×⁺ meta⁺ (All (pivot ≤_) l₂) ×⁺ meta⁺ (l₁ ++ l₂ ↭ xs)) λ _ → F unit}
           (bind (F unit) (partition pivot xs)) $
@@ -143,7 +143,7 @@ module QuickSort (M : Comparable) where
       ( bind (F unit) (bind (F unit) (partition pivot xs) λ _ → ret triv) λ _ →
         step⋆ 1
       )
-    ≤⟨ ≤⁻-mono (λ e → bind (F unit) (bind (F unit) e λ _ → ret triv) λ _ → step (F unit) 1 (ret triv)) (partition/is-bounded pivot xs) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind (F unit) (bind (F unit) e λ _ → ret triv) λ _ → step (F unit) 1 (ret triv)) (partition/is-bounded pivot xs) ⟩
       ( bind (F unit) (step (F unit) (length xs) (ret triv)) λ _ →
         step⋆ 1
       )
@@ -191,7 +191,7 @@ module QuickSort (M : Comparable) where
         bind (F _) (sort l₂) λ _ →
         ret triv
       )
-    ≤⟨
+    ≲⟨
       ( ≤⁻-mono
           {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit}
           {F unit}
@@ -220,7 +220,7 @@ module QuickSort (M : Comparable) where
         bind (F _) (sort l₁) λ _ →
         step⋆ (length l₂ ²)
       )
-    ≤⟨
+    ≲⟨
       ( ≤⁻-mono
           {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit}
           {F unit}
@@ -245,7 +245,7 @@ module QuickSort (M : Comparable) where
         bind (F _) (partition pivot l) λ (l₁ , l₂ , h₁ , h₂ , l₁++l₂↭l) →
         step⋆ (length l₁ ² + length l₂ ²)
       )
-    ≤⟨
+    ≲⟨
       ( ≤⁻-mono
           {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit}
           {F unit}
@@ -270,7 +270,7 @@ module QuickSort (M : Comparable) where
         bind (F _) (partition pivot l) λ _ →
         step⋆ (length l ²)
       )
-    ≤⟨
+    ≲⟨
       ( ≤⁻-mono
           {Π (Σ⁺ A λ pivot → Σ⁺ (list A) λ l' → meta⁺ (x ∷ xs ↭ pivot ∷ l')) λ _ → F unit}
           {F unit}
@@ -295,9 +295,9 @@ module QuickSort (M : Comparable) where
       ( bind (F _) (choose (x ∷ xs)) λ _ →
         step⋆ (length xs + length xs ²)
       )
-    ≤⟨ bind-irr-monoˡ-≤⁻ (choose/is-bounded x xs) ⟩
+    ≲⟨ bind-irr-monoˡ-≤⁻ (choose/is-bounded x xs) ⟩
       step⋆ (length xs + length xs ²)
-    ≤⟨ step⋆-mono-≤⁻ (Nat.+-mono-≤ (Nat.n≤1+n (length xs)) (Nat.*-monoʳ-≤ (length xs) (Nat.n≤1+n (length xs)))) ⟩
+    ≲⟨ step⋆-mono-≤⁻ (Nat.+-mono-≤ (Nat.n≤1+n (length xs)) (Nat.*-monoʳ-≤ (length xs) (Nat.n≤1+n (length xs)))) ⟩
       step⋆ (length (x ∷ xs) + length xs * length (x ∷ xs))
     ≡⟨⟩
       step⋆ (length (x ∷ xs) ²)
@@ -330,7 +330,7 @@ module Lookup {A : tp⁺} where
         let open ≤⁻-Reasoning (F _) in
         begin
           step (F _) 1 (lookup xs i)
-        ≤⟨ ≤⁻-mono (step (F _) 1) (lemma xs i p) ⟩
+        ≲⟨ ≤⁻-mono (step (F _) 1) (lemma xs i p) ⟩
           step (F _) 1 (fail (F _))
         ≡⟨ fail/step 1 ⟩
           fail (F _)
@@ -353,7 +353,7 @@ module Pervasive where
       branch (F bool)
         (step (F bool) 3 (ret true))
         (step (F bool) 12 (ret false))
-    ≤⟨
+    ≲⟨
       ≤⁻-mono
         (λ e → branch (F bool) e (step (F bool) 12 (ret false)))
         (step-monoˡ-≤⁻ {F bool} (ret true) (Nat.s≤s (Nat.s≤s (Nat.s≤s Nat.z≤n))))
@@ -370,7 +370,7 @@ module Pervasive where
     let open ≤⁻-Reasoning (F unit) in
     begin
       bind (F unit) e (λ _ → ret triv)
-    ≤⟨ ≤⁻-mono (λ e → bind (F _) e (λ _ → ret triv)) e/is-bounded ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind (F _) e (λ _ → ret triv)) e/is-bounded ⟩
       bind (F unit) (step (F bool) 12 (branch (F bool) (ret true) (ret false))) (λ _ → ret triv)
     ≡⟨⟩
       step (F unit) 12 (branch (F unit) (ret triv) (ret triv))

src/Examples/Decalf/ProbabilisticChoice.agda

@@ -64,7 +64,7 @@ module _ where
     let open ≤⁻-Reasoning cost in
     begin
       flip cost ½ (step⋆ 0) (step⋆ 1)
-    ≤⟨ ≤⁻-mono {cost} (λ e → flip cost ½ e (step⋆ 1)) (≤⁺-mono step⋆ (≤⇒≤⁺ (z≤n {1}))) ⟩
+    ≲⟨ ≤⁻-mono {cost} (λ e → flip cost ½ e (step⋆ 1)) (≤⁺-mono step⋆ (≤⇒≤⁺ (z≤n {1}))) ⟩
       flip cost ½ (step⋆ 1) (step⋆ 1)
     ≡⟨ flip/same cost (step⋆ 1) {½} ⟩
       step⋆ 1
@@ -123,13 +123,13 @@ module _ where
       ( bind cost bernoulli λ _ →
         binomial n
       )
-    ≤⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial n) bernoulli/upper ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → binomial n) bernoulli/upper ⟩
       ( bind cost (step⋆ 1) λ _ →
         binomial n
       )
     ≡⟨⟩
       step cost 1 (binomial n)
-    ≤⟨ ≤⁻-mono (step cost 1) (binomial/upper n) ⟩
+    ≲⟨ ≤⁻-mono (step cost 1) (binomial/upper n) ⟩
       step⋆ (suc n)
     ∎
 
@@ -161,7 +161,7 @@ sublist/is-bounded {A} (x ∷ xs) =
       ( bind cost (sublist {A} xs) λ _ →
         bernoulli
       )
-    ≤⟨ ≤⁻-mono (λ e → bind cost e λ _ → bernoulli) (sublist/is-bounded {A} xs) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind cost e λ _ → bernoulli) (sublist/is-bounded {A} xs) ⟩
       ( bind cost (binomial (length xs)) λ _ →
         bernoulli
       )

src/Examples/Exp2.agda

@@ -43,7 +43,7 @@ module Slow where
     begin
       (bind (F nat) (exp₂ n ∥ exp₂ n) λ (r₁ , r₂) →
         step (F nat) (1 , 1) (ret (r₁ + r₂)))
-    ≤⟨
+    ≲⟨
       ≤⁻-mono₂ (λ e₁ e₂ → bind (F nat) (e₁ ∥ e₂) λ (r₁ , r₂) → step (F nat) (1 , 1) (ret (r₁ + r₂)))
         (exp₂/is-bounded n)
         (exp₂/is-bounded n)
@@ -90,7 +90,7 @@ module Fast where
     begin
       (bind (F nat) (exp₂ n) λ r →
         step (F nat) (1 , 1) (ret (r + r)))
-    ≤⟨ ≤⁻-mono (λ e → bind (F nat) e λ r → step (F nat) (1 , 1) (ret (r + r))) (exp₂/is-bounded n) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind (F nat) e λ r → step (F nat) (1 , 1) (ret (r + r))) (exp₂/is-bounded n) ⟩
       (bind (F nat) (step (F nat) (n , n) (ret (2 ^ n))) λ r →
         step (F nat) (1 , 1) (ret (r + r)))
     ≡⟨⟩

src/Examples/Id.agda

@@ -52,7 +52,7 @@ module Hard where
     ≤⁻-mono (step (F nat) 1) $
     begin
       bind (F nat) (id n) (λ n' → ret (suc n'))
-    ≤⟨ ≤⁻-mono (λ e → bind (F nat) e (ret ∘ suc)) (id/is-bounded n) ⟩
+    ≲⟨ ≤⁻-mono (λ e → bind (F nat) e (ret ∘ suc)) (id/is-bounded n) ⟩
       bind (F nat) (step (F nat) n (ret n)) (λ n' → ret (suc n'))
     ≡⟨⟩
       step (F nat) n (ret (suc n))