From a10e66b3ef9666db4548bdd5276df8ff8e97334a Mon Sep 17 00:00:00 2001 From: Junyoung/Clare Jang Date: Thu, 5 Sep 2024 15:01:26 -0400 Subject: [PATCH] Update entrypoint a bit --- driver/lexer.mll | 58 ++++++++++++++++++++++++--------------- driver/main.ml | 20 +++++++++++--- theories/Entrypoint.v | 16 ++++++++--- theories/Extraction/NbE.v | 2 +- 4 files changed, 65 insertions(+), 31 deletions(-) diff --git a/driver/lexer.mll b/driver/lexer.mll index a4c3f1e2..b36fe514 100644 --- a/driver/lexer.mll +++ b/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 + "@[%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 "@[Lexer error:@ @[Unexpected character %C@ at %a@]@]@." c format_position lexbuf.lex_start_p) } and comment = parse | "*)" { read lexbuf } diff --git a/driver/main.ml b/driver/main.ml index 50640ada..7bc7a62d 100644 --- a/driver/main.ml +++ b/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 diff --git a/theories/Entrypoint.v b/theories/Entrypoint.v index 20cdb080..4105e594 100644 --- a/theories/Entrypoint.v +++ b/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. diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v index c224cef6..fa5ff9f3 100644 --- a/theories/Extraction/NbE.v +++ b/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.