module hoareRedBlackTree where


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
open import logic



record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    putImpl : treeImpl → a → (treeImpl → t) → t
    getImpl  : treeImpl → (treeImpl → Maybe a → t) → t
open TreeMethods

record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
  field
    tree : treeImpl
    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
  putTree : a → (Tree treeImpl → t) → t
  putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
  getTree : (Tree treeImpl → Maybe a → t) → t
  getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )

open Tree

SingleLinkedStack = List

emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
emptySingleLinkedStack = []

clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data  → ( SingleLinkedStack Data → t) → t
clearSingleLinkedStack [] cg = cg []
clearSingleLinkedStack (x ∷ as) cg = cg []

pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n}  -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack stack datum next = next ( datum ∷ stack )

popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack [] cs = cs [] nothing
popSingleLinkedStack (data1 ∷ s)  cs = cs s (just data1)

data Color {n : Level } : Set n where
  Red   : Color
  Black : Color

record Node {n : Level } (a : Set n) : Set n where
  inductive
  field
    key   : ℕ
    value : a
    right : Maybe (Node a )
    left  : Maybe (Node a )
    color : Color {n}
open Node

record RedBlackTree {n : Level } (a : Set n) : Set n where
  field
    root : Maybe (Node a )
    nodeStack : SingleLinkedStack  (Node a )


open RedBlackTree

-- record datum {n : Level} (a : Set n) : Set n where
--   field
--     key : ℕ
--     val : a

--  leaf nodes key is 0.
-- 
-- data BTree {n : Level} (a : Set n) (lk nk rk : ℕ) : Set n where
--   leaf : (l<n : lk < nk) → BTree a lk nk rk
--   node : (left : BTree a lk nk rk)
--        → (datum : ℕ) → (right : BTree a lk nk rk)
--        → BTree a lk nk rk


{-- tree に サイズ比較をつけたい(持ち運びたい)が leaf をどう扱うか問題(0にするとright についたときにおわる)
終わってほしくないので node のときだけにしたいがそれだと根本的に厳しい（BTree a の再帰構造なので）


--}

-- data BTree {n : Level} (a : Set n) : Set n where
--   leaf :  BTree a
--   node : (left : BTree a )
--          → (datum : ℕ)
--          → (right : BTree a )
--          → BTree a

-- {a b c : ℕ} {a≤b : a ≤ b } {b≤c : b ≤ c} →
-- trans≤ : {n : Level} {a : Set n} → Trans {_} {_} {_} {_} {_} {_} {ℕ} {ℕ} {ℕ} (λ x y → x < y) (λ y z → y < z) (λ x z → (x < z)) -- a≤b b≤c
-- trans≤ {n} {a} {i} {j} {k} i<j j<k = ≤-trans i<j {!!}
-- with i <? k
-- trans≤ {n} {a} {i} {j} {k} i<j j<k | yes p = p
-- trans≤ {n} {a} {i} {j} {k} i<j j<k | no ¬p = {!!}


-- data BTree {n : Level} {a : Set n} (p q : ℕ) : ℕ → Set n where
--   leaf : (p<q : p ≤ q ) → BTree p q 0
--   node : ∀ {hl hr h : ℕ}
--              → (key : ℕ)
--              → (left : BTree {n} {a} p key hl )
--              → (right : BTree {n} {a} key q hr )
--              → BTree p q (suc h)

-- leaf-inj : {n : Level} {a : Set n} {p q : ℕ} {pp qq : p ≤ q}
--            → (leaf {n} {a} pp) ≡ (leaf qq) → pp ≡ qq
-- leaf-inj refl = refl



-- node-inj : {n : Level} {a : Set n}
--   {k1 k2 h : ℕ} {l1 r1 : BTree {n} {a} h} {l2 r2 : BTree {n} {a} h}
--   → ((node {n} {a} {h} l1 k1 r1)) ≡ (node l2 k2 r2) → k1 ≡ k2
-- node-inj refl = refl

-- node-inj1 : {n : Level} {a : Set n}
--   {k1 k2 h hl1 hl2 hr1 hr2 p q : ℕ }
--   {l1 : BTree {n} {a} p k1 hl1 } {l2 : BTree {n} {a} p k2 hl2} {l1 : BTree {n} {a} k1 q hr1} {r2 : BTree {n} {a} k2 q hr2}
--   → (node {n} {a} {h} {?} {?} {?}  {!!} {!!} ) ≡ (node  {!!} {!!} {!!} ) → k1 ≡ k2
-- node-inj1 as = {!!}



--- add relation find functions
-- fTree is start codeGear. findT2 is loop codeGear.
-- findT2 : {n m  : Level } {a : Set n} {b lk rk kk1 kk2 : ℕ} {t : Set m}
--       → (k1<k2 : kk1 ≤ kk2) → BTree {n} {a} b lk rk → (key : ℕ)
--       → SingleLinkedStack (BTree {n} {a} b lk rk)
--       → ( (lk ≤ rk) →  BTree {n} {a} b lk rk → SingleLinkedStack (BTree {n} {a} b lk rk) → t)   → t
-- findT2 k1<k2 (leaf p<q) key stack cg = cg {!!} (leaf p<q) stack
-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg with <-cmp key1 key
-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri≈ ¬a b ¬c = {!!}
-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri< a ¬b ¬c = {!!}
-- findT2 k1<k2 (node key1 tree₁ tree₂) key stack cg | tri> ¬a ¬b c = {!!}

-- cg k1<k2 (leaf p<q) stack
-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 lt) key stack cg with <-cmp key1 key
-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 tree@(node rt key1 lt) key stack cg | tri≈ ¬lt eq ¬gt = cg {!!} tree stack
-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri< lt ¬eq ¬gt = {!!}
-- findT2 {n} {m} {a} {b} {kk1} {kk2} {t} k1<k2 (node rt key1 ltt) key stack cg | tri> ¬lt ¬eq gt = {!!}


-- fTree : {n m  : Level } {a : Set n} {b k1 k2 : ℕ} {t : Set m}
--      → BTree {n} {a} b → (key : ℕ)
--      → SingleLinkedStack (BTree {n} {a} b) → ( k1 < k2  →  BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t)  → t
-- fTree {n} {m} {a} {b} tree key stack cg  = clearSingleLinkedStack stack (λ cstack → findT2 {n} {m} {a} {b} {0} {key} z≤n tree key cstack λ x x₁ x₂ → {!!})

{--
そもそも Tree は 高さを受け取るのではなく 関係だけを持つ
leaf は関係を受け取って tran で (0 < n < m)をつくる
--}


{-- 思いつき
 Max Hight を持ち運んで必ず規定回数で止まるようにするのはあり…ｎきがする
 Tree を作ったあとに 左右の最大 hight を比較して Max にするのは良い
 操作時はMaxが減る。 途中で終わった場合や、値が見つかった場合は
 受け取って Max を減らすだけの関数で既定回数数を減らすだけ

 関数に持たせる?データに持たせる?
 とりあえず関数(Data だと 再帰的な構造上定義が難しい)

--}

data BTree {n : Level} {a : Set n} : (hight : ℕ) → Set n where
  leaf : {p q h : ℕ } → (p<q : p ≤ q ) → BTree (suc h)
  node : { h : ℕ }
             → (left : BTree {n} {a} (suc h) )
             → (key : ℕ)
             → (right : BTree {n} {a} (suc h) )
             → BTree h

maxHight : {n m : Level} {a : Set n} {t : Set m} {h : ℕ} → (searchHight : ℕ) → (BTree {n} {a} h) → ℕ
maxHight {n} {m} {a} {t} zero (leaf p<q) = 0                  -- root is leaf
maxHight {n} {m} {a} {t} (suc hi) (leaf p<q) = (suc hi)       -- max
maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) with (maxHight {n} {m} {a} {t} hi tree₁) | (maxHight {n} {m} {a} {t} hi tree₂)
... | lh | rh with <-cmp lh rh
maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri< a₁ ¬b ¬c = rh
maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri≈ ¬a b ¬c = lh
maxHight {n} {m} {a} {t} hi (node tree₁ key₁ tree₂) | lh | rh | tri> ¬a ¬b c = lh
-- maxHight {n} {m} {a} {t} hi (rnode tree₁ key₁ tree₂) = {!!}


LastNodeIsLeaf :  {n : Level} {a : Set n} → (h : ℕ) →  (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool
LastNodeIsLeaf h (leaf p<q) P = true
LastNodeIsLeaf h (node rt k1 lt) P = (P rt k1 lt) /\ LastNodeIsLeaf (suc h) lt (λ _ z _ → P lt z lt) /\ LastNodeIsLeaf (suc h) rt λ _ z _ → P lt z lt

-- allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
-- allnodes leafEx p = true
-- allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p

-- MaxHightStop? :  {n : Level} {a : Set n} → {h : ℕ} → (hight : ℕ) → (tree : BTree {n} {a} h) → (P : BTree {n} {a} (suc h) → ℕ → BTree {n} {a} (suc h) → Bool) → Bool
-- MaxHightStop? {n} {a} {.(suc _)} zero (leaf p<q) P = true
-- MaxHightStop? {n} {a} {.(suc _)} (suc allh) (leaf p<q) P = false
-- MaxHightStop? {n} {a} {h} zero (node lt k rt) P = false
-- MaxHightStop? {n} {a} {h} (suc allh) (node lt k rt) P = (P lt k lt) /\ (MaxHightStop? allh lt λ _ z _ → ) /\ (MaxHightStop? allh rt λ _ z _ → P rt z rt)


SearchLeaf : {n : Level} {a : Set n} → (h : ℕ) → (t : BTree {n} {a} h) → Bool
SearchLeaf h tree = LastNodeIsLeaf h tree (λ l k r → LastNodeIsLeaf (suc h) l (λ _ j _ → j <B? k) /\ LastNodeIsLeaf (suc h) r (λ _ n _ → k <B? n))


{-- whats leaf relation...?
i think keys relation...
"leaf relation" maybe 0<"parent node key" ???
--}
test : {n : Level} {a : Set n} {h : ℕ} → BTree {n} {a} h
test {n} {a} {h} = (node (leaf {n} {a} {0} {2} z≤n) 2 (node (leaf {n} {a} {0} {3} z≤n) 3 (leaf {n} {a} {0} {3} z≤n)))

c : {n : Level} {a : Set n} → Bool
c {n} {a} = SearchLeaf {n} {a} 3 test

cm : {n : Level} {a : Set n} → ℕ
cm {n} {a} = maxHight {n} {n} {a} {a} {zero} {!!} test

lemma-all-leaf : {n : Level} {a : Set n} → (h : ℕ) → (tree : BTree {n} {a} h) → SearchLeaf h tree ≡ true
lemma-all-leaf .(suc _) (leaf p<q) = refl
lemma-all-leaf h tt@(node pltree k1 rtree) = {!!} -- lemma-all-leaf h tt
-- lemma-all-leaf .0 tt@(rnode ltree k1 rtree) = lemma-all-leaf zero tt

findT : {n m  : Level } {a : Set n} {b left current : ℕ} {t : Set m}
      → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
      → SingleLinkedStack (BTree {n} {a} b)
      →   (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t) → t
findT = {!!}

-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
-- findT l<c (node tree₁ key1 tree₂) key st cg | tri< a ¬b ¬c = {!!}
-- findT l<c (node tree₁ key1 tree₂) key st cg | tri≈ ¬a b ¬c = {!!}
-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬a ¬b c = {!!}
-- -- findT l<c tree@(node ltree key1 rtree) key st cg                          | tri≈ ¬lt eq ¬gt = cg tree st
-- findT {n} {m} {a} {b} {l} {cu} {?} l<c tree@(node {b} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = ?
-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {l} {cu} {!!} ({!!}) key st2 cg)
-- findT の {!!} の部分は trans したやつが入ってほしい(型が合わない)


--- nomal find
-- findT : {n m  : Level } {a : Set n} {b left current : ℕ} {t : Set m}
--       → (ta<tb : left ≤ current) → BTree {n} {a} b → (key : ℕ)
--       → SingleLinkedStack (BTree {n} {a} b)
--       →   (BTree {n} {a} b → SingleLinkedStack (BTree {n} {a} b) → t)   → t

-- findT {n} {m} {a} {b} {l} l<c (leaf p<q) key st cg = cg (leaf {n} {a} {b} {key} (z≤n)) st
-- findT l<c (node tree₁ key1 tree₂) key st cg with <-cmp key key1
-- findT l<c tree@(node ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st

-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node (leaf p<q) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → {!!}) -- findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} (leaf {n} {a} ⦃ !! ⦄ {cu} {!!}) key st2 cg)

-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltt@(node ltree key₁ ltree₁) key1 rtree) key st cg | tri< lt ¬eq ¬gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} ⦃ !! ⦄ ⦃ !! ⦄ {!!} {!!} key st2 cg)

-- findT {n} {m} {a} {b} {l} {cu} l<c tree@(node ltree key1 rtree) key st cg | tri> ¬lt ¬eq gt = pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {b} {key} {key1} {!!} (rtree) key st2 cg)


-- findT l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri≈ ¬lt eq ¬gt = cg tree st

-- findT {n} {m} {a} {b} {l} l<c tree@(node {lh} {rh} {h} ltree key1 rtree) key st cg | tri< lt ¬eq ¬gt = {!!} --  pushSingleLinkedStack st tree (λ st2 → findT {n} {m} {a} {lh} {rh} {h} {!!} ({!!}) key {!!} λ x x₁ → {!!})
-- findT l<c (node tree₁ key1 tree₂) key st cg | tri> ¬lt ¬eq gt = {!!}
-- findT (leaf p<q) key st cg = cg (leaf p<q ) st
-- findT (node tree₁ key₁ tree₂) key st cg with <-cmp key key₁
-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri≈ ¬a b ¬c = cg tree st
-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri< a ¬b ¬c = {!!}
-- findT tree@(node tree₁ key₁ tree₂) key st cg | tri> ¬a ¬b c = {!!}


data BTreeEx {n : Level} {a : Set n} : Set n where
  leafEx : BTreeEx
  nodeEx :(left : BTreeEx {n} {a} )
    → (key : ℕ)
    → (right : BTreeEx {n} {a} )
    → BTreeEx


cmpMax : ℕ → ℕ → ℕ
cmpMax lh rh with <-cmp lh rh
cmpMax lh rh | tri< a ¬b ¬c = rh
cmpMax lh rh | tri≈ ¬a b ¬c = lh
cmpMax lh rh | tri> ¬a ¬b c₁ = lh


max1 : {n m : Level} {a : Set n} {t : Set m} → ℕ → (BTreeEx {n} {a}) → (ℕ → t) → t
max1 {n} {m} {a} {t} hi leafEx cg = cg hi
max1 {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg = (max1 {n} {m} {a} {t} (suc hi) tree₁
                    (λ lh → (max1 {n} {m} {a} {t} (suc hi) tree₂ (λ rh → cg (cmpMax lh rh))) ))


max : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → (ℕ → t) → t
max {n} {m} {a} {t} tree = max1 zero tree


maxI : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ℕ
maxI {n} {m} {a} {t} tree = max tree (λ x → x)

-- bad proof
-- isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max 0 tr (λ n → n ≡ n))
-- isStopMax? leafEx = refl
-- isStopMax? (nodeEx tree₁ key₁ tree₂) = {!!}

isStopMax? : {n m : Level} {a : Set n} {t : Set m} → ( tr : BTreeEx {n} {a}) → (max tr (λ eq → eq ≡ eq))
isStopMax? leafEx = refl
isStopMax? (nodeEx tree₁ key₁ tree₂) = max (nodeEx tree₁ key₁ tree₂) (λ n₁ →  {!!})

ltreeSearchLeaf : {n m : Level} {a : Set n} {t : Set m} → (BTreeEx {n} {a}) → ((BTreeEx {n} {a}) → t) → t
ltreeSearchLeaf leafEx cg = cg leafEx
ltreeSearchLeaf (nodeEx tree₁ key₁ tree₂) cg = ltreeSearchLeaf tree₁ cg

ltreeStop? : {n m : Level} {a : Set n} {t : Set m} → (tree : BTreeEx {n} {a}) → ltreeSearchLeaf tree (λ tt →  tt ≡ tt)
ltreeStop? leafEx = refl
ltreeStop? {n} {m} {a} {t} (nodeEx tree₁ key₁ tree₂) =  ltreeStop? {n} {m} {a} {t} tree₁

ltreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
ltreeSearchNode key leafEx cg = cg leafEx
ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = ltreeSearchNode key tree₁ cg
ltreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt
ltreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = cg tree₂




-- 何らかの集合のサイズが減っていれば良い…？
ltreeStoplem : {n m : Level} {a : Set n} {t : Set m}
  → (key : ℕ) → (lt : BTreeEx {n} {a}) → (key1 : ℕ) → (rt : BTreeEx {n} {a}) → (p<q : key < key1 )
  → (ℕ → BTreeEx {n} {a} → t ) → t

ltreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → ltreeSearchNode key tree (λ tt →  tt ≡ tt)
ltreeNodeStop? key leafEx = refl
ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = {!!}

-- ltreeNodeStop? {!!} {!!}
{--
Failed to solve the following constraints:
[720] ltreeSearchNode ?4 ?5 (λ tt → tt ≡ tt)
=< ltreeSearchNode key tree₁ (λ tt → tt ≡ tt)
: Set n
--}
ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl
ltreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = refl



-- rtreeSearchNode : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (BTreeEx {n} {a}) → ( (BTreeEx {n} {a}) → t) → t
-- rtreeSearchNode key leafEx cg = cg leafEx
-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg with <-cmp key key₁
-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri< a ¬b ¬c = cg tree₂
-- rtreeSearchNode key tt@(nodeEx tree₁ key₁ tree₂) cg | tri≈ ¬a b ¬c = cg tt
-- rtreeSearchNode key (nodeEx tree₁ key₁ tree₂) cg | tri> ¬a ¬b c₁ = rtreeSearchNode key tree₁ cg


-- rtreeNodeStop? : {n m : Level} {a : Set n} {t : Set m} → (key : ℕ) → (tree : BTreeEx {n} {a}) → rtreeSearchNode key tree (λ tt →  tt ≡ tt)
-- rtreeNodeStop? key leafEx = refl
-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) with <-cmp key key₁
-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri< a ¬b ¬c = refl
-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri≈ ¬a b ¬c = refl
-- rtreeNodeStop? key (nodeEx tree₁ key₁ tree₂) | tri> ¬a ¬b c₁ = rtreeNodeStop? key {!!}


ltreeStoplem key lt key1 rt p<q cg = cg key (nodeEx lt key1 rt)




-- with (max {n} {m} {a} {t} (suc hi) tree₁ cg) | (max {n} {m} {a} {t} (suc hi) tree₂ cg)
-- ... | lh | rh = {!!}

-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri< a₁ ¬b ¬c = cg rh
-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri≈ ¬a b ¬c = cg lh
-- max {n} {m} {a} {t} hi (nodeEx tree₁ key₁ tree₂) cg | lh | rh | tri> ¬a ¬b c = cg lh


-- findStop : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
-- findStop = {!!}

findTEx : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
findTEx leafEx sd st next = next leafEx st
findTEx (nodeEx ltree datum rtree) sd st  next with <-cmp sd datum
findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri≈ ¬a b ¬c = next tree st
findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri< a ¬b ¬c = pushSingleLinkedStack st tree (λ st2 → findTEx ltree sd st2 next)
findTEx tree@(nodeEx ltree datum rtree) sd st  next | tri> ¬a ¬b c = pushSingleLinkedStack st tree (λ st2 → findTEx rtree sd st2 next)

findL : {n m  : Level } {a : Set n} {t : Set m}  → BTreeEx {n} {a} → (key : ℕ) → SingleLinkedStack (BTreeEx) → (BTreeEx {n} → SingleLinkedStack (BTreeEx) → t) → t
findL leafEx key stack cg = cg leafEx stack
findL (nodeEx tree₁ key1 tree₂) key stack cg with (key1 ≤? key)
findL (nodeEx tree₁ key1 tree₂) key stack cg | yes p with key1 ≟ key
findL tree@(nodeEx tree₁ key1 tree₂) key stack cg | yes p | yes p₁ = cg tree stack
findL tree@(nodeEx ltree key1 tree₂) key stack cg | yes p | no ¬p = pushSingleLinkedStack stack tree (λ stack1 → findL ltree key stack1 cg)
findL (nodeEx tree₁ key1 tree₂) key stack cg | no ¬p = cg leafEx stack



allnodes : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → (P : BTreeEx {n} {a} → ℕ → BTreeEx {n} {a} → Bool) → Bool
allnodes leafEx p = true
allnodes (nodeEx lt k rt) p = (p lt k rt) /\ allnodes lt p /\ allnodes rt p

find-leaf : {n : Level} {a : Set n} → (t : BTreeEx {n} {a}) → Bool
find-leaf tree = allnodes tree (λ l k r → allnodes l (λ _ j _ → j <B? k) /\ allnodes r (λ _ n _ → k <B? n))

testTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
testTree {n} {a} = (nodeEx (nodeEx leafEx 1 leafEx) 2 (nodeEx leafEx 3 (nodeEx (nodeEx leafEx 4 leafEx) 5 (nodeEx leafEx 6 leafEx))))

badTree : {n : Level} {a : Set n} → BTreeEx {n} {a}
badTree {n} {a} = (nodeEx (nodeEx leafEx 3 leafEx) 2 leafEx)



lemm : {n : Level} {a : Set n} → find-leaf {n} {a} testTree ≡ true
lemm = refl


bool-⊥ : true ≡ false → ⊥
bool-⊥ ()

{-- badTree  --}
-- lemm1 : {n : level} {a : set n} → find-leaf {n} {a} badtree ≡ true
-- lemm1 {n} {a} with badtree
-- lemm1 {n} {a} | leafex = {!!}
-- lemm1 {n} {a} | nodeex gda key₁ gda₁ = {!!}

-- lemm-all : {n : Level} {a : Set n} (any-tree : BTreeEx {n} {a}) → find-leaf {n} {a} any-tree ≡ true
-- lemm-all leafEx = refl
-- lemm-all t@(nodeEx ltree k rtree) with (find-leaf t) ≟B true
-- lemm-all (nodeEx ltree k rtree) | yes p = p
-- lemm-all (nodeEx ltree k rtree) | no ¬p = {!!}

-- findT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} {a}  → (key : ℕ) → SingleLinkedStack (BTree a) → (BTree {n} a → SingleLinkedStack (BTree a) → t) → t
-- findT = ?

-- {--
-- 一旦の方針は hight を使って書く, 大小関係 (片方だけ) を持って証明しながら降りてく
-- --}


-- hoge = findTEx testTree 44 [] (λ t s → s)

-- {--
--   Tree に対して l < x < r の条件を足すときに気になるのは l or r が leaf の場合
--   leaf のときだけ例外的な証明を書く必要ありそう
-- --}


-- {-- AVL Tree メモ
-- - $AGDA-HOME/Data/AVL.agda 関連を眺めた Tips
-- AVL は特徴として すべての枝の長さの差が1以内に収まっている木。バランスもできる。

-- AVL Tree には key , value , left right の他にkeyの 上限、下限、高さを持ってるらしい
-- (後ろに付いてるのは高さ+- 1 の関係をもってる)

-- cast operation は木のサイズの log になる
-- (cast operation は… わすれた)

-- insert では 同じ key の値があったら Node を置き換え


-- --}

-- -- findT testTreeType 44 [] (λ t st → t)
-- -- leaf

-- -- findT testTree 44 [] (λ t st → st)
-- -- node leaf 3 leaf ∷ node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []


-- -- findT testTreeType 3 [] (λ t st → t)
-- -- node leaf 3 leaf

-- -- findT testTreeType 3 [] (λ t st → st)
-- -- node (node leaf 1 leaf) 2 (node leaf 3 leaf) ∷ []


-- replaceT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
-- replaceT {n} {m} {a} {t} leaf n0 [] next = next (node leaf n0 leaf)
-- replaceT {n} {m} {a} {t} tree@(node x datum x₁) n0 [] next = next tree

-- replaceT {n} {m} {a} {t} leaf n0 (leaf ∷ rstack) next = replaceT (node leaf n0 leaf) n0 rstack next


-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next with <-cmp n0 datum
-- replaceT {n} {m} {a} {t} leaf n0 (tree@(node x datum x₁) ∷ rstack) next | tri≈ ¬a b ¬c =  replaceT tree n0 rstack next
-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri< a₁ ¬b ¬c = replaceT (node (node leaf n0 leaf) datum x₁) n0 rstack next
-- replaceT {n} {m} {a} {t} leaf n0 (node x datum x₁ ∷ rstack) next | tri> ¬a ¬b c =  replaceT (node x datum (node leaf n0 leaf)) n0 rstack next



-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 (leaf ∷ rstack) next = replaceT tree n0 rstack next

-- -- bad some code
-- replaceT {n} {m} {a} {t} tree@(node ltree datum rtree) n0 ((node x rdatum x₁) ∷ rstack) next with <-cmp datum rdatum
-- replaceT {n} {m} {a} {t} (node ltree datum rtree) n0 (tree@(node x rdatum x₁) ∷ rstack) next
--          | tri≈ ¬a b ¬c = replaceT tree n0 rstack next
-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
--          | tri< a₁ ¬b ¬c = replaceT (node tree rdatum x₁) n0 rstack next
-- replaceT {n} {m} {a} {t} tree n0 (node x rdatum x₁ ∷ rstack) next
--          | tri> ¬a ¬b c = replaceT (node x rdatum tree) n0 rstack next

-- insertT : {n m  : Level } {a : Set n} {t : Set m}  → BTree {n} a → ℕ → SingleLinkedStack (BTree a) → (BTree {n}  a  → t) → t
-- insertT tree n0 st next =  findT tree n0 st ( λ new st2 → replaceT new n0 st2 next )


-- c1 : {n : Level} {a : Set n} → BTree {n} a
-- c1 = insertT leaf 1 [] (λ t → insertT t 3 [] (λ t → insertT t 5 [] (λ t → insertT t 7 [] (λ t → t))))

-- c2 : {n : Level} {a : Set n} → BTree {n} a
-- c2 = insertT leaf 5 [] (λ t → insertT t 3 [] (λ t → insertT t 1 [] (λ t → insertT t 7 [] (λ t → t))))

-- -- -- 末
-- -- findDownEnd : {n m : Level} {a : Set n} {t : Set m} → (find : ℕ) → (any : BTree a) → findT any find [] (λ tt stack → {!!})
-- -- findDownEnd d tree = {!!}

-- find-insert : {n m  : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (key ≡  {!!})))
-- find-insert leaf key with <-cmp key key
-- find-insert leaf key | tri< a ¬b ¬c = ⊥-elim (¬c a )
-- find-insert leaf key | tri≈ ¬a b ¬c = {!!}
-- find-insert leaf key | tri> ¬a ¬b c = ⊥-elim (¬a c )
-- find-insert tr@(node any₁ datum any₂) key with <-cmp key datum
-- find-insert (node any₁ datum any₂) key | tri< a ¬b ¬c = {!!}
-- find-insert (node any₁ datum any₂) key | tri> ¬a ¬b c = {!!}
-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c with <-cmp key datum
-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = {!!}
-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = {!!}
-- find-insert (node any₁ datum any₂) key | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = {!!}

-- -- where
-- find-lemma : {n m : Level} {a : Set n} {t : Set m} → BTree a → ℕ → SingleLinkedStack (BTree a) → (BTree a → SingleLinkedStack (BTree a) → t) → t
-- find-lemma leaf ke st nt = nt leaf st
-- find-lemma (node tr datum tr₁) ke st nt with <-cmp ke datum
-- find-lemma tt@(node tr datum tr₁) ke st nt | tri< a ¬b ¬c = find-lemma tr ke (tt ∷ st) nt
-- find-lemma tt@(node tr datum tr₁) ke st nt | tri≈ ¬a b ¬c = nt tt st
-- find-lemma tt@(node tr datum tr₁) ke st nt | tri> ¬a ¬b c = find-lemma tr₁ ke (tt ∷ st) nt

----
-- find node potition to insert or to delete, the path will be in the stack
--

{-# TERMINATING #-}
findNode : {n m  : Level } {a : Set n} {t : Set m} → RedBlackTree {n}  a  → (Node a ) → (RedBlackTree {n}  a → t) → t
findNode {n} {m} {a}  {t} tree n0 next with root tree
findNode {n} {m} {a}  {t} tree n0 next | nothing = next tree
findNode {n} {m} {a}  {t} tree n0 next | just x with <-cmp (key x) (key n0)
findNode {n} {m} {a}  {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
findNode {n} {m} {a}  {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
findNode {n} {m} {a}  {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)



findNode1 : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree)
  module FindNode where
    findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t
    findNode2 nothing st = next record { root = nothing ; nodeStack = st }
    findNode2 (just x) st with <-cmp (key n0) (key x)
    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st })
    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1)
    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1)

node001 : Node  ℕ
node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black }
node002 : Node  ℕ
node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black }
node003 : Node  ℕ
node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black }

tes0t01 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )
test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } )
   node001 ( λ tree → tree )

replaceNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
replaceNode {n} {m} {a} {t} tree n0 next = replaceNode2 (nodeStack tree) (λ newNode → next record { root = just newNode ; nodeStack = emptySingleLinkedStack } )
  module FindNodeR where
      replaceNode1 : (Maybe (Node a )) → Node a
      replaceNode1 nothing  = record n0 { left = nothing ; right = nothing  }
      replaceNode1 (just x)  = record n0 { left = left x ; right = right x }
      replaceNode2 : SingleLinkedStack (Node a ) → (Node a  → t)  → t
      replaceNode2 [] next = next ( replaceNode1 (root tree) )
      replaceNode2 (x ∷ st) next with <-cmp (key x) (key n0)
      replaceNode2 (x ∷ st) next | tri< a ¬b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new } ) )
      replaceNode2 (x ∷ st) next | tri≈ ¬a b ¬c = replaceNode2 st ( λ new → next ( record x { left = left new ; right = right new } ) )
      replaceNode2 (x ∷ st) next | tri> ¬a ¬b c = replaceNode2 st ( λ new → next ( record x { right = right new } ) )

insertNode : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → t) → t
insertNode tree n0 next = findNode1 tree n0 ( λ new → replaceNode tree n0 next )

createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
     → RedBlackTree {n}  a
createEmptyRedBlackTreeℕ a b = record {
        root = nothing
     ;  nodeStack = emptySingleLinkedStack
   }

findNodeLeft : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeLeft x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) -- stack の top と比較するのはたぶん replace ...?

findNodeRight : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeRight x [] =  (left x ≡ nothing ) ∧ (right x ≡ nothing )
findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h))

data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node :  Maybe (Node a) ) → Set n where
   fni-stackEmpty  : (now :  Maybe (Node a) ) → FindNodeInvariant [] now 
   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st nothing
   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
      →  FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st →  FindNodeInvariant st node
   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (node :  Maybe (Node a ))
      →  FindNodeInvariant ( x ∷ st ) node → findNodeRight x st →  FindNodeInvariant st node 
findNodeLoop : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))

findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) (root new ) → t ) 
     → ( FindNodeInvariant (nodeStack tree)  (root tree) ) → t
findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev
  module FindNodeH where
    findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t
    findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev
    findNode2h (just x) st prev with <-cmp (key n0) (key x)
    ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev
    ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) )
    ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) )


-- replaceNodeH : {n m  : Level } {a : Set n} {t : Set m}  → RedBlackTree {n} a  → (Node a ) → (RedBlackTree {n}  a  → {!!} → t) → {!!} → t
-- replaceNodeH = {!!}