module bt where


open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary


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 ℕ bst bst ) → bst

-- insert
bt-insert : ℕ → bst → bst
bt-insert n bt-empty = (bt-node (record { key = n ; ltree = bt-empty ; rtree = bt-empty }) )
bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) with <-cmp n x
bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri≈ ¬a b ¬c = (bt-node (record { key = x ; ltree = l ; rtree = r }) )
bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri< a ¬b ¬c = (bt-node (record { key = x ; ltree = l ; rtree = (bt-insert n r) }) ) -- nの方が小さい
bt-insert n (bt-node (record { key = x ; ltree = l ; rtree = r }) ) | tri> ¬a ¬b c = (bt-node (record { key = x ; ltree = (bt-insert n l) ; rtree = r }) ) -- nの方が大きい

-- 以下test部分

test-insert1 : bst
test-insert1 = bt-insert 2 bt-empty

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

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

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