--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/rbt_t.agda	Tue Nov 24 19:28:52 2020 +0900
@@ -0,0 +1,340 @@
+module rbt_t where
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+open import Data.List
+
+-- → t を適用するために必要だった
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Level
+
+
+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 rbt : Set where
+  bt-empty : rbt
+  bt-node  : (node : tree (node col ℕ) rbt rbt ) → rbt
+
+record Env : Set (succ Zero) where
+  field
+    vart : rbt
+    varn : ℕ
+    varl : List rbt
+open Env
+
+whileTest_next : {l : Level} {t : Set l}  → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
+whileTest_next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
+
+--whileTest_exit : {l : Level} {t : Set l}  → (c10 : bst) → (n : ℕ) → (list : List bst) → (next : Env → t) → (exit : Env → t) → t
+--whileTest_exit c10 n list next exit = exit (record {vart = c10 ; varn = n ; varl = list} )
+
+merge-tree :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+
+-- 全てmerge-treeへ
+split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ }
+  ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr })
+  ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) })
+  ; varn = varn ; varl = varl } next exit
+  = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ }
+    ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr })
+    ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
+    ; varn = varn ; varl = varl }
+
+{-
+split bt-empty n stack = bt-empty
+split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) n stack = node
+
+split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) n stack = 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 }) )}) ) n stack
+  = {!!}
+-}
+{-
+merge-tree (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 }) )})) n stack
+-}
+
+-- 右回転
+-- 実行時splitへ、それ以外はmerge-treeへ
+merge-rotate_right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-rotate_right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate_right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate_right record { vart = 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 }
+  ; varn = varn ; varl = varl } next exit
+    = next record { vart = 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 }) }
+      ; varn = varn ; varl = varl }
+
+{-
+merge-rotate_right bt-empty n stack = bt-empty
+merge-rotate_right node@(bt-node (record { key = _; ltree = bt-empty; rtree = _ }) ) n stack = node
+merge-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 }) ) n stack
+    = {!!}
+-}
+{-
+split (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 }) ) }) ) n stack
+-}
+
+-- split
+split_branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+split_branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split_branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split_branch node@record{ vart = bt-node record { key = key₁
+  ; ltree = (bt-node record { key = record { coler = red ; number = number₁ }
+    ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ })
+    ; rtree = lr })
+  ; rtree = rtree }
+  ; varn = varn ; varl = varl } next exit
+  = next node
+
+
+{-
+split_branch bt-empty n stack = bt-empty
+split_branch node@(bt-node (record { key = _; ltree = bt-empty; rtree = _}) ) n stack = 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 }) ) n stack
+    = {!!}
+    --merge-rotate_right node n stack
+
+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 }) ) n stack
+    = {!!}
+    --merge-tree node n stack
+
+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}) ) n stack
+    = {!!}
+    --merge-tree node n stack
+
+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 }) ) n stack
+    = {!!}
+    --merge-tree node n stack
+-}
+-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
+merge-rotate_left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-rotate_left node@record { vart = bt-empty ; varn = varn ; varl = varl }  next exit = exit node
+merge-rotate_left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate_left record { vart = 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 }) } ; varn = varn ; varl = varl } next exit
+  = next record { vart = 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}
+  　　; varn = varn ; varl = varl }
+
+{-
+merge-rotate_left bt-empty n stack = bt-empty
+merge-rotate_left node@(bt-node (record { key = _; ltree = _; rtree = bt-empty }) ) n stack = node
+merge-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 }) ) }) ) n stack
+  = split_branch (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 }) ) n stack
+-}
+
+-- skew exitがsplitへ　nextが左回転
+skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit =  exit node
+skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+skew-bt node@record { vart = (bt-node record { key = key₁
+  ; ltree = ltree₁
+  ; rtree = (bt-node record { key = record { coler = black ; number = number }
+  ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit
+    = exit node
+skew-bt node@record { vart = (bt-node record { key = key₁
+  ; ltree = ltree₁
+  ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) })
+  ; varn = varn ; varl = varl } next exit
+    = next node
+
+
+{-
+skew bt-empty n stack = bt-empty
+skew node@(bt-node (record { key = _; ltree = _ ; rtree = bt-empty }) ) n stack = node
+skew node@(bt-node (record { key = record { coler = y ; number = x }
+  ; ltree = l
+  ; rtree = r@(bt-node (record { key = record { coler = red ; number = lx }; ltree = ll; rtree = lr }) )}) ) n stack
+    = merge-rotate_left node n stack
+
+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 }) ) }) ) n stack
+    = split_branch node n stack
+-}
+
+
+-- test : {l : Level} {t : Set l} → (Code : Env → t) → t
+-- test next = next (record {vart = bt-node (record { key = record { coler = red ; number = 0 }; ltree = bt-empty; rtree = bt-empty }); varn = 3; varl = []} )
+
+
+init_node_coler : Env → Env
+init_node_coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
+init_node_coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+  = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+
+
+
+merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit (init_node_coler node)
+merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri> ¬a ¬b c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
+
+{-
+merge-tree {le} {t} node n []  = node
+merge-tree node n (bt-empty ∷ xs) =  bt-empty
+merge-tree target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) with <-cmp n x
+merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri≈ ¬a b ¬c
+  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) x xs
+
+merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri> ¬a ¬b c
+  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) x xs
+
+merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri< a ¬b ¬c
+  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) x xs
+-}
+
+
+
+-- insert
+bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+-- mergeへ遷移する
+bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit
+  = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl })
+
+-- 場合分けを行う
+bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n
+bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c
+  = exit node
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c
+  = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl })
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
+  = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
+
+-- normal loop without termination
+{-# TERMINATING #-}
+insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+insert env exit = bt-insert env (λ env → insert env exit ) exit
+
+{-# TERMINATING #-}
+merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+
+{-# TERMINATING #-}
+split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit
+
+{-# TERMINATING #-}
+rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+rotate_right env exit = merge-rotate_right env (λ env → split-p env (λ env → merge env exit ) ) exit
+
+{-# TERMINATING #-}
+split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+split-b env exit = split_branch env (λ env → rotate_right env exit ) λ env → merge env exit
+
+{-# TERMINATING #-}
+rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+rotate_left env exit = merge-rotate_left env (λ env → split-b env exit ) exit
+
+{-# TERMINATING #-}
+skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit
+
+merge env exit = merge-tree env (λ env → skew env exit ) exit
+
+
+-- equivalent of whileLoopP but it looks like an induction on varn
+
+--whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
+--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
+whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
+
+whileTestPCall : (tree : rbt) → (n : ℕ)  → Env
+whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env →  env)) )
+
+test1 = whileTestPCall bt-empty 0
+test2 = whileTestPCall (vart test1) 1
+test3 = whileTestPCall (vart test2) 2
+test4 = whileTestPCall (vart test3) 3
+test5 = whileTestPCall (vart test4) 4
+test6 = whileTestPCall (vart test5) 5
+test7 = whileTestPCall (vart test6) 6
+
+--whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → merge env (λ env2 →  env2))
+{-
+bt-insert bt-empty n stack = merge-tree {le} {t} (bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) n stack
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n
+bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri≈ ¬a b ¬c
+  = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
+bt-insert {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri> ¬a ¬b c
+  = bt-insert {le} {t} l n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) ∷ stack)
+bt-insert  {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri< a ¬b ¬c
+  = bt-insert {le} {t} r n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) ∷ stack )
+-}
+
+--insert : bst → ℕ → bst
+--insert node x = init_node_coler (bt-insert node x)
+
+{-
+-- 以下test部分
+test-rbt1 : {le : Level} {t : Set le} → bst
+test-rbt1 {le} {t} = bt-insert {le} {t} bt-empty 0 []
+
+test-rbt2 : {le : Level} {t : Set le} → bst
+test-rbt2 {le} {t} = bt-insert {le} {t} test-rbt1 1 []
+
+--test-rbt3 = bt-insert test-rbt2 2 []
+--test-rbt4 = bt-insert test-rbt3 3 []
+--test-rbt5 = bt-insert test-rbt4 4 []
+--test-rbt6 = bt-insert test-rbt5 5 []
+-}
+