module rbt_imple where

open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Binary
open import Data.Nat hiding (_≤_  ; _≤?_)
open import Data.List hiding ([_])
open import Data.Product
open import Data.Nat.Properties as NP

open import rbt_t

--このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう
mutual
  data  right-List : Set where
    [] : right-List
    [_] : ℕ → right-List
    _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List

  top-r : right-List → ℕ
  top-r [] = {!!}
  top-r [ x ] = x
  top-r (x ∷> l Cond x₁) = x

  insert-r : ℕ → right-List → right-List
  insert-r x [] = [ x ]
  insert-r x l@([ y ]) with <-cmp x y
  ... | tri< a ¬b ¬c = l
  ... | tri≈ ¬a b ¬c = l
  ... | tri> ¬a ¬b c = x ∷> l Cond c
  insert-r x l@(y ∷> ys Cond p) with <-cmp x y
  ... | tri< a ¬b ¬c = l
  ... | tri≈ ¬a b ¬c = l
  ... | tri> ¬a ¬b c = x ∷> l Cond c

  data  left-List : Set where
    [] : left-List
    [_] : ℕ -> left-List
    _<∷_Cond_ : (x : ℕ) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List

  top-l : left-List → ℕ
  top-l [] = {!!}
  top-l [ x ] = x
  top-l (x <∷ l Cond x₁) = x

  insert-l : ℕ -> left-List -> left-List
  insert-l x [] = [ x ]
  insert-l x l@([ y ]) with <-cmp x y
  ... | tri< a ¬b ¬c = x <∷ l Cond a
  ... | tri≈ ¬a b ¬c = l
  ... | tri> ¬a ¬b c = l
  insert-l x l@(y <∷ ys Cond p) with <-cmp x y
  ... | tri< a ¬b ¬c = x <∷ l Cond a
  ... | tri≈ ¬a b ¬c = l
  ... | tri> ¬a ¬b c = l


record meta : Set where
  field
    deeps : ℕ
    black-nodes : ℕ
    l-list : left-List
    r-list : right-List
open meta

record tree-meta (A B C D : Set) : Set where
  field
    key : A
    meta-data : B
    ltree : C
    rtree : D
open tree

data rbt-meta : Set where
  bt-empty : rbt-meta
  bt-node  : (node : tree-meta (node col ℕ ) meta rbt-meta rbt-meta ) → rbt-meta

test'1 = whileTestPCall' bt-empty 0
test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14

testdata = rbt_t.Env.vart test'7

-- ここからmetaの作成

makemeta-comm : rbt_t.rbt → ℕ → meta → rbt-meta

--make meta black nodes
makemeta-black-nodes :  rbt_t.rbt → ℕ → meta → rbt-meta
makemeta-black-nodes = {!!}

-- make meta deeps
set-black-nodes : rbt_t.rbt → meta → ℕ
set-black-nodes rbt fls with rbt
... | bt-empty = (suc (black-nodes fls) )
... | bt-node node with (node.coler (key node))
... | black = (suc (black-nodes fls) )
... | red = (black-nodes fls)

--make meta list
makemeta-comm rbt num fls with rbt
... | bt-empty = bt-empty
... | bt-node node = bt-node ( record { key = key node
  ; meta-data = ( record {deeps = (deeps fls)
    ; black-nodes = set-black-nodes rbt fls
    ; l-list = insert-l (node.number (key node)) (l-list fls)
    ; r-list = insert-r (node.number (key node))  (r-list fls) } )
  ; ltree = makemeta-comm (ltree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
    ; black-nodes = set-black-nodes rbt fls
    ; l-list = insert-l (node.number (key node)) (l-list fls)
    ; r-list = (r-list fls) } )
  ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
    ; black-nodes = set-black-nodes rbt fls
    ; l-list = (l-list fls)
    ; r-list = insert-r (node.number (key node)) (r-list fls) } ) })

-- init
makemeta : rbt → rbt-meta
makemeta rbt with rbt
... | bt-empty = bt-empty
... | bt-node node = bt-node ( record { key = key node
  ; meta-data =  ( record { deeps = 0 ; black-nodes = 1; l-list = [] ; r-list = [] } )
  ; ltree = makemeta-comm (ltree node) (node.number (key node))
    ( record { deeps = 1 ; black-nodes = 1 ; l-list = insert-l (node.number (key node)) [] ; r-list = [] } )
  ; rtree = makemeta-comm (rtree node) (node.number (key node))
    ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) })

test11 = makemeta (rbt_t.Env.vart test'11)