# HG changeset patch
# User soto
# Date 1605937805 -32400
# Node ID fb1b3d066f6354e641499a50eec34223639c083a
# Parent  c0bcdd0552f16dd569c706dba2548426dc07496c
WIP continuation insert at LLRB-Tree

diff -r c0bcdd0552f1 -r fb1b3d066f63 bt.agda
--- a/bt.agda	Mon Nov 16 15:15:58 2020 +0900
+++ b/bt.agda	Sat Nov 21 14:50:05 2020 +0900
@@ -4,7 +4,7 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp -- <-cmp
 open import Relation.Binary
-
+open import Data.List
 
 data col : Set where
   black : col
@@ -122,7 +122,62 @@
 insert : bst → ℕ → bst
 insert node x = init_node_coler (bt-insert node x)
 
+-- 赤黒木のinsertをする
+
+
+rbt-insert2 : bst → ℕ → List bst → bst
+rbt-insert2 bt-empty n stack = ( bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) )
+rbt-insert2 (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n
+rbt-insert2 (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri≈ ¬a b ¬c = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
+rbt-insert2 (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri> ¬a ¬b c = (insert_pipeline (bt-node (record { key = record { coler = y ; number = x }; ltree = (rbt-insert2 l n stack); rtree = r }) ) )
+rbt-insert2 (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri< a ¬b ¬c = (insert_pipeline (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = (rbt-insert2 r n stack) }) ) )
+
+--treeをmerge
+merge-tree : bst → List bst → bst
+merge-tree node []  = init_node_coler (insert_pipeline node)
+merge-tree x (bt-empty ∷ xs) =  bt-empty
+merge-tree bt-empty s = bt-empty
+merge-tree target@(bt-node (record { key = record { coler = ty; number = tx }; ltree = tl; rtree = tr }) ) ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) with <-cmp tx x
+merge-tree target@(bt-node (record { key = record { coler = ty; number = tx }; ltree = tl; rtree = tr }) ) ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri≈ ¬a b ¬c
+  = merge-tree ( insert_pipeline  (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) ) xs
+  -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) xs
+
+merge-tree target@(bt-node (record { key = record { coler = ty; number = tx }; ltree = tl; rtree = tr }) ) ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri> ¬a ¬b c
+  = merge-tree ( insert_pipeline (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) ) xs
+  -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) xs
+
+merge-tree target@(bt-node (record { key = record { coler = ty; number = tx }; ltree = tl; rtree = tr }) ) ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri< a ¬b ¬c
+  =  merge-tree ( insert_pipeline  (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) ) xs
+  -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) xs
+
+--(bt-node (record { key = record { coler = red ; number = 1 }; ltree = bt-empty; rtree = bt-empty }))
+-- merge-tree node ( (bt-node (record { key = record { coler = y; number = x }; ltree = bt-empty; rtree = bt-node r }) ) ∷ xs) = merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = node ; rtree = bt-node r }) ) xs
+-- merge-tree node ( (bt-node (record { key = record { coler = y; number = x }; ltree = bt-node l; rtree = bt-empty }) ) ∷ xs) = merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = bt-node l ; rtree = node }) ) xs
+--merge-tree node ( (bt-node (record { key = record { coler = y; number = x }; ltree = bt-node _; rtree = bt-node _ }) ) ∷ xs) = bt-empty
+
+
+rbt-insert : bst → ℕ → List bst → bst
+rbt-insert bt-empty n stack = merge-tree (bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) stack
+-- ( bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) -- mergeに遷移する
+rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n
+rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri≈ ¬a b ¬c
+  = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
+rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri> ¬a ¬b c
+  = rbt-insert l n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) ∷ stack)
+rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri< a ¬b ¬c
+  = rbt-insert r n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) ∷ stack )
+
+
 -- 以下test部分
+
+test-rbt1 = rbt-insert bt-empty 0 []
+test-rbt2 = rbt-insert test-rbt1 1 []
+test-rbt3 = rbt-insert test-rbt2 2 []
+test-rbt4 = rbt-insert test-rbt3 3 []
+test-rbt5 = rbt-insert test-rbt4 4 []
+test-rbt6 = rbt-insert test-rbt5 5 []
+
+
 test-insert1 : bst
 test-insert1 = insert bt-empty 0