module Struct.SimpleTree where

open import Core
import List as L

data Tree (m n : ℕ) : Set where
  empty : m ≤ n → Tree m n
  node : ∀ x → m ≤ x → x < n
    → Tree m x
    → Tree (suc x) n
    → Tree m n

tree-≤ : ∀ {m n} → Tree m n → m ≤ n
tree-≤ (empty m≤n) = m≤n
tree-≤ (node x m≤x x<n l r) = <-trans m≤x (sx<sy x<n)

`_ : ∀ x → Tree x (suc x)
` x = node x ≤-refl x<sx (empty ≤-refl) (empty ≤-refl)

module Sample where
  just-0 : Tree 0 1
  just-0 = ` 0

  --  2
  -- 1 3
  t-123 : Tree 1 4
  t-123 = node 2 (sx<sy z<s) (sx<sy (sx<sy z<s)) (` 1) (` 3)

weakenˡ : ∀ {m m′ n} → m′ ≤ m → Tree m n → Tree m′ n
weakenˡ m′≤m (empty m≤n) = empty (≤-trans m′≤m m≤n)
weakenˡ m′≤m (node x m≤x x<n l r) = node x (≤-trans m′≤m m≤x) x<n (weakenˡ m′≤m l) r

weakenʳ : ∀ {m n n′} → n ≤ n′ → Tree m n → Tree m n′
weakenʳ n<n′ (empty m≤n) = empty (≤-trans m≤n n<n′)
weakenʳ {m} {n} {n′} n≤n′ (node x m≤x x<n l r) = node x m≤x x<n′ l (weakenʳ n≤n′ r)
  where
    x<n′ : x < n′
    x<n′ with ≤⇒<∨= n≤n′
    ... | inj₁ n<n′ = <-trans x<n n<n′
    ... | inj₂ n=n′ = subst n=n′ x<n

insertˡ : ∀ {m n} x → x < m → Tree m n → Tree x n
insertˡ {m} {n} x x<m tree = node x ≤-refl x<n (empty ≤-refl) (weakenˡ (sx<sy x<m) tree)
  where
    x<n : x < n
    x<n = <-≤-trans x<m (tree-≤ tree)

insertʳ : ∀ {m n} x → x ≥ n → Tree m n → Tree m (suc x)
insertʳ x x≥n tree = node x (≤-trans (tree-≤ tree) x≥n) x<sx (weakenʳ x≥n tree) (empty ≤-refl)

insert-m : ∀ {m n} x → x ≥ m → x < n → Tree m n → Tree m n
insert-m x x≥m x<n (empty _) = {!!}
insert-m x x≥m x<n (node y m≤y y<n l r)
  with x <?> y
... | le x<y = node y m≤y y<n (insert-m x x≥m x<y l) r
... | eq x=y = node y m≤y y<n l r
... | gt x>y = node y m≤y y<n l (insert-m x (sx<sy x>y) x<n r)

insert : ∀ {m n} x → Tree m n → Tree (min m x) (max n (suc x))
insert {m} {n} x tree
  with x <?> m | min m x
... | le x<m | minx = {!!}
... | eq x=m | minx = {!!}
... | gt x>m | minx = {!!}
  -- with x <?> n
-- ... | le x<n = {!!}
-- ... | eq x=n = {!!}
-- ... | gt x>n = {!!}

module Sample2 where
  t-123 : Tree 1 4
  t-123 = insertˡ 1 1<2 (insertˡ 2 2<3 (` 3))
    where
      1<2 = sx<sy z<s
      2<3 = sx<sy (sx<sy z<s)


toList : ∀ {m n} → Tree m n → L.List
toList (empty _) = L.[]
toList (node x m<x x<n l r) = toList l L.++ (x L.∷ toList r)

toList-≥ : ∀ {m n} (tree : Tree m n) {x} → x < m → x L.<∈ toList tree
toList-≥ (empty _) x<m = L.[]
toList-≥ (node y m≤y y<n l r) {x} x<m = L.++-all x<l (x<y L.∷ x<r)
  where
    x<l = toList-≥ l {x} x<m
    x<r = toList-≥ r {x} (<-trans x<m m≤y)
    x<y : x < y
    x<y with ≤⇒<∨= m≤y
    ... | inj₁ m<y = <-trans x<m m<y
    ... | inj₂ m=y = subst m=y x<m

toList-< : ∀ {m n} (tree : Tree m n) {x} → x ≥ n → x L.>∈ toList tree
toList-< (empty _) x≥n = L.[]
toList-< (node y m≤y y<n l r) {x} x≥n = L.++-all x>l (x>y L.∷ x>r)
  where
    x>l = toList-< l {x} (<-trans y<n x≥n)
    x>r = toList-< r {x} x≥n
    x>y = <-≤-trans y<n x≥n

toList-sorted : ∀ {m n} (tree : Tree m n) → L.Sorted (toList tree)
toList-sorted (empty _) = L.[]
toList-sorted (node x m≤x x<n l r) =
  L.++-sorted-bounded x>l (≤-refl L.∷ L.all-subst ≤-weaken x<r) l-sorted (L.s-insert-lower x x<r r-sorted)
  where
    x>l : x L.>∈ toList l
    x>l = toList-< l ≤-refl
    x<r : x L.<∈ toList r
    x<r = toList-≥ r x<sx
    l-sorted = toList-sorted l
    r-sorted = toList-sorted r
