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
open node

record tree (A B C : Set) : Set where
  field
    key : A
    ltree : B
    rtree : C
open tree

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

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へ、それ以外は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 }


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


-- 左回転、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 }


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


set-node-coler : Env → Env
set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
set-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 }

init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
  = exit 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 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-tree1 :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
merge-tree1 env next exit with varl env
... | [] = exit env
... | bt-empty ∷ nl = exit env
... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ ))
... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl })
-- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl })
... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
-- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl })

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



init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
init-col env exit = init-node-coler 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
-}
-- skewはnextがrotate-right。exitはsplitとなる
-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
-- それはskewのexitと等しいので同時に記述してやる。
skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit

split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit


{-
merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit
-}

whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )



{-# TERMINATING #-}
mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit

{-
mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!}
-}

{-
merge-tree env
  (λ env → skew-bt env
    (λ env → merge-rotate-left env
      (λ env → split-branch env
        (λ env →  merge-rotate-right env
          (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit)
      (λ env → mergeP env exit ) )
    exit )
  exit ) exit
-}

--whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )

--whileTestPCall : (tree : rbt) → (n : ℕ)  → Env
--whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) )

whileTestPCall' : (tree : rbt) → (n : ℕ)  → Env
whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )


-- 以下test部分
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