Require Import PeanoNat.
Require Import List.

(* Print list. *)
(* Shows definition for the <list> type *)
(* nil = null list *)
(* cons 0 nil = constructs a new list with elements 0 and nil *)
(* 2::1::0    = constructs a new list with elements 2 1 and 0 *)
(* cons = :: -> constructs new list *)
(* app = ++ -> appends to list*)

Inductive btree :=
| empty : btree
| node  : btree->nat->btree->btree.

Fixpoint searchBT (t:btree) (value:nat) : bool :=
match t with
| empty       => false
| node l v r  =>
    if v =? value then
      true
    else
      orb (searchBT l value) (searchBT r value)
end.

(* Ex 1 *)
Fixpoint inOrdineBT (t:btree) : list nat :=
match t with
| empty       => nil
| node l v r  => (inOrdineBT l) ++v:: (inOrdineBT r)
end.

(*
Definition Zero := (node empty 0 empty).
Definition One := (node empty 1 empty).
Definition Two := (node Zero 2 One).

Compute inOrdineBT Two.
*)

(* Ex 2 *)
Fixpoint siblings (t:btree) (val:nat) : btree :=
match t with
| empty       => empty
| node l v r  =>
  match l with
  | empty         => siblings r val
  | node ll lv lr =>
    if lv =? val then r
    else
      match r with
      | empty         => siblings l val
      | node rl rv rr =>
        if rv =? val then l
        else
          empty
      end
  end
end.

Fixpoint parent (t:btree) (val:nat) : btree :=
match t with
| empty       => empty
| node l v r  =>
  match l, r with
  | node ll lv lr, node rl rv rr =>
    if orb (lv =? val) (rv =? val) then t
    else
      match (parent l val) with
      | empty => (parent r val)
      | _     => (parent l val)
      end
  | _, _                         =>
    match (parent l val) with
      | empty => (parent r val)
      | _     => (parent l val)
    end
  end
end.

Fixpoint degree (t:btree) (val:nat) : nat :=
match t with
| empty       => 0
| node l v r  =>
  if v =? val then
    match l, r with
    | empty, empty                  => 0
    | node ll lv lr, node rl rv rr  => 2
    | _, _                          => 1
    end
  else
    degree l val + degree r val
end.

Definition Zero := (node empty 0 empty).
Definition One := (node empty 1 empty).
Definition Two := (node Zero 2 One).

Compute parent Two 0.
Compute parent Two 1.
Compute parent Two 2.

Compute degree Two 0.
Compute degree Two 1.
Compute degree Two 2.

Compute siblings Two 0.
Compute siblings Two 1.
Compute siblings Two 2.