------------------------------------------------------------------------
-- The Agda standard library
--
-- Binary Trees
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Tree.Binary where

open import Level using (Level; _⊔_)
open import Data.List.Base using (List)
open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _∷ʳ_; _++_; [_])
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Function.Base

private
  variable
    n l n₁ l₁ a : Level
    N : Set n
    L : Set l
    N₁ : Set n₁
    L₁ : Set l₁
    A : Set a

-- Trees with node values of type N and leaf values of type L
data Tree (N : Set n) (L : Set l) : Set (n ⊔ l) where
  leaf : L → Tree N L
  node : Tree N L → N → Tree N L → Tree N L

map : (N → N₁) → (L → L₁) → Tree N L → Tree N₁ L₁
map f g (leaf x)     = leaf (g x)
map f g (node l m r) = node (map f g l) (f m) (map f g r)

mapₙ : (N → N₁) → Tree N L → Tree N₁ L
mapₙ f t = map f id t

mapₗ : (L → L₁) → Tree N L → Tree N L₁
mapₗ f t = map id f t

#nodes : Tree N L → ℕ
#nodes (leaf x)     = 0
#nodes (node l m r) = #nodes l + suc (#nodes r)

#leaves : Tree N L → ℕ
#leaves (leaf x)     = 1
#leaves (node l m r) = #leaves l + #leaves r

foldr : (A → N → A → A) → (L → A) → Tree N L → A
foldr f g (leaf x)     = g x
foldr f g (node l m r) = f (foldr f g l) m (foldr f g r)

------------------------------------------------------------------------
-- Extraction to lists, depth first and left to right.

module Prefix where

  toDiffList : Tree N L → DiffList N
  toDiffList = foldr (λ l m r → m ∷ l ++ r) (λ _ → [])

  toList : Tree N L → List N
  toList = DiffList.toList ∘′ toDiffList

module Infix where

  toDiffList : Tree N L → DiffList N
  toDiffList = foldr (λ l m r → l ++ m ∷ r) (λ _ → [])

  toList : Tree N L → List N
  toList = DiffList.toList ∘′ toDiffList

module Suffix where

  toDiffList : Tree N L → DiffList N
  toDiffList = foldr (λ l m r → l ++ r ∷ʳ m) (λ _ → [])

  toList : Tree N L → List N
  toList = DiffList.toList ∘′ toDiffList

module Leaves where

  toDiffList : Tree N L → DiffList L
  toDiffList (leaf x)     = [ x ]
  toDiffList (node l m r) = toDiffList l ++ toDiffList r

  toList : Tree N L → List L
  toList = DiffList.toList ∘′ toDiffList