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 })

-- 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
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 = red ; number = lx }
    ; ltree = ll
    ; rtree = (bt-node (record { key = record { coler = y ; number = x }; ltree = lr; rtree = r }) ) }) )


{-
lnode = node.left
node.left = lnode.right
lnode.right = node
lnode.color = node.color
node.color = RED
return lnode


-- 以下test部分
test-insert1 : bst
test-insert1 = bt-insert bt-empty 2

test-insert2 : bst
test-insert2 = bt-insert test-insert1 3

test-insert3 : bst
test-insert3 = bt-insert test-insert2 1

test-insert4 : bst
test-insert4 = bt-insert test-insert3 4
-}