module rbt where

open import Data.Nat
open import Level renaming (zero to Z ; suc to succ)
open import Data.List

open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Product

open import Function as F hiding (const)

open import Level renaming (zero to Z ; suc to succ)

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product

open import Function as F hiding (const)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

data coler : Set where
  red : coler
  black : coler

data bool : Set where
  true : bool
  false : bool

data rbt {n : Level} (A : Set n) : Set n where
  leaf : rbt A
  node : (key-t : ℕ) →  (col : coler) → (value : A) →
    (ltree : rbt A ) → (rtree : rbt A ) → rbt A

record Env {n : Level} (A : Set n) : Set n where
  field
    varn : ℕ
    varv : A
    vart : rbt A
    varl : List (rbt A)
    flag : bool
open Env

find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → t
find env next exit = find-c (vart env) env next exit where
    find-c : {n m : Level} {A : Set n} {t : Set m} → (tree : rbt A) → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → t
    find-c leaf env next exit = exit env
    find-c n@(node key-t col value ltree rtree) env next exit with <-cmp (varn env) key-t
    ... | tri< a ¬b ¬c = find-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit
    ... | tri≈ ¬a b ¬c = exit record env {vart = n}
    ... | tri> ¬a ¬b c = find-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit

replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (next : Env A → t) → t
replaceNode1 env next with vart env
... | leaf = next record env {vart = (node (varn env) red (varv env) leaf leaf) }
... | node key-t col value ltree rtree = next record env {vart = (node (varn env) col (varv env) ltree rtree) }

replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (next : Env A → t )
    → (exit : Env A → t) → t
replace env next exit = replace-c (varl env) env exit where
    split-c : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t
    split-c env exit with (vart env)
    ... | leaf = {!!}  -- replace-c
    ... | node key-t col value leaf leaf = {!!}
    ... | node key-t col value leaf (node key-t₁ col₁ value₁ rtree rtree₁) = {!!}
    ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) leaf = {!!}
    ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) (node key-t₂ col₂ value₂ rtree rtree₁) = {!!}
    marge-left-tree : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t
    marge-left-tree env exit with (varl env)
    ... | [] = {!!} -- split
    ... | tree ∷ st with (vart env)
    ... | leaf = {!!} -- split
    ... | node key-t col value x x₁ = {!!} -- split
    rotate-left : {n m : Level} {A : Set n} {t : Set m} → (rbt A) → Env A → (next : Env A → t) → (exit : Env A → t) → t
    rotate-left tree env next exit with varl env
    ... | [] = {!!} -- split
    ... | tree ∷ st with vart env
    ... | leaf = {!!} -- split
    ... | node nkey-t ncol nvalue nltree nrtree with tree
    ... | leaf = {!!} -- split
    ... | node key-t col value ltree leaf = exit env
    ... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree)
        = next record env { vart = node nkey-t ncol nvalue
          (node rkey-t col rvalue (node key-t red value ltree rltree) rrtree) -- ltree
          nrtree
        ; varn = varn env; varl = varl env }
    replace-c : {n m : Level} {A : Set n} {t : Set m} → List (rbt A) → (env : Env A)
        → (exit : Env A → t) → t
    balance_insert_left : {n m : Level} {A : Set n} {t : Set m} → List (rbt A)  → (rbt A) → (env : Env A)
        → (exit : Env A → t ) → t
    balance_insert_left st tree env exit with flag env
    ... | true = replace-c st env exit
    ... | false with tree
    ... | leaf = {!!} -- split
    ... | node key-t col value leaf rtree = {!!} --split
    ... | node key-t col value ltree@(node lkey-t lcol lvalue lltree lrtree) rtree with lrtree
    ... | leaf = {!!} --split
    ... | (node lrkey-t black lrvalue lrltree lrrtree) = {!!} -- split
    ... | (node lrkey-t red lrvalue lrltree lrrtree)
        = rotate-left ltree env (λ env → replace-c st env exit) (λ env → {!!}) -- rotate left
    replace-c st env exit with st
    ... | [] = exit env
    ... | leaf ∷ st1 = replace-c st1 env  exit
    ... | n@(node key-t col value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t)
    ... | tri< a ¬b ¬c = balance_insert_left st1 (node key-t col value (vart env) rtree) record env{vart = (node key-t col value (vart env) rtree); varl = st1} exit -- balance left
    ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t col (varv env) ltree rtree); varl = st1} exit -- そのままloop
    ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t col value ltree (vart env)); varl = st1} exit -- balance right

-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
rotate-left : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t
rotate-left env next exit with vart env
... | leaf = exit env
... | node key-t col value ltree leaf = exit env
... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree)
    = next record env { vart = (node rkey-t col rvalue
      (node key-t red value ltree rltree)
      rrtree)
    ; varn = varn env; varl = varl env }

-- 右回転、実行時splitへ、それ以外はmerge-treeへ
rotate-right : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t
rotate-right env next exit with vart env
... | leaf = exit env
... | node key-t col value leaf rtree = exit env
... | node key-t col value (node lkey-t lcol lvalue lltree lrtree) rtree
    = next record env { vart = (node lkey-t col lvalue
      lltree
      (node key-t red value lrtree rtree) )
    ; varn = varn env; varl = varl env }