Task

Implement a binary tree where each node carries an integer,   and implement:

   pre-order,
   in-order, 
   post-order,     and 
   level-order   traversal. 


Use those traversals to output the following tree:

         1
        / \
       /   \
      /     \
     2       3
    / \     /
   4   5   6
  /       / \
 7       8   9

The correct output should look like this:

preorder:    1 2 4 7 5 3 6 8 9
inorder:     7 4 2 5 1 8 6 9 3
postorder:   7 4 5 2 8 9 6 3 1
level-order: 1 2 3 4 5 6 7 8 9



See also

   Wikipedia article:   Tree traversal.


open import Data.List using (List; _∷_; []; concat)
open import Data.Nat using (ℕ; suc; zero)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
data Tree {a} (A : Set a) : Set a where
  leaf : Tree A
  node : A → Tree A → Tree A → Tree A
 
variable
  a : Level
  A : Set a
 
preorder : Tree A → List A
preorder tr = go tr []
  where
  go : Tree A → List A → List A
  go leaf           ys = ys
  go (node x ls rs) ys = x ∷ go ls (go rs ys)
 
inorder : Tree A → List A
inorder tr = go tr []
  where
  go : Tree A → List A → List A
  go leaf           ys = ys
  go (node x ls rs) ys = go ls (x ∷ go rs ys)
 
postorder : Tree A → List A
postorder tr = go tr []
  where
  go : Tree A → List A → List A
  go leaf           ys = ys
  go (node x ls rs) ys = go ls (go rs (x ∷ ys))
 
level-order : Tree A → List A
level-order tr = concat (go tr [])
  where
  go : Tree A → List (List A) → List (List A)
  go leaf qs                 = qs
  go (node x ls rs) []       = (x ∷ []) ∷ go ls (go rs [])
  go (node x ls rs) (q ∷ qs) = (x ∷ q ) ∷ go ls (go rs qs)
 
example-tree : Tree ℕ
example-tree =
  node 1
    (node 2
      (node 4
        (node 7
          leaf
          leaf)
        leaf)
      (node 5
        leaf
        leaf))
    (node 3
      (node 6
        (node 8
          leaf
          leaf)
        (node 9
          leaf
          leaf))
      leaf)
 
_ : preorder example-tree ≡ 1 ∷ 2 ∷ 4 ∷ 7 ∷ 5 ∷ 3 ∷ 6 ∷ 8 ∷ 9 ∷ []
_ = refl
 
_ : inorder example-tree ≡ 7 ∷ 4 ∷ 2 ∷ 5 ∷ 1 ∷ 8 ∷ 6 ∷ 9 ∷ 3 ∷ []
_ = refl
 
_ : postorder example-tree ≡ 7 ∷ 4 ∷ 5 ∷ 2 ∷ 8 ∷ 9 ∷ 6 ∷ 3 ∷ 1 ∷ []
_ = refl
 
_ : level-order example-tree ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ []
_ = refl