(* week-02_accumulators.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 24 Jan 2025 *)

(* ********** *)

Require Import Arith Bool.

(* ********** *)

Fixpoint copy_nat (n : nat) :  nat :=
  match n with
    O =>
    O
  | S n' =>
    S (copy_nat n')
  end.

Fixpoint power (x n : nat) : nat :=
  match n with
    O =>
    1
  | S n' =>
    x * (power x n')
  end.

(* ********** *)

Fixpoint copy_nat_acc (n a : nat) : nat :=
  match n with
    O =>
    a
  | S n' =>
    copy_nat_acc n' (S a)
  end.

Definition copy_nat_alt (n : nat) : nat :=
  copy_nat_acc n 0.

Fixpoint power_acc (x n a : nat) : nat :=
  match n with
    O =>
    a
  | S n' =>
    power_acc x n' (x * a)
  end.

Definition power_alt (x n : nat) : nat :=
  power_acc x n 1.

(* ********** *)

Fixpoint fac (n : nat) : nat :=
  match n with
    O =>
    1
  | S n' =>
    S n' * fac n'
  end.

Fixpoint fac_acc (n a : nat) : nat :=
  match n with
    O =>
    a
  | S n' =>
    fac_acc n' (S n' * a)
  end.

Definition fac_alt (n : nat) : nat :=
  fac_acc n 1.

(* ********** *)

Inductive binary_tree_nat : Type :=
  L : nat -> binary_tree_nat
| N : binary_tree_nat -> binary_tree_nat -> binary_tree_nat.

(* ***** *)

Fixpoint height (t : binary_tree_nat) : nat :=
  match t with
    L n =>
    0
  | N t1 t2 =>
    S (max (height t1) (height t2))
  end.

Compute (height (N (N (L 1) (L 2)) (N (L 3) (L 4))) =? 2).

Compute (height (N (N (L 0) (N (L 1) (L 2))) (N (N (L 3) (L 4)) (N (N (L 5) (L 6)) (L 7)))) =? 4).

Compute (height (N (L 0) (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))))) =? 6).

Fixpoint height_acc (t : binary_tree_nat) (a : nat) : nat :=
  match t with
    L n =>
    a
  | N t1 t2 =>
    max (height_acc t1 (S a)) (height_acc t2 (S a))
  end.

Definition height_alt (t : binary_tree_nat) : nat :=
  height_acc t 0.

Compute (height_alt (N (L 0) (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))))) =? 6).

Compute (height_alt (N (L 0) (N (L 1) (N (L 2) (L 3)))) =? 3).

Compute (height (N (L 0) (L 1)), height_alt (N (L 0) (L 1))).

(* ***** *)

Fixpoint number_of_leaves (t : binary_tree_nat) : nat :=
  match t with
    L _ =>
    1
  | N t1 t2 =>
    number_of_leaves t1 + number_of_leaves t2
  end.

Fixpoint number_of_leaves_acc (t : binary_tree_nat) (a : nat) : nat :=
  match t with
    L _ =>
    S a
  | N t1 t2 =>
    number_of_leaves_acc t2 (number_of_leaves_acc t1 a)
  end.

Definition number_of_leaves_alt (t : binary_tree_nat) : nat :=
  number_of_leaves_acc t 0.

Compute (let t := N (N (L 0)
                       (N (L 1)
                          (L 2)))
                    (N (N (L 3)
                          (L 4))
                       (N (N (L 5)
                             (L 6))
                          (L 7)))
         in number_of_leaves t =? number_of_leaves_alt t).

(* ***** *)

Fixpoint number_of_nodes (t : binary_tree_nat) : nat :=
  match t with
    L _ =>
    0
  | N t1 t2 =>
    S (number_of_nodes t1 + number_of_nodes t2)
  end.

Fixpoint number_of_nodes_cps (t : binary_tree_nat) (k : nat -> nat) : nat :=
  match t with
    L _ =>
    k 0
  | N t1 t2 =>
    number_of_nodes_cps t1 (fun n1 =>
                              number_of_nodes_cps t2 (fun n2 =>
                                                        k (S (n1 + n2))))
  end.

Definition number_of_nodes_alt2 (t : binary_tree_nat) : nat :=
  number_of_nodes_cps t (fun n => n).

Compute (let t := N (N (L 0)
                       (N (L 1)
                          (L 2)))
                    (N (N (L 3)
                          (L 4))
                       (N (N (L 5)
                             (L 6))
                          (L 7)))
         in number_of_nodes t =? number_of_nodes_alt2 t).

(* ********** *)

(* end of week-02_accumulators.v *)