Fix Id/TreeSum

jonsterling · Oct 4, 2023 · c984233 · c984233
1 parent 5e196b5
commit c984233
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 28 deletions.
diff --git a/src/Examples/Id.agda b/src/Examples/Id.agda
@@ -1,15 +1,16 @@
+{-# OPTIONS --rewriting #-}
+
 module Examples.Id where
 
-open import Calf.CostMonoid
-open import Calf.CostMonoids using (ℕ-CostMonoid)
+open import Algebra.Cost
 
 costMonoid = ℕ-CostMonoid
 open CostMonoid costMonoid
 
 open import Calf costMonoid
-open import Calf.Types.Nat
-open import Calf.Types.Bounded costMonoid
-open import Calf.Types.BigO costMonoid
+open import Calf.Data.Nat
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.BigO costMonoid
 
 open import Function using (_∘_; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
@@ -24,11 +25,11 @@ module Easy where
   id/bound : cmp (Π nat λ _ → F nat)
   id/bound n = ret n
 
-  id/is-bounded : ∀ n → id n ≲[ F nat ] id/bound n
-  id/is-bounded n = ≲-refl
+  id/is-bounded : ∀ n → id n ≤⁻[ F nat ] id/bound n
+  id/is-bounded n = ≤⁻-refl
 
   id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → 0)
-  id/asymptotic = f[n]≤g[n]via (≲-mono (λ e → bind (F _) e (λ _ → ret _)) ∘ id/is-bounded)
+  id/asymptotic = f[n]≤g[n]via (≤⁻-mono (λ e → bind (F _) e (λ _ → ret _)) ∘ id/is-bounded)
 
 module Hard where
   id : cmp (Π nat λ _ → F nat)
@@ -42,34 +43,34 @@ module Hard where
   id/bound : cmp (Π nat λ _ → F nat)
   id/bound n = step (F nat) n (ret n)
 
-  id/is-bounded : ∀ n → id n ≲[ F nat ] id/bound n
-  id/is-bounded zero    = ≲-refl
+  id/is-bounded : ∀ n → id n ≤⁻[ F nat ] id/bound n
+  id/is-bounded zero    = ≤⁻-refl
   id/is-bounded (suc n) =
-    let open ≲-Reasoning (F nat) in
-    ≲-mono (step (F nat) 1) $
+    let open ≤⁻-Reasoning (F nat) in
+    ≤⁻-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))
     ∎
 
   id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → n)
-  id/asymptotic = f[n]≤g[n]via (≲-mono (λ e → bind (F _) e _) ∘ id/is-bounded)
+  id/asymptotic = f[n]≤g[n]via (≤⁻-mono (λ e → bind (F _) e _) ∘ id/is-bounded)
 
 easy≡hard : ◯ (Easy.id ≡ Hard.id)
 easy≡hard u =
   funext λ n →
     begin
       Easy.id n
-    ≡⟨ ≲-ext-≡ u (Easy.id/is-bounded n) ⟩
+    ≡⟨ ≤⁻-ext-≡ u (Easy.id/is-bounded n) ⟩
       Easy.id/bound n
     ≡⟨⟩
       ret n
     ≡˘⟨ step/ext (F nat) (ret n) n u ⟩
       Hard.id/bound n
-    ≡˘⟨ ≲-ext-≡ u (Hard.id/is-bounded n) ⟩
+    ≡˘⟨ ≤⁻-ext-≡ u (Hard.id/is-bounded n) ⟩
       Hard.id n
     ∎
       where open ≡-Reasoning
diff --git a/src/Examples/TreeSum.agda b/src/Examples/TreeSum.agda
@@ -1,15 +1,16 @@
+{-# OPTIONS --rewriting #-}
+
 module Examples.TreeSum where
 
-open import Calf.CostMonoid
-open import Calf.CostMonoids using (ℕ²-ParCostMonoid)
+open import Algebra.Cost
 
 parCostMonoid = ℕ²-ParCostMonoid
 open ParCostMonoid parCostMonoid
 
 open import Calf costMonoid
-open import Calf.ParMetalanguage parCostMonoid
-open import Calf.Types.Nat
-open import Calf.Types.Bounded costMonoid
+open import Calf.Parallel parCostMonoid
+open import Calf.Data.Nat
+open import Calf.Data.IsBounded costMonoid
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning)
 open import Data.Nat as Nat using (_+_; _⊔_)
@@ -25,12 +26,12 @@ data Tree : Set where
   node : Tree → Tree → Tree
 
 tree : tp pos
-tree = U (meta Tree)
+tree = meta⁺ Tree
 
 sum : cmp (Π tree λ _ → F nat)
 sum (leaf x)     = ret x
 sum (node t₁ t₂) =
-  bind (F nat) (sum t₁ & sum t₂) λ (n₁ , n₂) →
+  bind (F nat) (sum t₁ ∥ sum t₂) λ (n₁ , n₂) →
     add n₁ n₂
 
 sum/spec : val tree → val nat
@@ -62,9 +63,9 @@ sum/has-cost = funext aux
     aux (node t₁ t₂) =
       let open ≡-Reasoning in
       begin
-        bind (F nat) (sum t₁ & sum t₂) (λ (n₁ , n₂) → add n₁ n₂)
-      ≡⟨ Eq.cong₂ (λ e₁ e₂ → bind (F nat) (e₁ & e₂) (λ (n₁ , n₂) → add n₁ n₂)) (aux t₁) (aux t₂) ⟩
-        bind (F nat) (sum/bound t₁ & sum/bound t₂) (λ (n₁ , n₂) → add n₁ n₂)
+        bind (F nat) (sum t₁ ∥ sum t₂) (λ (n₁ , n₂) → add n₁ n₂)
+      ≡⟨ Eq.cong₂ (λ e₁ e₂ → bind (F nat) (e₁ ∥ e₂) (λ (n₁ , n₂) → add n₁ n₂)) (aux t₁) (aux t₂) ⟩
+        bind (F nat) (sum/bound t₁ ∥ sum/bound t₂) (λ (n₁ , n₂) → add n₁ n₂)
       ≡⟨⟩
         step (F nat)
           (((size t₁ , depth t₁) ⊗ (size t₂ , depth t₂)) ⊕ (1 , 1))
@@ -73,5 +74,5 @@ sum/has-cost = funext aux
         sum/bound (node t₁ t₂)
       ∎
 
-sum/is-bounded : sum ≲[ (Π tree λ _ → F nat) ] sum/bound
-sum/is-bounded = ≲-reflexive sum/has-cost
+sum/is-bounded : sum ≤⁻[ (Π tree λ _ → F nat) ] sum/bound
+sum/is-bounded = ≤⁻-reflexive sum/has-cost