51 lines
1.6 KiB
Coq
51 lines
1.6 KiB
Coq
Require Import Utf8.
|
|
Require Import List.
|
|
|
|
Unset Elimination Schemes.
|
|
|
|
(* Rose tree, with numbers on nodes *)
|
|
Inductive tree := Tree { value : nat ; children : list tree }.
|
|
|
|
Fixpoint height (t: tree) : nat :=
|
|
1 + fold_left (? n t, max n (height t)) (children t) 0.
|
|
|
|
Example leaf n : tree := {| value := n ; children := nil |}.
|
|
|
|
Example t2 : tree := {| value := 2 ; children := {| value := 4 ; children := leaf 7 :: nil |} :: leaf 5 :: nil |}.
|
|
|
|
Example t3 : tree := {| value := 3 ; children := {| value := 6 ; children := leaf 8 :: leaf 9 :: nil |} :: nil |}.
|
|
|
|
Example t9 : tree := {| value := 1 ; children := t2 :: t3 :: nil |}.
|
|
|
|
Fixpoint preorder (t: tree) : list nat :=
|
|
let '{| value := n ; children := c |} := t in
|
|
n :: flat_map preorder c.
|
|
|
|
Fixpoint inorder (t: tree) : list nat :=
|
|
let '{| value := n ; children := c |} := t in
|
|
match c with
|
|
| nil => n :: nil
|
|
| l :: r => inorder l ++ n :: flat_map inorder r
|
|
end.
|
|
|
|
Fixpoint postorder (t: tree) : list nat :=
|
|
let '{| value := n ; children := c |} := t in
|
|
flat_map postorder c ++ n :: nil.
|
|
|
|
(* Auxiliary function for levelorder, which operates on forests *)
|
|
(* Since the recursion is tricky, it relies on a fuel parameter which obviously decreases. *)
|
|
Fixpoint levelorder_forest (fuel: nat) (f: list tree) : list nat:=
|
|
match fuel with
|
|
| O => nil
|
|
| S fuel' =>
|
|
let '(p, f) := fold_right (? t r, let '(x, f) := r in (value t :: x, children t ++ f) ) (nil, nil) f in
|
|
p ++ levelorder_forest fuel' f
|
|
end.
|
|
|
|
Definition levelorder (t: tree) : list nat :=
|
|
levelorder_forest (height t) (t :: nil).
|
|
|
|
Compute preorder t9.
|
|
Compute inorder t9.
|
|
Compute postorder t9.
|
|
Compute levelorder t9.
|