module rbt_imple where

open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Binary
open import Data.Nat hiding (_!$\leq$!_  ; _!$\leq$!?_)
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
    [_] : !$\mathbb{N}$! !$\rightarrow$! right-List
    _!$\text{::}$!>_Cond_ : (x : !$\mathbb{N}$!) !$\rightarrow$! (xs : right-List ) !$\rightarrow$! (p : x Data.Nat.> top-r xs) !$\rightarrow$! right-List

  top-r : right-List !$\rightarrow$! !$\mathbb{N}$!
  top-r [] = {!!}
  top-r [ x ] = x
  top-r (x !$\text{::}$!> l Cond x!$\_{1}$!) = x

  insert-r : !$\mathbb{N}$! !$\rightarrow$! right-List !$\rightarrow$! right-List
  insert-r x l with l
  ... | [] = {!!}
  ... | [ y ] = ?
  ... | y !$\text{::}$!> ys Cond p with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = l
  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
  ... | tri> !$\neg$!a !$\neg$!b c = x !$\text{::}$!> l Cond c

  data  left-List : Set where
    [] : left-List
    [_] : !$\mathbb{N}$! !$\rightarrow$! left-List
    _<!$\text{::}$!_Cond_ : (x : !$\mathbb{N}$!) !$\rightarrow$! (xs : left-List ) !$\rightarrow$! (p : x Data.Nat.< top-l xs) !$\rightarrow$! left-List

  top-l : left-List !$\rightarrow$! !$\mathbb{N}$!
  top-l [] = {!!}
  top-l [ x ] = x
  top-l (x <!$\text{::}$! l Cond x!$\_{1}$!) = x

  insert-l : !$\mathbb{N}$! !$\rightarrow$! left-List !$\rightarrow$! left-List
  insert-l x [] = [ x ]
  insert-l x l@([ y ]) with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
  ... | tri> !$\neg$!a !$\neg$!b c = l
  insert-l x l@(y <!$\text{::}$! ys Cond p) with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
  ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = l
  ... | tri> !$\neg$!a !$\neg$!b c = l


record meta : Set where
  field
    deeps : !$\mathbb{N}$!
    black-nodes : !$\mathbb{N}$!
    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 !$\mathbb{N}$! ) meta rbt-meta rbt-meta ) !$\rightarrow$! rbt-meta

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

testdata = rbt_t.Env.vart test!$\prime$!7

-- ここからmetaの作成

makemeta-comm : rbt_t.rbt !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! meta !$\rightarrow$! rbt-meta

--make meta black nodes
makemeta-black-nodes :  rbt_t.rbt !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! meta !$\rightarrow$! rbt-meta
makemeta-black-nodes = {!!}

-- make meta deeps
set-black-nodes : rbt_t.rbt !$\rightarrow$! meta !$\rightarrow$! !$\mathbb{N}$!
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 !$\rightarrow$! 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!$\prime$!11)
-}