(* week-02_polymorphism.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@compnus.edu.sg> *)
(* Version of 16 Feb 2025, with uniformly formatted unit-test functions *)
(* was: *)
(* Version of 02 Feb 2025, with some examples of optional values *)
(* was: *)
(* Version of 24 Jan 2025 *)

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

Require Import Arith Bool.

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

Definition make_pair_v0 : forall (A : Type) (B : Type), A -> B -> A * B :=
  fun A B a b => (a, b).

Definition make_pair_v1 (A : Type) : forall B : Type, A -> B -> A * B :=
  fun B a b => (a, b).

Definition make_pair_v2 (A : Type) (B : Type) : A -> B -> A * B :=
  fun a b => (a, b).

Definition make_pair_v3 (A : Type) (B : Type) (a : A) : B -> A * B :=
  fun b => (a, b).

Definition make_pair_v4 (A : Type) (B : Type) (a : A) (b : B) : A * B :=
  (a, b).

(* ***** *)

Compute (make_pair_v4 nat bool 1 true).
(* = (1, true) : nat * bool *)

Definition dupl (V : Type) (v : V) : V * V :=
  make_pair_v4 V V v v.

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

Inductive polymorphic_binary_tree (V : Type) : Type :=
  PLeaf : V -> polymorphic_binary_tree V
| PNode : polymorphic_binary_tree V -> polymorphic_binary_tree V -> polymorphic_binary_tree V.

Definition test_number_of_leaves (candidate : forall V : Type, polymorphic_binary_tree V -> nat) : bool :=
  true
    &&
    (candidate bool (PLeaf bool true) =? 1)
    &&
    (candidate nat (PNode nat (PLeaf nat 0) (PLeaf nat 1)) =? 2).

Fixpoint number_of_leaves (V : Type) (t : polymorphic_binary_tree V) : nat :=
  match t with
    PLeaf _ v =>
    1
  | PNode _ t1 t2 =>
    number_of_leaves V t1 + number_of_leaves V t2
  end.

Compute (test_number_of_leaves number_of_leaves).

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

Definition test_eqb_polymorphic_binary_tree_easily_defeated (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
  true
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PLeaf nat 0))
       true)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PNode 
             nat
             (PLeaf nat 0)
             (PLeaf nat 0))
          (PNode 
             nat
             (PLeaf nat 0)
             (PLeaf nat 0)))
       true).

Compute (test_eqb_polymorphic_binary_tree_easily_defeated
           (fun (V : Type)
                (eqb_V : V -> V -> bool)
                (t1 t2 : polymorphic_binary_tree V) =>
              true)).

Definition test_eqb_polymorphic_binary_tree_without_code_coverage (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
  true
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PLeaf nat 0))
       true)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PLeaf nat 1))
       false)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PNode 
             nat
             (PLeaf nat 0)
             (PLeaf nat 0))
          (PNode 
             nat
             (PLeaf nat 0)
             (PLeaf nat 0)))
       true).

Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
  true
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PLeaf nat 0))
       true)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PLeaf nat 1))
       false)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PLeaf nat 0)
          (PNode 
             nat
             (PLeaf nat 1)
             (PLeaf nat 2)))
       false)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PNode 
             nat
             (PLeaf nat 1)
             (PLeaf nat 2))
          (PLeaf nat 0))
       false)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PNode 
             nat
             (PLeaf nat 1)
             (PLeaf nat 2))
          (PNode 
             nat
             (PLeaf nat 1)
             (PLeaf nat 2)))
       true)
    &&
    (Bool.eqb
       (candidate
          nat
          Nat.eqb
          (PNode 
             nat
             (PLeaf nat 2)
             (PLeaf nat 1))
          (PNode 
             nat
             (PLeaf nat 1)
             (PLeaf nat 2)))
       false).

Fixpoint eqb_polymorphic_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
  match t1 with
    PLeaf _ v1 =>
    match t2 with
     PLeaf _ v2 =>
      eqb_V v1 v2
    | PNode _ t11 t12 =>
      false
    end
  | PNode _ t11 t12 =>
    match t2 with
      PLeaf _ v2 =>
      false
    | PNode _ t21 t22 =>
      eqb_polymorphic_binary_tree V eqb_V t11 t21
      &&
      eqb_polymorphic_binary_tree V eqb_V t12 t22
    end
  end.

Compute (test_eqb_polymorphic_binary_tree eqb_polymorphic_binary_tree).

Fixpoint eqb_polymorphic_binary_tree' (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
  match (t1, t2) with
    (PLeaf _ v1, PLeaf _ v2) =>
    eqb_V v1 v2
  | (PNode _ t11 t12, PNode _ t21 t22) =>
    eqb_polymorphic_binary_tree' V eqb_V t11 t21
    &&
    eqb_polymorphic_binary_tree' V eqb_V t12 t22
  | _ =>
    false
  end.

Compute (test_eqb_polymorphic_binary_tree eqb_polymorphic_binary_tree').

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

Definition eqb_nat := Nat.eqb.

Definition eqb_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree nat) : bool :=
  eqb_polymorphic_binary_tree nat eqb_nat t1 t2.

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

Definition eqb_bool := Bool.eqb.

Definition eqb_binary_tree_of_bools (t1 t2 : polymorphic_binary_tree bool) : bool :=
  eqb_polymorphic_binary_tree bool eqb_bool t1 t2.

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

Check (Some 2).

Check (Some (1, false)).

Check (Some (Some false)).

Check (fun (on : option nat) => match on with Some n => true | None => false end).

(* ***** *)

(* Exercise 07 *)

Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
  match ov1 with
    Some v1 =>
    match ov2 with
     | Some v2 =>
      eqb_V v1 v2
    | None =>
      false
    end
  | None =>
    match ov2 with
      Some v =>
      false
    | None =>
      true
    end
  end.

Check (eqb_polymorphic_binary_tree nat).
Check (eqb_polymorphic_binary_tree (option nat)).
Check (eqb_option (polymorphic_binary_tree nat)).

(*
Definition eqb_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option nat)) : bool :=
*)

(*
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
*)

(*
Definition eqb_optional_binary_tree_of_optional_nats (t1 t2 : option (polymorphic_binary_tree (option nat))) : bool :=
*)

(*
Definition eqb_binary_tree_of_optional_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree nat))) : bool :=
*)

(*
Definition eqb_binary_tree_of_optional_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree (option nat)))) : bool :=
*)

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

(* Implicit parameters: *)

Inductive option' (V : Type) : Type :=
  Some' : V -> option' V
| None' : option' V.

Print option'.

Set Implicit Arguments.

Inductive option'' (V : Type) : Type :=
| Some'' : V -> option'' V
| None'' : option'' V.

Print option''.

Check (Some 10, Some true).
Check (Some' nat 10, Some' bool true).
Check (Some'' 10, Some'' true).

Check None.
Check None'.
Check None''.
Check (@None nat).
Check (@None' nat).
Check (@None'' nat).

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

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