changeset 3:c0bcdd0552f1

fix llrbt insert
author soto
date Mon, 16 Nov 2020 15:15:58 +0900
parents 0af3d02b3474
children fb1b3d066f63
files bt.agda
diffstat 1 files changed, 32 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/bt.agda	Mon Nov 16 00:44:50 2020 +0900
+++ b/bt.agda	Mon Nov 16 15:15:58 2020 +0900
@@ -47,20 +47,20 @@
   ; 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 }) )
+    ; ltree = (bt-node (record { key = record { coler = red ; number = x }; ltree = l; rtree = rl }) )
     ; 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 = _; ltree = _ ; rtree = bt-empty }) ) = 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
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = red ; number = lx }; ltree = ll; rtree = lr }) )}) )
+  = rotate_left 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 }) )
+  ; ltree = l
+  ; rtree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) ) }) )
   = node
 
 split : bst → bst
@@ -77,31 +77,31 @@
 -- 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 = _; ltree = bt-empty; rtree = _}) ) = 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)
+  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree = (bt-node (record { key = record { coler = red ; number = rrx }; ltree = rrl; rtree = rrr }) )
+    ; rtree = lr }))
+  ; rtree = r }) )
+    = split (rotate_right 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 }) ) }) ) }) )
+  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree = (bt-node (record { key = record { coler = black ; number = rrx }; ltree = lll; rtree = rrr }))
+    ; rtree = lr  }) )
+  ; rtree = r }) )
     = 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 }) ) }) )
+  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
+    ; ltree =  bt-empty
+    ; rtree = rr }) )
+  ; rtree = r}) )
     = 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 }) ) }) )
+  ; ltree = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) )
+  ; rtree = r }) )
   = node
 
 insert_pipeline : bst → bst
@@ -119,37 +119,30 @@
 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 }) )
 
-
-{-
-lnode = node.left
-node.left = lnode.right
-lnode.right = node
-lnode.color = node.color
-node.color = RED
-return lnode
--}
+insert : bst → ℕ → bst
+insert node x = init_node_coler (bt-insert node x)
 
 -- 以下test部分
 test-insert1 : bst
-test-insert1 = init_node_coler (bt-insert bt-empty 0)
+test-insert1 = insert bt-empty 0
 
 test-insert2 : bst
-test-insert2 = init_node_coler (bt-insert test-insert1 1)
+test-insert2 = insert test-insert1 1
 
 test-insert3 : bst
-test-insert3 = init_node_coler (bt-insert test-insert2 2)
+test-insert3 = insert test-insert2 2
 
 test-insert4 : bst
-test-insert4 = init_node_coler (bt-insert test-insert3 3)
+test-insert4 = insert test-insert3 3
 
 test-insert5 : bst
-test-insert5 = init_node_coler (bt-insert test-insert4 4)
+test-insert5 = insert test-insert4 4
 
 test-insert6 : bst
-test-insert6 = init_node_coler (bt-insert test-insert5 5)
+test-insert6 = insert test-insert5 5
 
 test-insert7 : bst
-test-insert7 = init_node_coler (bt-insert test-insert6 6)
+test-insert7 = insert test-insert6 6