Fix build

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

@@ -27,7 +27,8 @@ record CostMonoid : Set₁ where
   Preorder._≲_ ≤-preorder = _≤_
   Preorder.isPreorder ≤-preorder = isPreorder
 
-  open import Relation.Binary.Reasoning.Preorder ≤-preorder public
+  module ≤-Reasoning where
+    open import Relation.Binary.Reasoning.Preorder ≤-preorder public
 
 
 record ParCostMonoid : Set₁ where
@@ -63,4 +64,5 @@ record ParCostMonoid : Set₁ where
   Preorder._≲_ ≤-preorder = _≤_
   Preorder.isPreorder ≤-preorder = isPreorder
 
-  open import Relation.Binary.Reasoning.Preorder ≤-preorder public
+  module ≤-Reasoning where
+    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/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
       )
@@ -171,7 +171,7 @@ module QuickSort (M : Comparable) where
     let open Nat.≤-Reasoning in
     begin
       m ² + n ²
-    ≤⁻⟨ Nat.+-mono-≤ (Nat.m≤m+n (m * m) (n * m)) (Nat.m≤n+m (n * n) (m * n)) ⟩
+    ≤⟨ Nat.+-mono-≤ (Nat.m≤m+n (m * m) (n * m)) (Nat.m≤n+m (n * n) (m * n)) ⟩
       (m * m + n * m) + (m * n + n * n)
     ≡˘⟨ Eq.cong₂ _+_ (Nat.*-distribʳ-+ m m n) (Nat.*-distribʳ-+ n m n) ⟩
       (m + n) * m + (m + n) * n
@@ -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))

src/Examples/Sorting/Sequential/InsertionSort.agda

@@ -118,7 +118,7 @@ sort/is-bounded (x ∷ xs) =
       bind cost (insert x xs' sorted-xs') λ _ →
       step⋆ zero
     )
-  ≤⁻⟨ bind-monoʳ-≤⁻ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩
+  ≲⟨ bind-monoʳ-≤⁻ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩
     ( bind cost (sort xs) λ (xs' , xs↭xs' , sorted-xs') →
       step⋆ (length xs')
     )
@@ -130,9 +130,9 @@ sort/is-bounded (x ∷ xs) =
     ( bind cost (sort xs) λ _ →
       step⋆ (length xs)
     )
-  ≤⁻⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩
+  ≲⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩
     step⋆ ((length xs ²) + length xs)
-  ≤⁻⟨ step⋆-mono-≤⁻ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩
+  ≲⟨ step⋆-mono-≤⁻ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩
     step⋆ (length xs * length (x ∷ xs) + length (x ∷ xs))
   ≡⟨ Eq.cong step⋆ (N.+-comm (length xs * length (x ∷ xs)) (length (x ∷ xs))) ⟩
     step⋆ (length (x ∷ xs) ²)

src/Examples/Sorting/Sequential/MergeSort.agda

@@ -37,7 +37,7 @@ sort/clocked (suc k) l h =
   bind (F (sort-result l)) (split l) λ ((l₁ , l₂) , length₁ , length₂ , l↭l₁++l₂) →
   let
     h₁ , h₂ =
-      let open ≤-Reasoning in
+      let open N.≤-Reasoning in
       (begin
         ⌈log₂ length l₁ ⌉
       ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩
@@ -66,7 +66,7 @@ sort/clocked/total (suc k) l h u rewrite Valuable.proof (split/total l u) = ↓
   let
     ((l₁ , l₂) , length₁ , length₂ , l↭l₁++l₂) = Valuable.value (split/total l u)
     h₁ , h₂ =
-      let open ≤-Reasoning in
+      let open N.≤-Reasoning in
       (begin
         ⌈log₂ length l₁ ⌉
       ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩