Mercurial > hg > Gears > GearsAgda

changeset 798:794f6d8ddac2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
10/28
author Moririn
date Sat, 28 Oct 2023 19:11:12 +0900
parents 03831d974342
children 418ab1fa2aca
files hoareBinaryTree1.agda
diffstat 1 files changed, 26 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat Oct 28 10:47:31 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Oct 28 19:11:12 2023 +0900
@@ -877,14 +877,14 @@
     -- replaced done, clear stack and reconstruct tree
     --    we can do this in a codeGear, but to accept context switch during reconstruction, we have to call next
     --    this means we have to check prime simple case such as replaced not is exactly the same value / color / key.
-    insertCase11 : ?
-    insertCase11 = ?
+    insertCase11 : {!!}
+    insertCase11 = {!!}
     insertCase10 : (tr0 : bt (Color ∧ A)) → tr0 ≡ RBI.rot r → color tr0 ≡ Black → t
-    insertCase10 leaf eq refl = exit repl stack ? r     -- no stack, replace top node
+    insertCase10 leaf eq refl = exit repl stack {!!} r     -- no stack, replace top node
     insertCase10 tr0@(node key₁ ⟪ Black , value₁ ⟫ left right) tr0=rot refl with <-cmp key key₁ 
-    ... | tri< a ¬b ¬c = exit ? stack ? ?     
-    ... | tri≈ ¬a b ¬c = ?
-    ... | tri> ¬a ¬b c = ?
+    ... | tri< a ¬b ¬c = exit {!!} stack {!!} {!!}     
+    ... | tri≈ ¬a b ¬c = {!!}
+    ... | tri> ¬a ¬b c = {!!}
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
@@ -895,10 +895,10 @@
         insertCase12 :  (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
            → stackInvariant key (RBI.tree r) orig stack
            → t
-        insertCase12 leaf eq1 si = ? -- can't happen
+        insertCase12 leaf eq1 si = {!!} -- can't happen
         insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr
-        ... | tri< a ¬b ¬c | cr = ?
-        ... | tri≈ ¬a b ¬c | cr = ? -- can't happen
+        ... | tri< a ¬b ¬c | cr = {!!}
+        ... | tri≈ ¬a b ¬c | cr = {!!} -- can't happen
         ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
            --
            --    orig B
@@ -932,24 +932,27 @@
              ; repl-eq = rb07
              } where
                rb07 :  black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
-               rb07 = ?
-               -- rb05 should more general     
+               rb07 with <-cmp key key₁
+               ... | tri< a ¬b ¬c = {!!}
+               ... | tri≈ ¬a b ¬c = {!!}
+               ... | tri> ¬a ¬b c = {!!}
+               -- rb05 should more general
                rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree key value
                     (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
                rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl
-               ... | rb-single key₂ value₂ | refl | rb-single key value = ?
-               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ?
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = ?
-               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = ?
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ?
-               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = ?
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ?
-               ... | rb-right-black x x₁ t | refl | rb = ?
-               ... | rb-left-black x x₁ t | refl | rb = ?
-               ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = ?
+               ... | rb-single key₂ value₂ | refl | rb-single key₃ value₃ = ⟪ rb-right-red {!!} refl (RBI.replrb r) , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = {!!}
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = {!!}
+               ... | rb-right-black x x₁ t | refl | rb = {!!}
+               ... | rb-left-black x x₁ t | refl | rb = {!!}
+               ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = {!!}
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
-           ... | Black = exit ? ? ? ? 
-           ... | Red = exit ? ? ? ?
+           ... | Black = exit {!!} {!!} {!!} {!!} 
+           ... | Red = exit {!!} {!!} {!!} {!!}
            --       r = orig                            RBI.tree b
            --      / \                       =>         /    \
            --     b   b → r RBI.tree r             r = orig   o (r/b)