backward merge

README.md

@@ -1,12 +1,11 @@
 # McLTT: A Bottom-up Approach to Implementing A Proof Assistant
 
-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-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
-program in MLTT. This will be the first verified proof assistant (despite being
+McLTT 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. McLTT 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. 
 
 ## Online Documentation
@@ -83,7 +82,7 @@ or more directly
 _build/default/driver/mcltt.exe examples/nary.mcl # or your own example
 ```
 
-To build Coq proof only, you can go into and only build the Coq folder:
+To build Coq proof only, you can go into and only build the `theories` directory:
 ```
 cd theories
 make

driver/Lexer.mll

@@ -40,29 +40,37 @@
     | TYPE _ -> "Type"
     | VAR (_, s) -> s
     | EOF _ -> "<EOF>"
+    | DOT _ -> "."
+    | LET _ -> "let"
+    | IN _ -> "in"
+    | EQ _ -> ":="
 
   let get_range_of_token : token -> (position * position) =
     function
     | ARROW r
-      | AT r
-      | BAR r
-      | COLON r
-      | COMMA r
-      | DARROW r
-      | LPAREN r
-      | RPAREN r
-      | ZERO r
-      | SUCC r
-      | REC r
-      | RETURN r
-      | END r
-      | LAMBDA r
-      | PI r
-      | NAT r
-      | TYPE r
-      | EOF r
-      | INT (r, _)
-      | VAR (r, _) -> r
+    | AT r
+    | BAR r
+    | COLON r
+    | COMMA r
+    | DARROW r
+    | LPAREN r
+    | RPAREN r
+    | ZERO r
+    | SUCC r
+    | REC r
+    | RETURN r
+    | END r
+    | LAMBDA r
+    | PI r
+    | NAT r
+    | TYPE r
+    | EOF r
+    | INT (r, _)
+    | DOT r
+    | LET r
+    | IN r
+    | EQ r
+    | VAR (r, _) -> r
 
   let format_token (f: Format.formatter) (t: token): unit =
     Format.fprintf
@@ -97,8 +105,12 @@ rule read =
   | "Nat" { NAT (get_range lexbuf) }
   | ['0'-'9']+ as lxm { INT (get_range lexbuf, int_of_string lxm) }
   | "Type" { TYPE (get_range lexbuf) }
-  | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) }
   | eof { EOF (get_range lexbuf) }
+  | "." { DOT (get_range lexbuf) }
+  | "let" {LET (get_range lexbuf) }
+  | "in" {IN (get_range lexbuf) }
+  | ":=" {EQ (get_range lexbuf) }
+  | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) }
   | _ as c { failwith (Format.asprintf "@[<v 2>Lexer error:@ @[<v 2>Unexpected character %C@ at %a@]@]@." c format_position lexbuf.lex_start_p) }
 and comment =
   parse

driver/PrettyPrinter.ml

@@ -56,7 +56,7 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
   | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) ->
      let impl f () =
        fprintf f
-         "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ \
+         "@[<hv 0>@[<hov 2>rec %a@ return %s . %a@]@ @[<hov 2>| zero =>@ \
           %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
          format_obj escr mx format_obj em format_obj ez sx sr format_obj es
      in