Mercurial > hg > Gears > GearsAgda

changeset 749:923f72af015c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Apr 2023 19:13:13 +0900
parents 1d7803a2c4c0
children 61e16b7489b8
files hoareBinaryTree1.agda
diffstat 1 files changed, 49 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 25 16:50:12 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 25 19:13:13 2023 +0900
@@ -553,7 +553,8 @@
 --    rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf)
 
 color : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → Color
-color {n} A rb = ?
+color {n} A leaf = Red
+color {n} A (node key ⟪ c , v ⟫ rb rb₁) = c
 
 RB→bt : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → bt A
 RB→bt {n} A leaf = leaf
@@ -587,48 +588,50 @@
           → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
           → rotatedTree (node kb vb d (node ka va e c) ) (node ka va (node kb vb d₁ e₁)  c₁) 
 
-record PG {n : Level } (A : Set n) (stack : List (bt A)) : Set n where
+record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
     field
-       self parent grand : bt A
+       parent grand : bt A
        pg : ParentGrand self parent grand
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
-           → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A stack
+           → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl)
 stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right {.tree} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t5} {k2} {v2} x₁ s-nil)) = case2 (case2 
-    record { self = tree ; parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2 
-    record { self = tree ; parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ s-nil)) = case2 (case2
-    record { self = tree ; parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x s-nil) = case2 (case1 refl)
 stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ s-nil)) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-right x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-left x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ s-nil)) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-right x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2
-    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
+    record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 
 
-rbsi-len :  {n : Level} {A : Set n} {orig parent grand : bt A}
-     → ParentGrand orig parent grand → ℕ
-rbsi-len {n} {A} {s} {p} {g} st = ?
+PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) )
+           →  RBtreeInvariant orig d0 
+           →  (stack : List (bt (Color ∧ A)))  → (pg : PG (Color ∧ A) tree stack )
+           →  RBtreeInvariant tree ds ∧  RBtreeInvariant (PG.parent pg) dp ∧  RBtreeInvariant (PG.grand pg) dg 
+PGtoRBinvariant = ?
 
 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → {d d0 : ℕ}
            →  RBtreeInvariant tree0 d0 
@@ -652,7 +655,7 @@
      → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 repl1 : bt (Color ∧ A))
          → (si1 : ParentGrand ? ? ?)
          → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
-         → rbsi-len si1 < rbsi-len si → t )
+         → length ? < length ? → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 repl1 : bt (Color ∧ A)) 
          → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
@@ -660,8 +663,10 @@
     insertCase51 : (key1 : ℕ)  (si : ParentGrand ? ? ? )  → t
     insertCase51 = ?
 
+-- if we have replacedNode on RBTree, we have RBtreeInvariant
+
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color}  
+     → (key : ℕ) → (value : A) → {d0 : ℕ} 
      → (orig tree : bt (Color ∧ A)) {d0 : ℕ}
      →  RBtreeInvariant orig d0 
      →  {d : ℕ} → RBtreeInvariant tree d → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
@@ -674,17 +679,31 @@
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
         →  {d : ℕ} → RBtreeInvariant repl d 
         → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
-replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = ? where
-    insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree parent grand : bt (Color ∧ A)) 
-      → (stack : List (bt (Color ∧ A))) → (tr to : bt (Color ∧ A)) → (si : stackInvariant key tr to stack ) 
+replaceRBP {n} {m} {A} {t} key value orig tree rbio rbit stack si next exit = insertCase1 where
+    insertCase2 : (tree parent grand : bt (Color ∧ A)) 
+      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent grand ) → t
-    insertCase2 tree parent grand stack tr to = ?
-    insertCase1 : (stack : List (bt (Color ∧ A))) → (to tr : bt (Color ∧ A)) → (si : stackInvariant key tr to stack ) → t
-    insertCase1 stack to tr si with stackToPG tr to stack si
+    insertCase2 tree parent grand stack si pg with color A parent
+    ... | Black = ?   -- tree stuctre is preserved
+    ... | Red = insertCase3 grand refl where
+        --
+        --  in some case, stack is poped and loop to replaceRBP
+        --     it means, we have to create replacedTree
+        insertCase3 : ( tr : bt (Color ∧ A) ) → tr ≡ grand → t
+        insertCase3 leaf eq = ?
+        insertCase3 (node kg value leaf tr₁) eq = ?
+        insertCase3 (node kg value (node ku ⟪ Red , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c = ?
+        insertCase3 (node kg value (node ku ⟪ Black , vu ⟫ tr tr₂) tr₁) eq with <-cmp kg ku
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c = ?
+    insertCase1 : t
+    insertCase1 with stackToPG tree orig stack si
     ... | case1 eq = ?
     ... | case2 (case1 eq ) = ?
-    ... | case2 (case2 pg) = insertCase2 ? ? ? ? ? ? ? (PG.pg pg) where
-          si00 : stackInvariant key ? ? ?
-          si00 = ?
+    ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.grand pg) stack si (PG.pg pg)