module hoareRedBlackTree where


open import Level hiding (zero)

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.Bool
open import Data.Empty
open import Data.List

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 = []

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 )
    -- compare : k → k → Tri A B C
    -- <-cmp

open RedBlackTree

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

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



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


testTreeType : {n : Level} {a : Set n} → BTree {n} a
testTreeType = (node (node leaf 1 leaf) 2 (node leaf 3 leaf))

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

-- findT testTreeType 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))))


getkey : {n : Level } {a : Set n} → BTree {n} a → Maybe ℕ
getkey leaf = nothing
getkey (node tree₁ datum tree₂) = just datum

find-insert : {n m  : Level } {a : Set n} {t : Set m} → (any : BTree {n} a) → (key : ℕ) → insertT any key [] (λ x → findT x key [] (λ return _ → (just key ≡  (getkey {n} return))))
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 = refl
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 }

test001 = 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))

findNodeLoop : {n  : Level } {a : Set n}  (r : Node a ) (t : SingleLinkedStack (Node a))  → Set n
findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st))



data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → Set n where
   fni-stackEmpty  : (now :  RedBlackTree {n}  a ) → FindNodeInvariant [] now
   fni-treeEmpty  : (st : SingleLinkedStack (Node a))  → FindNodeInvariant st record { root = nothing ; nodeStack = st }
   fni-Left  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
      →  FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st →  FindNodeInvariant st original
   fni-Right  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a )
      →  FindNodeInvariant ( x ∷ st ) original → findNodeRight x st →  FindNodeInvariant st original
   -- fni-loop  : (x : Node a) (st : SingleLinkedStack (Node a)) (original :  RedBlackTree {n}  a ) → FindNodeInvariant st original


findNode1h : {n m  : Level } {a : Set n} {t : Set m}  → (tree : RedBlackTree {n} a )  → (Node a )
     → ((new : RedBlackTree {n} a) →  FindNodeInvariant (nodeStack new) tree → t )
     → ( FindNodeInvariant (nodeStack tree)  tree) → t
findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev
  module FindNodeH where
    findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree  → t
    findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev
    findNode2h (just x) st n0 prev with <-cmp (key n0) (key x)
    ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? )
    ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) )
        where
          nextInvaliant : ({!!})
          nextInvaliant = {!!}
          lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a)
          lproof ns [] with left ns | right ns
          lproof ns [] | just x | just x₁ = {!!}
          lproof ns [] | just x | nothing =  {!!}
          lproof ns [] | nothing | just x = {!!}
          lproof ns [] | nothing | nothing = {!!}
          lproof ns (x ∷ ss) = {!!}

    ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) )


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