Mercurial > hg > Gears > GearsAgda

changeset 787:d0080588ccf4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
1016
author Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
date Mon, 16 Oct 2023 10:38:34 +0900
parents 12e19644535e
children 1e8cb65cccef
files hoareBinaryTree1.agda
diffstat 1 files changed, 21 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Oct 02 18:44:21 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Oct 16 10:38:34 2023 +0900
@@ -301,7 +301,7 @@
         ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
         ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
         repl12 : replacedTree key value (child-replaced key  tree1  ) repl
-        repl12 = subst₂ {!!} {!!} {!!} {!!}
+        repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07) ) (sym (rt-property-leaf (replacePR.ri Pre ))) r-leaf
        -- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
@@ -928,37 +928,38 @@
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    ... | case1 eq = exit repl stack eq  record {  -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+    
+    ... | case1 eq  = exit repl stack eq r {- record { -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
         od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
         tree = RBI.tree r ; rot = RBI.rot r
        ; origti = RBI.origti r
        ; origrb = RBI.origrb r 
        ; treerb = RBI.treerb r
        ; replrb = RBI.replrb r
-       ; d=rd = RBI.d=rd r
+       ; d=rd = RBI.d=d r
        ; si = RBI.si r
        ; rotated = RBI.rotated r
-       ; ri = RBI.ri r } 
+       ; ri = RBI.ri r }  -}
     ... | case2 (case1 eq) = {!!} where -- insertCase12
         insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig   → to ≡ orig
-          → (rr : bt (Color ∧ A)) → RBtreeInvariant repl → rr ≡ repl
-          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key rr to stack ) 
-          → stack ≡ rr  ∷ to ∷ [] → t
-        insertCase12 to origrb to≡orig rr rrrb rr≡repl si s≡  = next rr stack 
-{-         record {
-         od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
-         tree = rr ; rot = RBI.rot r
+          → (rr : bt (Color ∧ A)) → RBtreeInvariant {!!}  → rr ≡ {!!}
+          → (stack1 : List (bt (Color ∧ A))) → (si : stackInvariant key {!!} to stack1 ) 
+          → stack1 ≡ rr  ∷ to ∷ [] → t
+        insertCase12 to or t≡o rr rbt r≡r  stack1 sti stack≡ = next rr stack1
+         record {
+         od = RBI.od r ; d = RBI.rd r  ; rd = RBI.rd r ; --r
+         tree = to ; rot = {!!}
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
-         ; treerb = rrrb
-         ; replrb = rrrb
-         ; d=rd = RBI.d=rd r
-         ; si = si
-         ; rotated = RBI.rotated r
-         ; ri = {!!} }
-         -}
-         ? {!!}
-    -- exit rot repl rbir ? ? 
+         ; treerb = subst (λ k → RBtreeInvariant k) (sym t≡o) (or)
+         ; replrb = {!!} --subst (λ k → RBtreeInvariant k) (sym t≡o) (RBI.origrb r)
+         ; d=rd = {!!}
+         ; si =  subst₂ (λ j k → stackInvariant key j k stack1) (r≡r) (t≡o) (sti)
+         ; rotated = {!!}
+         ; ri = {!!} --subst (λ k → replacedRBTree key value (child-replaced key (RBI.rot r)) k) (sym t≡o) ({!ct!})
+         }
+         {!!}
+               -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)