Change McLTT into McTT (#262)

.github/workflows/ci_build.yaml

@@ -30,7 +30,7 @@ jobs:
       contents: write
     env:
       REGISTRY: "ghcr.io"
-      IMAGE_TAG: "beluga-lang/mcltt:main"
+      IMAGE_TAG: "beluga-lang/mctt:main"
       # Only deploy if the build follows from pushing to one of main branches
       DOC_DEPLOY: ${{ (github.ref_name == 'main' || startsWith(github.ref_name, 'ext/')) && 'true' || 'false' }}
       DOC_DEPLOY_DEST: ${{ startsWith(github.ref_name, 'ext/') && github.ref_name || '' }}
@@ -73,8 +73,8 @@ jobs:
                 mv theories/dep.html html/dep.html
                 cp assets/styling.css html/styling.css
                 cp -r assets/images html/images
-                sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McLTT/dep\.html)![Coqdoc](dep.html)!' README.md
-                pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McLTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html
+                sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McTT/dep\.html)![Coqdoc](dep.html)!' README.md
+                pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html
               fi
             endGroup
             startGroup "Run inline tests"

README.md

@@ -76,11 +76,11 @@ possible.
 
 Once `make` finishes, you can run the binary:
 ```
-dune exec mcltt examples/nary.mcl # or your own example
+dune exec mctt examples/nary.mctt # or your own example
 ```
 or more directly
 ```
-_build/default/driver/mcltt.exe examples/nary.mcl # or your own example
+_build/default/driver/mctt.exe examples/nary.mctt # or your own example
 ```
 
 To build Coq proof only, you can go into and only build the `theories` directory:

assets/include.html

@@ -16,7 +16,7 @@
      var header = $(`<div id="header_wrap" class="outer">
         <header class="inner">
           
-            <a id="forkme_banner" href="https://github.com/Beluga-lang/McLTT">Fork on GitHub</a>
+            <a id="forkme_banner" href="https://github.com/Beluga-lang/McTT">Fork on GitHub</a>
           ${h1elem.outerHTML}
         </header>
     </div>`);

driver/Lexer.mli

@@ -1,7 +1,7 @@
 val format_position : Format.formatter -> Lexing.position -> unit
 val format_range : Format.formatter -> Lexing.position * Lexing.position -> unit
-val format_token : Format.formatter -> MclttExtracted.Parser.token -> unit
-val read : Lexing.lexbuf -> MclttExtracted.Parser.token
+val format_token : Format.formatter -> McttExtracted.Parser.token -> unit
+val read : Lexing.lexbuf -> McttExtracted.Parser.token
 
 val lexbuf_to_token_buffer :
-  Lexing.lexbuf -> MclttExtracted.Parser.MenhirLibParser.Inter.buffer
+  Lexing.lexbuf -> McttExtracted.Parser.MenhirLibParser.Inter.buffer

driver/Lexer.mll

@@ -1,6 +1,6 @@
 {
   open Lexing
-  open MclttExtracted.Parser
+  open McttExtracted.Parser
 
   let get_range lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p)
 

driver/Main.ml

@@ -1,5 +1,5 @@
-module Parser = MclttExtracted.Parser
-module Entrypoint = MclttExtracted.Entrypoint
+module Parser = McttExtracted.Parser
+module Entrypoint = McttExtracted.Entrypoint
 open Parser
 open MenhirLibParser.Inter
 open Entrypoint

driver/Mcltt.ml → driver/Mctt.ml

@@ -1,4 +1,4 @@
-open Mcltt.Main
+open Mctt.Main
 
 let () =
   if Array.length Sys.argv <> 2

driver/PrettyPrinter.ml

@@ -1,7 +1,7 @@
-open MclttExtracted.Entrypoint
-open MclttExtracted.Syntax
-module Parser = MclttExtracted.Parser
-module ParserMessages = MclttExtracted.ParserMessages
+open McttExtracted.Entrypoint
+open McttExtracted.Syntax
+module Parser = McttExtracted.Parser
+module ParserMessages = McttExtracted.ParserMessages
 
 (************************************************************)
 (* Formatting helpers *)

driver/PrettyPrinter.mli

@@ -1,6 +1,6 @@
-val format_obj : Format.formatter -> MclttExtracted.Syntax.Cst.obj -> unit
-val format_exp : Format.formatter -> MclttExtracted.Syntax.exp -> unit
-val format_nf : Format.formatter -> MclttExtracted.Syntax.nf -> unit
+val format_obj : Format.formatter -> McttExtracted.Syntax.Cst.obj -> unit
+val format_exp : Format.formatter -> McttExtracted.Syntax.exp -> unit
+val format_nf : Format.formatter -> McttExtracted.Syntax.nf -> unit
 
 val format_main_result :
-  Format.formatter -> MclttExtracted.Entrypoint.main_result -> unit
+  Format.formatter -> McttExtracted.Entrypoint.main_result -> unit

driver/Test.ml

@@ -1,7 +1,7 @@
 (* Unit test cases for parsing *)
 
 open Main
-open MclttExtracted.Entrypoint
+open McttExtracted.Entrypoint
 
 (** Helper definitions *)
 
@@ -100,8 +100,8 @@ let%expect_test "recursion on a natural number that always returns zero is of \
       0 : Nat
   |}]
 
-let%expect_test "simple_nat.mcl works" =
-  let _ = main_of_example "simple_nat.mcl" in
+let%expect_test "simple_nat.mctt works" =
+  let _ = main_of_example "simple_nat.mctt" in
   [%expect
     {|
     Parsed:
@@ -112,8 +112,8 @@ let%expect_test "simple_nat.mcl works" =
       4 : Nat
   |}]
 
-let%expect_test "simple_rec.mcl works" =
-  let _ = main_of_example "simple_rec.mcl" in
+let%expect_test "simple_rec.mctt works" =
+  let _ = main_of_example "simple_rec.mctt" in
   [%expect
     {|
     Parsed:
@@ -129,8 +129,8 @@ let%expect_test "simple_rec.mcl works" =
       : forall (x1 : Nat) -> Nat
   |}]
 
-let%expect_test "pair.mcl works" =
-  let _ = main_of_example "pair.mcl" in
+let%expect_test "pair.mctt works" =
+  let _ = main_of_example "pair.mctt" in
   [%expect
     {|
     Parsed:
@@ -255,8 +255,8 @@ let%expect_test "pair.mcl works" =
       5 : Nat
   |}]
 
-let%expect_test "vector.mcl works" =
-  let _ = main_of_example "vector.mcl" in
+let%expect_test "vector.mctt works" =
+  let _ = main_of_example "vector.mctt" in
   [%expect
     {|
     Parsed:
@@ -463,8 +463,8 @@ let%expect_test "vector.mcl works" =
       7 : Nat
   |}]
 
-let%expect_test "nary.mcl works" =
-  let _ = main_of_example "nary.mcl" in
+let%expect_test "nary.mctt works" =
+  let _ = main_of_example "nary.mctt" in
   [%expect
     {|
     Parsed:
@@ -553,8 +553,8 @@ let%expect_test "nary.mcl works" =
       6 : Nat
   |}]
 
-let%expect_test "simple_let.mcl works" =
-  let _ = main_of_example "simple_let.mcl" in
+let%expect_test "simple_let.mctt works" =
+  let _ = main_of_example "simple_let.mctt" in
   [%expect
     {| 
       Parsed:
@@ -565,8 +565,8 @@ let%expect_test "simple_let.mcl works" =
         1 : Nat      
   |}]
 
-let%expect_test "let_two_vars.mcl works" =
-  let _ = main_of_example "let_two_vars.mcl" in
+let%expect_test "let_two_vars.mctt works" =
+  let _ = main_of_example "let_two_vars.mctt" in
   [%expect
      {|
        Parsed:
@@ -584,8 +584,8 @@ let%expect_test "let_two_vars.mcl works" =
          0 : Nat
   |}]
 
-let%expect_test "let_nary.mcl works" =
-  let _ = main_of_example "let_nary.mcl" in
+let%expect_test "let_nary.mctt works" =
+  let _ = main_of_example "let_nary.mctt" in
   [%expect
      {|
        Parsed:
@@ -675,8 +675,8 @@ let%expect_test "let_nary.mcl works" =
   |}]
 
 
-let%expect_test "let_vector.mcl works" =
-  let _ = main_of_example "let_vector.mcl" in
+let%expect_test "let_vector.mctt works" =
+  let _ = main_of_example "let_vector.mctt" in
   [%expect
     {| 
       Parsed:

driver/dune

@@ -1,21 +1,21 @@
 (include_subdirs no)
 
 (library
- (name Mcltt)
- (public_name mcltt.driver)
+ (name Mctt)
+ (public_name mctt.driver)
  (modules Main Lexer PrettyPrinter Test)
- (libraries MclttExtracted)
+ (libraries McttExtracted)
  (inline_tests
   (deps
-   (glob_files_rec ../examples/*.mcl)))
+   (glob_files_rec ../examples/*.mctt)))
  (preprocess
   (pps ppx_expect)))
 
 (executable
- (name mcltt)
- (public_name mcltt)
- (modules Mcltt)
- (libraries Mcltt))
+ (name mctt)
+ (public_name mctt)
+ (modules Mctt)
+ (libraries Mctt))
 
 (env
  (dev

driver/extracted/dune

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

dune-project

@@ -1,6 +1,6 @@
 (lang dune 3.13)
 (using menhir 2.1)
-(name mcltt)
+(name mctt)
 
 (generate_opam_files)
 
@@ -9,20 +9,20 @@
          "Jason Hu"
          "Junyoung Jang")
 (maintainers "the CompLogic group, McGill University")
-(homepage "https://beluga-lang.github.io/McLTT/")
-(documentation "https://beluga-lang.github.io/McLTT/")
-(source (github Beluga-lang/McLTT))
+(homepage "https://beluga-lang.github.io/McTT/")
+(documentation "https://beluga-lang.github.io/McTT/")
+(source (github Beluga-lang/McTT))
 
 (package
- (name mcltt)
- (synopsis "A Bottom-up Approach to Implementing A Proof Assistant")
- (description "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
-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
-program in MLTT. This will be the first verified proof assistant (despite being
+ (name mctt)
+ (synopsis "A Correct-By-Construction Proof Checkers For Type Theories")
+ (description "McTT is a verified, runnable typechecker for Martin-Löf type 
+theory. This project provides an executable, to which we can feed a program 
+in Martin-Löf type theory to check whether this program has the specified type. 
+McTT is novel in that it is implemented and verified in Coq. More specifically, 
+we proved that the typechecking algorithm extracted from Coq is sound and 
+complete: a program passes typechecker if and only if it is a well-typed 
+program in MLTT. This is the first verified proof assistant (despite being 
 elementary) and serves as a basis for future extensions.")
  (depends
   (ocaml (>= "4.14.2"))

scripts/generate_dep.py

@@ -4,7 +4,7 @@
 
 PROJECT_ROOT = Path(__file__).resolve().parents[1]
 THEORIES_ROOT = PROJECT_ROOT / "theories"
-ROOT_MODULE_NAME = "Mcltt"
+ROOT_MODULE_NAME = "Mctt"
 COLORS = {
     "Algorithmic": "darkturquoise",
     "Completeness": "deeppink3",
@@ -57,11 +57,11 @@ def node_of_path(path: str) -> str:
 
     # Handle special case for two main theorems
     # so that printed graph looks better
-    if module_name == "Mcltt.Core.Completeness" or module_name == "Mcltt.Core.Soundness":
+    if module_name == "Mctt.Core.Completeness" or module_name == "Mctt.Core.Soundness":
         result = under_subgraph(f"Core/{node_label}", f""""{module_name}"[label="{node_label}",tooltip="{module_name}",color={color},fillcolor=white];""")
-    elif module_name == "Mcltt.LibTactics":
+    elif module_name == "Mctt.LibTactics":
         result = f"""{{ graph[cluster=false,rank=min]; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
-    elif module_name == "Mcltt.Core.Semantic.Consequences":
+    elif module_name == "Mctt.Core.Semantic.Consequences":
         result = f"""{{ cluster=false; rank=max; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
     else:
         result = f""""{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}];"""
@@ -92,9 +92,9 @@ def data_of_depline(depline: str) -> str:
 def gen_graph() -> str:
     newline = "\n"
     return textwrap.dedent(f"""
-      digraph Mcltt {{
-        graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
-        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/{DOC_BASE}/\\N.html"];
+      digraph Mctt {{
+        graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mctt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
+        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McTT/{DOC_BASE}/\\N.html"];
         {default_subgraph_decl("Algorithmic")}
         {default_subgraph_decl("Core")}
         {core_subgraph_decl("Completeness")}

theories/Algorithmic/Subtyping.v

@@ -1 +1 @@
-From Mcltt.Algorithmic.Subtyping Require Export Definitions Lemmas.
+From Mctt.Algorithmic.Subtyping Require Export Definitions Lemmas.

theories/Algorithmic/Subtyping/Definitions.v

@@ -1,6 +1,6 @@
-From Mcltt.Core Require Import Base.
-From Mcltt.Core.Semantic Require Export NbE.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
+From Mctt.Core Require Import Base.
+From Mctt.Core.Semantic Require Export NbE.
+From Mctt.Core.Syntactic Require Export SystemOpt.
 Import Syntax_Notations.
 
 Reserved Notation "Γ ⊢a A ⊆ A'" (in custom judg at level 80, Γ custom exp, A custom exp, A' custom exp).
@@ -35,4 +35,4 @@ Inductive alg_subtyping : ctx -> typ -> typ -> Prop :=
 where "Γ ⊢a A ⊆ B" := (alg_subtyping Γ A B) (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors alg_subtyping_nf alg_subtyping: mcltt.
+Hint Constructors alg_subtyping_nf alg_subtyping: mctt.

theories/Algorithmic/Subtyping/Lemmas.v

@@ -1,8 +1,8 @@
-From Mcltt Require Import LibTactics.
-From Mcltt.Algorithmic.Subtyping Require Import Definitions.
-From Mcltt.Core Require Import Base Soundness.
-From Mcltt.Core.Syntactic Require Import SystemOpt.
-From Mcltt.Core.Completeness.Consequences Require Import Rules.
+From Mctt Require Import LibTactics.
+From Mctt.Algorithmic.Subtyping Require Import Definitions.
+From Mctt.Core Require Import Base Soundness.
+From Mctt.Core.Syntactic Require Import SystemOpt.
+From Mctt.Core.Completeness.Consequences Require Import Rules.
 Import Syntax_Notations.
 
 #[local]
@@ -61,7 +61,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mcltt.
+Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mctt.
 
 Lemma alg_subtyping_trans : forall Γ A0 A1 A2,
     {{ Γ ⊢a A0 ⊆ A1 }} ->
@@ -74,7 +74,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve alg_subtyping_trans : mcltt.
+Hint Resolve alg_subtyping_trans : mctt.
 
 Lemma alg_subtyping_complete : forall Γ A B,
     {{ Γ ⊢ A ⊆ B }} ->

theories/Algorithmic/Typing.v

@@ -1 +1 @@
-From Mcltt.Algorithmic.Typing Require Export Definitions Lemmas.
+From Mctt.Algorithmic.Typing Require Export Definitions Lemmas.

theories/Algorithmic/Typing/Definitions.v

@@ -1,5 +1,5 @@
-From Mcltt.Algorithmic.Subtyping Require Export Definitions.
-From Mcltt.Core Require Import Base.
+From Mctt.Algorithmic.Subtyping Require Export Definitions.
+From Mctt.Core Require Import Base.
 Import Domain_Notations.
 
 Reserved Notation "Γ '⊢a' M ⟹ A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom nf).
@@ -51,7 +51,7 @@ with alg_type_infer : ctx -> nf -> exp -> Prop :=
 where "Γ '⊢a' M ⟹ A" := (alg_type_infer Γ A M) (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors alg_type_check alg_type_infer : mcltt.
+Hint Constructors alg_type_check alg_type_infer : mctt.
 
 Scheme alg_type_check_mut_ind := Induction for alg_type_check Sort Prop
 with alg_type_infer_mut_ind := Induction for alg_type_infer Sort Prop.