Mercurial > hg > Gears > GearsAgda

changeset 776:576b35b1d2d7

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 Fri, 12 May 2023 13:01:13 +0900
parents fb74ba4fa38e
children 8e5159a02b76
files hoareBinaryTree1.agda
diffstat 1 files changed, 18 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu May 11 17:52:58 2023 +0900
+++ b/hoareBinaryTree1.agda	Fri May 12 13:01:13 2023 +0900
@@ -731,10 +731,11 @@
            →  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 : bt (Color ∧ A) ) 
-           → {d : ℕ} →  RBtreeInvariant tree d 
-           → (exit : (current : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
-               → RBI key value tree current stack → t ) → t
+findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree0 : bt (Color ∧ A) ) 
+           → {d : ℕ} →  RBtreeInvariant tree0 d 
+           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+                 → {d1 : ℕ} → RBtreeInvariant tree1 d1 
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
 findRBT = {!!}
 
 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
@@ -742,7 +743,7 @@
      → (orig tree : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
      → (r : RBI key value orig tree stack )
-     → (next : (tree1 (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) 
+     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) 
         → (r : RBI key value orig current stack1 ) 
         → length stack1 < length stack  → t )
      → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
@@ -751,8 +752,8 @@
         → t ) → t
 rotateLeft {n} {m} {A} {t} key value = ? where
     rotateLeft1 : t
-    rotateLeft1 with stackToPG ? orig stack si
-    ... | case1 x = exit {!!} {!!} {!!} {!!} rr
+    rotateLeft1 with stackToPG ? ? ? ?
+    ... | case1 x = ? -- {!!} {!!} {!!} {!!} rr
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
@@ -761,8 +762,8 @@
      → (orig tree : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
      → (r : RBI key value orig tree stack )
-     → (next : (stack1 : List (bt (Color ∧ A))) 
-        → (r : RBI key value orig stack1 ) 
+     → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig current stack1 ) 
         → length stack1 < length stack  → t )
      → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
         →  stack1 ≡ (orig ∷ [])
@@ -780,7 +781,7 @@
      → (orig tree : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
      → (r : RBI key value orig tree stack )
-     → (next : (tree1 (bt (Color ∧ A)))  (stack1 : List (bt (Color ∧ A))) 
+     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
         → (r : RBI key value orig tree1 stack1 ) 
         → length stack1 < length stack  → t )
      → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
@@ -789,7 +790,7 @@
         → t ) → t
 insertCase5 {n} {m} {A} {t} key value = ? where
     insertCase51 : t
-    insertCase51 with stackToPG ? orig stack ?
+    insertCase51 with stackToPG ? ? ? ?
     ... | case1 eq = {!!}
     ... | case2 (case1 eq ) = {!!}
     ... | case2 (case2 pg) with PG.pg pg
@@ -806,15 +807,15 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) 
-     → (orig repl : bt (Color ∧ A)) 
+     → (orig tree : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
-     → (r : RBI key value orig stack )
-     → (next : (stack1 : List (bt (Color ∧ A))) 
-        → (r : RBI key value orig stack1 ) 
+     → (r : RBI key value orig tree stack )
+     → (next : (tree1 : (bt (Color ∧ A))) →  (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig tree1 stack1 ) 
         → length stack1 < length stack  → t )
      → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
         →  stack1 ≡ (orig ∷ [])
-        →  RBI key value orig stack1
+        →  RBI key value orig repl stack1
         → t ) → t
 replaceRBP {n} {m} {A} {t} key value orig stack r next exit = ? where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
@@ -850,7 +851,7 @@
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
-    insertCase1 with stackToPG ? orig stack ?
+    insertCase1 with stackToPG ? orig ? ?
     ... | case1 eq = ? -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
     ... | case2 (case1 eq ) = ? where
         insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d  → to ≡ orig