module bt_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 bst : Set where
  bt-empty : bst
  bt-node  : (node : tree (node col ℕ) bst bst ) → bst

record Env : Set (succ Zero) where
  field
    vart : bst
    varn : ℕ
    varl : List bst
open Env

data Cond : Set (succ Zero) where
  nextcond : Env → Cond → Cond
  exitcond : Env → Cond
open Cond


whileTest_next : {l : Level} {t : Set l}  → (c10 : bst) → (n : ℕ) → (list : List bst) → (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

whileTest_next1 : {l : Level} {t : Set l}  → (c10 : bst) → (n : ℕ) → (list : List bst) → Cond → Cond
whileTest c10 next1 n list (nextcond x next) = {!!}
whileTest c10 next1 n list (exitcond x) = {!!}



-- 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 = []} )

merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit 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 = varn ; 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 = varn ; 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 = varn ; 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
merge env exit = merge-tree env (λ env → merge 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 : bst) → (n : ℕ) → (Code : Env → t) → t
whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )

whileTestPCall :  (tree : bst) → (n : ℕ)  → Env
whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env →  env)) )

test1 = whileTestPCall bt-empty 1
test2 = whileTestPCall (vart test1) 2

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

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-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 []
-}