Mercurial > hg > Members > soto > experimental
view bt.agda @ 3:c0bcdd0552f1
fix llrbt insert
author | soto |
---|---|
date | Mon, 16 Nov 2020 15:15:58 +0900 |
parents | 0af3d02b3474 |
children | fb1b3d066f63 |
line wrap: on
line source
module bt where open import Data.Nat hiding (compare) open import Data.Nat.Properties as NatProp -- <-cmp open import Relation.Binary data col : Set where black : col red : col record node (A B : Set) : Set where field coler : A number : B record tree (A B C : Set) : Set where field key : A ltree : B rtree : C data bst : Set where bt-empty : bst bt-node : (node : tree (node col ℕ) bst bst ) → bst test : bst test = bt-node (record { key = record { coler = red ; number = zero }; ltree = bt-empty; rtree = bt-empty }) -- 右回転 rotate_right : bst → bst rotate_right bt-empty = bt-empty rotate_right node@(bt-node (record { key = _; ltree = bt-empty; rtree = _ }) ) = node 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 = y ; number = lx } ; ltree = ll ; 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 = l; rtree = rl }) ) ; rtree = rr }) ) -- skew skew : bst → bst skew bt-empty = bt-empty skew node@(bt-node (record { key = _; ltree = _ ; rtree = bt-empty }) ) = node skew node@(bt-node (record { key = record { coler = y ; number = x } ; 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 = l ; rtree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) ) }) ) = 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 = bt-empty; rtree = _}) ) = node split_branch node@(bt-node (record { key = record { coler = y ; number = x } ; 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 = (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 = (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 = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) ) ; rtree = r }) ) = 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 }) ) insert : bst → ℕ → bst insert node x = init_node_coler (bt-insert node x) -- 以下test部分 test-insert1 : bst test-insert1 = insert bt-empty 0 test-insert2 : bst test-insert2 = insert test-insert1 1 test-insert3 : bst test-insert3 = insert test-insert2 2 test-insert4 : bst test-insert4 = insert test-insert3 3 test-insert5 : bst test-insert5 = insert test-insert4 4 test-insert6 : bst test-insert6 = insert test-insert5 5 test-insert7 : bst test-insert7 = insert test-insert6 6