Mercurial > hg > Gears > GearsAgda

changeset 918:1d34a752add0

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, 04 Jun 2024 11:30:20 +0900
parents e5502b865a94
children 4d379ebc53c8
files hoareBinaryTree1.agda
diffstat 1 files changed, 24 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Jun 04 09:59:51 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Jun 04 11:30:20 2024 +0900
@@ -1732,29 +1732,29 @@
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
  → (exit : (r : RBI key value tree0 stack ) → t ) → t
-replaceRBTNode key value .leaf rbi ti leaf .(leaf ∷ []) s-nil (case1 refl) exit = exit record {
-     tree = leaf
-   ; repl = node key ⟪ Red , value ⟫ leaf leaf
-   ; origti = ti
-   ; origrb = rbi
-   ; treerb = rb-leaf
-   ; replrb = rb-red _ value refl refl refl  rb-leaf rb-leaf
-   ; si = s-nil
-   ; state = top-black refl (case1 rbr-leaf)
-  }
-replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ value₁ x₁ x₂ ∷ stack) si2@(s-right .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = ?
-replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ ⟪ Black , value₁ ⟫ x₁ x₂ ∷ stack) si2@(s-left .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = ?
-replaceRBTNode key value orig rbi ti leaf (leaf ∷ node key₁ ⟪ Red , value₁ ⟫ x₁ x₂ ∷ stack) si2@(s-left .leaf .orig tree {k1} {v1} x si) (case1 refl) exit = exit record {
-     tree = leaf
-   ; repl = node key ⟪ Red , value ⟫ leaf leaf 
-   ; origti = ti
-   ; origrb = rbi
-   ; treerb = ? -- PGtoRBinvariant1 tree orig rbi stack si
-   ; replrb = ?
-   ; si = ?
-   ; state = ?
-  }
-replaceRBTNode key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record {
+replaceRBTNode {n} {m} {A}  {t} key value orig rbi ti leaf stack si (case1 refl) exit with stackToPG leaf orig stack si
+... | case1 x = ?
+... | case2 (case1 x) = ?
+... | case2 (case2 pg) = rp00 where
+   buildCase : t
+   buildCase = ?
+   rotateCase : t
+   rotateCase = exit record {
+         tree = ?
+       ; repl = ?
+       ; origti = ti
+       ; origrb = rbi
+       ; treerb = ?
+       ; replrb = ?
+       ; si = ?
+       ; state = rotate ? ? ? ? }
+   rp00 : t
+   rp00 with PG.pg pg
+   ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
+   ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+replaceRBTNode {n} {m} {A}  key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record {
      tree = tree
    ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
    ; origti = ti
@@ -1762,8 +1762,7 @@
    ; treerb = PGtoRBinvariant1 tree orig rbi stack si
    ; replrb = ?
    ; si = si
-   ; state = rebuild ? ? ?
-  }
+   ; state = rebuild ? ? ? }
 
 --
 --   rotate and rebuild replaceTree and rb-invariant