Merge branch 'main' into pr-merge-main

README.md

@@ -2,7 +2,7 @@
 
 In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After
 the accomplishment of this project, we will obtain an executable, to which we can feed
-a program in Martin-Loef type theory, and this executable will check whether this
+a program in Martin-Löf type theory, and this executable will check whether this
 program has the specified type. McLTT is novel in that it is implemented in
 Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is
 sound and complete: a program passes typechecking if and only if it is a well-typed

driver/Main.ml

@@ -4,12 +4,21 @@ open Parser
 open MenhirLibParser.Inter
 open Entrypoint
 
+let get_exit_code result : int =
+  match result with
+  | AllGood _ -> 0
+  (* 1 and 2 have special meanings in Bash-like shells *)
+  | TypeCheckingFailure _ -> 3
+  | ElaborationFailure _ -> 4
+  | ParserFailure _ -> 5
+  | ParserTimeout _ -> 6
+
 let main_of_lexbuf lexbuf =
   Lexer.lexbuf_to_token_buffer lexbuf
   (* Here, the integer argument is a *log* version of fuel.
      Thus, 500 means 2^500. *)
   |> Entrypoint.main 500
-  |> Format.printf "%a@." PrettyPrinter.format_main_result
+  |> fun r -> Format.printf "%a@." PrettyPrinter.format_main_result r; get_exit_code r
 
 let main_of_filename filename =
   Lexing.from_channel (open_in filename) |> main_of_lexbuf

driver/Main.mli

@@ -1,2 +1,2 @@
-val main_of_filename : string -> unit
-val main_of_program_string : string -> unit
+val main_of_filename : string -> int
+val main_of_program_string : string -> int

driver/Mcltt.ml

@@ -5,7 +5,8 @@ let () =
   then begin
     Printf.fprintf stderr
       "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
-    exit 1
+    exit 7
   end;
   let filename = Sys.argv.(1) in
-  main_of_filename filename
+  let code = main_of_filename filename in
+  exit code

driver/Test.ml

@@ -11,7 +11,7 @@ let main_of_example s = main_of_filename ("../examples/" ^ s)
 (* We never expect parser timeout. 2^500 fuel should be large enough! *)
 
 let%expect_test "Type@0 is of Type@1" =
-  main_of_program_string "Type@0 : Type@1";
+  let _ = main_of_program_string "Type@0 : Type@1" in
   [%expect
     {|
     Parsed:
@@ -23,7 +23,7 @@ let%expect_test "Type@0 is of Type@1" =
   |}]
 
 let%expect_test "zero is of Nat" =
-  main_of_program_string "zero : Nat";
+  let _ = main_of_program_string "zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -35,7 +35,7 @@ let%expect_test "zero is of Nat" =
   |}]
 
 let%expect_test "zero is not of Type@0" =
-  main_of_program_string "zero : Type@0";
+  let _ = main_of_program_string "zero : Type@0" in
   [%expect
     {|
     Type Checking Failure:
@@ -45,7 +45,7 @@ let%expect_test "zero is not of Type@0" =
   |}]
 
 let%expect_test "succ zero is of Nat" =
-  main_of_program_string "succ zero : Nat";
+  let _ = main_of_program_string "succ zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -57,7 +57,7 @@ let%expect_test "succ zero is of Nat" =
   |}]
 
 let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
-  main_of_program_string "succ Type@0 : Nat";
+  let _ = main_of_program_string "succ Type@0 : Nat" in
   [%expect
     {|
     Type Checking Failure:
@@ -67,15 +67,15 @@ let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
   |}]
 
 let%expect_test "variable x is ill-scoped" =
-  main_of_program_string "x : Type@0";
+  let _ = main_of_program_string "x : Type@0" in
   [%expect {|
     Elaboration Failure:
       x
     cannot be elaborated
   |}]
 
 let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
-  main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat";
+  let _ = main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat" in
   [%expect
     {|
     Parsed:
@@ -88,8 +88,8 @@ let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
 
 let%expect_test "recursion on a natural number that always returns zero is of \
                  Nat" =
-  main_of_program_string
-    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat";
+  let _ = main_of_program_string
+    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat" in
   [%expect
     {|
     Parsed:
@@ -101,7 +101,7 @@ let%expect_test "recursion on a natural number that always returns zero is of \
   |}]
 
 let%expect_test "simple_nat.mcl works" =
-  main_of_example "simple_nat.mcl";
+  let _ = main_of_example "simple_nat.mcl" in
   [%expect
     {|
     Parsed:
@@ -113,7 +113,7 @@ let%expect_test "simple_nat.mcl works" =
   |}]
 
 let%expect_test "simple_rec.mcl works" =
-  main_of_example "simple_rec.mcl";
+  let _ = main_of_example "simple_rec.mcl" in
   [%expect
     {|
     Parsed:
@@ -131,7 +131,7 @@ let%expect_test "simple_rec.mcl works" =
   |}]
 
 let%expect_test "pair.mcl works" =
-  main_of_example "pair.mcl";
+  let _ = main_of_example "pair.mcl" in
   [%expect
     {|
     Parsed:
@@ -257,7 +257,7 @@ let%expect_test "pair.mcl works" =
   |}]
 
 let%expect_test "vector.mcl works" =
-  main_of_example "vector.mcl";
+  let _ = main_of_example "vector.mcl" in
   [%expect
     {|
     Parsed:
@@ -465,7 +465,7 @@ let%expect_test "vector.mcl works" =
   |}]
 
 let%expect_test "nary.mcl works" =
-  main_of_example "nary.mcl";
+  let _ = main_of_example "nary.mcl" in
   [%expect
     {|
     Parsed:

driver/dune

@@ -23,3 +23,5 @@
    (:standard -w -67 -w -32 -w -33 -w -39))))
 
 (ocamllex Lexer)
+
+(documentation)

driver/extracted/dune

@@ -1,3 +1,5 @@
 (library
  (name MclttExtracted)
  (public_name mcltt.extracted))
+
+(documentation)

theories/Core/Completeness/Consequences/Types.v

@@ -84,152 +84,3 @@ Qed.
 
 #[export]
 Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mcltt.
-
-(* We cannot use this spec as the definition of [typ_subsumption] as
-   then its transitivity requires [exp_eq_typ_implies_eq_level] or a similar semantic lemma *)
-
-(* Lemma typ_subsumption_spec : forall {Γ A A'}, *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H. *)
-(*   dependent induction H; split; mauto 3. *)
-(*   - (* typ_subsumption_typ *) *)
-(*     eexists. *)
-(*     right. *)
-(*     do 2 eexists. *)
-(*     repeat split; revgoals; mauto. *)
-(*   - (* typ_subsumption_trans *) *)
-(*     destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]]; *)
-(*       destruct_conjs; *)
-(*       only 1: mautosolve 4; *)
-(*       eexists; right; do 2 eexists. *)
-(*     + (* left & right *) *)
-(*       split; [eassumption |]. *)
-(*       solve [mauto using lift_exp_eq_max_left]. *)
-(*     + (* right & left *) *)
-(*       split; [eassumption |]. *)
-(*       solve [mauto using lift_exp_eq_max_right]. *)
-(*     + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto). *)
-(*       replace i2 with i1' in * by mauto. *)
-(*       split; [etransitivity; revgoals; eassumption |]. *)
-(*       mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_spec : mcltt. *)
-
-(* Lemma not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A -> *)
-(*     (forall i, A <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : mcltt. *)
-
-(* Lemma not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A' -> *)
-(*     (forall i, A' <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : mcltt. *)
-
-(* Corollary typ_subsumption_left_nat : forall {Γ A'}, *)
-(*     {{ Γ ⊢ ℕ ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_nat : mcltt. *)
-
-(* Corollary typ_subsumption_left_pi : forall {Γ A B C'}, *)
-(*     {{ Γ ⊢ Π A B ⊆ C' }} -> *)
-(*     exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_pi : mcltt. *)
-
-(* Corollary typ_subsumption_left_typ : forall {Γ i A'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ A' }} -> *)
-(*     exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_typ : mcltt. *)
-
-(* Corollary typ_subsumption_right_nat : forall {Γ A}, *)
-(*     {{ Γ ⊢ A ⊆ ℕ }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ ℕ : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_nat : mcltt. *)
-
-(* Corollary typ_subsumption_right_pi : forall {Γ C A' B'}, *)
-(*     {{ Γ ⊢ C ⊆ Π A' B' }} -> *)
-(*     exists j, {{ Γ ⊢ C ≈ Π A' B' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_pi : mcltt. *)
-
-(* Corollary typ_subsumption_right_typ : forall {Γ A i'}, *)
-(*     {{ Γ ⊢ A ⊆ Type@i' }} -> *)
-(*     exists j i, i <= i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_typ : mcltt. *)
-
-(* Corollary typ_subsumption_typ_spec : forall {Γ i i'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ Type@i' }} -> *)
-(*     {{ ⊢ Γ }} /\ i <= i'. *)
-(* Proof with mautosolve. *)
-(*   intros * H. *)
-(*   pose proof (typ_subsumption_left_typ H). *)
-(*   destruct_conjs. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst... *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_typ_spec : mcltt. *)

theories/Core/Completeness/FunctionCases.v

@@ -70,7 +70,7 @@ Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
     (forall c c',
         R c c' ->
         rel_exp B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (per_univ i)) ->
-    (* We use this equality to make unification on `out_rel` works *)
+    (** We use the next equality to make unification on `out_rel` works *)
     (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
                  forall R',
                    rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R' ->
@@ -108,8 +108,7 @@ Proof with mautosolve.
   - intros.
     eapply rel_exp_pi_core; eauto.
     reflexivity.
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
 Qed.
 
 #[export]
@@ -140,8 +139,7 @@ Proof with mautosolve.
   - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
     extract_output_info_with ρσ c ρ'σ' c' env_relΔA...
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
 Qed.
 
 #[export]

theories/Core/Completeness/SubtypingCases.v

@@ -99,7 +99,7 @@ Proof.
   assert (forall c c', head_rel ρ ρ' equiv_ρ_ρ' c c' -> env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as HΓA'
       by (intros; apply_relation_equivalence; unshelve eexists; eassumption).
 
-  (* The proofs for the next two assertions are basically the same *)
+  (** The proofs for the next two assertions are basically the same *)
   exvar (relation domain)
     ltac:(fun R => assert ({{ DF Π m0 ρ B ≈ Π m1 ρ' B ∈ per_univ_elem (Nat.max i k) ↘ R }})).
   {