--- a/bt.agda	Thu Nov 12 21:35:03 2020 +0900
+++ b/bt.agda	Sat Nov 14 02:38:04 2020 +0900
@@ -6,6 +6,15 @@
 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
@@ -14,27 +23,51 @@
 
 data bst : Set where
   bt-empty : bst
-  bt-node  : (node : tree ℕ bst bst ) → 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 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の方が大きい
+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 2 bt-empty
+test-insert1 = bt-insert bt-empty 2
 
 test-insert2 : bst
-test-insert2 = bt-insert 3 test-insert1
+test-insert2 = bt-insert test-insert1 3
 
 test-insert3 : bst
-test-insert3 = bt-insert 1 test-insert2
+test-insert3 = bt-insert test-insert2 1
 
 test-insert4 : bst
-test-insert4 = bt-insert 4 test-insert3
-
+test-insert4 = bt-insert test-insert3 4
+-}