module hoareBinaryTree1 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 hiding (proof)
open import logic


data bt {n : Level} (A : Set n) : Set n where
  bt-leaf :  bt A
  bt-node : (key : ℕ) → A →
    (ltree : bt A) → (rtree : bt A) → bt A

bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
    → ( bt A → List (bt A) → t ) → t
bt-find {n} {m} {A} {t}  key leaf@(bt-leaf) stack exit = exit leaf stack
bt-find {n} {m} {A} {t}  key (bt-node key₁ AA tree tree₁) stack next with <-cmp key key₁
bt-find {n} {m} {A} {t}  key node@(bt-node key₁ AA tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack
bt-find {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (node ∷ stack) next
bt-find {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (node ∷ stack) next

bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → List (bt A) → (bt A → t ) → t
bt-replace {n} {m} {A} {t} ikey a otree stack next = bt-replace0 otree where
    bt-replace1 : bt A → List (bt A) → t
    bt-replace1 tree [] = next tree
    bt-replace1 node ((bt-leaf) ∷ stack) = bt-replace1 node stack
    bt-replace1 node ((bt-node key₁ b x x₁) ∷ stack) = bt-replace1 (bt-node key₁ b node x₁) stack
    bt-replace0 : (tree : bt A) → t
    bt-replace0 tree@(bt-node key _ ltr rtr) = bt-replace1 (bt-node ikey a ltr rtr) stack  -- find case
    bt-replace0 bt-leaf = bt-replace1 (bt-node ikey a bt-leaf bt-leaf) stack




bt-empty : {n : Level} {A : Set n} → bt A
bt-empty = bt-leaf

bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t
bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree  stack (λ tree → next tree) )

find-test :  bt ℕ
find-test = bt-find 5 bt-empty [] (λ x y → x)


insert-test :  bt ℕ
insert-test = bt-insert 5 7 bt-empty (λ x → x)

insert-test1 :  bt ℕ
insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y))


tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
tree+stack0 {n} {A} tree mtree [] = {!!}
tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!}

tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) →  (stack : List (bt A))  → Set n
tree+stack {n} {A} bt-leaf mtree stack = (mtree ≡ bt-leaf) ∧ (stack ≡ [])
tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree) 

data _implies_  (A B : Set ) : Set (succ Z) where
    proof : ( A → B ) → A implies B

implies2p : {A B : Set } → A implies B  → A → B
implies2p (proof x) = x


bt-find-hoare1  : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A))
  → (tree+stack tree mtree stack)
  → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
bt-find-hoare1 {n} {m} {A} {t}  key leaf@(bt-leaf) mtree stack t+s exit = exit leaf stack {!!}
bt-find-hoare1 {n} {m} {A} {t}  key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁
bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA tree tree₁) mtree stack t+s exit | tri≈ ¬a b ¬c = exit node stack {!!}
bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri< a ¬b ¬c = bt-find-hoare1 {n} {m} {A} {t} key ltree {!!} (node ∷ stack) {!!} {!!}
bt-find-hoare1 {n} {m} {A} {t}  key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri> ¬a ¬b c = bt-find-hoare1 key rtree {!!} (node ∷ stack) {!!} {!!}


bt-find-hoare : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t
bt-find-hoare {n} {m} {A} {t}  key node exit = bt-find-hoare1 {n} {m} {A} {t} key node bt-empty [] ({!!}) exit