module Tree where

open import Data.List using (List; _∷_; []; [_]; _++_)

data Tree {a} (A : Set a) : Set a where
  Tip  :                       Tree A
  Node : Tree A → A → Tree A → Tree A

inorder : ∀ {a} {A : Set a} → Tree A → List A
inorder Tip          = []
inorder (Node l x r) = inorder l ++ [ x ] ++ inorder r

-- Proofs that some element in a tree satisfies a particular predicate P
data AnyTree {a ℓ} {A : Set a} (P : A → Set ℓ) : Tree A -> Set ℓ where
  OnLeft  : ∀ {l} (Pl : AnyTree P l) x r → AnyTree P (Node l x r)
  AtRoot  : ∀ l {x} (Px : P x) r         → AnyTree P (Node l x r)
  OnRight : ∀ l x {r} (Pr : AnyTree P r) → AnyTree P (Node l x r)

-- Correspondence between AnyTree and List's Any on inorder traversal of a tree
module _ {a ℓ} {A : Set a} {P : A → Set ℓ} where

  open import Data.List.Relation.Unary.Any            using (Any; here; there)
  open import Data.List.Relation.Unary.Any.Properties using (++⁺ˡ; ++⁺ʳ; ++⁻)
  open import Data.Sum                                using (inj₁; inj₂)

  treeToList : ∀ {t} → AnyTree P t → Any P (inorder t)
  treeToList (OnLeft  Pl x r) = ++⁺ˡ (treeToList Pl)
  treeToList (AtRoot  l Px r) = ++⁺ʳ (inorder l) (here Px)
  treeToList (OnRight l x Pr) = ++⁺ʳ (inorder l) (there (treeToList Pr))

  listToTree : ∀ {t} → Any P (inorder t) → AnyTree P t
  listToTree {Node l x r} Pt
   with ++⁻ (inorder l) Pt
  ... | inj₁ Pl         = OnLeft (listToTree Pl) x r
  ... | inj₂ (here  Px) = AtRoot l Px r
  ... | inj₂ (there Pr) = OnRight l x (listToTree Pr)

-- Instantiation of generic AnyTree to tree element membership
module _ {a} {A : Set a} where

  open import Data.List.Membership.Propositional    using (_∈_)
  open import Relation.Binary.PropositionalEquality using (_≡_)

  -- Proposition that element x is contained within tree t
  _∈ᵗ_ : A → Tree A → Set a
  x ∈ᵗ t = AnyTree (_≡_ x) t

  inTreeToInList : ∀ {x t} → x ∈ᵗ t → x ∈ inorder t
  inTreeToInList = treeToList

  inListToInTree : ∀ {x t} → x ∈ inorder t → x ∈ᵗ t
  inListToInTree = listToTree