module bt where

open import Data.Nat
open import Level renaming (zero to Z ; suc to succ)
open import Data.List

open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Product

open import Function as F hiding (const)

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

open import logic

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

record Env {n : Level} (A : Set n) : Set n where
  field
    varn : ℕ
    varv : A
    vart : bt A
    varl : List (bt A)
open Env

bt-depth : {n : Level} {a : Set n} → (tree : bt a ) → ℕ
bt-depth leaf = 0
bt-depth (node key value ltree rtree) = suc (Data.Nat._⊔_ (bt-depth ltree) (bt-depth rtree))

bt-depth1 : {n : Level} {A : Set n} → (env : Env A ) → ℕ
bt-depth1 env  with vart env
... | tree = bt-depth-c tree where
    bt-depth-c : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
    bt-depth-c leaf = zero
    bt-depth-c (node key value lt rt) = suc (Data.Nat._⊔_ (bt-depth-c lt ) ( bt-depth-c rt))

test-env : {n : Level} {A : Set n} →  Env ℕ
test-env = record {varn = 0; varv = 4 ; vart = (node 3 2 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []}

test-depth1 :  ℕ
test-depth1 = bt-depth1 record {varn = 0; varv = 4;  vart = (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []}

find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → t
find env next exit = find-c (vart env) env next exit where
    find-c : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (env : Env A )
           → (next : (env : Env A ) → t )
           → (exit : (env : Env A ) → t ) → t
    find-c leaf env next exit = exit env
    find-c n@(node key-t value ltree rtree) env next exit with <-cmp (varn env) key-t
    ... | tri< a ¬b ¬c = find-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit
    ... | tri≈ ¬a b ¬c = exit record env {vart = n}
    ... | tri> ¬a ¬b c = find-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit

find-loop-1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (exit : (env : Env A ) → t) → t
find-loop-1 env exit = find env exit exit

fin-cg : {n m : Level} {A : Set n} {t : Set m} → t → (env : Env A ) → Env A
fin-cg t = (λ env → env )

test-cg = find-loop-1 record {varn = 5; varv = 4; vart = (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))); varl = []} (λ env → env )

replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (next : Env A → t) → t
replaceNode1 env next with vart env
... | leaf = next record env {vart = (node (varn env) (varv env) leaf leaf) }
... | node key-t value ltree rtree = next record env {vart = (node (varn env) (varv env) ltree rtree) }

replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (next : Env A → t )
    → (exit : Env A → t) → t
replace env next exit = replace-c (varl env) env next exit where
    replace-c : {n m : Level} {A : Set n} {t : Set m} → List (bt A) → (env : Env A)
        → (next : Env A → t)
        → (exit : Env A → t) → t
    replace-c st env next exit with st
    ... | [] = exit env
    ... | leaf ∷ st1 = replace-c st1 env next exit
    ... | n@(node key-t value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t)
    ... | tri< a ¬b ¬c = replace-c st1 record env{vart = (node key-t value (vart env) rtree); varl = st1} next exit
    ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit
    ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit

replace-loop1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
    → (exit : (env : Env A ) → t) → t
replace-loop1 env exit = replace env exit exit

insertTree1 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A  → t ) → t
insertTree1 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []}
  $ λ env → replaceNode1 env
    $ λ env → replace-loop1 env exit

replaceTree1 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A  → t ) → t
replaceTree1 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []}
  $ λ env → replaceNode1 env exit

test-insert = insertTree1 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )

test-insert1 = replaceTree1 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )

open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)


treeInvariant : {n : Level} {A : Set n} → (env : Env A) → Set n
treeInvariant env = treeInvariant-c (vart env) env where
    treeInvariant-c : {n : Level} {A : Set n} → (tree : bt A) → (env : Env A) → Set n
    treeInvariant-c tree env with tree
    ... | leaf = Lift _ ⊤
    ... | node key-t value leaf leaf = Lift _ ⊤
    ... | node key-t value leaf rt@(node rkey-t rvalue rltree rrtree₁) = (key-t < rkey-t) ∧ treeInvariant-c rt env
    ... | node key-t value lt@(node lkey-t lvalue lltree lrtree) leaf = treeInvariant-c lt env ∧ (lkey-t < key-t)
    ... | node key-t value lt@(node lkey-t lvalue lltree lrtree) rt@(node rkey-t rvalue rltree rrtree) = treeInvariant-c lt env ∧  (lkey-t < key-t ) ∧ (key-t < rkey-t) ∧ treeInvariant-c rt env

treeInvariant1 : {n : Level} {A : Set n} → (tree : bt A) → Set
treeInvariant1 leaf = ⊤
treeInvariant1 (node key value leaf leaf) = ⊤
treeInvariant1 (node key value leaf n@(node key₁ value₁ t₁ t₂)) = (key < key₁) ∧ treeInvariant1 n
treeInvariant1 (node key value n@(node key₁ value₁ t t₁) leaf) = treeInvariant1 n ∧ (key < key₁)
treeInvariant1 (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant1 n ∧ (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant1 m

treeInvariantTest1  = treeInvariant1 (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))

stackInvariant : {n : Level} {A : Set n} → (env : Env A) → Set n
stackInvariant {_} {A} env = stackInvariant-c (varl env) env where
    stackInvariant-c : {n : Level} {A : Set n} → (stack : List (bt A)) → (env : Env A) → Set n
    stackInvariant-c stack env with stack
    ... | [] = Lift _ ⊤
    ... | x ∷ [] = Lift _ ⊤
    ... | x ∷ leaf ∷ st =  Lift _ ⊥
    ... | x ∷ tail@(node key-t value ltree rtree ∷ st) = ((ltree ≡ x) ∧ stackInvariant-c tail env) ∨ ((rtree ≡ x) ∧ stackInvariant-c tail env)

{-
= Lift _ ⊤
stackInvariant {_} {A} tree (tree1 ∷ [] ) = tree1 ≡ tree
stackInvariant {_} {A} tree (x ∷ tail @ (node key value leaf right ∷ _) ) = (right ≡ x) ∧ stackInvariant tree tail
stackInvariant {_} {A} tree (x ∷ tail @ (node key value left leaf ∷ _) ) = (left ≡ x) ∧ stackInvariant tree tail
stackInvariant {_} {A} tree (x ∷ tail @ (node key value left right ∷ _) ) = ( (left ≡ x) ∧ stackInvariant tree tail) ∨ ( (right ≡ x) ∧ stackInvariant tree tail)
stackInvariant {_} {A} tree s = Lift _ ⊥
-}

findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
           → treeInvariant env ∧ stackInvariant env
           → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
findP env Cond exit = findP-c (vart env) env Cond exit where
    findP-c : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (env : Env A)
           → treeInvariant env ∧ stackInvariant env
           → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
    findP-c leaf env Cond exit = exit env Cond
    findP-c n@(node key-t value ltree rtree) env Cond exit with <-cmp key-t (varn env)
    ... | tri< a ¬b ¬c = findP-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} {!!} exit
    ... | tri≈ ¬a b ¬c = exit record env {vart = n} {!!}
    ... | tri> ¬a ¬b c = findP-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} {!!} exit

{-
findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!}
findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁
findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!}
findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!}
findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!}
-}