# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572738780 -32400
# Node ID d18df2e6135d525d449ef82080760deb75034a66
# Parent  1a5dd71199f113a4721072664e6a5207fa2340ab
add replaceNode

diff -r 1a5dd71199f1 -r d18df2e6135d hoareRedBlackTree.agda
--- a/hoareRedBlackTree.agda	Sat Nov 02 19:33:37 2019 +0900
+++ b/hoareRedBlackTree.agda	Sun Nov 03 08:53:00 2019 +0900
@@ -108,6 +108,22 @@
 test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
    node001 ( λ tree → tree )
 
+replaceNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
+replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
+  module FindNodeR where
+      replaceNode1 : (Maybe (Node a )) → Node a
+      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  } 
+      replaceNode1 (just x)  = record n0 { left = left x ; right = right x } 
+      replaceNode2 : SingleLinkedStack (Node a ) → (Node a  → t)  → t
+      replaceNode2 [] next = next ( replaceNode1 (root tree) ) 
+      replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
+      replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
+      replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
+      replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )
+
+insertNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
+insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )
+
 createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
      → RedBlackTree {n}  a 
 createEmptyRedBlackTreeℕ a b = record {
@@ -143,4 +159,6 @@
     ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )
 
 
+replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
+replaceNodeH = {!!}