partially port rbt to decalf

jonsterling · Nov 7, 2023 · 2713bbd · 2713bbd
1 parent 8825566
commit 2713bbd
Show file tree

Hide file tree

Showing 5 changed files with 1,014 additions and 0 deletions.
diff --git a/src/Examples/Sequence.agda b/src/Examples/Sequence.agda
@@ -0,0 +1,219 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+open import Calf.Parallel parCostMonoid
+
+open import Calf.Data.Product
+open import Calf.Data.Sum
+open import Calf.Data.Bool
+open import Calf.Data.Maybe
+open import Calf.Data.Nat hiding (compare)
+open import Calf.Data.List hiding (filter)
+
+open import Level using (0ℓ)
+open import Relation.Binary
+open import Data.Nat as Nat using (_<_; _+_)
+import Data.Nat.Properties as Nat
+open import Data.String using (String)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+
+open import Function using (case_of_; _$_)
+
+open import Examples.Sequence.MSequence
+open import Examples.Sequence.ListMSequence
+open import Examples.Sequence.RedBlackMSequence
+
+
+module Ex/FromList where
+  open MSequence RedBlackMSequence
+
+  fromList : cmp (Π (list nat) λ _ → F (seq nat))
+  fromList [] = empty
+  fromList (x ∷ l) =
+    bind (F (seq nat)) empty λ s₁ →
+    bind (F (seq nat)) (fromList l) λ s₂ →
+    join s₁ x s₂
+
+  example : cmp (F (seq nat))
+  example = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
+
+
+module BinarySearchTree
+  (MSeq : MSequence)
+  (Key : StrictTotalOrder 0ℓ 0ℓ 0ℓ)
+  where
+
+  open StrictTotalOrder Key
+
+  𝕂 : tp⁺
+  𝕂 = meta⁺ (StrictTotalOrder.Carrier Key)
+
+  open MSequence MSeq public
+
+  singleton : cmp (Π 𝕂 λ _ → F (seq 𝕂))
+  singleton a =
+    bind (F (seq 𝕂)) empty λ t →
+    join t a t
+
+  Split : tp⁻
+  Split = F ((seq 𝕂) ×⁺ ((maybe 𝕂) ×⁺ (seq 𝕂)))
+
+  split : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → Split)
+  split t a =
+    rec
+      {X = Split}
+      (bind Split empty λ t →
+        ret (t , nothing , t))
+      (λ t₁ ih₁ a' t₂ ih₂ →
+        case compare a a' of λ
+          { (tri< a<a' ¬a≡a' ¬a>a') →
+              bind Split ih₁ λ ( t₁₁ , a? , t₁₂ ) →
+              bind Split (join t₁₂ a' t₂) λ t →
+              ret (t₁₁ , a? , t)
+          ; (tri≈ ¬a<a' a≡a' ¬a>a') → ret (t₁ , just a' , t₂)
+          ; (tri> ¬a<a' ¬a≡a' a>a') →
+              bind Split ih₂ λ ( t₂₁ , a? , t₂₂ ) →
+              bind Split (join t₁ a' t₂₁) λ t →
+              ret (t , a? , t₂₂)
+          })
+      t
+
+  find : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (maybe 𝕂))
+  find t a = bind (F (maybe 𝕂)) (split t a) λ { (_ , a? , _) → ret a? }
+
+  insert : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂))
+  insert t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → join t₁ a t₂ }
+
+  append : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  append t₁ t₂ =
+    rec
+      {X = F (seq 𝕂)}
+      (ret t₂)
+      (λ t'₁ ih₁ a' t'₂ ih₂ →
+        bind (F (seq 𝕂)) ih₂ λ t' →
+        join t'₁ a' t')
+    t₁
+
+  delete : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂))
+  delete t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → append t₁ t₂ }
+
+  union : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  union =
+    rec
+      {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+      ret
+      λ t'₁ ih₁ a' t'₂ ih₂ t₂ →
+        bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) →
+        bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) →
+        join s₁ a' s₂ }
+
+  intersection : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  intersection =
+    rec
+      {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+      (λ t₂ → empty)
+      λ t'₁ ih₁ a' t'₂ ih₂ t₂ →
+        bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) →
+        bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) →
+          case a? of
+            λ { (just a) → join s₁ a s₂
+              ; nothing → append s₁ s₂ }
+        }
+
+  difference : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  difference t₁ t₂ = helper t₁
+    where
+      helper : cmp (Π (seq 𝕂) λ _ → F (seq 𝕂))
+      helper =
+        rec
+          {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+          ret
+          (λ t'₁ ih₁ a' t'₂ ih₂ t₁ →
+            bind (F (seq 𝕂)) (split t₁ a') λ { (t₁₁ , a? , t₁₂) →
+            bind (F (seq 𝕂)) ((ih₁ t₁₁) ∥ (ih₂ t₁₂)) λ (s₁ , s₂) →
+            append s₁ s₂
+            })
+        t₂
+
+  filter : cmp (Π (seq 𝕂) λ _ → Π (U (Π 𝕂 λ _ → F bool)) λ _ → F (seq 𝕂))
+  filter t f =
+    rec
+      {X = F (seq 𝕂)}
+      (bind (F (seq 𝕂)) empty ret)
+      (λ t'₁ ih₁ a' t'₂ ih₂ →
+        bind (F (seq 𝕂)) (ih₁ ∥ ih₂) (λ (s₁ , s₂) →
+        bind (F (seq 𝕂)) (f a') λ b →
+          if b then (join s₁ a' s₂) else (append s₁ s₂)))
+    t
+
+  mapreduce : {X : tp⁻} →
+    cmp (
+      Π (seq 𝕂) λ _ →
+      Π (U (Π 𝕂 λ _ → X)) λ _ →
+      Π (U (Π (U X) λ _ → Π (U X) λ _ → X)) λ _ →
+      Π (U X) λ _ →
+      X
+    )
+  mapreduce {X} t g f l =
+    rec {X = X} l (λ t'₁ ih₁ a' t'₂ ih₂ → f ih₁ (f (g a') ih₂)) t
+
+
+module Ex/NatSet where
+  open BinarySearchTree RedBlackMSequence Nat.<-strictTotalOrder
+
+  example : cmp Split
+  example =
+    bind Split (singleton 1) λ t₁ →
+    bind Split (insert t₁ 2) λ t₁ →
+    bind Split (singleton 4) λ t₂ →
+    bind Split (join t₁ 3 t₂) λ t →
+    split t 2
+
+  sum/seq : cmp (Π (seq nat) λ _ → F (nat))
+  sum/seq =
+    rec
+      {X = F (nat)}
+      (ret 0)
+      λ t'₁ ih₁ a' t'₂ ih₂ →
+        step (F nat) (1 , 1) $
+        bind (F (nat)) (ih₁ ∥ ih₂)
+        (λ (s₁ , s₂) → ret (s₁ + a' + s₂))
+
+
+
+module Ex/NatStringDict where
+  strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
+  strictTotalOrder =
+    record
+      { Carrier = ℕ × String
+      ; _≈_ = λ (n₁ , _) (n₂ , _) → n₁ ≡ n₂
+      ; _<_ = λ (n₁ , _) (n₂ , _) → n₁ Nat.< n₂
+      ; isStrictTotalOrder =
+          record
+            { isEquivalence =
+                record
+                  { refl = Eq.refl
+                  ; sym = Eq.sym
+                  ; trans = Eq.trans
+                  }
+            ; trans = Nat.<-trans
+            ; compare = λ (n₁ , _) (n₂ , _) → Nat.<-cmp n₁ n₂
+            }
+      }
+
+  open BinarySearchTree RedBlackMSequence strictTotalOrder
+
+  example : cmp Split
+  example =
+    bind Split (singleton (1 , "red")) λ t₁ →
+    bind Split (insert t₁ (2 , "orange")) λ t₁ →
+    bind Split (singleton (4 , "green")) λ t₂ →
+    bind Split (join t₁ (3 , "yellow") t₂) λ t →
+    split t (2 , "")
diff --git a/src/Examples/Sequence/ListMSequence.agda b/src/Examples/Sequence/ListMSequence.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.ListMSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+open import Calf.Data.List
+open import Data.Nat as Nat using (_+_)
+
+open import Examples.Sequence.MSequence
+
+ListMSequence : MSequence
+ListMSequence =
+  record
+    { seq = list
+    ; empty = ret []
+    ; join =
+        λ {A} l₁ a l₂ →
+          let n = length l₁ + 1 + length l₂ in
+          step (F (list A)) (n , n) (ret (l₁ ++ [ a ] ++ l₂))
+    ; rec = λ {A} {X} → rec {A} {X}
+    }
+  where
+    rec : {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (list A) λ _ → Π (U X) λ _ → Π A λ _ → Π (list A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (list A) λ _ → X
+        )
+    rec {A} {X} z f []      = z
+    rec {A} {X} z f (x ∷ l) = step X (1 , 1) (f [] z x l (rec {A} {X} z f l))
diff --git a/src/Examples/Sequence/MSequence.agda b/src/Examples/Sequence/MSequence.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.MSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+
+-- Middle Sequence
+record MSequence : Set where
+  field
+    seq : tp⁺ → tp⁺
+
+    empty : cmp (F (seq A))
+    join : cmp (Π (seq A) λ s₁ → Π A λ a → Π (seq A) λ s₂ → F (seq A))
+
+    rec : {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (seq A) λ _ → Π (U X) λ _ → Π A λ _ → Π (seq A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (seq A) λ _ → X
+        )
diff --git a/src/Examples/Sequence/RedBlackMSequence.agda b/src/Examples/Sequence/RedBlackMSequence.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.RedBlackMSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+
+open import Calf.Data.Nat
+open import Calf.Data.List
+open import Calf.Data.Product
+open import Calf.Data.Sum
+open import Calf.Data.IsBounded costMonoid
+
+open import Data.Nat as Nat using (_+_; _*_; ⌊_/2⌋; _≥_; _∸_)
+import Data.Nat.Properties as Nat
+open import Data.Nat.Logarithm
+
+open import Examples.Sequence.MSequence
+open import Examples.Sequence.RedBlackTree
+
+
+RedBlackMSequence : MSequence
+RedBlackMSequence =
+  record
+    { seq = rbt
+    ; empty = ret ⟪ leaf ⟫
+    ; join = join
+    ; rec = λ {A} {X} → rec {A} {X}
+    }
+  where
+    record RBT (A : tp⁺) : Set where
+      pattern
+      constructor ⟪_⟫
+      field
+        {y} : val color
+        {n} : val nat
+        {l} : val (list A)
+        t : val (irbt A y n l)
+    rbt : (A : tp⁺) → tp⁺
+    rbt A = meta⁺ (RBT A)
+
+    join : cmp (Π (rbt A) λ _ → Π A λ _ → Π (rbt A) λ _ → F (rbt A))
+    join {A} t₁ a t₂ = bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) λ { (_ , _ , _ , inj₁ t) → ret ⟪ t ⟫
+                                                                                       ; (_ , _ , _ , inj₂ t) → ret ⟪ t ⟫ }
+
+    -- join/is-bounded : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂)
+    --   (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))
+    -- join/is-bounded {A} t₁ a t₂ =
+    --   Eq.subst
+    --     (IsBounded _ _) {x = 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0 , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) + 0}
+    --     (Eq.cong₂ _,_ (Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))))
+    --       ((Eq.cong suc (Nat.+-identityʳ (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))))))
+    --     (bound/bind/const (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂))) (0 , 0)
+    --       (i-join/is-bounded _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂))
+    --       (λ { (_ , _ , _ , inj₁ t) → bound/ret
+    --          ; (_ , _ , _ , inj₂ t) → bound/ret}))
+
+    nodes : RBT A → val nat
+    nodes ⟪ t ⟫ = i-nodes t
+
+    nodes/upper-bound : (t : RBT A) → RBT.n t Nat.≤ ⌈log₂ (1 + (nodes t)) ⌉
+    nodes/upper-bound ⟪ t ⟫ = i-nodes/bound/log-node-black-height t
+
+    nodes/lower-bound : (t : RBT A) → RBT.n t Nat.≥ ⌊ (⌈log₂ (1 + (nodes t)) ⌉ ∸ 1) /2⌋
+    nodes/lower-bound ⟪ t ⟫ = i-nodes/lower-bound/log-node-black-height t 
+
+    join/cost : ∀ {A} (t₁ : RBT A) (t₂ : RBT A) → ℂ
+    join/cost {A} t₁ t₂ =
+      let max = ⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ in
+      let min = ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋ in
+        (1 + 2 * (max ∸ min)) , (1 + 2 * (max ∸ min))
+
+    -- join/is-bounded/nodes : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) (join/cost t₁ t₂)
+    -- join/is-bounded/nodes {A} t₁ a t₂ =
+    --   bound/relax
+    --     (λ u →
+    --       (let open Nat.≤-Reasoning in
+    --         begin
+    --           1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+    --         ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩
+    --           1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+    --         ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩
+    --           1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋)
+    --         ∎) ,
+    --       (let open Nat.≤-Reasoning in
+    --         begin
+    --           1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+    --         ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩
+    --           1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+    --         ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩
+    --           1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋)
+    --         ∎)
+    --     )
+    --     (join/is-bounded t₁ a t₂)
+
+    rec : {A : tp⁺} {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (rbt A) λ _ → Π (U X) λ _ → Π A λ _ → Π (rbt A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (rbt A) λ _ → X
+        )
+    rec {A} {X} z f ⟪ t ⟫ =
+      i-rec {A} {X}
+        z
+        (λ _ _ _ t₁ ih₁ a _ _ _ t₂ ih₂ → f ⟪ t₁ ⟫ ih₁ a ⟪ t₂ ⟫ ih₂)
+        _ _ _ t