Mercurial > hg > Members > soto > experimental
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