Mercurial > hg > Members > soto > experimental

changeset 2:0af3d02b3474

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add rbt insert
author soto
date Mon, 16 Nov 2020 00:44:50 +0900
parents 1b087eaf1c4b
children c0bcdd0552f1
files bt.agda
diffstat 1 files changed, 101 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/bt.agda	Sat Nov 14 02:38:04 2020 +0900
+++ b/bt.agda	Mon Nov 16 00:44:50 2020 +0900
@@ -28,15 +28,6 @@
 test : bst
 test = bt-node (record { key = record { coler = red ; number = zero }; ltree = bt-empty; rtree = bt-empty })
 
--- insert
-bt-insert : bst → ℕ → bst
-bt-insert bt-empty n = ( bt-node (record { key = record { coler = red ; number = zero }; ltree = bt-empty; rtree = bt-empty }) )
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n  with <-cmp x n
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri≈ ¬a b ¬c = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri> ¬a ¬b c = (bt-node (record { key = record { coler = y ; number = x }; ltree = l ; rtree = (bt-insert r n) }) )
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri< a ¬b ¬c = (bt-node (record { key = record { coler = y ; number = x }; ltree = (bt-insert l n) ; rtree = r }) )
-
-
 -- 右回転
 rotate_right : bst → bst
 rotate_right bt-empty = bt-empty
@@ -44,9 +35,89 @@
 rotate_right (bt-node (record { key = record { coler = y ; number = x }
   ; ltree = (bt-node (record { key = record { coler = ly ; number = lx }; ltree = ll; rtree = lr }) )
   ; rtree = r }) )
-  = (bt-node (record { key = record { coler = red ; number = lx }
+  = (bt-node (record { key = record { coler = y ; number = lx }
     ; ltree = ll
-    ; rtree = (bt-node (record { key = record { coler = y ; number = x }; ltree = lr; rtree = r }) ) }) )
+    ; rtree = (bt-node (record { key = record { coler = red ; number = x }; ltree = lr; rtree = r }) ) }) )
+
+-- 左回転
+rotate_left : bst → bst
+rotate_left bt-empty = bt-empty
+rotate_left node@(bt-node (record { key = _; ltree = _; rtree = bt-empty }) ) = node
+rotate_left (bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = ry ; number = rx }; ltree = rl; rtree = rr }) ) }) )
+  = (bt-node (record { key = record { coler = y ; number = rx }
+    ; ltree = (bt-node (record { key = record { coler = red ; number = x }; ltree = rl; rtree = l }) )
+    ; rtree = rr }) )
+
+-- skew
+skew : bst → bst
+skew bt-empty = bt-empty
+skew node@(bt-node (record { key = _; ltree = bt-empty ; rtree = _ }) ) = node
+skew node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = (bt-node (record { key = record { coler = red ; number = lx }; ltree = ll; rtree = lr }) )
+  ; rtree = r}) )
+  = rotate_right node
+skew node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) )
+  ; rtree = r }) )
+  = node
+
+split : bst → bst
+split bt-empty = bt-empty
+split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) = node
+split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) = node
+split node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = (bt-node (record { key = record { coler = ly ; number = lx }; ltree = ll; rtree = lr }) )
+  ; rtree = (bt-node (record { key = record { coler = ry ; number = rx }; ltree = rl; rtree = rr }) )}) )
+  = bt-node (record { key = record { coler = red ; number = x }
+    ; ltree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) )
+    ; rtree = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) )})
+
+-- split
+split_branch : bst → bst
+split_branch bt-empty = bt-empty
+split_branch node@(bt-node (record { key = _; ltree = _; rtree = bt-empty }) ) = node
+split_branch node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree = ll
+    ; rtree = (bt-node (record { key = record { coler = red ; number = rrx }; ltree = rrl; rtree = rrr }) ) }) ) }) )
+    = split (rotate_left node)
+
+split_branch node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree = ll
+    ; rtree = (bt-node (record { key = record { coler = black ; number = rrx }; ltree = lll; rtree = rrr }) ) }) ) }) )
+    = node
+
+split_branch node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree = rl
+    ; rtree = bt-empty }) ) }) )
+    = node
+
+split_branch node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) ) }) )
+  = node
+
+insert_pipeline : bst → bst
+insert_pipeline node = split_branch (skew node)
+
+-- insert
+bt-insert : bst → ℕ → bst
+bt-insert bt-empty n = ( bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) )
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n  with <-cmp x n
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri≈ ¬a b ¬c = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri> ¬a ¬b c = (insert_pipeline (bt-node (record { key = record { coler = y ; number = x }; ltree = (bt-insert l n); rtree = r }) ) )
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n | tri< a ¬b ¬c = (insert_pipeline (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = (bt-insert r n) }) ) )
+
+init_node_coler : bst → bst
+init_node_coler bt-empty = bt-empty
+init_node_coler (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) = (bt-node (record { key = record { coler = black; number = x }; ltree = l; rtree = r }) )
 
 
 {-
@@ -56,18 +127,31 @@
 lnode.color = node.color
 node.color = RED
 return lnode
-
+-}
 
 -- 以下test部分
 test-insert1 : bst
-test-insert1 = bt-insert bt-empty 2
+test-insert1 = init_node_coler (bt-insert bt-empty 0)
 
 test-insert2 : bst
-test-insert2 = bt-insert test-insert1 3
+test-insert2 = init_node_coler (bt-insert test-insert1 1)
 
 test-insert3 : bst
-test-insert3 = bt-insert test-insert2 1
+test-insert3 = init_node_coler (bt-insert test-insert2 2)
 
 test-insert4 : bst
-test-insert4 = bt-insert test-insert3 4
--}
+test-insert4 = init_node_coler (bt-insert test-insert3 3)
+
+test-insert5 : bst
+test-insert5 = init_node_coler (bt-insert test-insert4 4)
+
+test-insert6 : bst
+test-insert6 = init_node_coler (bt-insert test-insert5 5)
+
+test-insert7 : bst
+test-insert7 = init_node_coler (bt-insert test-insert6 6)
+
+
+
+
+