(* week-11_demand-driven-computation.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 06 Apr 2025 *)

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

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith Bool.

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

CoInductive lazy_option (V : Type) : Type :=
  LSome : V -> lazy_option V
| LNone : lazy_option V.

(* ***** *)

CoInductive lazy_nat : Type :=
  LO : lazy_nat
| LS : lazy_nat -> lazy_nat.

CoFixpoint lazy_add (ln1 ln2 : lazy_nat) : lazy_nat :=
  match ln1 with
    LO =>
    ln2
  | LS ln1' =>
    LS (lazy_add ln1' ln2)
  end.

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

CoInductive lazy_binary_tree (V : Type) : Type :=
  LLeaf : V -> lazy_binary_tree V
| LNode : lazy_binary_tree V -> lazy_binary_tree V -> lazy_binary_tree V.

CoFixpoint lazy_mirror (V : Type) (lt : lazy_binary_tree V) : lazy_binary_tree V :=
  match lt with
    LLeaf _ v =>
    LLeaf V v
  | LNode _ lt1 lt2 =>
    LNode V (lazy_mirror V lt2) (lazy_mirror V lt1)
  end.

(* Unguarded recursive call: 
CoFixpoint lazy_number_of_nodes (V : Type) (lt : lazy_binary_tree V) : lazy_nat :=
  match lt with
    LLeaf _ _ =>
    LO
  | LNode _ lt1 lt2 =>
    LS (lazy_add (lazy_number_of_nodes V lt1) (lazy_number_of_nodes V lt2))
  end.
*)

(* Nested recursive occurrences:
CoFixpoint lazy_number_of_nodes_aux (V : Type) (lt : lazy_binary_tree V) (a : lazy_nat) : lazy_nat :=
  match lt with
    LLeaf _ _ =>
    a
  | LNode _ lt1 lt2 =>
    LS (lazy_number_of_nodes_aux V lt1 (LS (lazy_number_of_nodes_aux V lt2 a)))
  end.

Definition lazy_number_of_nodes (V : Type) (lt : lazy_binary_tree V) : lazy_nat :=
  lazy_number_of_nodes_aux V lt LO.
*)

(* Unguarded recursive call:
CoFixpoint lazy_number_of_nodes (V : Type) (lt : lazy_binary_tree V) : lazy_nat :=
  match lt with
    LLeaf _ _ =>
    LO
  | LNode _ lt1 lt2 =>
    LS (lazy_add (LS (lazy_number_of_nodes V lt1)) (LS (lazy_number_of_nodes V lt2)))
  end.
*)

(* Nested recursive occurrences:
CoFixpoint lazy_number_of_nodes (V : Type) (lt : lazy_binary_tree V) : lazy_nat :=
  match lt with
    LLeaf _ _ =>
    LO
  | LNode _ lt1 lt2 =>
    LS (lazy_add' (LS (lazy_number_of_nodes V lt1)) (LS (lazy_number_of_nodes V lt2)))
  end
with lazy_add' (ln1 ln2 : lazy_nat) : lazy_nat :=
  match ln1 with
    LO =>
    ln2
  | LS ln1' =>
    LS (lazy_add' ln1' ln2)
  end.
*)

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

(* end of week-11_demand-driven-computation.v *)