From d43ab2ca6edc480a5969aadec8c3a63f45bebdf9 Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Sun, 8 Sep 2024 00:11:42 -0400 Subject: [PATCH] Add a more "proper" entrypoint with fuller parser (#170) * Implement better entrypoint * Add some examples * Add vector example * Update entrypoint a bit * Minor update * Add PrettyPrinter * Add parser error message * Fix compatability with Coq-8.20.0 * Fix dune version * Change the example extension * Update PrettyPrinter * Add some more examples * Fix type checker time * Update nary argument order --- driver/Lexer.mll | 106 ++++ driver/Main.ml | 39 ++ driver/PrettyPrinter.ml | 207 ++++++++ driver/{test.ml => Test.ml} | 2 +- driver/dune | 18 +- driver/extracted/.gitignore | 3 + driver/extracted/dune | 2 + driver/lexer.mll | 22 - driver/main.ml | 11 - dune-project | 2 +- examples/nary.mcl | 49 ++ examples/pair.mcl | 23 + examples/simple_nat.mcl | 1 + examples/simple_rec.mcl | 4 + examples/vector.mcl | 41 ++ theories/CoqMakefile.mk.local-late | 29 +- theories/Core/Completeness/NatCases.v | 2 +- theories/Core/Semantic/PER/Definitions.v | 2 +- theories/Core/Semantic/PER/Lemmas.v | 8 +- theories/Core/Soundness/FunctionCases.v | 13 +- .../Soundness/LogicalRelation/Definitions.v | 2 +- .../Core/Soundness/LogicalRelation/Lemmas.v | 12 +- theories/Core/Soundness/Realizability.v | 8 +- theories/Core/Soundness/SubtypingCases.v | 2 +- theories/Core/Soundness/TermStructureCases.v | 2 +- theories/Entrypoint.v | 66 +++ theories/Extraction/NbE.v | 2 +- theories/Extraction/TypeCheck.v | 57 ++- theories/Frontend/Elaborator.v | 28 +- theories/Frontend/Parser.vy | 99 ++-- theories/Frontend/ParserExtraction.v | 10 - theories/Frontend/parserMessages.messages | 464 ++++++++++++++++++ theories/LibTactics.v | 10 +- theories/Makefile | 18 +- theories/_CoqProject | 44 +- 35 files changed, 1192 insertions(+), 216 deletions(-) create mode 100644 driver/Lexer.mll create mode 100644 driver/Main.ml create mode 100644 driver/PrettyPrinter.ml rename driver/{test.ml => Test.ml} (98%) create mode 100644 driver/extracted/.gitignore create mode 100644 driver/extracted/dune delete mode 100644 driver/lexer.mll delete mode 100644 driver/main.ml create mode 100644 examples/nary.mcl create mode 100644 examples/pair.mcl create mode 100644 examples/simple_nat.mcl create mode 100644 examples/simple_rec.mcl create mode 100644 examples/vector.mcl create mode 100644 theories/Entrypoint.v delete mode 100644 theories/Frontend/ParserExtraction.v create mode 100644 theories/Frontend/parserMessages.messages diff --git a/driver/Lexer.mll b/driver/Lexer.mll new file mode 100644 index 00000000..cd92ae95 --- /dev/null +++ b/driver/Lexer.mll @@ -0,0 +1,106 @@ +{ + open Lexing + open MclttExtracted.Parser + + 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 token_to_string : token -> string = + function + | ARROW _ -> "->" + | AT _ -> "@" + | BAR _ -> "|" + | COLON _ -> ":" + | COMMA _ -> "," + | DARROW _ -> "=>" + | LPAREN _ -> "(" + | RPAREN _ -> ")" + | ZERO _ -> "zero" + | SUCC _ -> "succ" + | REC _ -> "rec" + | RETURN _ -> "return" + | END _ -> "end" + | LAMBDA _ -> "fun" + | PI _ -> "forall" + | NAT _ -> "Nat" + | INT (_, i) -> string_of_int i + | TYPE _ -> "Type" + | VAR (_, s) -> s + | EOF _ -> "" + + 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 + + let format_token (f: Format.formatter) (t: token): unit = + Format.fprintf + f + "@[\"%s\" (at %a)@]" + (token_to_string t) + format_range (get_range_of_token t) +} + +let string = ['a'-'z''A'-'Z']+ + +rule read = + parse + | "->" { 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_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_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 } + | _ { comment lexbuf } diff --git a/driver/Main.ml b/driver/Main.ml new file mode 100644 index 00000000..004011eb --- /dev/null +++ b/driver/Main.ml @@ -0,0 +1,39 @@ +module Parser = MclttExtracted.Parser +module Entrypoint = MclttExtracted.Entrypoint +open Parser +open MenhirLibParser.Inter +open Entrypoint + +let parse text = + (* 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 token_stream = loop (Lexing.from_string text) in + match Parser.prog 50 token_stream with + | Parsed_pr ((exp, _typ), _) -> Some exp + | Fail_pr_full (_, _) -> None + | _ -> None + +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 ( + 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 + let res = Entrypoint.main 50 token_stream in + Format.printf "%a@." + PrettyPrinter.format_main_result res diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml new file mode 100644 index 00000000..dcb3f873 --- /dev/null +++ b/driver/PrettyPrinter.ml @@ -0,0 +1,207 @@ +open MclttExtracted.Entrypoint +open MclttExtracted.Syntax + +module Parser = MclttExtracted.Parser +module ParserMessages = MclttExtracted.ParserMessages + +(************************************************************) +(* Formatting helpers *) +(************************************************************) + +let pp_print_paren_if (cond: bool) (body: Format.formatter -> unit -> unit) (f: Format.formatter) (): unit = + (if cond then Format.pp_print_char f '('); + body f (); + (if cond then Format.pp_print_char f ')') + +(************************************************************) +(* Formatting Cst.obj *) +(************************************************************) +let rec get_nat_of_obj: Cst.obj -> int option = + function + | Cst.Coq_zero -> Some 0 + | Cst.Coq_succ e -> Option.map ((+) 1) (get_nat_of_obj e) + | _ -> None + +let rec get_fn_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj = + function + | Cst.Coq_fn (px, ep, ebody) -> + let params, ebody' = get_fn_params_of_obj ebody in + ((px, ep) :: params, ebody') + | ebody -> ([], ebody) + +let rec get_pi_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj = + function + | Cst.Coq_pi (px, ep, eret) -> + let params, eret' = get_pi_params_of_obj eret in + ((px, ep) :: params, eret') + | eret -> ([], eret) + +let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit = + let open Format in + function + | Cst.Coq_typ i -> fprintf f "Type@%d" i + | Cst.Coq_nat -> fprintf f "Nat" + | Cst.Coq_zero -> fprintf f "0" + | Cst.Coq_succ e -> + begin + match get_nat_of_obj e with + | Some n -> fprintf f "%d" (1 + n) + | None -> + let impl f () = fprintf f "succ@ %a" (format_obj_prec 2) e in + pp_open_hovbox f 2; + pp_print_paren_if (p >= 2) impl f (); + pp_close_box f () + end + | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) -> + let impl f () = + fprintf f "@[@[rec %a@ return %s -> %a@]@ @[| zero =>@ %a@]@ @[| succ %s, %s =>@ %a@]@ end@]" + format_obj escr + mx + format_obj em + format_obj ez + sx + sr + format_obj es + in + pp_print_paren_if (p >= 1) impl f () + | Cst.Coq_app (ef, ea) -> + let impl f () = + fprintf f "%a@ %a" + (format_obj_prec 1) ef + (format_obj_prec 2) ea; + in + pp_open_hvbox f 2; + pp_print_paren_if (p >= 2) impl f (); + pp_close_box f () + | Cst.Coq_fn (px, ep, ebody) -> + let params, ebody' = get_fn_params_of_obj ebody in + let impl f () = + pp_print_string f "fun "; + pp_open_tbox f (); + pp_set_tab f (); + pp_print_list ~pp_sep:pp_print_tab format_obj_param f ((px, ep) :: params); + pp_close_tbox f (); + begin + if List.compare_length_with params 0 = 0 + then pp_print_space f () + else pp_force_newline f () + end; + fprintf f "-> @[%a@]" + format_obj ebody' + in + pp_open_hvbox f 2; + pp_print_paren_if (p >= 1) impl f (); + pp_close_box f () + | Cst.Coq_pi (px, ep, eret) -> + let params, eret' = get_pi_params_of_obj eret in + let impl f () = + pp_print_string f "forall "; + pp_open_tbox f (); + pp_set_tab f (); + pp_print_list ~pp_sep:pp_print_tab format_obj_param f ((px, ep) :: params); + pp_close_tbox f (); + begin + if List.compare_length_with params 0 = 0 + then pp_print_space f () + else pp_force_newline f () + end; + fprintf f "-> @[%a@]" + format_obj eret' + in + pp_open_hvbox f 2; + pp_print_paren_if (p >= 1) impl f (); + pp_close_box f () + | Cst.Coq_var x -> pp_print_string f x +and format_obj_param f (px, ep) = + Format.fprintf f "(%s : %a)" + px + format_obj ep +and format_obj f = format_obj_prec 0 f + +(************************************************************) +(* Formatting exp *) +(************************************************************) +let exp_to_obj = + let new_var = + let suffix = ref 0 in + fun () -> + incr suffix; + "x" ^ string_of_int !suffix + in + let new_tyvar = + let suffix = ref 0 in + fun () -> + incr suffix; + "A" ^ string_of_int !suffix + in + let rec impl (ctx: string list): exp -> Cst.obj = + function + | Coq_a_zero -> Cst.Coq_zero + | Coq_a_succ e -> Cst.Coq_succ (impl ctx e) + | Coq_a_natrec (em, ez, es, escr) -> + let mx, sx, sr = new_var (), new_var (), new_var () in + Cst.Coq_natrec (impl ctx escr, mx, impl (mx :: ctx) em, impl ctx ez, sx, sr, impl (sr :: sx :: ctx) es) + | Coq_a_nat -> Cst.Coq_nat + | Coq_a_typ i -> Cst.Coq_typ i + | Coq_a_var x -> Cst.Coq_var (List.nth ctx x) + | Coq_a_fn (ep, ebody) -> + let px = + match ep with + | Coq_a_typ _ -> new_tyvar () + | _ -> new_var () + in + Cst.Coq_fn (px, impl ctx ep, impl (px :: ctx) ebody) + | Coq_a_app (ef, ea) -> + Cst.Coq_app (impl ctx ef, impl ctx ea) + | Coq_a_pi (ep, eret) -> + let px = + match ep with + | Coq_a_typ _ -> new_tyvar () + | _ -> new_var () + in + Cst.Coq_pi (px, impl ctx ep, impl (px :: ctx) eret) + | Coq_a_sub _ -> failwith "Invalid internal language construct" + in + impl [] + +let format_exp f exp = format_obj f (exp_to_obj exp) + +(************************************************************) +(* Formatting nf *) +(************************************************************) + +let format_nf f nf = format_exp f (nf_to_exp nf) + +(************************************************************) +(* Formatting main_result *) +(************************************************************) + +let format_main_result (f: Format.formatter): main_result -> unit = + let open Format in + function + | AllGood (cst_typ, cst_exp, typ, exp, nf) -> + fprintf f "@[Parsed:@ @[%a@ : %a@]@]" + format_obj cst_exp + format_obj cst_typ; + pp_force_newline f (); + fprintf f "@[Elaborated:@ @[%a@ : %a@]@]" + format_exp exp + format_exp typ; + pp_force_newline f (); + fprintf f "@[Normalized Result:@ @[%a@ : %a@]@]" + format_nf nf + format_exp typ + | TypeCheckingFailure (typ, exp) -> + printf "@[Type Checking Failure:@ %a@;<1 -2>is not of@ %a@]" + format_exp exp + format_exp typ + | ElaborationFailure cst_exp -> + printf "@[Elaboration Failure:@ %a@;<1 -2>cannot be elaborated@]" + format_obj cst_exp + | ParserFailure (s, t) -> + printf "@[Parser Failure:@ on %a:@ @ @[%a@]@]" + Lexer.format_token t + pp_print_text (ParserMessages.message (Parser.Aut.coq_N_of_state s)) + | ParserTimeout fuel -> + printf "@[Parser Timeout with Fuel %d@]" + fuel diff --git a/driver/test.ml b/driver/Test.ml similarity index 98% rename from driver/test.ml rename to driver/Test.ml index 374e8648..c25b8dcd 100644 --- a/driver/test.ml +++ b/driver/Test.ml @@ -1,7 +1,7 @@ (* Unit test cases for parsing *) open Main -open Parser.Cst +open Entrypoint.Cst let x, y, z = ("x", "y", "z") diff --git a/driver/dune b/driver/dune index 78be42a3..d0049195 100644 --- a/driver/dune +++ b/driver/dune @@ -1,13 +1,17 @@ +(include_subdirs no) + (library - (name mcltt) - (modules main parser lexer test) - (inline_tests) - (preprocess - (pps ppx_inline_test))) + (name Mcltt) + (modules Main Lexer PrettyPrinter) + (libraries MclttExtracted) + ; (inline_tests) + ; (preprocess + ; (pps ppx_inline_test)) +) (env (dev (flags - (:standard -w -67 -w -32 -w -39)))) + (:standard -w -67 -w -32 -w -33 -w -39)))) -(ocamllex lexer) +(ocamllex Lexer) diff --git a/driver/extracted/.gitignore b/driver/extracted/.gitignore new file mode 100644 index 00000000..2cbab739 --- /dev/null +++ b/driver/extracted/.gitignore @@ -0,0 +1,3 @@ +# Generated Files +*.ml +*.mli diff --git a/driver/extracted/dune b/driver/extracted/dune new file mode 100644 index 00000000..9622ae66 --- /dev/null +++ b/driver/extracted/dune @@ -0,0 +1,2 @@ +(library + (name MclttExtracted)) diff --git a/driver/lexer.mll b/driver/lexer.mll deleted file mode 100644 index 810f1196..00000000 --- a/driver/lexer.mll +++ /dev/null @@ -1,22 +0,0 @@ -{ - open Parser -} - -let string = ['a'-'z']+ - -rule read = - parse - | '(' { LPAREN () } - | ')' { RPAREN () } - | '.' { DOT () } - | ':' { COLON () } - | "zero" { ZERO () } - | "succ " { SUCC () } - | "fun" { LAMBDA () } - | "pi" { PI () } - | [' ' '\t' '\n' ] { read lexbuf } - | "Nat" { NAT () } - | ['0'-'9']+ as lxm { INT (int_of_string lxm) } - | "Type" { TYPE () } - | string { VAR (Lexing.lexeme lexbuf) } - | eof { EOF () } diff --git a/driver/main.ml b/driver/main.ml deleted file mode 100644 index 20d853fb..00000000 --- a/driver/main.ml +++ /dev/null @@ -1,11 +0,0 @@ -open Parser.MenhirLibParser.Inter - -let parse text = - (* 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 token_stream = loop (Lexing.from_string text) in - match Parser.prog 50 token_stream with - | Parsed_pr (e, _) -> Some e - | Fail_pr_full (_, _) -> None - | _ -> None diff --git a/dune-project b/dune-project index 2546eaec..88b2a868 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 3.4) +(lang dune 3.13) (using menhir 2.1) (name mcltt) diff --git a/examples/nary.mcl b/examples/nary.mcl new file mode 100644 index 00000000..cf9ffe62 --- /dev/null +++ b/examples/nary.mcl @@ -0,0 +1,49 @@ +(* main body *) +( + fun (Nary : forall (n : Nat) -> Type@0) + (toNat : forall (f : Nary 0) -> Nat) + (appNary : forall (n : Nat) (f : Nary (succ n)) (arg : Nat) -> Nary n) + (n : Nat) + (f : Nary n) + -> (rec n return y -> (forall (g : Nary y) -> Nat) + | zero => toNat + | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m)) + end) f +) +(* Nary definition *) +( + fun (n : Nat) + -> rec n return y -> Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end +) +(* toNat definition *) +(fun (f : Nat) -> f) +(* appNary definition *) +( + fun (n : Nat) + (f : rec succ n return y -> Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end) + (arg : Nat) + -> f arg +) +(* arguments n and f + + This function sums up all its 3 inputs. +*) +3 +( + (fun (add : forall (a : Nat) (b : Nat) -> Nat) -> (fun (a : Nat) (b : Nat) (c : Nat) -> add a (add b c))) + ( + fun (a : Nat) + (b : Nat) + -> rec a return y -> Nat + | zero => b + | succ m, r => succ r + end + ) +) +: Nat diff --git a/examples/pair.mcl b/examples/pair.mcl new file mode 100644 index 00000000..640e1561 --- /dev/null +++ b/examples/pair.mcl @@ -0,0 +1,23 @@ +( + (* Main example *) + ( + fun (Pair : forall (A : Type@0) (B : Type@0) -> Type@1) + (pair : forall (A : Type@0) (B : Type@0) (a : A) (b : B) -> Pair A B) + (fst : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> A) + (snd : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> B) -> + ( + fun (p : Pair Nat (forall (x : Nat) -> Nat)) -> + snd Nat (forall (x : Nat) -> Nat) p + (fst Nat (forall (x : Nat) -> Nat) p) + ) + (pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x))) + ) + (* Church pair *) + (fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) + (* Church pair constructor *) + (fun (A : Type@0) (B : Type@0) (a : A) (b : B) (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> pair a b) + (* Church pair fst *) + (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p A (fun (a : A) (b : B) -> a)) + (* Church pair snd *) + (fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p B (fun (a : A) (b : B) -> b)) +) : Nat diff --git a/examples/simple_nat.mcl b/examples/simple_nat.mcl new file mode 100644 index 00000000..43e6251b --- /dev/null +++ b/examples/simple_nat.mcl @@ -0,0 +1 @@ +succ 3 : Nat diff --git a/examples/simple_rec.mcl b/examples/simple_rec.mcl new file mode 100644 index 00000000..1fc48404 --- /dev/null +++ b/examples/simple_rec.mcl @@ -0,0 +1,4 @@ +(fun (x : Nat) -> rec x return y -> Nat + | zero => 1 + | succ n, r => succ r + end) : forall (x : Nat) -> Nat diff --git a/examples/vector.mcl b/examples/vector.mcl new file mode 100644 index 00000000..5cd1bd14 --- /dev/null +++ b/examples/vector.mcl @@ -0,0 +1,41 @@ +( + (* Main example *) + ( + fun (Vec : forall (A : Type@0) (n : Nat) -> Type@2) + (nil : forall (A : Type@0) -> Vec A 0) + (cons : forall (A : Type@0) (n : Nat) (head : A) (tail : Vec A n) -> Vec A (succ n)) + (vecRec : forall (A : Type@0) (n : Nat) (vec : Vec A n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) -> + ( + fun (totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A) + (vec : Vec (forall (n : Nat) -> Nat) 3) -> + totalHead ((forall (n : Nat) -> Nat)) 2 vec 4 + ) + (* total head function *) + ( + fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> + vecRec A (succ n) vec (fun (l : Nat) -> rec l return r -> Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r -> Type@0 | zero => Nat | succ l, r => A end) -> a) + ) + (* example vector *) + ( + cons (forall (n : Nat) -> Nat) 2 + (fun (n : Nat) -> succ (succ (succ n))) + ( + cons (forall (n : Nat) -> Nat) 1 + (fun (n : Nat) -> succ n) + ( + cons (forall (n : Nat) -> Nat) 0 + (fun (n : Nat) -> succ (succ n)) + (nil (forall (n : Nat) -> Nat)) + ) + ) + ) + ) + (* Church vector *) + (fun (A : Type@0) (n : Nat) -> forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) + (* Church vector nil *) + (fun (A : Type@0) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> nil) + (* Church vector cons *) + (fun (A : Type@0) (n : Nat) (head : A) (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> cons n head (tail C nil cons)) + (* Church vector recursor *) + (fun (A : Type@0) (n : Nat) (vec : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> vec C nil cons) +) : Nat diff --git a/theories/CoqMakefile.mk.local-late b/theories/CoqMakefile.mk.local-late index 14eb2701..336904ec 100644 --- a/theories/CoqMakefile.mk.local-late +++ b/theories/CoqMakefile.mk.local-late @@ -3,27 +3,18 @@ space := $(empty) $(empty) MENHIR := menhir -COQMAKEFILE := CoqMakefile.mk -COQPROJECTFILE := _CoqProject -PARSERBASE := parser.ml -PARSERFILE := ../driver/$(PARSERBASE) -PARSEREXTRACTIONDIR := Frontend -PARSEREXTRACTIONCOQFILE := $(PARSEREXTRACTIONDIR)/ParserExtraction.v -PARSEREXTRACTIONRESULTFILE := $(PARSEREXTRACTIONDIR)/$(PARSERBASE) -COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy')) -COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE)) +PARSERMESSAGEBASE := parserMessages.messages +FRONTENDDIR := Frontend +PARSERMESSAGEFILE := $(FRONTENDDIR)/$(PARSERMESSAGEBASE) +PARSERMESSAGEEXTRACTIONFILE := ../driver/extracted/ParserMessages.ml +COQPARSERORIGFILE := $(shell find ./ -name '*.vy') +COQPARSERFILE := $(COQPARSERORIGFILE:%.vy=%.v) -post-all:: $(COQPARSERFILE) - @+$(MAKE) "$(PARSERFILE)" +post-all:: $(COQPARSERFILE) $(PARSERMESSAGEEXTRACTIONFILE) + @echo "Separate Extraction main." | $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile Entrypoint.v -l Entrypoint.v $(COQPARSERFILE): %.v : %.vy $(MENHIR) --coq "$?" -$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE) - @+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)" - -$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE) - @+$(MAKE) "$(PARSERBASE)" - @echo "MOVE $(PARSERBASE) => $@" - @mv "$(PARSERBASE)" "$@" - @mv "$(patsubst %.ml,%.mli,$(PARSERBASE))" "$(patsubst %.ml,%.mli,$@)" +$(PARSERMESSAGEEXTRACTIONFILE): $(PARSERMESSAGEFILE) $(COQPARSERORIGFILE) + $(MENHIR) --coq "$(COQPARSERORIGFILE)" --compile-errors "$(PARSERMESSAGEFILE)" > "$(PARSERMESSAGEEXTRACTIONFILE)" diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v index fc8ed9b6..9efe0508 100644 --- a/theories/Core/Completeness/NatCases.v +++ b/theories/Core/Completeness/NatCases.v @@ -561,7 +561,7 @@ Proof. apply_relation_equivalence. (on_all_hyp: fun H => directed destruct (H _ _ HinΔℕ)). destruct_by_head per_univ. - unshelve epose proof (IHequiv_m_m' _ _ equiv_ρ_ρ' _ _) as [? [? [? []]]]; shelve_unifiable; only 4: solve [mauto]; eauto. + unshelve epose proof (IHequiv_m_m' _ _ equiv_ρ_ρ' _ _ _ _ _ _ _) as [? [? [? []]]]; shelve_unifiable; only 4: solve [mauto]; eauto. handle_per_univ_elem_irrel. match goal with | _: {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ ~_ ↘ ~?r0 }}, diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v index 3e38aafa..52b9535b 100644 --- a/theories/Core/Semantic/PER/Definitions.v +++ b/theories/Core/Semantic/PER/Definitions.v @@ -209,7 +209,7 @@ Section Per_univ_elem_ind_def. motive i elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}}). #[local] - Ltac def_simp := simp per_univ_elem in *. + Ltac def_simp := simp per_univ_elem in *; mauto 3. #[derive(equations=no, eliminator=no), tactic="def_simp"] Equations per_univ_elem_ind' (i : nat) (R : relation domain) (a b : domain) diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index 01ec4fed..826c36ea 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -535,8 +535,8 @@ Qed. Instance per_elem_PER {i R a b} `(H : per_univ_elem i R a b) : PER R. Proof. split. - - eauto using (per_elem_sym _ _ _ _ _ _ H). - - eauto using (per_elem_trans _ _ _ _ _ _ _ H). + - pose proof (fun m m' => per_elem_sym _ _ _ _ m m' H). eauto. + - pose proof (fun m0 m1 m2 => per_elem_trans _ _ _ _ m0 m1 m2 H); eauto. Qed. (* This lemma gets rid of the unnecessary PER premise. *) @@ -995,8 +995,8 @@ Qed. Instance per_env_PER {R Γ Δ} (H : per_ctx_env R Γ Δ) : PER R. Proof. split. - - auto using (per_env_sym _ _ _ _ _ H). - - eauto using (per_env_trans _ _ _ _ _ _ H). + - pose proof (fun ρ ρ' => per_env_sym _ _ _ ρ ρ' H); auto. + - pose proof (fun ρ0 ρ1 ρ2 => per_env_trans _ _ _ ρ0 ρ1 ρ2 H); eauto. Qed. (* This lemma removes the PER argument *) diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v index 6fe838af..8134cf2c 100644 --- a/theories/Core/Soundness/FunctionCases.v +++ b/theories/Core/Soundness/FunctionCases.v @@ -280,10 +280,13 @@ Proof. match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). inversion_clear_by_head pi_glu_exp_pred. match goal with - | _: {{ ⟦ A ⟧ ρ ↘ ~?a' }}, + | _: glu_univ_elem i ?P' ?El' a, + _: {{ ⟦ A ⟧ ρ ↘ ~?a' }}, _: {{ ⟦ N ⟧ ρ ↘ ~?n' }} |- _ => rename a' into a; - rename n' into n + rename n' into n; + rename P' into Pa; + rename El' into Ela end. assert {{ Dom a ≈ a ∈ per_univ i }} as [] by mauto 3. handle_per_univ_elem_irrel. @@ -302,15 +305,15 @@ Proof. assert {{ DG b ∈ glu_univ_elem i ↘ OP n equiv_n ↘ OEl n equiv_n }} by mauto 3. handle_functional_glu_univ_elem. assert {{ Δ ⊢w Id : Δ }} by mauto 3. - assert {{ Δ ⊢ IT[Id] ® P1 }} by mauto 2. + assert {{ Δ ⊢ IT[Id] ® Pa }} by mauto 2. assert {{ Δ ⊢ IT[Id] : Type@i }} by (eapply glu_univ_elem_univ_lvl; revgoals; eassumption). assert {{ Δ ⊢ IT : Type@i }} by mauto 2. assert {{ Δ ⊢ IT[Id] ≈ A[σ] : Type@i }} as HAeq by (eapply glu_univ_elem_typ_unique_upto_exp_eq'; revgoals; eassumption). - assert {{ Δ ⊢ N[σ] : IT[Id] ® n ∈ El1 }} by (rewrite HAeq; eassumption). + assert {{ Δ ⊢ N[σ] : IT[Id] ® n ∈ Ela }} by (rewrite HAeq; eassumption). assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{ Δ ⊢ M[σ][Id] N[σ] : OT[Id,,N[σ]] ® mn ∈ OEl n equiv_n }}) as [] by mauto 2. destruct_conjs. functional_eval_rewrite_clear. - assert {{ Δ ⊢ N[σ] : A[σ][Id] ® n ∈ El1 }} by (autorewrite with mcltt; eassumption). + assert {{ Δ ⊢ N[σ] : A[σ][Id] ® n ∈ Ela }} by (autorewrite with mcltt; eassumption). assert {{ Δ ⊢s σ∘Id,,N[σ] ® ρ ↦ n ∈ SbΓA }} as Hcons by (unfold SbΓA; mauto 2). (on_all_hyp: destruct_glu_rel_by_assumption SbΓA). simplify_evals. diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v index 9802d177..9c512399 100644 --- a/theories/Core/Soundness/LogicalRelation/Definitions.v +++ b/theories/Core/Soundness/LogicalRelation/Definitions.v @@ -229,7 +229,7 @@ Section GluingInduction. . #[local] - Ltac def_simp := simp glu_univ_elem in *. + Ltac def_simp := simp glu_univ_elem in *; mauto 3. #[derive(equations=no, eliminator=no), tactic="def_simp"] Equations glu_univ_elem_ind i P El a diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index b23b245d..df1780b4 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -522,9 +522,9 @@ Proof. simpl in *. autorewrite with mcltt in *; mauto 3. } - assert {{ Δ ⊢ IT[σ] ≈ IT'[σ] : Type@i }} by mauto 4 using glu_univ_elem_per_univ_typ_escape. - assert {{ Δ ⊢ N : IT[σ] ® n ∈ IEl }} by (simpl; bulky_rewrite1; eassumption). - assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{Δ ⊢ M[σ] N : OT[σ,,N] ® mn ∈ OEl n equiv_n }}) by mauto 3. + assert {{ Δ ⊢ IT'[σ] ≈ IT[σ] : Type@i }} by (symmetry; mauto 4 using glu_univ_elem_per_univ_typ_escape). + assert {{ Δ ⊢ N : IT'[σ] ® n ∈ IEl }} by (simpl; bulky_rewrite1; eassumption). + assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{Δ ⊢ M[σ] N : OT'[σ,,N] ® mn ∈ OEl n equiv_n }}) by mauto 3. destruct_conjs. eexists; split; mauto 3. match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). @@ -538,9 +538,9 @@ Proof. end. assert {{ DG b ∈ glu_univ_elem i ↘ OP n equiv_n ↘ OEl n equiv_n }} by mauto 3. assert {{ DG b' ∈ glu_univ_elem i ↘ OP' n equiv_n ↘ OEl' n equiv_n }} by mauto 3. - assert {{ Δ ⊢ OT[σ,,N] ® OP n equiv_n }} by (eapply glu_univ_elem_trm_typ; mauto 3). + assert {{ Δ ⊢ OT'[σ,,N] ® OP n equiv_n }} by (eapply glu_univ_elem_trm_typ; mauto 3). assert {{ Sub b <: b' at i }} by mauto 3. - assert {{ Δ ⊢ OT[σ,,N] ⊆ OT'[σ,,N] }} by mauto 3. + assert {{ Δ ⊢ OT'[σ,,N] ⊆ OT[σ,,N] }} by mauto 3. intuition. Qed. @@ -823,7 +823,7 @@ Proof. apply_predicate_equivalence; invert_per_ctx_env Hper; handle_per_ctx_env_irrel; - gintuition. + try firstorder. rename i0 into j. rename Γ0 into Γ'. diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v index ae0be94c..e5d45e6c 100644 --- a/theories/Core/Soundness/Realizability.v +++ b/theories/Core/Soundness/Realizability.v @@ -31,7 +31,7 @@ Lemma var_arith : forall Γ1 Γ2 (A : typ), length (Γ1 ++ A :: Γ2) - length Γ2 - 1 = length Γ1. Proof. intros. - rewrite List.app_length. simpl. + rewrite List.length_app. simpl. lia. Qed. @@ -48,7 +48,7 @@ Proof. apply wf_sub_id_inversion in Hτ. pose proof (wf_ctx_sub_length _ _ Hτ). transitivity {{{ #(length Γ1)[Id] }}}; [mauto 3 |]. - replace (length Γ) with (length (Γ1 ++ {{{ Γ2, A0 }}})) by eassumption. + replace (length Γ) with (length (Γ1 ++ {{{ Γ2, A0 }}})) by lia. rewrite var_arith, H. bulky_rewrite. - pose proof (app_ctx_vlookup _ _ _ _ HΔ0 eq_refl) as Hvar. @@ -64,8 +64,8 @@ Proof. rewrite <- @exp_eq_sub_compose_typ; mauto 2. deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [Γ1' [? [Γ2' [? [-> [? [-> []]]]]]]]). - repeat rewrite List.app_length in *. - replace (length Γ1) with (length Γ1') in * by eassumption. + repeat rewrite List.length_app in *. + replace (length Γ1) with (length Γ1') in * by lia. clear_refl_eqs. replace (length Γ2) with (length Γ2') by (simpl in *; lia). diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v index b799fbc6..b587db7c 100644 --- a/theories/Core/Soundness/SubtypingCases.v +++ b/theories/Core/Soundness/SubtypingCases.v @@ -29,7 +29,7 @@ Proof. handle_per_univ_elem_irrel. unfold univ_glu_exp_pred' in *. destruct_conjs. - eapply mk_glu_rel_exp_with_sub''; gintuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right. + eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right. eapply glu_univ_elem_per_subtyp_trm_conv; mauto. assert (i <= max i k) by lia. eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto. diff --git a/theories/Core/Soundness/TermStructureCases.v b/theories/Core/Soundness/TermStructureCases.v index b0467bb1..883a3854 100644 --- a/theories/Core/Soundness/TermStructureCases.v +++ b/theories/Core/Soundness/TermStructureCases.v @@ -67,7 +67,7 @@ Proof. rename a into b. rename a0 into a. assert {{ Dom a ≈ a ∈ per_univ k }} as [] by mauto. - eapply mk_glu_rel_exp_with_sub''; gintuition mauto using per_univ_elem_cumu_max_right. + eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_right. assert {{ ⊢ Γ, B }} by mauto 3. assert {{ Δ ⊢ A[Wk][σ] ≈ A[Wk∘σ] : Type@j }} by mauto 3. assert {{ Δ ⊢ A[Wk][σ] ≈ A[Wk∘σ] : Type@(max j k) }} as -> by mauto 3 using lift_exp_eq_max_left. diff --git a/theories/Entrypoint.v b/theories/Entrypoint.v new file mode 100644 index 00000000..929cca5d --- /dev/null +++ b/theories/Entrypoint.v @@ -0,0 +1,66 @@ +From Coq Require Extraction. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlNativeString ExtrOcamlZInt. + +From Equations Require Import Equations. + +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 NbE TypeCheck. +From Mcltt.Frontend Require Import Elaborator Parser. +Import MenhirLibParser.Inter. +Import Syntax_Notations. + +Variant main_result := + | AllGood : forall cst_typ cst_exp A M W, + elaborate cst_typ nil = Some A -> + elaborate cst_exp nil = Some M -> + {{ ⋅ ⊢ 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 + | ParserTimeout : nat -> main_result +. + +Definition inspect {A} (x : A) : { y | x = y } := exist _ x eq_refl. +Extraction Inline inspect. + +#[local] +Ltac impl_obl_tac := try eassumption. +#[tactic="impl_obl_tac"] +Equations main (log_fuel : nat) (buf : buffer) : main_result := +| log_fuel, buf with Parser.prog log_fuel buf => { + | 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 _ with nbe_impl {{{ ⋅ }}} M A _ => { + | exist _ W _ => AllGood cst_typ cst_exp A M W _ _ _ _ + } + | right _ => TypeCheckingFailure A M _ + } + | exist _ None _ => ElaborationFailure cst_exp _ + } + | exist _ None _ => ElaborationFailure cst_typ _ + } + | Fail_pr_full s t => ParserFailure s t + | Timeout_pr => ParserTimeout log_fuel + } +. +Next Obligation. + eapply elaborator_gives_user_exp; eassumption. +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. + +Set Extraction Flag 1007. +Set Extraction Output Directory "../driver/extracted". 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. diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v index 316e978e..cec25457 100644 --- a/theories/Extraction/TypeCheck.v +++ b/theories/Extraction/TypeCheck.v @@ -33,7 +33,7 @@ Section lookup. repeat impl_obl_tac1; intuition (mauto 4). - #[tactic="impl_obl_tac"] + #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)] Equations lookup G (HG : {{ ⊢ G }}) x : { A | {{ #x : A ∈ G }} } + { forall A, ~ {{ #x : A ∈ G }} } := | {{{ G, A }}}, HG, x with x => { | 0 => pureo (exist _ {{{ A[Wk] }}} _) @@ -51,12 +51,12 @@ Section type_check. . (* Don't forget to use 9th bit of [Extraction Flag] (for example, [Set Extraction Flag 1007.]) *) - Equations get_subterms_of_type_pi (A : nf) : { B & { C | A = n{{{ Π B C }}} } } + { forall B C, A <> n{{{ Π B C }}} } := + Equations get_subterms_of_pi_nf (A : nf) : { B & { C | A = n{{{ Π B C }}} } } + { forall B C, A <> n{{{ Π B C }}} } := | n{{{ Π B C }}} => pureo (existT _ B (exist _ C _)) | _ => inright _ . - Extraction Inline get_level_of_type_nf get_subterms_of_type_pi. + Extraction Inline get_level_of_type_nf get_subterms_of_pi_nf. Inductive type_check_order : exp -> Prop := | tc_ti : forall {A}, type_infer_order A -> type_check_order A @@ -125,24 +125,30 @@ Section type_check. #[local] Ltac impl_obl_tac := clear_defs; - repeat impl_obl_tac_helper; + try match goal with + | H: type_check_order _ |- _ => progressive_invert H + end; + repeat match goal with + | H: type_infer_order _ |- _ => progressive_invert H + end; destruct_conjs; match goal with | |- {{ ⊢ ~_ }} => gen_presups; mautosolve 4 | H: {{ ~?G ⊢ ~?A : Type@?i }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_left; mautosolve 4 | H: {{ ~?G ⊢ ~?A : Type@?j }} |- {{ ~?G ⊢ ~?A : Type@(Nat.max ?i ?j) }} => apply lift_exp_max_right; mautosolve 4 | |- {{ ~_ ⊢ ~_ : ~_ }} => gen_presups; mautosolve 4 - | |- (~ {{ ~_ ⊢a ~_ ⊆ ~_ }} -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) => + | |- _ -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }} => let H := fresh "H" in intros ? H; - inversion H; + directed dependent destruction H; functional_alg_type_infer_rewrite_clear; firstorder - | |- ((forall A : nf, ~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) -> ~ {{ ~_ ⊢a ~_ ⟸ ~_ }}) => - let H := fresh "H" in - intros ? H; - inversion H; - firstorder + | |- _ -> (forall A : nf, ~ {{ ~_ ⊢a ~_ ⟹ ~_ }}) => + unfold not in *; + intros; + progressive_inversion; + functional_alg_type_infer_rewrite_clear; + solve [congruence | mautosolve 3] | |- type_infer_order _ => eassumption; fail 1 | |- type_check_order _ => eassumption; fail 1 | |- subtyping_order ?G ?A ?B => @@ -150,26 +156,20 @@ Section type_check. only 1: enough (exists j, {{ G ⊢ B : ~n{{{ Type@j }}} }}) as [? [? []]%soundness_ty]; only 1: solve [econstructor; eauto 3 using nbe_ty_order_sound]; solve [mauto 4 using alg_type_infer_sound] - | _ => - unfold not; - intros; - progressive_inversion; - functional_alg_type_infer_rewrite_clear; - solve [congruence | mautosolve 3] - | _ => idtac + | _ => try mautosolve 3 end. #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)] Equations type_check G A (HA : (exists i, {{ G ⊢ A : Type@i }})) M (H : type_check_order M) : { {{ G ⊢a M ⟸ A }} } + { ~ {{ G ⊢a M ⟸ A }} } by struct H := | G, A, HA, M, H => let*o->b (exist _ B _) := type_infer G _ M _ while _ in - let*b _ := subtyping_impl G B A _ while _ in + let*b _ := subtyping_impl G (B : nf) A _ while _ in pureb _ with type_infer G (HG : {{ ⊢ G }}) M (H : type_infer_order M) : { A : nf | {{ G ⊢a M ⟹ A }} /\ (exists i, {{ G ⊢a A ⟹ Type@i }}) } + { forall A, ~ {{ G ⊢a M ⟹ A }} } by struct H := | G, HG, M, H with M => { | {{{ Type@j }}} => pureo (exist _ n{{{ Type@(S j) }}} _) - | {{{ ℕ }}} => + | {{{ ℕ }}} => pureo (exist _ n{{{ Type@0 }}} _) | {{{ zero }}} => pureo (exist _ n{{{ ℕ }}} _) @@ -198,9 +198,9 @@ Section type_check. pureo (exist _ n{{{ Π A'' B' }}} _) | {{{ M' N' }}} => let*o (exist _ C _) := type_infer G _ M' _ while _ in - let*o (existT _ A (exist _ B _)) := get_subterms_of_type_pi C while _ in - let*b->o _ := type_check G A _ N' _ while _ in - let (B', _) := nbe_ty_impl G {{{ B[Id,,N'] }}} _ in + let*o (existT _ A (exist _ B _)) := get_subterms_of_pi_nf C while _ in + let*b->o _ := type_check G (A : nf) _ N' _ while _ in + let (B', _) := nbe_ty_impl G {{{ ~(B : nf)[Id,,N'] }}} _ in pureo (exist _ B' _) | {{{ #x }}} => let*o (exist _ A _) := lookup G _ x while _ in @@ -214,7 +214,7 @@ Section type_check. clear_defs. mautosolve 4. Qed. - + Next Obligation (* exists j, {{ G ⊢ A'[Id,,zero] : Type@j }} *). clear_defs. functional_alg_type_infer_rewrite_clear. @@ -293,14 +293,14 @@ Section type_check. firstorder mauto 3. Qed. - Next Obligation. (* exists i : nat, {{ G ⊢ n : Type@i }} *) + Next Obligation. (* exists i : nat, {{ G ⊢ A : Type@i }} *) clear_defs. functional_alg_type_infer_rewrite_clear. progressive_inversion. eexists; mauto 4 using alg_type_infer_sound. Qed. - Next Obligation. (* nbe_ty_order G {{{ B[Id,,N'] }}} *) + Next Obligation. (* nbe_ty_order G {{{ s[Id,,N'] }}} *) clear_defs. functional_alg_type_infer_rewrite_clear. progressive_inversion. @@ -340,7 +340,10 @@ End type_check. Section type_check_closed. #[local] - Ltac impl_obl_tac := unfold not; intros; mauto 3 using user_exp_to_type_infer_order, type_check_order, type_infer_order. + Ltac impl_obl_tac := + unfold not in *; + intros; + mauto 3 using user_exp_to_type_infer_order, type_check_order, type_infer_order. #[tactic="impl_obl_tac",derive(equations=no,eliminator=no)] Equations type_check_closed A (HA : user_exp A) M (HM : user_exp M) : { {{ ⋅ ⊢ M : A }} } + { ~ {{ ⋅ ⊢ M : A }} } := diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v index 6c583f32..c060068b 100644 --- a/theories/Frontend/Elaborator.v +++ b/theories/Frontend/Elaborator.v @@ -39,7 +39,7 @@ Fixpoint elaborate (cst : Cst.obj) (ctx : list string) : option exp := | None => None end | Cst.natrec n mx m z sx sr s => - match elaborate m (mx :: ctx), elaborate z ctx, elaborate s (sx :: sr :: ctx), elaborate n ctx with + match elaborate m (mx :: ctx), elaborate z ctx, elaborate s (sr :: sx :: ctx), elaborate n ctx with | Some m, Some z, Some s, Some n => Some (a_natrec m z s n) | _, _, _, _ => None end @@ -180,19 +180,17 @@ Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (List.length c + simpl in H. destruct string_dec in H. * contradiction n. - * destruct (lookup s ctx). - --inversion H. - rewrite H1. - simpl. - pose (IHctx (m-1)). - rewrite <- H1 in l. - rewrite (Nat.add_sub n1 1) in l. - rewrite <- H1. - rewrite Nat.add_1_r. - apply (Arith_prebase.lt_n_S_stt (n1) (List.length ctx)). - apply l. - reflexivity. - --discriminate H. + * destruct (lookup s ctx); + try discriminate. + inversion H. + rewrite H1. + simpl. + pose (IHctx (m-1)). + rewrite <- H1 in l. + rewrite (Nat.add_sub n1 1) in l. + rewrite <- H1. + specialize (l eq_refl). + lia. Qed. Import StrSProp.Dec. @@ -221,7 +219,7 @@ Proof. - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec. assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec). assert (cst_variables cst3 [<=] StrSProp.of_list ctx) by fsetdec. - assert (cst_variables cst4 [<=] StrSProp.of_list (s0 :: s1 :: ctx)) by (simpl; fsetdec). + assert (cst_variables cst4 [<=] StrSProp.of_list (s1 :: s0 :: ctx)) by (simpl; fsetdec). destruct (IHcst1 _ H0) as [ast [-> ?]]; destruct (IHcst2 _ H1) as [ast' [-> ?]]; destruct (IHcst3 _ H2) as [ast'' [-> ?]]; diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 86f9ac0c..18010618 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -1,58 +1,69 @@ %{ -From Coq Require Import List String. +From Coq Require Import List Arith.PeanoNat String. From Mcltt Require Import Syntax. +Parameter loc : Type. + %} -%token VAR -%token INT -%token ZERO LAMBDA PI SUCC NAT TYPE (* keywords *) -%token LPAREN RPAREN DOT COLON EOF (* delimiters *) +%token VAR +%token INT +%token END LAMBDA NAT PI REC RETURN SUCC TYPE ZERO (* keywords *) +%token ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" EOF (* symbols *) + +%start prog +%type obj app_obj atomic_obj +%type param +%type params +%type Cst.obj -> Cst.obj -> Cst.obj> fnbinder -%start prog -%type obj app_obj simpl_obj -%type args_obj -%type args_list +%on_error_reduce obj params app_obj atomic_obj %% -prog: - | obj EOF { $1 } - -obj: - | LAMBDA args_list DOT obj { - List.fold_left (fun acc arg => Cst.fn (fst arg) (snd arg) acc) $2 $4 - } - | PI args_list DOT obj { - List.fold_left (fun acc arg => Cst.pi (fst arg) (snd arg) acc) $2 $4 - } - | SUCC obj { Cst.succ $2 } - (* Application is a special case, where we must avoid conflict by associativity: *) - (* see https://github.com/utgwkk/lambda-chama/blob/master/parser.mly *) - | app_obj { $1 } - -args_list: - (* Nonempty list of arguments *) - | args_list args_obj { $2 :: $1 } - | args_obj { [$1] } +let prog := + exp = obj; ":"; typ = obj; EOF; <> + +let fnbinder := + | PI; { Cst.pi } + | LAMBDA; { Cst.fn } + +let obj := + | ~ = fnbinder; ~ = params; "->"; ~ = obj; { List.fold_left (fun acc arg => fnbinder (fst arg) (snd arg) acc) params obj } + | ~ = app_obj; <> + + | REC; escr = obj; RETURN; mx = VAR; "->"; em = obj; + "|"; ZERO; "=>"; ez = obj; + "|"; SUCC; sx = VAR; ","; sr = VAR; "=>"; ms = obj; + END; { Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) ms } + | SUCC; ~ = obj; { Cst.succ obj } + +let app_obj := + | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj } + | ~ = atomic_obj; <> + +let atomic_obj := + | TYPE; "@"; n = INT; { Cst.typ (snd n) } + + | NAT; { Cst.nat } + | ZERO; { Cst.zero } + | n = INT; { nat_rect (fun _ => Cst.obj) Cst.zero (fun _ => Cst.succ) (snd n) } + + | x = VAR; { Cst.var (snd x) } + + | "("; ~ = obj; ")"; <> + +(* Reversed nonempty list of parameters *) +let params := + | ~ = params; ~ = param; { param :: params } + | ~ = param; { [param] } (* (x : A) *) -args_obj: - | LPAREN VAR COLON obj RPAREN { ($2, $4) } - -(* M N *) -app_obj: - (* simpl_obj prevents conflict by associativity *) - | app_obj simpl_obj { Cst.app $1 $2 } - | simpl_obj { $1 } - -(* Either a variable or parentheses around a complex object *) -simpl_obj: - | VAR { Cst.var $1 } - | NAT { Cst.nat } - | ZERO { Cst.zero } - | TYPE INT { Cst.typ $2 } - | LPAREN obj RPAREN { $2 } +let param := + | "("; x = VAR; ":"; ~ = obj; ")"; { (snd x, obj) } + +%% +Extract Constant loc => "Lexing.position * Lexing.position". diff --git a/theories/Frontend/ParserExtraction.v b/theories/Frontend/ParserExtraction.v deleted file mode 100644 index 1aafd5b6..00000000 --- a/theories/Frontend/ParserExtraction.v +++ /dev/null @@ -1,10 +0,0 @@ -From Coq Require Extraction. - -From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlNativeString. - -From Mcltt Require Import Parser. -Import MenhirLibParser.Inter. - -Extraction Language OCaml. - -Extraction "parser.ml" Parser.prog. diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages new file mode 100644 index 00000000..d3002c11 --- /dev/null +++ b/theories/Frontend/parserMessages.messages @@ -0,0 +1,464 @@ +prog: INT COLON INT SUCC +## +## Ends in an error in state: 50. +## +## prog -> obj COLON obj . EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or the end of file is expected. +This token is invalid for the beginning of an expression. + +prog: RPAREN +## +## Ends in an error in state: 0. +## +## prog' -> . prog [ # ] +## +## The known suffix of the stack is as follows: +## +## + +This token is invalid for the beginning of a program. + +prog: TYPE ZERO +## +## Ends in an error in state: 3. +## +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE +## + +"Type" requires "@". + +prog: TYPE AT ZERO +## +## Ends in an error in state: 4. +## +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE AT +## + +"Type" requires "@?level", where "?level" is an arabic numeral. + +prog: SUCC RPAREN +## +## Ends in an error in state: 6. +## +## obj -> SUCC . obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## SUCC +## + +An expression is expected after "succ". +This token is invalid for the beginning of an expression. + +prog: REC RPAREN +## +## Ends in an error in state: 7. +## +## obj -> REC . obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC +## + +An expression is expected after "rec". +This token is invalid for the beginning of an expression. + +prog: LAMBDA ZERO +## +## Ends in an error in state: 15. +## +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder +## + +"forall" requires a list of parenthesized parameters. +For example, + "(x : Nat) (y : Nat)" in "forall (x : Nat) (y : Nat) -> Nat" + +prog: LAMBDA LPAREN ZERO +## +## Ends in an error in state: 16. +## +## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +A parameter should start with a valid identifier. + +prog: LAMBDA LPAREN VAR ZERO +## +## Ends in an error in state: 17. +## +## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR +## + +A parameter should have ": ?type" after the parameter name, +where "?type" is the type of the parameter. + +prog: LAMBDA LPAREN VAR COLON RPAREN +## +## Ends in an error in state: 18. +## +## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON +## + +A parameter should have "?type" after ":", +where "?type" is the type of the parameter. + +prog: LPAREN RPAREN +## +## Ends in an error in state: 10. +## +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +"()" is an invalid expression. +"()" should have an expression in it to be an expression. + +prog: LPAREN INT DARROW +## +## Ends in an error in state: 13. +## +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT DARROW +## +## Ends in an error in state: 19. +## +## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 24. +## +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN EOF END COLON BAR ] +## params -> params . param [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## fnbinder params +## + +"->" or another parameter is expected after a list of parameters for "fun". + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN +## +## Ends in an error in state: 25. +## +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder params ARROW +## + +An expression is expected after "->". +This token is invalid for the beginning of an expression. + +prog: REC INT DARROW +## +## Ends in an error in state: 29. +## +## obj -> REC obj . RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or "return" keyword is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN ZERO +## +## Ends in an error in state: 30. +## +## obj -> REC obj RETURN . VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN +## + +A motif should start with a valid identifier. + +prog: REC INT RETURN VAR ZERO +## +## Ends in an error in state: 31. +## +## obj -> REC obj RETURN VAR . ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR +## + +A motif should have "->" after the scrutinee name. + +prog: REC INT RETURN VAR ARROW RPAREN +## +## Ends in an error in state: 32. +## +## obj -> REC obj RETURN VAR ARROW . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW +## + +An expression is expected for a motif. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN VAR ARROW INT DARROW +## +## Ends in an error in state: 33. +## +## obj -> REC obj RETURN VAR ARROW obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or "|" is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN VAR ARROW INT BAR VAR +## +## Ends in an error in state: 34. +## +## obj -> REC obj RETURN VAR ARROW obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR +## + +"zero" is expected for the first branch of "rec". + +prog: REC INT RETURN VAR ARROW INT BAR ZERO ZERO +## +## Ends in an error in state: 35. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO +## + +"=>" is expected after a pattern for "rec". + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW RPAREN +## +## Ends in an error in state: 36. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW +## + +An expression is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT DARROW +## +## Ends in an error in state: 37. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or "|" is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR ZERO +## +## Ends in an error in state: 38. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR +## + +"succ" is expected for the second branch of "rec". + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC ZERO +## +## Ends in an error in state: 39. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC +## + +An identifier for the predecessor of the scrutinee is expected. + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR ZERO +## +## Ends in an error in state: 40. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR +## + +"," is expected after "succ ?x". + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO +## +## Ends in an error in state: 41. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA +## + +An identifier for the recursion result is expected. + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO +## +## Ends in an error in state: 42. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR +## + +"=>" is expected after a pattern for "rec". + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN +## +## Ends in an error in state: 43. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW +## + +An expression is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW +## +## Ends in an error in state: 44. +## +## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or "end" is expected. +This token is invalid for the beginning of an expression. + +prog: INT DARROW +## +## Ends in an error in state: 48. +## +## prog -> obj . COLON obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 22, spurious reduction of production obj -> app_obj +## + +Either an expression or ":" is expected. +This token is invalid for the beginning of an expression. + +prog: INT COLON RPAREN +## +## Ends in an error in state: 49. +## +## prog -> obj COLON . obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON +## + +An expression is expected. +This token is invalid for the beginning of an expression. \ No newline at end of file diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 61e23ad5..af0b538d 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -432,17 +432,13 @@ Hint Extern 1 (subrelation (@subrelation ?A) _) => (let H := fresh "H" in intros #[export] Instance predicate_implication_equivalence Ts : subrelation (@predicate_equivalence Ts) (@predicate_implication Ts). Proof. - induction Ts; gintuition. - - intros ? ? H v. - apply IHTs. - exact (H v). + induction Ts; firstorder eauto 2. Qed. Add Parametric Morphism Ts : (@predicate_implication Ts) with signature (@predicate_equivalence Ts) ==> (@predicate_equivalence Ts) ==> iff as predicate_implication_morphism. Proof. - induction Ts; split; intros; gintuition. + induction Ts; split; intros; try firstorder. - rewrite <- H. transitivity x0; try eassumption. rewrite H0; reflexivity. @@ -466,7 +462,7 @@ Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) := Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) : Proper R a. Proof. - cbv. auto using per_elem. + cbv. pose proof per_elem; auto. Qed. diff --git a/theories/Makefile b/theories/Makefile index 68c3d572..cb16c21e 100644 --- a/theories/Makefile +++ b/theories/Makefile @@ -6,10 +6,14 @@ MENHIR := menhir COQMAKEFILE := CoqMakefile.mk COQPROJECTFILE := _CoqProject PARSERBASE := parser.ml +POSTPARSERBASE := type_checker.ml PARSERFILE := ../driver/$(PARSERBASE) -PARSEREXTRACTIONDIR := Frontend -PARSEREXTRACTIONCOQFILE := $(PARSEREXTRACTIONDIR)/ParserExtraction.v -PARSEREXTRACTIONRESULTFILE := $(PARSEREXTRACTIONDIR)/$(PARSERBASE) +POSTPARSERFILE := ../driver/$(POSTPARSERBASE) +FRONTENDDIR := Frontend +PARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/ParserExtraction.v +PARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(PARSERBASE) +POSTPARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/PostParserExtraction.v +POSTPARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(POSTPARSERBASE) COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy')) COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE)) @@ -20,8 +24,12 @@ all: $(COQMAKEFILE) .PHONY: clean clean: $(COQMAKEFILE) @+$(MAKE) -f "$(COQMAKEFILE)" cleanall - @echo "CLEAN $(COQPARSERFILE) $(PARSERBASE) $(patsubst %.ml,%.mli,$(PARSERBASE)) $(PARSERFILE) $(patsubst %.ml,%.mli,$(PARSERFILE)) $(COQMAKEFILE) $(COQMAKEFILE).conf" - @rm -f "$(COQPARSERFILE)" "$(PARSERBASE)" "$(patsubst %.ml,%.mli,$(PARSERBASE))" "$(PARSERFILE)" "$(patsubst %.ml,%.mli,$(PARSERFILE))" "$(COQMAKEFILE)" "$(COQMAKEFILE).conf" + @echo "CLEAN $(COQPARSERFILE) $(PARSERBASE) $(patsubst %.ml,%.mli,$(PARSERBASE)) $(PARSERFILE) $(patsubst %.ml,%.mli,$(PARSERFILE))" + @rm -f "$(COQPARSERFILE)" "$(PARSERBASE)" "$(patsubst %.ml,%.mli,$(PARSERBASE))" "$(PARSERFILE)" "$(patsubst %.ml,%.mli,$(PARSERFILE))" + @echo "CLEAN $(POSTPARSERBASE) $(patsubst %.ml,%.mli,$(POSTPARSERBASE)) $(POSTPARSERFILE) $(patsubst %.ml,%.mli,$(POSTPARSERFILE))" + @rm -f "$(POSTPARSERBASE)" "$(patsubst %.ml,%.mli,$(POSTPARSERBASE))" "$(POSTPARSERFILE)" "$(patsubst %.ml,%.mli,$(POSTPARSERFILE))" + @echo "CLEAN $(COQMAKEFILE) $(COQMAKEFILE).conf" + @rm -f "$(COQMAKEFILE)" "$(COQMAKEFILE).conf" .PHONY: update_CoqProject update_CoqProject: clean diff --git a/theories/_CoqProject b/theories/_CoqProject index 69522341..a18df2a5 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -7,29 +7,30 @@ ./Algorithmic/Typing/Definitions.v ./Algorithmic/Typing/Lemmas.v ./Core/Base.v +./Core/Completeness.v +./Core/Completeness/Consequences/Inversions.v ./Core/Completeness/Consequences/Rules.v ./Core/Completeness/Consequences/Types.v -./Core/Completeness/Consequences/Inversions.v ./Core/Completeness/ContextCases.v ./Core/Completeness/FunctionCases.v ./Core/Completeness/FundamentalTheorem.v +./Core/Completeness/LogicalRelation.v ./Core/Completeness/LogicalRelation/Definitions.v ./Core/Completeness/LogicalRelation/Lemmas.v ./Core/Completeness/LogicalRelation/Tactics.v -./Core/Completeness/LogicalRelation.v ./Core/Completeness/NatCases.v ./Core/Completeness/SubstitutionCases.v +./Core/Completeness/SubtypingCases.v ./Core/Completeness/TermStructureCases.v ./Core/Completeness/UniverseCases.v ./Core/Completeness/VariableCases.v -./Core/Completeness/SubtypingCases.v -./Core/Completeness.v ./Core/Semantic/Consequences.v ./Core/Semantic/Domain.v ./Core/Semantic/Evaluation.v ./Core/Semantic/Evaluation/Definitions.v ./Core/Semantic/Evaluation/Lemmas.v ./Core/Semantic/Evaluation/Tactics.v +./Core/Semantic/NbE.v ./Core/Semantic/PER.v ./Core/Semantic/PER/CoreTactics.v ./Core/Semantic/PER/Definitions.v @@ -38,20 +39,6 @@ ./Core/Semantic/Readback/Definitions.v ./Core/Semantic/Readback/Lemmas.v ./Core/Semantic/Realizability.v -./Core/Semantic/NbE.v -./Core/Syntactic/CoreInversions.v -./Core/Syntactic/CoreTypeInversions.v -./Core/Syntactic/Corollaries.v -./Core/Syntactic/CtxEq.v -./Core/Syntactic/CtxSub.v -./Core/Syntactic/Presup.v -./Core/Syntactic/Syntax.v -./Core/Syntactic/ExpNoConfusion.v -./Core/Syntactic/System.v -./Core/Syntactic/System/Definitions.v -./Core/Syntactic/System/Lemmas.v -./Core/Syntactic/System/Tactics.v -./Core/Syntactic/SystemOpt.v ./Core/Soundness.v ./Core/Soundness/ContextCases.v ./Core/Soundness/FunctionCases.v @@ -71,13 +58,26 @@ ./Core/Soundness/Weakening.v ./Core/Soundness/Weakening/Definition.v ./Core/Soundness/Weakening/Lemmas.v -./Frontend/Elaborator.v -./Frontend/Parser.v -./Frontend/ParserExtraction.v +./Core/Syntactic/CoreInversions.v +./Core/Syntactic/CoreTypeInversions.v +./Core/Syntactic/Corollaries.v +./Core/Syntactic/CtxEq.v +./Core/Syntactic/CtxSub.v +./Core/Syntactic/ExpNoConfusion.v +./Core/Syntactic/Presup.v +./Core/Syntactic/Syntax.v +./Core/Syntactic/System.v +./Core/Syntactic/System/Definitions.v +./Core/Syntactic/System/Lemmas.v +./Core/Syntactic/System/Tactics.v +./Core/Syntactic/SystemOpt.v +./Entrypoint.v ./Extraction/Evaluation.v ./Extraction/NbE.v -./Extraction/Readback.v ./Extraction/PseudoMonadic.v +./Extraction/Readback.v ./Extraction/Subtyping.v ./Extraction/TypeCheck.v +./Frontend/Elaborator.v +./Frontend/Parser.v ./LibTactics.v