Update entrypoint a bit

driver/lexer.mll

@@ -2,37 +2,51 @@
   open Lexing
   open MclttExtracted.Parser
 
-  let get_position lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p)
+  let get_range lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p)
+
+  let format_position (f: Format.formatter) (p: position): unit =
+    Format.fprintf
+      f
+      "line %d, column %d"
+      p.pos_lnum
+      (p.pos_cnum - p.pos_bol + 1)
+
+  let format_range (f: Format.formatter) (p: position * position): unit =
+    Format.fprintf
+      f
+      "@[<h>%a - %a@]"
+      format_position (fst p)
+      format_position (snd p)
 }
 
 let string = ['a'-'z''A'-'Z']+
 
 rule read =
   parse
-  | "->" { ARROW (get_position lexbuf) }
-  | '@' { AT (get_position lexbuf) }
-  | '|' { BAR (get_position lexbuf) }
-  | ':' { COLON (get_position lexbuf) }
-  | ',' { COMMA (get_position lexbuf) }
-  | "=>" { DARROW (get_position lexbuf) }
+  | "->" { ARROW (get_range lexbuf) }
+  | '@' { AT (get_range lexbuf) }
+  | '|' { BAR (get_range lexbuf) }
+  | ':' { COLON (get_range lexbuf) }
+  | ',' { COMMA (get_range lexbuf) }
+  | "=>" { DARROW (get_range lexbuf) }
   | "(*" { comment lexbuf }
-  | '(' { LPAREN (get_position lexbuf) }
-  | ')' { RPAREN (get_position lexbuf) }
-  | "zero" { ZERO (get_position lexbuf) }
-  | "succ" { SUCC (get_position lexbuf) }
-  | "rec" { REC (get_position lexbuf) }
-  | "return" { RETURN (get_position lexbuf) }
-  | "end" { END (get_position lexbuf) }
-  | "fun" { LAMBDA (get_position lexbuf) }
-  | "forall" { PI (get_position lexbuf) }
+  | '(' { LPAREN (get_range lexbuf) }
+  | ')' { RPAREN (get_range lexbuf) }
+  | "zero" { ZERO (get_range lexbuf) }
+  | "succ" { SUCC (get_range lexbuf) }
+  | "rec" { REC (get_range lexbuf) }
+  | "return" { RETURN (get_range lexbuf) }
+  | "end" { END (get_range lexbuf) }
+  | "fun" { LAMBDA (get_range lexbuf) }
+  | "forall" { PI (get_range lexbuf) }
   | [' ' '\t'] { read lexbuf }
   | ['\n'] { new_line lexbuf; read lexbuf }
-  | "Nat" { NAT (get_position lexbuf) }
-  | ['0'-'9']+ as lxm { INT (get_position lexbuf, int_of_string lxm) }
-  | "Type" { TYPE (get_position lexbuf) }
-  | string { VAR (get_position lexbuf, Lexing.lexeme lexbuf) }
-  | eof { EOF (get_position lexbuf) }
-  | _ as c { failwith (Printf.sprintf "unexpected character: %C at line %d, column %d" c lexbuf.lex_start_p.pos_lnum (lexbuf.lex_start_p.pos_cnum - lexbuf.lex_start_p.pos_bol)) }
+  | "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) }
+  | _ 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
   | "*)" { read lexbuf }

driver/main.ml

@@ -14,12 +14,24 @@ let parse text =
   | Fail_pr_full (_, _) -> None
   | _ -> None
 
-let main () =
-  print_string "File path to load: ";
-  let fp = read_line () in
+let main ?(default_fp = "") () =
+  let fp =
+    if default_fp <> ""
+    then default_fp
+    else
+      begin
+        print_string "File path to load: ";
+        read_line ()
+      end
+  in
   let chan = open_in fp in
   (* Before parsing, we must generate a token stream from a lexer buffer,
      which we then feed into the parser. *)
-  let rec loop lexbuf = lazy (Buf_cons (Lexer.read lexbuf, loop lexbuf)) in
+  let rec loop lexbuf =
+    lazy (
+        try
+          Buf_cons (Lexer.read lexbuf, loop lexbuf)
+        with
+        | Failure s -> prerr_string s; raise Exit) in
   let token_stream = loop (Lexing.from_channel chan) in
   Entrypoint.main 50 token_stream

theories/Entrypoint.v

@@ -3,15 +3,16 @@ From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlNativeString.
 
 From Equations Require Import Equations.
 
-From Mcltt.Core Require Import Base.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base Completeness Soundness.
 From Mcltt.Core.Syntactic Require Import SystemOpt.
-From Mcltt.Extraction Require Import TypeCheck.
+From Mcltt.Extraction Require Import NbE TypeCheck.
 From Mcltt.Frontend Require Import Elaborator Parser.
 Import MenhirLibParser.Inter.
 Import Syntax_Notations.
 
 Variant main_result :=
-  | AllGood : forall A M, {{ ⋅ ⊢ M : A }} -> main_result
+  | AllGood : forall A M W, {{ ⋅ ⊢ M : A }} -> nbe {{{ ⋅ }}} M A W -> main_result
   | TypeCheckingFailure : forall A M, ~ {{ ⋅ ⊢ M : A }} -> main_result
   | ElaborationFailure : forall cst, elaborate cst nil = None -> main_result
   | ParserFailure : Aut.state -> Aut.Gram.token -> main_result
@@ -29,7 +30,9 @@ Equations main (log_fuel : nat) (buf : buffer) : main_result :=
   | Parsed_pr (cst_exp, cst_typ) _ with inspect (elaborate cst_typ nil) => {
     | exist _ (Some A) _ with inspect (elaborate cst_exp nil) => {
       | exist _ (Some M) _ with type_check_closed A _ M _ => {
-        | left  _ => AllGood A M _
+        | left  _ with nbe_impl {{{ ⋅ }}} M A _ => {
+          | exist _ W _ => AllGood A M W _ _
+          }
         | right _ => TypeCheckingFailure A M _
         }
       | exist _ None     _ => ElaborationFailure cst_exp _
@@ -46,6 +49,11 @@ Qed.
 Next Obligation.
   eapply elaborator_gives_user_exp; eassumption.
 Qed.
+Next Obligation.
+  (on_all_hyp: fun H => apply soundness in H as [? []]).
+  eapply nbe_order_sound.
+  eassumption.
+Qed.
 
 Extraction Language OCaml.
 

theories/Extraction/NbE.v

@@ -1,5 +1,5 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import NbE.
+From Mcltt.Core Require Export NbE.
 From Mcltt.Extraction Require Import Evaluation Readback.
 From Equations Require Import Equations.
 Import Domain_Notations.