From Tealeaves Require
  Examples.VariadicLet.Terms
  Examples.VariadicLet.Instances.Simple
  Examples.VariadicLet.Instances.Tele
  Examples.VariadicLet.Instances.LetRec.

Import Terms.

Parameters (x y z: atom).

Definition term1: term LN :=
  letin [tvar (Fr x)] (tvar (Bd 0)).
Definition term2: term LN :=
  letin [tvar (Bd 0)] (tvar (Bd 0)).
Definition term3: term LN :=
  letin [tvar (Fr x); tvar (Bd 0)] (tvar (Bd 0)).
Definition term4: term LN :=
  letin [tvar (Fr x); tvar (Bd 1)] (tvar (Bd 0)).
Definition term5: term LN :=
  letin [tvar (Fr x); tvar (Bd 0) ; tvar (Bd 1)] (tvar (Bd 2)).
Definition term6: term LN :=
  letin [tvar (Bd 1) ; tvar (Bd 2) ; tvar (Bd 3)] (tvar (Bd 2)).

Definition compute_which_are_closed `{mapdt: Mapdt nat term}: list bool :=
  map (LCb (Mapdt_U := mapdt))  [term1; term2; term3; term4; term5; term6].

Definition compute_column_of_table `{mapdt: Mapdt nat term}: list nat :=
  map (level (Mapdt_U := mapdt))  [term1; term2; term3; term4; term5; term6].

Section JAR_table.

  Compute compute_column_of_table (mapdt := Simple.Mapdt_term).
= [0; 1; 1; 2; 2; 4]
: list nat
  (* = [0; 1; 1; 2; 2; 4] *)
  Compute compute_column_of_table (mapdt := Tele.Mapdt_term).
= [0; 1; 0; 1; 0; 2]
: list nat
  (* = [0; 1; 0; 1; 0; 2] *)
  Compute compute_column_of_table (mapdt := LetRec.Mapdt_term).
= [0; 0; 0; 0; 0; 1]
: list nat
  (* = [0; 0; 0; 0; 0; 1] *)

End JAR_table.


Compute compute_which_are_closed (mapdt := Simple.Mapdt_term).
= [true; false; false; false; false; false]
: list bool
(* = [true; false; false; false; false; false] *)
Compute compute_which_are_closed (mapdt := Tele.Mapdt_term).
= [true; false; true; false; true; false]
: list bool
(* = [true; false; true; false; true; false] *)
Compute compute_which_are_closed (mapdt := LetRec.Mapdt_term).
= [true; true; true; true; true; false]
: list bool
(* = [true; true; true; true; true; false] *)

Module demo1.

  Import Simple.

  Goal LCnb 0 term1 = true.
LCnb 0 term1 = true reflexivity. Qed.

  Goal LCnb 0 term2 = false.
LCnb 0 term2 = false reflexivity. Qed.
  Goal LCnb 1 term2 = true.
LCnb 1 term2 = true reflexivity. Qed.

  Goal LCnb 0 term4 = false.
LCnb 0 term4 = false reflexivity. Qed.
  Goal LCnb 1 term4 = false.
LCnb 1 term4 = false reflexivity. Qed.

  Goal LCnb 0 term6 = false.
LCnb 0 term6 = false reflexivity. Qed.
  Goal LCnb 1 term6 = false.
LCnb 1 term6 = false reflexivity. Qed.
  Goal LCnb 2 term6 = false.
LCnb 2 term6 = false reflexivity. Qed.

  Example ex1: level term1 = 0 := ltac:(trivial).
  Example ex2: level term2 = 1 := ltac:(trivial).
  Example ex23: level term3 = 1 := ltac:(trivial).
  Example ex3: level term4 = 2 := ltac:(trivial).
  Example ex4: level term5 = 2 := ltac:(trivial).
  Example ex5: level term6 = 4 := ltac:(trivial).

End demo1.

Module demo2.

  Import Tele.

  Example ex1: level term1 = 0 := ltac:(trivial).
  Example ex2: level term2 = 1 := ltac:(trivial).
  Example ex23: level term3 = 0 := ltac:(trivial).
  Example ex3: level term4 = 1 := ltac:(trivial).
  Example ex4: level term5 = 0 := ltac:(trivial).
  Example ex5: level term6 = 2 := ltac:(trivial).

End demo2.

Module demo3.

  Import LetRec.

  Goal LCnb 0 term1 = true.
LCnb 0 term1 = true reflexivity. Qed.
  Goal LCnb 0 term2 = true.
LCnb 0 term2 = true reflexivity. Qed.
  Goal LCnb 0 term4 = true.
LCnb 0 term4 = true reflexivity. Qed.

  Example ex1: level term1 = 0 := ltac:(trivial).
  Example ex2: level term2 = 0 := ltac:(trivial).
  Example ex23: level term3 = 0 := ltac:(trivial).
  Example ex3: level term4 = 0 := ltac:(trivial).
  Example ex4: level term5 = 0 := ltac:(trivial).
  Example ex5: level term6 = 1 := ltac:(trivial).
End demo3.