From eb29dc01e0f305f0b77f1c002aff810c17a1532d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Jun 2021 09:55:52 +0200 Subject: [PATCH 01/22] split syntax file --- _CoqProject | 1 + src/coq_elpi_arg_syntax.ml | 944 +++++++++++++++++++++++++++++ src/coq_elpi_arg_syntax.mlg | 270 +++++++++ src/coq_elpi_vernacular.ml | 20 +- src/coq_elpi_vernacular.mli | 7 +- src/coq_elpi_vernacular_syntax.mlg | 265 +------- src/elpi_plugin.mlpack | 1 + 7 files changed, 1231 insertions(+), 277 deletions(-) create mode 100644 src/coq_elpi_arg_syntax.ml create mode 100644 src/coq_elpi_arg_syntax.mlg diff --git a/_CoqProject b/_CoqProject index 6dff4c0e8..839d76c7f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -32,6 +32,7 @@ src/coq_elpi_glob_quotation.ml src/coq_elpi_glob_quotation.mli src/coq_elpi_arg_HOAS.ml src/coq_elpi_arg_HOAS.mli +src/coq_elpi_arg_syntax.mlg src/coq_elpi_builtins_HOAS.ml src/coq_elpi_builtins.ml src/coq_elpi_builtins.mli diff --git a/src/coq_elpi_arg_syntax.ml b/src/coq_elpi_arg_syntax.ml new file mode 100644 index 000000000..b887e2aaa --- /dev/null +++ b/src/coq_elpi_arg_syntax.ml @@ -0,0 +1,944 @@ +let __coq_plugin_name = "elpi_plugin" +let _ = Mltop.add_known_module __coq_plugin_name + +# 7 "src/coq_elpi_arg_syntax.mlg" + + +open Ltac_plugin + +open Pcoq.Constr +open Pcoq.Prim + +module EA = Coq_elpi_arg_HOAS +module U = Coq_elpi_utils + +(* Arguments ************************************************************* *) +let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) + +let trim_loc loc = + let open Loc in + { loc with bp = loc.bp + 1; ep = loc.ep - 1 } + +let idents_of loc s = + let s = String.sub s 1 (String.length s - 2) in + let l = Str.(split (regexp "[\t \n]+") s) in + List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; + Coq_elpi_utils.of_coq_loc (trim_loc loc), l + +let rec strip_curly loc s = + if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_round loc s = + if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_square loc s = + if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s + + + +let (wit_elpi_string, elpi_string) = Tacentries.argument_extend ~name:"elpi_string" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "xxxxxxxx")))) + (fun _ loc -> + +# 43 "src/coq_elpi_arg_syntax.mlg" + (Elpi.API.Ast.Loc.initial "dummy", "") + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + ), (fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + ), (fun env sigma -> + +# 42 "src/coq_elpi_arg_syntax.mlg" + pr_elpi_string + )); + } +let _ = (wit_elpi_string, elpi_string) + +let _ = let () = + Pcoq.grammar_extend elpi_string + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PSTRING (None))))) + (fun s loc -> +# 53 "src/coq_elpi_arg_syntax.mlg" + + Coq_elpi_utils.of_coq_loc loc, s + + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PQUOTATION "lp:")))) + (fun s loc -> +# 47 "src/coq_elpi_arg_syntax.mlg" + + if s.[0] = '\123' then strip_curly loc s + else if s.[0] = '(' then strip_round loc s + else if s.[0] = '[' then strip_square loc s + else Coq_elpi_utils.of_coq_loc loc, s + + )])]} + in () + + +# 59 "src/coq_elpi_arg_syntax.mlg" + +let pr_fp _ _ _ (_,x) = U.pr_qualified_name x +let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () + +let the_qname = ref "" +let any_qname loc_fun strm = + let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> + let pos = Stream.count strm in + Stream.junk strm; + let _, ep = Loc.unloc (loc_fun pos) in + begin match Stream.peek strm with + | Some (Tok.IDENT id) -> + let bp, _ = Loc.unloc (loc_fun (pos+1)) in + if Int.equal ep bp then + (Stream.junk strm; the_qname := sym ^ id) + else + the_qname := sym + | _ -> the_qname := sym + end + | _ -> raise Stream.Failure +let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname + + + +let (wit_qualified_name, qualified_name) = Tacentries.argument_extend ~name:"qualified_name" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + []); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + ), (fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + ), (fun env sigma -> + +# 85 "src/coq_elpi_arg_syntax.mlg" + pr_fp + )); + } +let _ = (wit_qualified_name, qualified_name) + +let _ = let () = + Pcoq.grammar_extend qualified_name + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm any_qname))) + (fun _ loc -> +# 91 "src/coq_elpi_arg_syntax.mlg" + loc, Str.split_delim (Str.regexp_string ".") !the_qname + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("_"))))) + (fun _ loc -> +# 90 "src/coq_elpi_arg_syntax.mlg" + loc, [] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PIDENT (None))))) + ((Pcoq.Symbol.list0 (Pcoq.Symbol.token (Tok.PFIELD (None)))))) + (fun s i loc -> +# 89 "src/coq_elpi_arg_syntax.mlg" + loc, i :: s + )])]} + in () + +let (wit_elpi_loc, elpi_loc) = Tacentries.argument_extend ~name:"elpi_loc" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.stop) + (fun loc -> +# 97 "src/coq_elpi_arg_syntax.mlg" + loc + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + ), (fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + ), (fun env sigma -> + +# 96 "src/coq_elpi_arg_syntax.mlg" + pp_elpi_loc + )); + } +let _ = (wit_elpi_loc, elpi_loc) + + +# 100 "src/coq_elpi_arg_syntax.mlg" + + +let record_fields = Pcoq.Entry.create "elpi:record_fields" +let telescope = Pcoq.Entry.create "elpi:telescope" +let colon_sort = Pcoq.Entry.create "elpi:colon_sort" +let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" +let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" + +let any_attribute : Attributes.vernac_flags Attributes.attribute = + Attributes.make_attribute (fun x -> [],x) +let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = + let open Attributes.Notations in + let o2l = function None -> [] | Some l -> l in + Attributes.attribute_of_list + ["skip", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] + ++ + Attributes.attribute_of_list + ["only", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] + +let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" + +let opt2list = function None -> [] | Some l -> l + +let the_kwd = ref "" +let any_kwd _ strm = + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym + | _ -> raise Stream.Failure +let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd + + +let pr_attributes _ _ _ atts = + Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) + +let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg + + + +let _ = let constructor = Pcoq.Entry.make "constructor" + and constructor_type = Pcoq.Entry.make "constructor_type" + in + let () = + Pcoq.grammar_extend record_fields + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make (Pcoq.Rule.stop) + (fun loc -> +# 151 "src/coq_elpi_arg_syntax.mlg" + [] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm G_vernac.record_field))) + (fun f loc -> +# 150 "src/coq_elpi_arg_syntax.mlg" + [f] + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm G_vernac.record_field))) + ((Pcoq.Symbol.token (Tok.PKEYWORD (";"))))) + ((Pcoq.Symbol.nterm record_fields))) + (fun fs _ f loc -> +# 149 "src/coq_elpi_arg_syntax.mlg" + f :: fs + )])]} + in let () = + Pcoq.grammar_extend inductive_constructors + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm identref))) + ((Pcoq.Symbol.nterm constructor_type))) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm constructor)) ((Pcoq.Symbol.token (Tok.PKEYWORD ("|")))) false))) + (fun l _ c id loc -> +# 157 "src/coq_elpi_arg_syntax.mlg" + c id :: l + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm constructor)) ((Pcoq.Symbol.token (Tok.PKEYWORD ("|")))) false))) + (fun l _ loc -> +# 156 "src/coq_elpi_arg_syntax.mlg" + l + )])]} + in let () = + Pcoq.grammar_extend constructor + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm identref))) + ((Pcoq.Symbol.nterm constructor_type))) + (fun c id loc -> +# 161 "src/coq_elpi_arg_syntax.mlg" + c id + )])]} + in let () = + Pcoq.grammar_extend constructor_type + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm binders))) + ((Pcoq.Symbol.rules [Pcoq.Rules.make + (Pcoq.Rule.stop) + (fun + loc -> + +# 167 "src/coq_elpi_arg_syntax.mlg" + fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) + ); + Pcoq.Rules.make + (Pcoq.Rule.next_norec + (Pcoq.Rule.next_norec + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm lconstr))) + (fun c _ + loc -> + +# 166 "src/coq_elpi_arg_syntax.mlg" + fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c + )]))) + (fun t l loc -> +# 168 "src/coq_elpi_arg_syntax.mlg" + t l + )])]} + in let () = + Pcoq.grammar_extend pipe_telescope + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("|"))))) + ((Pcoq.Symbol.nterm binders))) + (fun bl _ loc -> +# 173 "src/coq_elpi_arg_syntax.mlg" + bl + )])]} + in let () = + Pcoq.grammar_extend telescope + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm binders))) + (fun bl loc -> +# 176 "src/coq_elpi_arg_syntax.mlg" + bl + )])]} + in let () = + Pcoq.grammar_extend colon_sort + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm sort))) + (fun s _ loc -> +# 179 "src/coq_elpi_arg_syntax.mlg" + s + )])]} + in let () = + Pcoq.grammar_extend colon_constr + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD (":"))))) + ((Pcoq.Symbol.nterm lconstr))) + (fun s _ loc -> +# 182 "src/coq_elpi_arg_syntax.mlg" + s + )])]} + in let () = + Pcoq.grammar_extend coq_kwd_or_symbol + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm any_kwd))) + (fun _ loc -> +# 185 "src/coq_elpi_arg_syntax.mlg" + !the_kwd + )])]} + in () + +let (wit_elpi_arg, elpi_arg) = Tacentries.argument_extend ~name:"elpi_arg" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm coq_kwd_or_symbol))) + (fun x loc -> +# 215 "src/coq_elpi_arg_syntax.mlg" + EA.String x + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm lconstr))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ loc -> +# 213 "src/coq_elpi_arg_syntax.mlg" + EA.Term t + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Context")))) + ((Pcoq.Symbol.nterm telescope))) + (fun ty _ loc -> +# 212 "src/coq_elpi_arg_syntax.mlg" + EA.Context ty + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Axiom")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.nterm colon_constr))) + (fun t typ name _ + loc -> +# 210 "src/coq_elpi_arg_syntax.mlg" + + EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Definition")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm lconstr))) + (fun b _ t typ name + _ loc -> +# 208 "src/coq_elpi_arg_syntax.mlg" + + EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Class")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_sort)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm ident)))) + ((Pcoq.Symbol.token (CLexer.terminal "{")))) + ((Pcoq.Symbol.nterm record_fields))) + ((Pcoq.Symbol.token (CLexer.terminal "}")))) + (fun _ fs _ k _ s ps + name _ loc -> + +# 206 "src/coq_elpi_arg_syntax.mlg" + + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Record")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_sort)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm ident)))) + ((Pcoq.Symbol.token (CLexer.terminal "{")))) + ((Pcoq.Symbol.nterm record_fields))) + ((Pcoq.Symbol.token (CLexer.terminal "}")))) + (fun _ fs _ k _ s ps + name _ loc -> + +# 204 "src/coq_elpi_arg_syntax.mlg" + + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Variant")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 202 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "CoInductive")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 200 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "Inductive")))) + ((Pcoq.Symbol.nterm qualified_name))) + ((Pcoq.Symbol.nterm telescope))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm pipe_telescope)))) + ((Pcoq.Symbol.opt (Pcoq.Symbol.nterm colon_constr)))) + ((Pcoq.Symbol.token (CLexer.terminal ":=")))) + ((Pcoq.Symbol.nterm inductive_constructors))) + (fun cs _ s nups ps + name _ loc -> + +# 198 "src/coq_elpi_arg_syntax.mlg" + + EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm string))) + (fun s loc -> +# 197 "src/coq_elpi_arg_syntax.mlg" + EA.String s + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm integer))) + (fun n loc -> +# 196 "src/coq_elpi_arg_syntax.mlg" + EA.Int n + )); + (Pcoq.Production.make + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm qualified_name))) + (fun s loc -> +# 195 "src/coq_elpi_arg_syntax.mlg" + EA.String (String.concat "." (snd s)) + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun ((fun f ist v -> (ist, f ist v)) ( + +# 191 "src/coq_elpi_arg_syntax.mlg" + EA.glob_arg + )); + Tacentries.arg_subst = Tacentries.ArgSubstFun ( + +# 192 "src/coq_elpi_arg_syntax.mlg" + EA.subst_arg + ); + Tacentries.arg_interp = Tacentries.ArgInterpLegacy ( + +# 190 "src/coq_elpi_arg_syntax.mlg" + EA.interp_arg + ); + Tacentries.arg_printer = ((fun env sigma -> + +# 193 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_raw_arg env sigma + ), (fun env sigma -> + +# 194 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_glob_arg env sigma + ), (fun env sigma -> + +# 189 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> EA.pp_top_arg env sigma + )); + } +let _ = (wit_elpi_arg, elpi_arg) + +let (wit_elpi_tactic_arg, elpi_tactic_arg) = Tacentries.argument_extend ~name:"elpi_tactic_arg" + { + Tacentries.arg_parsing = + Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_term_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 229 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_term")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 228 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_int_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 227 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_int")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 226 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_string_list")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 225 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "ltac_string")))) + ((Pcoq.Symbol.token (CLexer.terminal ":")))) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ _ _ loc -> +# 224 "src/coq_elpi_arg_syntax.mlg" + EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (CLexer.terminal "(")))) + ((Pcoq.Symbol.nterm lconstr))) + ((Pcoq.Symbol.token (CLexer.terminal ")")))) + (fun _ t _ loc -> +# 223 "src/coq_elpi_arg_syntax.mlg" + EA.Term t + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm string))) + (fun s loc -> +# 222 "src/coq_elpi_arg_syntax.mlg" + EA.String s + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm integer))) + (fun n loc -> +# 221 "src/coq_elpi_arg_syntax.mlg" + EA.Int n + )); + (Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm qualified_name))) + (fun s loc -> +# 220 "src/coq_elpi_arg_syntax.mlg" + EA.String (String.concat "." (snd s)) + ))]); + Tacentries.arg_tag = Some + (Geninterp.val_tag (Genarg.topwit wit_elpi_ftactic_arg)); + Tacentries.arg_intern = + Tacentries.ArgInternWit (wit_elpi_ftactic_arg); + Tacentries.arg_subst = Tacentries.ArgSubstWit (wit_elpi_ftactic_arg); + Tacentries.arg_interp = + Tacentries.ArgInterpWit (wit_elpi_ftactic_arg); + Tacentries.arg_printer = + ((fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + ), (fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + ), (fun env sigma -> +# 0 "" +fun _ _ _ _ -> Pp.str "missing printer" + )); + } +let _ = (wit_elpi_tactic_arg, elpi_tactic_arg) + +let (wit_attributes, attributes) = Tacentries.argument_extend ~name:"attributes" + { + Tacentries.arg_parsing = Vernacextend.Arg_rules ( + []); + Tacentries.arg_tag = None; + Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v)); + Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v); + Tacentries.arg_interp = Tacentries.ArgInterpRet; + Tacentries.arg_printer = ((fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + ), (fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + ), (fun env sigma -> + +# 233 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + )); + } +let _ = (wit_attributes, attributes) + +let _ = let my_attribute_list = Pcoq.Entry.make "my_attribute_list" + and my_attribute = Pcoq.Entry.make "my_attribute" + and my_attr_value = Pcoq.Entry.make "my_attr_value" + in + let () = + Pcoq.grammar_extend my_attribute_list + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.list0sep ((Pcoq.Symbol.nterm my_attribute)) ((Pcoq.Symbol.token (Tok.PKEYWORD (",")))) false))) + (fun a loc -> +# 237 "src/coq_elpi_arg_syntax.mlg" + a + )])]} + in let () = + Pcoq.grammar_extend my_attribute + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PIDENT (Some + ("using")))))) + ((Pcoq.Symbol.nterm my_attr_value))) + (fun v _ loc -> +# 243 "src/coq_elpi_arg_syntax.mlg" + "using", v + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm ident))) + ((Pcoq.Symbol.nterm my_attr_value))) + (fun v k loc -> +# 241 "src/coq_elpi_arg_syntax.mlg" + Names.Id.to_string k, v + )])]} + in let () = + Pcoq.grammar_extend my_attr_value + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make (Pcoq.Rule.stop) + (fun loc -> +# 250 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagEmpty + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next + (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("("))))) + ((Pcoq.Symbol.nterm my_attribute_list))) + ((Pcoq.Symbol.token (Tok.PKEYWORD (")"))))) + (fun _ a _ loc -> +# 249 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagList a + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("="))))) + ((Pcoq.Symbol.token (Tok.PIDENT (None))))) + (fun v _ loc -> +# 248 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagLeaf (Attributes.FlagIdent v) + ); + Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.token (Tok.PKEYWORD ("="))))) + ((Pcoq.Symbol.nterm string))) + (fun v _ loc -> +# 247 "src/coq_elpi_arg_syntax.mlg" + Attributes.VernacFlagLeaf (Attributes.FlagString v) + )])]} + in let () = + Pcoq.grammar_extend attributes + { Pcoq.pos=None; data=[(None, None, + [Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.list1sep ((Pcoq.Symbol.nterm my_attribute)) ((Pcoq.Symbol.token (Tok.PKEYWORD (",")))) false))) + (fun atts loc -> +# 254 "src/coq_elpi_arg_syntax.mlg" + atts + )])]} + in () + +let (wit_ltac_attributes, ltac_attributes) = Tacentries.argument_extend ~name:"ltac_attributes" + { + Tacentries.arg_parsing = + Vernacextend.Arg_rules ( + [(Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.stop) + ((Pcoq.Symbol.nterm ident))) + (fun v loc -> +# 268 "src/coq_elpi_arg_syntax.mlg" + (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) + ))]); + Tacentries.arg_tag = None; + Tacentries.arg_intern = + Tacentries.ArgInternFun ((fun f ist v -> (ist, f ist v)) ( + +# 264 "src/coq_elpi_arg_syntax.mlg" + fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t + )); + Tacentries.arg_subst = Tacentries.ArgSubstFun ( + +# 265 "src/coq_elpi_arg_syntax.mlg" + Detyping.subst_glob_constr (Global.env()) + ); + Tacentries.arg_interp = + Tacentries.ArgInterpLegacy ( +# 259 "src/coq_elpi_arg_syntax.mlg" + fun ist evd x -> match DAst.get x with + | Glob_term.GVar id -> + evd.Evd.sigma, + Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) + | _ -> assert false + ); + Tacentries.arg_printer = + ((fun env sigma -> +# 266 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> Ppconstr.pr_constr_expr env sigma + ), (fun env sigma -> +# 267 "src/coq_elpi_arg_syntax.mlg" + fun _ _ _ -> Printer.pr_glob_constr_env env sigma + ), (fun env sigma -> +# 258 "src/coq_elpi_arg_syntax.mlg" + pr_attributes + )); + } +let _ = (wit_ltac_attributes, ltac_attributes) + diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg new file mode 100644 index 000000000..eea9d7c52 --- /dev/null +++ b/src/coq_elpi_arg_syntax.mlg @@ -0,0 +1,270 @@ +(* coq-elpi: Coq terms as the object language of elpi *) +(* license: GNU Lesser General Public License Version 2.1 or later *) +(* ------------------------------------------------------------------------- *) + +DECLARE PLUGIN "elpi_plugin" + +{ + +open Ltac_plugin + +open Pcoq.Constr +open Pcoq.Prim + +module EA = Coq_elpi_arg_HOAS +module U = Coq_elpi_utils + +(* Arguments ************************************************************* *) +let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) + +let trim_loc loc = + let open Loc in + { loc with bp = loc.bp + 1; ep = loc.ep - 1 } + +let idents_of loc s = + let s = String.sub s 1 (String.length s - 2) in + let l = Str.(split (regexp "[\t \n]+") s) in + List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; + Coq_elpi_utils.of_coq_loc (trim_loc loc), l + +let rec strip_curly loc s = + if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_round loc s = + if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s +let rec strip_square loc s = + if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) + else Coq_elpi_utils.of_coq_loc loc, s + +} + +ARGUMENT EXTEND elpi_string PRINTED BY { pr_elpi_string } +| [ "xxxxxxxx" ] -> { (Elpi.API.Ast.Loc.initial "dummy", "") } (* XXX To be removed when maxime's patches gets merged *) +END +GRAMMAR EXTEND Gram GLOBAL: elpi_string; +elpi_string : [ + [ s = QUOTATION "lp:" -> { + if s.[0] = '\123' then strip_curly loc s + else if s.[0] = '(' then strip_round loc s + else if s.[0] = '[' then strip_square loc s + else Coq_elpi_utils.of_coq_loc loc, s + } + | s = STRING -> { + Coq_elpi_utils.of_coq_loc loc, s + } + ]]; +END + +{ +let pr_fp _ _ _ (_,x) = U.pr_qualified_name x +let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () + +let the_qname = ref "" +let any_qname loc_fun strm = + let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> + let pos = Stream.count strm in + Stream.junk strm; + let _, ep = Loc.unloc (loc_fun pos) in + begin match Stream.peek strm with + | Some (Tok.IDENT id) -> + let bp, _ = Loc.unloc (loc_fun (pos+1)) in + if Int.equal ep bp then + (Stream.junk strm; the_qname := sym ^ id) + else + the_qname := sym + | _ -> the_qname := sym + end + | _ -> raise Stream.Failure +let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname + +} + +ARGUMENT EXTEND qualified_name PRINTED BY { pr_fp } +END +GRAMMAR EXTEND Gram GLOBAL: qualified_name; +qualified_name : + [ [ i = IDENT; s = LIST0 FIELD -> { loc, i :: s } + | "_" -> { loc, [] } + | any_qname -> { loc, Str.split_delim (Str.regexp_string ".") !the_qname } ] + ]; +END + +ARGUMENT EXTEND elpi_loc +PRINTED BY { pp_elpi_loc } +| [ ] -> { loc } +END + +{ + +let record_fields = Pcoq.Entry.create "elpi:record_fields" +let telescope = Pcoq.Entry.create "elpi:telescope" +let colon_sort = Pcoq.Entry.create "elpi:colon_sort" +let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" +let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" + +let any_attribute : Attributes.vernac_flags Attributes.attribute = + Attributes.make_attribute (fun x -> [],x) +let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = + let open Attributes.Notations in + let o2l = function None -> [] | Some l -> l in + Attributes.attribute_of_list + ["skip", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] + ++ + Attributes.attribute_of_list + ["only", + fun old -> function + | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old + | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] + +let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" + +let opt2list = function None -> [] | Some l -> l + +let the_kwd = ref "" +let any_kwd _ strm = + match Stream.peek strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym + | _ -> raise Stream.Failure +let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd + + +let pr_attributes _ _ _ atts = + Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) + +let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg + +} + +GRAMMAR EXTEND Gram + GLOBAL: record_fields inductive_constructors telescope colon_sort colon_constr coq_kwd_or_symbol pipe_telescope; + + record_fields: + [ [ f = G_vernac.record_field; ";"; fs = record_fields -> { f :: fs } + | f = G_vernac.record_field -> { [f] } + | -> { [] } + ] ] + ; + + inductive_constructors: + [ [ "|"; l = LIST1 constructor SEP "|" -> { l } + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { c id :: l } + ] ] + ; + constructor: + [ [ id = identref; c = constructor_type -> { c id } ] ] + ; + + constructor_type: + [[ l = binders; + t = [ ":"; c = lconstr -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c } + | -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) } ] + -> { t l } + ]] + ; + + pipe_telescope: + [ [ "|"; bl = binders -> { bl } ] ]; + + telescope: + [ [ bl = binders -> { bl } ] ]; + + colon_sort: + [ [ ":"; s = sort -> { s } ] ]; + + colon_constr: + [ [ ":"; s = lconstr -> { s } ] ]; + + coq_kwd_or_symbol: + [ [ any_kwd -> { !the_kwd }] ]; +END + +ARGUMENT EXTEND elpi_arg +PRINTED BY { fun _ _ _ -> EA.pp_top_arg env sigma } +INTERPRETED BY { EA.interp_arg } +GLOBALIZED BY { EA.glob_arg } +SUBSTITUTED BY { EA.subst_arg } +RAW_PRINTED BY { fun _ _ _ -> EA.pp_raw_arg env sigma } +GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma } +| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } +| [ integer(n) ] -> { EA.Int n } +| [ string(s) ] -> { EA.String s } +| [ "Inductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "CoInductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "Variant" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { + EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } +| [ "Record" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } +| [ "Class" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { + EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } +| [ "Definition" qualified_name(name) telescope(typ) colon_constr_opt(t) ":=" lconstr(b) ] -> { + EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } } +| [ "Axiom" qualified_name(name) telescope(typ) colon_constr(t) ] -> { + EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } } +| [ "Context" telescope(ty) ] -> { EA.Context ty } +| [ "(" lconstr(t) ")" ] -> { EA.Term t } + +| [ coq_kwd_or_symbol(x) ] -> { EA.String x } +END + +ARGUMENT EXTEND elpi_tactic_arg +TYPED AS elpi_ftactic_arg +| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } +| [ integer(n) ] -> { EA.Int n } +| [ string(s) ] -> { EA.String s } +| [ "(" lconstr(t) ")" ] -> { EA.Term t } +| [ "ltac_string" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_string_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_int" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +| [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) } +| [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } +END + +ARGUMENT EXTEND attributes + PRINTED BY { pr_attributes } +END +GRAMMAR EXTEND Gram GLOBAL: attributes; + my_attribute_list: + [ [ a = LIST0 my_attribute SEP "," -> { a } ] + ] + ; + my_attribute: + [ [ k = ident ; v = my_attr_value -> { Names.Id.to_string k, v } + (* Required because "ident" is declared a keyword when loading Ltac. *) + | IDENT "using" ; v = my_attr_value -> { "using", v } ] + ] + ; + my_attr_value: + [ [ "=" ; v = string -> { Attributes.VernacFlagLeaf (Attributes.FlagString v) } + | "=" ; v = IDENT -> { Attributes.VernacFlagLeaf (Attributes.FlagIdent v) } + | "(" ; a = my_attribute_list ; ")" -> { Attributes.VernacFlagList a } + | -> { Attributes.VernacFlagEmpty } ] + ] + ; + + attributes : [[ atts = LIST1 my_attribute SEP "," -> { atts } ]]; +END + +ARGUMENT EXTEND ltac_attributes + PRINTED BY { pr_attributes } + INTERPRETED BY { fun ist evd x -> match DAst.get x with + | Glob_term.GVar id -> + evd.Evd.sigma, + Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) + | _ -> assert false } + GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } + SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } + RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } + GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } +| [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } +END + diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index b87252d5e..49ae39230 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -147,7 +147,7 @@ and src_string = { sast : EC.compilation_unit } type nature = Command | Tactic | Program -let compare_src = Pervasives.compare +let compare_src = Stdlib.compare module SrcSet = Set.Make(struct type t = src let compare = compare_src end) @@ -190,7 +190,7 @@ let get_paths () = "." :: build_dir :: installed_dirs (* Setup called *) -let elpi = Pervasives.ref None +let elpi = Stdlib.ref None let elpi_builtins = API.BuiltIn.declare @@ -744,11 +744,9 @@ let loc_merge l1 l2 = try Loc.merge l1 l2 with Failure _ -> l1 -open Coq_elpi_arg_HOAS - -let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag * (cmd raw_arg, cmd glob_arg,top_arg) Genarg.ArgT.tag * (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag) -> Libobject.obj = +let in_exported_program : qualified_name -> Libobject.obj = Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED" - ~cache:(fun (_,(p,tag_loc,tag_arg,tag_attributes)) -> + ~cache:(fun (_,p) -> let p_str = String.concat "." p in match get_nature p with | Command -> @@ -757,10 +755,10 @@ let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag ~classifier:(fun _ -> Vernacextend.(VtSideff ([], VtNow))) ?entry:None [ Vernacextend.TyML (false, - Vernacextend.TyNonTerminal (Extend.TUentry tag_loc, + Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyTerminal (p_str, - Vernacextend.TyNonTerminal (Extend.TUlist0 (Extend.TUentry tag_arg), - Vernacextend.TyNonTerminal (Extend.TUentry tag_loc, + Vernacextend.TyNonTerminal (Extend.TUlist0 (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_arg)), + Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyNil)))), (fun loc0 args loc1 (* 8.14 ~loc*) ~atts -> Vernacextend.VtDefault (fun () -> run_program (loc_merge loc0 loc1) (*loc*) p ~atts args)), @@ -769,8 +767,8 @@ let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag CErrors.user_err Pp.(str "elpi: Only commands can be exported")) ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) -let export_command p tag_loc tag_arg tag_attributes = - Lib.add_anonymous_leaf (in_exported_program (p,tag_loc,tag_arg,tag_attributes)) +let export_command p = + Lib.add_anonymous_leaf (in_exported_program p) let skip ~atts:(skip,only) f x = let m rex = Str.string_match rex Coq_config.version 0 in diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 2d510fec6..fe70f9e35 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -41,10 +41,5 @@ val run_in_program : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> u val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geninterp.interp_sign -> top_tac_arg list -> unit Proofview.tactic val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Geninterp.interp_sign -> unit Proofview.tactic -val export_command : - qualified_name -> - (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag -> - (cmd raw_arg,cmd glob_arg,top_arg) Genarg.ArgT.tag -> - (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag -> - unit +val export_command : qualified_name -> unit diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 33867a52a..519c00911 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -10,96 +10,16 @@ open Stdarg open Ltac_plugin open Pcoq.Constr -open Pcoq.Prim +open Coq_elpi_arg_syntax module EV = Coq_elpi_vernacular module EA = Coq_elpi_arg_HOAS module U = Coq_elpi_utils -(* Arguments ************************************************************* *) -let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) - -let trim_loc loc = - let open Loc in - { loc with bp = loc.bp + 1; ep = loc.ep - 1 } - -let idents_of loc s = - let s = String.sub s 1 (String.length s - 2) in - let l = Str.(split (regexp "[\t \n]+") s) in - List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; - Coq_elpi_utils.of_coq_loc (trim_loc loc), l - -let rec strip_curly loc s = - if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s -let rec strip_round loc s = - if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s -let rec strip_square loc s = - if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s - -} - -ARGUMENT EXTEND elpi_string PRINTED BY { pr_elpi_string } -| [ "xxxxxxxx" ] -> { (Elpi.API.Ast.Loc.initial "dummy", "") } (* XXX To be removed when maxime's patches gets merged *) -END -GRAMMAR EXTEND Gram GLOBAL: elpi_string; -elpi_string : [ - [ s = QUOTATION "lp:" -> { - if s.[0] = '\123' then strip_curly loc s - else if s.[0] = '(' then strip_round loc s - else if s.[0] = '[' then strip_square loc s - else Coq_elpi_utils.of_coq_loc loc, s - } - | s = STRING -> { - Coq_elpi_utils.of_coq_loc loc, s - } - ]]; -END - -{ -let pr_fp _ _ _ (_,x) = U.pr_qualified_name x -let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () - -let the_qname = ref "" -let any_qname loc_fun strm = - let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in - match Stream.peek strm with - | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> - let pos = Stream.count strm in - Stream.junk strm; - let _, ep = Loc.unloc (loc_fun pos) in - begin match Stream.peek strm with - | Some (Tok.IDENT id) -> - let bp, _ = Loc.unloc (loc_fun (pos+1)) in - if Int.equal ep bp then - (Stream.junk strm; the_qname := sym ^ id) - else - the_qname := sym - | _ -> the_qname := sym - end - | _ -> raise Stream.Failure -let any_qname = Pcoq.Entry.of_parser "any_qname" any_qname - } -ARGUMENT EXTEND qualified_name PRINTED BY { pr_fp } -END -GRAMMAR EXTEND Gram GLOBAL: qualified_name; -qualified_name : - [ [ i = IDENT; s = LIST0 FIELD -> { loc, i :: s } - | "_" -> { loc, [] } - | any_qname -> { loc, Str.split_delim (Str.regexp_string ".") !the_qname } ] - ]; -END - -ARGUMENT EXTEND elpi_loc -PRINTED BY { pp_elpi_loc } -| [ ] -> { loc } -END - (* Anti-quotation ******************************************************** *) + { let pr_elpi_code _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) } @@ -145,7 +65,7 @@ GRAMMAR EXTEND Gram else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in CAst.make ~loc (Constrexpr.CHole (None, Namegen.IntroAnonymous, Some arg)) } ] - ] + ] ; END @@ -166,177 +86,6 @@ GRAMMAR EXTEND Gram END (* Syntax **************************************************************** *) -{ - -let record_fields = Pcoq.Entry.create "elpi:record_fields" -let telescope = Pcoq.Entry.create "elpi:telescope" -let colon_sort = Pcoq.Entry.create "elpi:colon_sort" -let colon_constr = Pcoq.Entry.create "elpi:colon_constr" -let pipe_telescope = Pcoq.Entry.create "elpi:pipe_telescope" -let inductive_constructors = Pcoq.Entry.create "elpi:inductive_constructors" - -let any_attribute : Attributes.vernac_flags Attributes.attribute = - Attributes.make_attribute (fun x -> [],x) -let skip_attribute : (Str.regexp list option * Str.regexp list option) Attributes.attribute = - let open Attributes.Notations in - let o2l = function None -> [] | Some l -> l in - Attributes.attribute_of_list - ["skip", - fun old -> function - | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old - | _ -> CErrors.user_err (Pp.str "Syntax error, use #[skip=\"rex\"]")] - ++ - Attributes.attribute_of_list - ["only", - fun old -> function - | Attributes.VernacFlagLeaf (Attributes.FlagString rex) -> Str.regexp rex :: o2l old - | _ -> CErrors.user_err (Pp.str "Syntax error, use #[only=\"rex\"]")] - -let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" - -let opt2list = function None -> [] | Some l -> l - -let the_kwd = ref "" -let any_kwd _ strm = - match Stream.peek strm with - | Some (Tok.KEYWORD sym) when sym <> "." -> Stream.junk strm; the_kwd := sym - | _ -> raise Stream.Failure -let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd - - -let pr_attributes _ _ _ atts = - Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts) - -let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg - -} - -GRAMMAR EXTEND Gram - GLOBAL: record_fields inductive_constructors telescope colon_sort colon_constr coq_kwd_or_symbol pipe_telescope; - - record_fields: - [ [ f = G_vernac.record_field; ";"; fs = record_fields -> { f :: fs } - | f = G_vernac.record_field -> { [f] } - | -> { [] } - ] ] - ; - - inductive_constructors: - [ [ "|"; l = LIST1 constructor SEP "|" -> { l } - | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { c id :: l } - ] ] - ; - constructor: - [ [ id = identref; c = constructor_type -> { c id } ] ] - ; - - constructor_type: - [[ l = binders; - t = [ ":"; c = lconstr -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l c } - | -> { fun l id -> id,Constrexpr_ops.mkProdCN ~loc l (CAst.make ~loc @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, None)) } ] - -> { t l } - ]] - ; - - pipe_telescope: - [ [ "|"; bl = binders -> { bl } ] ]; - - telescope: - [ [ bl = binders -> { bl } ] ]; - - colon_sort: - [ [ ":"; s = sort -> { s } ] ]; - - colon_constr: - [ [ ":"; s = lconstr -> { s } ] ]; - - coq_kwd_or_symbol: - [ [ any_kwd -> { !the_kwd }] ]; -END - -ARGUMENT EXTEND elpi_arg -PRINTED BY { fun _ _ _ -> EA.pp_top_arg env sigma } -INTERPRETED BY { EA.interp_arg } -GLOBALIZED BY { EA.glob_arg } -SUBSTITUTED BY { EA.subst_arg } -RAW_PRINTED BY { fun _ _ _ -> EA.pp_raw_arg env sigma } -GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma } -| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } -| [ integer(n) ] -> { EA.Int n } -| [ string(s) ] -> { EA.String s } -| [ "Inductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.Inductive_kw; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "CoInductive" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.CoInductive; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "Variant" qualified_name(name) telescope(ps) pipe_telescope_opt(nups) colon_constr_opt(s) ":=" inductive_constructors(cs) ] -> { - EA.IndtDecl { EA.finiteness = Vernacexpr.Variant; name = snd name; arity = s; parameters = ps; non_uniform_parameters = opt2list nups; constructors = cs } } -| [ "Record" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { - EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } -| [ "Class" qualified_name(name) telescope(ps) colon_sort_opt(s) ":=" ident_opt(k) "{" record_fields(fs) "}" ] -> { - EA.RecordDecl { EA.name = snd name; sort = s; parameters = ps; constructor = k; fields = fs } } -| [ "Definition" qualified_name(name) telescope(typ) colon_constr_opt(t) ":=" lconstr(b) ] -> { - EA.ConstantDecl { EA.name = snd name; typ = (typ,t); body = Some b } } -| [ "Axiom" qualified_name(name) telescope(typ) colon_constr(t) ] -> { - EA.ConstantDecl { EA.name = snd name; typ = (typ,Some t); body = None } } -| [ "Context" telescope(ty) ] -> { EA.Context ty } -| [ "(" lconstr(t) ")" ] -> { EA.Term t } - -| [ coq_kwd_or_symbol(x) ] -> { EA.String x } -END - -ARGUMENT EXTEND elpi_tactic_arg -TYPED AS elpi_ftactic_arg -| [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) } -| [ integer(n) ] -> { EA.Int n } -| [ string(s) ] -> { EA.String s } -| [ "(" lconstr(t) ")" ] -> { EA.Term t } -| [ "ltac_string" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_string_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_int" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -| [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) } -| [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.LTac(EA.List EA.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) } -END - -ARGUMENT EXTEND attributes - PRINTED BY { pr_attributes } -END -GRAMMAR EXTEND Gram GLOBAL: attributes; - my_attribute_list: - [ [ a = LIST0 my_attribute SEP "," -> { a } ] - ] - ; - my_attribute: - [ [ k = ident ; v = my_attr_value -> { Names.Id.to_string k, v } - (* Required because "ident" is declared a keyword when loading Ltac. *) - | IDENT "using" ; v = my_attr_value -> { "using", v } ] - ] - ; - my_attr_value: - [ [ "=" ; v = string -> { Attributes.VernacFlagLeaf (Attributes.FlagString v) } - | "=" ; v = IDENT -> { Attributes.VernacFlagLeaf (Attributes.FlagIdent v) } - | "(" ; a = my_attribute_list ; ")" -> { Attributes.VernacFlagList a } - | -> { Attributes.VernacFlagEmpty } ] - ] - ; - - attributes : [[ atts = LIST1 my_attribute SEP "," -> { atts } ]]; -END - -ARGUMENT EXTEND ltac_attributes - PRINTED BY { pr_attributes } - INTERPRETED BY { fun ist evd x -> match DAst.get x with - | Glob_term.GVar id -> - evd.Evd.sigma, - Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) - | _ -> assert false } - GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } - SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } - RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } - GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } -| [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } -END - VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF | #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) ] -> { EV.skip ~atts EV.accumulate_files s } @@ -384,12 +133,8 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([ { EV.run_in_program s } | [ "Elpi" "Query" qualified_name(p) elpi_string(s) ] -> { EV.run_in_program ~program:(snd p) s } -| [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } -> { - EV.export_command (snd p) - (Genarg.get_arg_tag wit_elpi_loc) - (Genarg.get_arg_tag wit_elpi_arg) - (Genarg.get_arg_tag wit_attributes) - } +| [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } -> + { EV.export_command (snd p) } | #[ atts = any_attribute ] [ "Elpi" qualified_name(p) elpi_arg_list(args) ] -> { EV.run_program (fst p) (snd p) ~atts args } diff --git a/src/elpi_plugin.mlpack b/src/elpi_plugin.mlpack index 604ec968f..02905c7e6 100644 --- a/src/elpi_plugin.mlpack +++ b/src/elpi_plugin.mlpack @@ -4,6 +4,7 @@ Coq_elpi_HOAS Coq_elpi_glob_quotation Coq_elpi_name_quotation Coq_elpi_arg_HOAS +Coq_elpi_arg_syntax Coq_elpi_builtins_HOAS Coq_elpi_builtins Coq_elpi_vernacular From 9fbe73b4290fa2fc37c6c56206fe3940a03aab74 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Jun 2021 18:33:58 +0200 Subject: [PATCH 02/22] Tactic abbreviations in terms --- coq-builtin.elpi | 15 ++++++++++ src/coq_elpi_builtins.ml | 60 ++++++++++++++++++++++++++++++++++++++++ tests/test_tactic.v | 15 ++++++++-- 3 files changed, 88 insertions(+), 2 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index b19a39b73..0e1cd77e3 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -927,6 +927,21 @@ external pred coq.notation.abbreviation i:abbreviation, i:list term, external pred coq.notation.abbreviation-body i:abbreviation, o:int, o:term. +% [coq.notation.add-abbreviation-for-tactic Name TacticName FixedArgs] +% Declares a parsing rule similar to +% Notation Name X1..Xn := ltac:(elpi TacticName FixedArgs (X1)..(Xn)) +% so that Name can be used in the middle of a term to invoke an +% elpi tactic. While FixedArgs can contain str, int, and trm all +% other arguments will necessarily be terms, and their number is +% not fixed (the user can pass as many as he likes). +% Name becomes a keyword. +% The tactic receives as the elpi.loc attribute the precise location +% at which the term is written (unlike if a regular abbreviation was +% declared by hand). +external pred coq.notation.add-abbreviation-for-tactic i:string, + i:string, + i:list argument. + % Generic attribute value kind attribute-value type. type leaf-str string -> attribute-value. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index fa588a24a..1e2b43c62 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -305,6 +305,14 @@ let goal : ( (Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context * Evar.t * Coq_elpi_a state, (ctx,k,args), gls1 @ gls2); } +let tactic_arg : (Coq_elpi_arg_HOAS.coq_arg, Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context, API.Data.constraints) CConv.t = { + CConv.ty = Conv.TyName "argument"; + pp_doc = (fun fmt () -> ()); + pp = (fun fmt _ -> Format.fprintf fmt "TODO"); + embed = (fun ~depth _ _ _ _ -> assert false); + readback = Coq_elpi_arg_HOAS.in_coq_arg; +} + let id = { B.string with API.Conversion.ty = Conv.TyName "id"; pp_doc = (fun fmt () -> @@ -2009,6 +2017,58 @@ Supported attributes: )), DocAbove); + MLCode(Pred("coq.notation.add-abbreviation-for-tactic", + In(B.string,"Name", + In(B.string,"TacticName", + CIn(CConv.(!>>) B.list tactic_arg,"FixedArgs", + Full(proof_context, {|Declares a parsing rule similar to + Notation Name X1..Xn := ltac:(elpi TacticName FixedArgs (X1)..(Xn)) +so that Name can be used in the middle of a term to invoke an +elpi tactic. While FixedArgs can contain str, int, and trm all +other arguments will necessarily be terms, and their number is +not fixed (the user can pass as many as he likes). +Name becomes a keyword. +The tactic receives as the elpi.loc attribute the precise location +at which the term is written (unlike if a regular abbreviation was +declared by hand).|})))), + (fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state -> + let sigma = get_sigma state in + let more_args = more_args |> List.map (function + | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Int n + | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.String s + | Coq_elpi_arg_HOAS.Ctrm t -> + let env = get_global_env state in (* no proof context allowed *) + let expr = Constrextern.extern_constr env sigma t in + let expr = + let rec aux () ({ CAst.v } as orig) = match v with + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in + aux () expr in + Coq_elpi_arg_HOAS.Term expr) in + let open Ltac_plugin in + Pcoq.grammar_extend Pcoq.Constr.term + { Pcoq.pos = Some (Gramlib.Gramext.Level "0"); + data = [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PKEYWORD name)))) + (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.term))) + (fun args _ loc -> + let tac = + let open Tacexpr in + let elpi_tac = { + mltac_plugin = "elpi_plugin"; + mltac_tactic = "elpi_tac"; } in + let elpi_tac_entry = { + mltac_name = elpi_tac; + mltac_index = 0; } in + let tacname = loc, [tacname] in + let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in + let args = args |> List.map (fun arg -> Coq_elpi_arg_HOAS.Term arg) in + let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in + (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in + CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac))) ])] }; + state, (), []))), + DocAbove); + MLData attribute_value; MLData attribute; diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 5b6f3ca7d..38c891fa2 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -284,10 +284,13 @@ Abort. Elpi Tactic test_m. Elpi Accumulate lp:{{ type type-arg open-tactic. - type-arg (goal _ _ _ _ [trm T] as G) GL :- + type-arg (goal _ _ _ _ [trm T|_] as G) GL :- refine T G GL. + type-arg (goal A B C D [X|R] as G) GL :- + coq.say "skip" X, + type-arg (goal A B C D R) GL. - msolve GL New :- + msolve GL New :- coq.say {attributes}, coq.ltac.all (coq.ltac.open type-arg) GL New. }}. Elpi Typecheck. @@ -297,4 +300,12 @@ split; intro x. all: elpi test_m (@eq_refl _ x). Qed. +Elpi Query lp:{{ + coq.notation.add-abbreviation-for-tactic "xxx" "test_m" [int 1, str "33", trm {{bool}}] +}}. + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (xxx (@eq_refl _ x)). +Qed. From 65b8ef02e04805fd51e154554bec19245815b859 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Jun 2021 11:05:09 +0200 Subject: [PATCH 03/22] update changelog --- Changelog.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Changelog.md b/Changelog.md index d171f4e9d..d98413f2d 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,15 @@ # Changelog +## [1.10.4] - 22-06-2021 + +Requires Elpi 1.13.6 and Coq 8.13. + +### API +- New `coq.notation.add-abbreviation-for-tactic` to add a parsing rule + for a tactic-in-term, along the lines of + `Notation foo := ltac:(elpi mytactic arguments)` + but passing `mytactic` the correct `elpi.loc` of invocation. + ## [1.10.3] - 18-06-2021 Requires Elpi 1.13.6 and Coq 8.13. From 5b64cfb27b639f22648e23fd85c4f15608a05e86 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Jun 2021 11:16:58 +0200 Subject: [PATCH 04/22] fix warning --- tests/test_tactic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 38c891fa2..6340ad37b 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -286,7 +286,7 @@ Elpi Accumulate lp:{{ type type-arg open-tactic. type-arg (goal _ _ _ _ [trm T|_] as G) GL :- refine T G GL. - type-arg (goal A B C D [X|R] as G) GL :- + type-arg (goal A B C D [X|R]) GL :- coq.say "skip" X, type-arg (goal A B C D R) GL. From fcffe289cd3975ef86392e6629b3b6a5605b1f2a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Jun 2021 15:55:12 +0200 Subject: [PATCH 05/22] take a list of strings to qualify the tac/term + libobject --- coq-builtin.elpi | 4 +- src/coq_elpi_arg_HOAS.ml | 11 +++- src/coq_elpi_arg_HOAS.mli | 14 +++--- src/coq_elpi_builtins.ml | 103 ++++++++++++++++++++++++++------------ tests/test_tactic.v | 8 ++- 5 files changed, 96 insertions(+), 44 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 0e1cd77e3..aa2302c75 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -934,11 +934,11 @@ external pred coq.notation.abbreviation-body i:abbreviation, o:int, % elpi tactic. While FixedArgs can contain str, int, and trm all % other arguments will necessarily be terms, and their number is % not fixed (the user can pass as many as he likes). -% Name becomes a keyword. +% Name = ["Foo", "Bar", "x"] becomes "Foo.Bar.x" in Coq's term grammar. % The tactic receives as the elpi.loc attribute the precise location % at which the term is written (unlike if a regular abbreviation was % declared by hand). -external pred coq.notation.add-abbreviation-for-tactic i:string, +external pred coq.notation.add-abbreviation-for-tactic i:list string, i:string, i:list argument. diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 9b3fea423..eb9698aeb 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -107,7 +107,7 @@ type ('a,'b,'c,'d,'e,'f,_) arg = | Context : 'e -> ('a,'b,'c,'d,'e,'f,cmd) arg type 'a raw_arg = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_ltac_arg,'a) arg -type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,glob_ltac_arg,'a) arg +type ('a,'b) glob_arg = ('b, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg @@ -342,7 +342,14 @@ let subst_tac_arg mod_subst = function Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t) | LTac(ty,t) -> LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t)) - +let subst_tac_arg_glob mod_subst = function + | Int _ as x -> x + | String _ as x -> x + | Term t -> + Term (Detyping.subst_glob_constr (Global.env()) mod_subst t) + | LTac(ty,t) -> + LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t)) + let interp_arg ist evd = function | Int _ as x -> evd.Evd.sigma, x | String _ as x -> evd.Evd.sigma, x diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index bfe3aa660..b0335d1ea 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -82,19 +82,21 @@ type ('a,'b,'c,'d,'e,'f,_) arg = | Context : 'e -> ('a,'b,'c,'d,'e,'f,cmd) arg type 'a raw_arg = (raw_term, raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_term,'a) arg -type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg +type ('a,'b) glob_arg = ('b, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg val pp_raw_arg : Environ.env -> Evd.evar_map -> cmd raw_arg -> Pp.t -val pp_glob_arg : Environ.env -> Evd.evar_map -> cmd glob_arg -> Pp.t +val pp_glob_arg : Environ.env -> Evd.evar_map -> (cmd,glob_term) glob_arg -> Pp.t val pp_top_arg : Environ.env -> Evd.evar_map -> top_arg -> Pp.t -val glob_arg : Genintern.glob_sign -> cmd raw_arg -> cmd glob_arg -val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> cmd glob_arg -> Evd.evar_map * top_arg -val subst_arg : Mod_subst.substitution -> cmd glob_arg -> cmd glob_arg +val glob_arg : Genintern.glob_sign -> cmd raw_arg -> (cmd,glob_term) glob_arg +val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> (cmd,glob_term) glob_arg -> Evd.evar_map * top_arg +val subst_arg : Mod_subst.substitution -> (cmd,glob_term) glob_arg -> (cmd,glob_term) glob_arg -val wit_elpi_ftactic_arg : (tac raw_arg, tac glob_arg, top_tac_arg) Genarg.genarg_type +val subst_tac_arg_glob : Mod_subst.substitution -> (tac,Glob_term.glob_constr) glob_arg -> (tac,Glob_term.glob_constr) glob_arg + +val wit_elpi_ftactic_arg : (tac raw_arg, (tac,glob_term) glob_arg, top_tac_arg) Genarg.genarg_type (* for tactics *) val in_elpi_tac_arg : diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 1e2b43c62..ffe6dde4a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -862,6 +862,71 @@ let add_axiom_or_variable api id sigma ty local = +let load_notation _ _ = () + + +let rec gbpmp = fun f -> function + | [x] -> Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a) + | x :: xs -> + let r, f = gbpmp f xs in + Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a) + | [] -> assert false + +let open_notation i (_, (name,tacname,more_args)) = + if Int.equal i 1 then begin + let action args loc = + let open Ltac_plugin in + let tac = + let open Tacexpr in + let elpi_tac = { + mltac_plugin = "elpi_plugin"; + mltac_tactic = "elpi_tac"; } in + let elpi_tac_entry = { + mltac_name = elpi_tac; + mltac_index = 0; } in + let more_args = more_args |> List.map (function + | Coq_elpi_arg_HOAS.Int _ as t -> t + | Coq_elpi_arg_HOAS.String _ as t -> t + | Coq_elpi_arg_HOAS.Term t -> + let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in + let rec aux () ({ CAst.v } as orig) = match v with + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in + Coq_elpi_arg_HOAS.Term (aux () expr) + | _ -> assert false) in + let tacname = loc, [tacname] in + let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in + let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Term arg) in + let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in + (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in + CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac)) in + let rule, action = gbpmp (Obj.magic action) name in + Pcoq.grammar_extend Pcoq.Constr.term { + Pcoq.pos = Some (Gramlib.Gramext.Before "10"); + data = [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) + (Obj.magic action) + ])] }; + + end + +let cache_notation o = + load_notation 1 o; + open_notation 1 o + +let subst_notation (subst, (name,tacname,args)) = (name,tacname,List.map (Coq_elpi_arg_HOAS.subst_tac_arg_glob subst) args) + +let classify_notation nobj = Libobject.Substitute nobj + +let inAbbreviationForTactic : (string list * string * (Coq_elpi_arg_HOAS.tac,Glob_term.glob_constr) Coq_elpi_arg_HOAS.glob_arg list) -> Libobject.obj = + Libobject.declare_object {(Libobject.default_object "elpi:abbreviation_for_tactic") with + Libobject.open_function = Libobject.simple_open open_notation; + cache_function = cache_notation; + subst_function = subst_notation; + load_function = load_notation; + classify_function = classify_notation} + + (*****************************************************************************) (*****************************************************************************) @@ -2018,7 +2083,7 @@ Supported attributes: DocAbove); MLCode(Pred("coq.notation.add-abbreviation-for-tactic", - In(B.string,"Name", + In(B.list B.string,"Name", In(B.string,"TacticName", CIn(CConv.(!>>) B.list tactic_arg,"FixedArgs", Full(proof_context, {|Declares a parsing rule similar to @@ -2027,45 +2092,19 @@ so that Name can be used in the middle of a term to invoke an elpi tactic. While FixedArgs can contain str, int, and trm all other arguments will necessarily be terms, and their number is not fixed (the user can pass as many as he likes). -Name becomes a keyword. +Name = ["Foo", "Bar", "x"] becomes "Foo.Bar.x" in Coq's term grammar. The tactic receives as the elpi.loc attribute the precise location at which the term is written (unlike if a regular abbreviation was declared by hand).|})))), (fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state -> let sigma = get_sigma state in + let env = get_global_env state in let more_args = more_args |> List.map (function | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Int n | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.String s - | Coq_elpi_arg_HOAS.Ctrm t -> - let env = get_global_env state in (* no proof context allowed *) - let expr = Constrextern.extern_constr env sigma t in - let expr = - let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) - | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in - aux () expr in - Coq_elpi_arg_HOAS.Term expr) in - let open Ltac_plugin in - Pcoq.grammar_extend Pcoq.Constr.term - { Pcoq.pos = Some (Gramlib.Gramext.Level "0"); - data = [ (None, None, [ Pcoq.Production.make - (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PKEYWORD name)))) - (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.term))) - (fun args _ loc -> - let tac = - let open Tacexpr in - let elpi_tac = { - mltac_plugin = "elpi_plugin"; - mltac_tactic = "elpi_tac"; } in - let elpi_tac_entry = { - mltac_name = elpi_tac; - mltac_index = 0; } in - let tacname = loc, [tacname] in - let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in - let args = args |> List.map (fun arg -> Coq_elpi_arg_HOAS.Term arg) in - let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in - (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in - CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac))) ])] }; + | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Term (Coq_elpi_utils.detype env sigma t)) in + let name = List.rev name in + Lib.add_anonymous_leaf @@ inAbbreviationForTactic (name, tacname, more_args); state, (), []))), DocAbove); diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 6340ad37b..664887f6b 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -301,11 +301,15 @@ all: elpi test_m (@eq_refl _ x). Qed. Elpi Query lp:{{ - coq.notation.add-abbreviation-for-tactic "xxx" "test_m" [int 1, str "33", trm {{bool}}] + coq.notation.add-abbreviation-for-tactic ["XX", "xxx"] "test_m" [int 1, str "33", trm {{bool}}] }}. +Print Grammar constr. + Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). split; intro x. -all: exact (xxx (@eq_refl _ x)). +all: exact (XX.xxx (@eq_refl _ x)). Qed. +Check forall xxx : nat, forall XX : bool, True. + From 6d2433b4206d8cd2bc3d3408a6970a1b1f8d60a5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jun 2021 15:34:52 +0200 Subject: [PATCH 06/22] @pplevel! --- Changelog.md | 4 +++- coq-builtin.elpi | 22 ++++++++++++++++++++++ elpi/coq-HOAS.elpi | 1 + src/coq_elpi_HOAS.ml | 4 ++++ src/coq_elpi_HOAS.mli | 1 + src/coq_elpi_builtins.ml | 4 +++- src/coq_elpi_builtins_HOAS.ml | 18 ++++++++++++++++++ 7 files changed, 52 insertions(+), 2 deletions(-) diff --git a/Changelog.md b/Changelog.md index d98413f2d..eaacf9e99 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,6 +1,6 @@ # Changelog -## [1.10.4] - 22-06-2021 +## [1.10.4] - 23-06-2021 Requires Elpi 1.13.6 and Coq 8.13. @@ -9,6 +9,8 @@ Requires Elpi 1.13.6 and Coq 8.13. for a tactic-in-term, along the lines of `Notation foo := ltac:(elpi mytactic arguments)` but passing `mytactic` the correct `elpi.loc` of invocation. +- New `@pplevel!` attribute to control outermost parentheses in `coq.term->pp` + and similar ## [1.10.3] - 18-06-2021 diff --git a/coq-builtin.elpi b/coq-builtin.elpi index aa2302c75..aff25ef51 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -42,6 +42,7 @@ pred attributes o:list attribute. % solve % Where [str "foo", int 3, trm (app[f,x])] is part of . % The encoding of goals is described below. +% msolve is for tactics that operate on multiple goals (called via all: ). pred solve i:goal, o:list sealed-goal. pred msolve i:list sealed-goal, o:list sealed-goal. @@ -323,6 +324,22 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal. % Ltac1 code on that term (e.g. to call vm_compute, see also the example % on the reflexive tactic). +% ----- Multi goals tactics. ---- +% Coq provides goal selectors, such as all:, to pass to a tactic more than one +% goal. In order to write such a tactic, Coq-Elpi provides another entry point +% called msolve. To be precise, if there are two goals under focus, say and +% , then all: elpi tac runs the following query +% +% msolve [,] NewGoals ; % note the disjunction +% coq.ltac.all (coq.ltac.open solve) [,] NewGoals +% +% So, if msolve has no clause, Coq-Elpi will use solve on all the goals +% independently. If msolve has a cluse, then it can manipulate the entire list +% of sealed goals. Note that the argument is in both and but +% it is interpreted in both contexts independently. If both goals have a proof +% variable named "x" then passing (@eq_refl _ x) as equips both goals with +% a (raw) proof that "x = x", no matter what their type is. + % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Declarations for Coq's API (environment read/write access, etc). % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -341,6 +358,7 @@ macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width macro @ppall! :- get-option "coq:pp" "all". % printing all macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents +macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses) macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute @@ -1118,6 +1136,8 @@ external pred coq.modtypath->path i:modtypath, o:list string. % - @ppwidth! N (default 80, max line length) % - @ppall! (default: false, prints all details) % - @ppmost! (default: false, prints most details) +% - @pplevel! (default: _, prints parentheses to reach that level, 200 = +% off) % - @holes! (default: false, prints evars as _) external pred coq.term->string i:term, o:string. @@ -1126,6 +1146,8 @@ external pred coq.term->string i:term, o:string. % Supported attributes: % - @ppall! (default: false, prints all details) % - @ppmost! (default: false, prints most details) +% - @pplevel! (default: _, prints parentheses to reach that level, 200 = +% off) % - @holes! (default: false, prints evars as _) external pred coq.term->pp i:term, o:coq.pp. diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 05c6ba854..dd4b1bc92 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -343,6 +343,7 @@ macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width macro @ppall! :- get-option "coq:pp" "all". % printing all macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents +macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses) macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 71a847daf..66695f074 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -82,6 +82,7 @@ type options = { failsafe : bool; (* don't fail, e.g. we are trying to print a term *) ppwidth : int; pp : ppoption; + pplevel : Constrexpr.entry_relative_level; using : string option; } @@ -93,6 +94,7 @@ let default_options = { failsafe = false; ppwidth = 80; pp = Normal; + pplevel = Constrexpr.LevelSome; using = None; } @@ -673,6 +675,7 @@ let get_options ~depth hyps state = else if s = Some "most" then Most else Normal in let ppwidth = function Some i -> i | None -> 80 in + let pplevel = function None -> Constrexpr.LevelSome | Some i -> Constrexpr.LevelLe i in let get_pair_option fst snd name = try let t, depth = API.Data.StrMap.find name map in @@ -698,6 +701,7 @@ let get_options ~depth hyps state = failsafe = false; ppwidth = ppwidth @@ get_int_option "coq:ppwidth"; pp = pp @@ get_string_option "coq:pp"; + pplevel = pplevel @@ get_int_option "coq:pplevel"; using = get_string_option "coq:using"; } diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index d4f20bbce..aa98f3d99 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -24,6 +24,7 @@ type options = { failsafe : bool; (* readback is resilient to illformed terms *) ppwidth : int; pp : ppoption; + pplevel : Constrexpr.entry_relative_level; using : string option; } diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ffe6dde4a..8d4c92457 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -96,7 +96,7 @@ let pr_econstr_env options env sigma t = | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in if options.hoas_holes = Some Heuristic then aux () expr else expr in - Ppconstr.pr_constr_expr env sigma expr) + Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) let tactic_mode = ref false let on_global_state api thunk = (); (fun state -> @@ -2612,6 +2612,7 @@ Supported attributes: - @ppwidth! N (default 80, max line length) - @ppall! (default: false, prints all details) - @ppmost! (default: false, prints most details) +- @pplevel! (default: _, prints parentheses to reach that level, 200 = off) - @holes! (default: false, prints evars as _)|}))), (fun t _ ~depth proof_context constraints state -> let sigma = get_sigma state in @@ -2626,6 +2627,7 @@ Supported attributes: Supported attributes: - @ppall! (default: false, prints all details) - @ppmost! (default: false, prints most details) +- @pplevel! (default: _, prints parentheses to reach that level, 200 = off) - @holes! (default: false, prints evars as _)|}))), (fun t _ ~depth proof_context constraints state -> let sigma = get_sigma state in diff --git a/src/coq_elpi_builtins_HOAS.ml b/src/coq_elpi_builtins_HOAS.ml index 3ef4b5cb1..533953889 100644 --- a/src/coq_elpi_builtins_HOAS.ml +++ b/src/coq_elpi_builtins_HOAS.ml @@ -29,6 +29,7 @@ pred attributes o:list attribute. % solve % Where [str "foo", int 3, trm (app[f,x])] is part of . % The encoding of goals is described below. +% msolve is for tactics that operate on multiple goals (called via all: ). pred solve i:goal, o:list sealed-goal. pred msolve i:list sealed-goal, o:list sealed-goal. @@ -310,6 +311,22 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal. % Ltac1 code on that term (e.g. to call vm_compute, see also the example % on the reflexive tactic). +% ----- Multi goals tactics. ---- +% Coq provides goal selectors, such as all:, to pass to a tactic more than one +% goal. In order to write such a tactic, Coq-Elpi provides another entry point +% called msolve. To be precise, if there are two goals under focus, say and +% , then all: elpi tac runs the following query +% +% msolve [,] NewGoals ; % note the disjunction +% coq.ltac.all (coq.ltac.open solve) [,] NewGoals +% +% So, if msolve has no clause, Coq-Elpi will use solve on all the goals +% independently. If msolve has a cluse, then it can manipulate the entire list +% of sealed goals. Note that the argument is in both and but +% it is interpreted in both contexts independently. If both goals have a proof +% variable named "x" then passing (@eq_refl _ x) as equips both goals with +% a (raw) proof that "x = x", no matter what their type is. + % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Declarations for Coq's API (environment read/write access, etc). % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -328,6 +345,7 @@ macro @primitive! :- get-option "coq:primitive" tt. % primitive records macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width macro @ppall! :- get-option "coq:pp" "all". % printing all macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents +macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses) macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute From 00443f87cbad495f9e8a46f9d5cb4beb0cef48e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 14:30:47 +0200 Subject: [PATCH 07/22] fix tac name --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 8d4c92457..f2119f94d 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -894,7 +894,7 @@ let open_notation i (_, (name,tacname,more_args)) = | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in Coq_elpi_arg_HOAS.Term (aux () expr) | _ -> assert false) in - let tacname = loc, [tacname] in + let tacname = loc, Coq_elpi_utils.string_split_on_char '.' tacname in let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Term arg) in let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in From e037e821b48c7dc810a5b405def04683d4f6a685 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 14:34:36 +0200 Subject: [PATCH 08/22] cleanup --- coq-builtin.elpi | 3 +-- src/coq_elpi_builtins.ml | 5 ++--- tests/test_tactic.v | 6 +++--- 3 files changed, 6 insertions(+), 8 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index aff25ef51..a0fc7e256 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -952,11 +952,10 @@ external pred coq.notation.abbreviation-body i:abbreviation, o:int, % elpi tactic. While FixedArgs can contain str, int, and trm all % other arguments will necessarily be terms, and their number is % not fixed (the user can pass as many as he likes). -% Name = ["Foo", "Bar", "x"] becomes "Foo.Bar.x" in Coq's term grammar. % The tactic receives as the elpi.loc attribute the precise location % at which the term is written (unlike if a regular abbreviation was % declared by hand). -external pred coq.notation.add-abbreviation-for-tactic i:list string, +external pred coq.notation.add-abbreviation-for-tactic i:string, i:string, i:list argument. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index f2119f94d..813e4f1fb 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2083,7 +2083,7 @@ Supported attributes: DocAbove); MLCode(Pred("coq.notation.add-abbreviation-for-tactic", - In(B.list B.string,"Name", + In(B.string,"Name", In(B.string,"TacticName", CIn(CConv.(!>>) B.list tactic_arg,"FixedArgs", Full(proof_context, {|Declares a parsing rule similar to @@ -2092,7 +2092,6 @@ so that Name can be used in the middle of a term to invoke an elpi tactic. While FixedArgs can contain str, int, and trm all other arguments will necessarily be terms, and their number is not fixed (the user can pass as many as he likes). -Name = ["Foo", "Bar", "x"] becomes "Foo.Bar.x" in Coq's term grammar. The tactic receives as the elpi.loc attribute the precise location at which the term is written (unlike if a regular abbreviation was declared by hand).|})))), @@ -2103,7 +2102,7 @@ declared by hand).|})))), | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Int n | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.String s | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Term (Coq_elpi_utils.detype env sigma t)) in - let name = List.rev name in + let name = List.rev (Coq_elpi_utils.string_split_on_char '.' name) in Lib.add_anonymous_leaf @@ inAbbreviationForTactic (name, tacname, more_args); state, (), []))), DocAbove); diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 664887f6b..c1f1cc830 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -281,7 +281,7 @@ Abort. (* ***************** *) -Elpi Tactic test_m. +Elpi Tactic test.m. Elpi Accumulate lp:{{ type type-arg open-tactic. type-arg (goal _ _ _ _ [trm T|_] as G) GL :- @@ -297,11 +297,11 @@ Elpi Typecheck. Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). split; intro x. -all: elpi test_m (@eq_refl _ x). +all: elpi test.m (@eq_refl _ x). Qed. Elpi Query lp:{{ - coq.notation.add-abbreviation-for-tactic ["XX", "xxx"] "test_m" [int 1, str "33", trm {{bool}}] + coq.notation.add-abbreviation-for-tactic "XX.xxx" "test.m" [int 1, str "33", trm {{bool}}] }}. Print Grammar constr. From 90723efc46e7fbd5cf6de857287bc9e0f9345b76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 15:28:55 +0200 Subject: [PATCH 09/22] Expor for tactics --- README.md | 7 ++- coq-builtin.elpi | 2 + src/coq_elpi_builtins.ml | 121 +++++++++++++++++++------------------ src/coq_elpi_builtins.mli | 7 ++- src/coq_elpi_vernacular.ml | 22 ++++--- tests/test_tactic.v | 24 ++++++++ 6 files changed, 111 insertions(+), 72 deletions(-) diff --git a/README.md b/README.md index f90e56c3e..5da06828d 100644 --- a/README.md +++ b/README.md @@ -214,8 +214,11 @@ where: is how you invoke a tactic. - `Elpi Export ` makes it possible to invoke command `` without - the `Elpi` prefix. Exporting tactics is not supported, but one can define - a `Tactic Notation` to give the tactic a better syntax and a shorter name. + the `Elpi` prefix or invoke tactic `` in the middle of a term just + writing ` args` instead of `ltac:(elpi args)`. Note that in + the case of tactics, all arguments are considered to be terms. + Moreover, remember that one can use `Tactic Notation` to give the tactic a + better syntax and a shorter name when used in the middle of a proof script. where `` can be: diff --git a/coq-builtin.elpi b/coq-builtin.elpi index a0fc7e256..908a423d1 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -955,6 +955,8 @@ external pred coq.notation.abbreviation-body i:abbreviation, o:int, % The tactic receives as the elpi.loc attribute the precise location % at which the term is written (unlike if a regular abbreviation was % declared by hand). +% A call to coq.notation.add-abbreviation-for-tactic TacName TacName [] +% is equivalent to Elpi Export TacName. external pred coq.notation.add-abbreviation-for-tactic i:string, i:string, i:list argument. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 813e4f1fb..92f542ebf 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -860,9 +860,11 @@ let add_axiom_or_variable api id sigma ty local = gr ;; - - -let load_notation _ _ = () +type tac_abbrev = { + abbrev_name : qualified_name; + tac_name : qualified_name; + tac_fixed_args : (Coq_elpi_arg_HOAS.tac, Glob_term.glob_constr) Coq_elpi_arg_HOAS.glob_arg list; +} let rec gbpmp = fun f -> function @@ -872,61 +874,57 @@ let rec gbpmp = fun f -> function Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a) | [] -> assert false -let open_notation i (_, (name,tacname,more_args)) = - if Int.equal i 1 then begin - let action args loc = - let open Ltac_plugin in - let tac = - let open Tacexpr in - let elpi_tac = { - mltac_plugin = "elpi_plugin"; - mltac_tactic = "elpi_tac"; } in - let elpi_tac_entry = { - mltac_name = elpi_tac; - mltac_index = 0; } in - let more_args = more_args |> List.map (function - | Coq_elpi_arg_HOAS.Int _ as t -> t - | Coq_elpi_arg_HOAS.String _ as t -> t - | Coq_elpi_arg_HOAS.Term t -> - let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in - let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) - | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in - Coq_elpi_arg_HOAS.Term (aux () expr) - | _ -> assert false) in - let tacname = loc, Coq_elpi_utils.string_split_on_char '.' tacname in - let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in - let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Term arg) in - let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in - (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in - CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac)) in - let rule, action = gbpmp (Obj.magic action) name in - Pcoq.grammar_extend Pcoq.Constr.term { - Pcoq.pos = Some (Gramlib.Gramext.Before "10"); - data = [ (None, None, [ Pcoq.Production.make - (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) - (Obj.magic action) - ])] }; - - end - -let cache_notation o = - load_notation 1 o; - open_notation 1 o - -let subst_notation (subst, (name,tacname,args)) = (name,tacname,List.map (Coq_elpi_arg_HOAS.subst_tac_arg_glob subst) args) - -let classify_notation nobj = Libobject.Substitute nobj - -let inAbbreviationForTactic : (string list * string * (Coq_elpi_arg_HOAS.tac,Glob_term.glob_constr) Coq_elpi_arg_HOAS.glob_arg list) -> Libobject.obj = - Libobject.declare_object {(Libobject.default_object "elpi:abbreviation_for_tactic") with - Libobject.open_function = Libobject.simple_open open_notation; - cache_function = cache_notation; - subst_function = subst_notation; - load_function = load_notation; - classify_function = classify_notation} +let cache_abbrev_for_tac (_, { abbrev_name; tac_name = tacname; tac_fixed_args = more_args }) = + let action args loc = + let open Ltac_plugin in + let tac = + let open Tacexpr in + let elpi_tac = { + mltac_plugin = "elpi_plugin"; + mltac_tactic = "elpi_tac"; } in + let elpi_tac_entry = { + mltac_name = elpi_tac; + mltac_index = 0; } in + let more_args = more_args |> List.map (function + | Coq_elpi_arg_HOAS.Int _ as t -> t + | Coq_elpi_arg_HOAS.String _ as t -> t + | Coq_elpi_arg_HOAS.Term t -> + let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in + let rec aux () ({ CAst.v } as orig) = match v with + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in + Coq_elpi_arg_HOAS.Term (aux () expr) + | _ -> assert false) in + let tacname = loc, tacname in + let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in + let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Term arg) in + let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in + (TacML (CAst.make (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)]))) in + CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac)) in + let rule, action = gbpmp (Obj.magic action) (List.rev abbrev_name) in + Pcoq.grammar_extend Pcoq.Constr.term { + Pcoq.pos = Some (Gramlib.Gramext.Before "10"); + data = [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) + (Obj.magic action) + ])] + } + +let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = { + abbrev_name; + tac_name; + tac_fixed_args = List.map (Coq_elpi_arg_HOAS.subst_tac_arg_glob subst) tac_fixed_args +} +let inAbbreviationForTactic : tac_abbrev -> Libobject.obj = + Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED-TAC-ABBREV" + ~cache:cache_abbrev_for_tac ~subst:(Some subst_abbrev_for_tac) +let cache_tac_abbrev (q,qualid) = cache_abbrev_for_tac (q,{ + abbrev_name = qualid; + tac_name = qualid; + tac_fixed_args = []; +}) (*****************************************************************************) (*****************************************************************************) @@ -2094,16 +2092,19 @@ other arguments will necessarily be terms, and their number is not fixed (the user can pass as many as he likes). The tactic receives as the elpi.loc attribute the precise location at which the term is written (unlike if a regular abbreviation was -declared by hand).|})))), +declared by hand). +A call to coq.notation.add-abbreviation-for-tactic TacName TacName [] +is equivalent to Elpi Export TacName.|})))), (fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state -> let sigma = get_sigma state in let env = get_global_env state in - let more_args = more_args |> List.map (function + let tac_fixed_args = more_args |> List.map (function | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Int n | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.String s | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Term (Coq_elpi_utils.detype env sigma t)) in - let name = List.rev (Coq_elpi_utils.string_split_on_char '.' name) in - Lib.add_anonymous_leaf @@ inAbbreviationForTactic (name, tacname, more_args); + let abbrev_name = Coq_elpi_utils.string_split_on_char '.' name in + let tac_name = Coq_elpi_utils.string_split_on_char '.' tacname in + Lib.add_anonymous_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args}; state, (), []))), DocAbove); diff --git a/src/coq_elpi_builtins.mli b/src/coq_elpi_builtins.mli index eee3bf21f..74b8d170e 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/coq_elpi_builtins.mli @@ -3,13 +3,14 @@ (* ------------------------------------------------------------------------- *) open Elpi.API +open Coq_elpi_utils val coq_builtins : BuiltIn.declaration list (* Clauses to be added to elpi programs when the execution is over *) val clauses_for_later : - (string list * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component + (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component val set_accumulate_to_db : ((string list -> Ast.program -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit)) -> unit type attribute_data = @@ -23,4 +24,6 @@ type attribute_value = val attribute : (string * attribute_value) Conversion.t (* In tactic mode some APIs are disabled *) -val tactic_mode : bool ref \ No newline at end of file +val tactic_mode : bool ref + +val cache_tac_abbrev : (Libobject.object_name * qualified_name) -> unit diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 49ae39230..972f9f60a 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -744,11 +744,10 @@ let loc_merge l1 l2 = try Loc.merge l1 l2 with Failure _ -> l1 -let in_exported_program : qualified_name -> Libobject.obj = +let in_exported_program : nature * qualified_name * string -> Libobject.obj = Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED" - ~cache:(fun (_,p) -> - let p_str = String.concat "." p in - match get_nature p with + ~cache:(fun (q,(nature,p,p_str)) -> + match nature with | Command -> Vernacextend.vernac_extend ~command:("Elpi"^p_str) @@ -763,12 +762,19 @@ let in_exported_program : qualified_name -> Libobject.obj = (fun loc0 args loc1 (* 8.14 ~loc*) ~atts -> Vernacextend.VtDefault (fun () -> run_program (loc_merge loc0 loc1) (*loc*) p ~atts args)), None)] - | (Tactic | Program) -> - CErrors.user_err Pp.(str "elpi: Only commands can be exported")) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) + | Tactic -> + Coq_elpi_builtins.cache_tac_abbrev (q,p) + | Program -> + CErrors.user_err Pp.(str "elpi: Only commands and tactics can be exported")) + ~subst:(Some (function + | _, (Command, _, _) ->CErrors.user_err Pp.(str"elpi: No functors yet") + | _, (Tactic,_,_ as x) -> x + | _, (Program,_,_) -> assert false)) let export_command p = - Lib.add_anonymous_leaf (in_exported_program p) + let p_str = String.concat "." p in + let nature = get_nature p in + Lib.add_anonymous_leaf (in_exported_program (nature,p,p_str)) let skip ~atts:(skip,only) f x = let m rex = Str.string_match rex Coq_config.version 0 in diff --git a/tests/test_tactic.v b/tests/test_tactic.v index c1f1cc830..16f5a809c 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -313,3 +313,27 @@ Qed. Check forall xxx : nat, forall XX : bool, True. +Elpi Export test.m. + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (test.m (@eq_refl _ x)). +Qed. + +Notation Foo pp := ltac:(elpi test.m (pp)). + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (Foo (@eq_refl _ x)). +Qed. + +Tactic Notation "Bar" open_constr(pp) := + elpi test.m (pp). +Notation Bar qq := ltac:(Bar (@eq_refl _ qq)). + +Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). +split; intro x. +all: exact (Bar x). +Qed. + + From 98dcadbfddce0b885b9f9aa5b4c34ac36deb0f2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 17:13:35 +0200 Subject: [PATCH 10/22] purge unreachable evars --- src/coq_elpi_HOAS.ml | 17 ++++++++++++----- src/coq_elpi_HOAS.mli | 2 +- src/coq_elpi_vernacular.ml | 2 +- 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 66695f074..4e02bce46 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1747,19 +1747,26 @@ let reachable sigma roots acc = prlist_with_sep spc Evar.print (Evar.Set.elements res)); res -let tclSOLUTION2EVD { API.Data.constraints; assignments; state; pp_ctx } = +let tclSOLUTION2EVD sigma0 { API.Data.constraints; assignments; state; pp_ctx } = let open Proofview.Unsafe in - let open Proofview.Notations in let open Tacticals.New in - tclGETGOALS >>= fun gls -> + let open Proofview.Notations in + tclGETGOALS >>= fun gls -> let gls = gls |> List.map Proofview.drop_state in let roots = List.fold_right Evar.Set.add gls Evar.Set.empty in let state, solved_goals, _, _gls = elpi_solution_to_coq_solution constraints state in - let all_goals = reachable (get_sigma state) roots Evar.Set.empty in + let sigma = get_sigma state in + let all_goals = reachable sigma roots Evar.Set.empty in let declared_goals, shelved_goals = get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in + if debug () then Feedback.msg_debug Pp.(str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals); + if debug () then Feedback.msg_debug Pp.(str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals); + let sigma = Evd.fold_undefined (fun k _ sigma -> + if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma + else Evd.remove sigma k + ) sigma sigma in tclTHENLIST [ - tclEVARS (S.get engine state).sigma; + tclEVARS sigma; tclSETGOALS @@ List.map Proofview.with_empty_state declared_goals; Proofview.shelve_goals shelved_goals ] diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index aa98f3d99..c63b10234 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -209,6 +209,6 @@ val goals2query : Evd.evar_map -> Goal.goal list -> Elpi.API.Ast.Loc.t -> main:'a tactic_main -> in_elpi_arg:(depth:int -> ?calldepth:int -> 'b coq_context -> hyp list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) -> depth:int -> State.t -> State.t * (Elpi.API.Ast.Loc.t * term) -val tclSOLUTION2EVD : 'a Elpi.API.Data.solution -> unit Proofview.tactic +val tclSOLUTION2EVD : Evd.evar_map -> 'a Elpi.API.Data.solution -> unit Proofview.tactic val show_engine : State.t -> string diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 972f9f60a..4653393c9 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -694,7 +694,7 @@ let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) () = in let program = get_and_compile program in match run ~tactic_mode:true ~static_check program (`Fun query) with - | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD solution + | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD sigma solution | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> CErrors.user_err Pp.(str "elpi fails") | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAIL level msg From 90ff5a17a836b9a00b622c8fea1cce4d9fdc3310 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 18:19:23 +0200 Subject: [PATCH 11/22] API coq.hints.* --- Changelog.md | 2 ++ coq-builtin.elpi | 18 ++++++++++++++ src/coq_elpi_builtins.ml | 52 ++++++++++++++++++++++++++++++++++++++++ tests/test_API2.v | 10 ++++++++ 4 files changed, 82 insertions(+) diff --git a/Changelog.md b/Changelog.md index eaacf9e99..52a59ba2b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -11,6 +11,8 @@ Requires Elpi 1.13.6 and Coq 8.13. but passing `mytactic` the correct `elpi.loc` of invocation. - New `@pplevel!` attribute to control outermost parentheses in `coq.term->pp` and similar +- New `coq.hints.add-mode` like the `Hint Mode` vernacular +- New `coq.hints.modes` ## [1.10.3] - 18-06-2021 diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 908a423d1..688ed5700 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -842,6 +842,24 @@ external pred coq.coercion.db o:list coercion. external pred coq.coercion.db-for i:class, i:class, o:list (pair gref int). +% -- Coq's Hint DB ------------------------------------- + +% Hint Mode +kind hint-mode type. +type mode-ground hint-mode. % No Evar +type mode-input hint-mode. % No Head Evar +type mode-output hint-mode. % Anything + +% [coq.hints.add-mode GR DB Mode] Adds a mode declaration to DB about +% GR. +% Supported attributes: +% - @local! (default: false) +external pred coq.hints.add-mode i:gref, i:string, i:list hint-mode. + +% [coq.hints.modes GR DB Modes] Gets all the mode declarations in DB about +% GR +external pred coq.hints.modes i:gref, i:string, o:list (list hint-mode). + % -- Coq's notational mechanisms ------------------------------------- % Implicit status of an argument diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 92f542ebf..d6f2047b0 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -926,6 +926,24 @@ let cache_tac_abbrev (q,qualid) = cache_abbrev_for_tac (q,{ tac_fixed_args = []; }) +let mode = let open API.AlgebraicData in let open Hints in declare { + ty = Conv.TyName "hint-mode"; + doc = "Hint Mode"; + pp = (fun fmt (x : hint_mode) -> Pp.pp_with fmt (pp_hint_mode x)); + constructors = [ + K ("mode-ground", "No Evar",N, + B ModeInput, + M (fun ~ok ~ko -> function ModeInput -> ok | _ -> ko ())); + K("mode-input","No Head Evar",N, + B ModeNoHeadEvar, + M (fun ~ok ~ko -> function ModeNoHeadEvar -> ok | _ -> ko ())); + K("mode-output","Anything",N, + B ModeOutput, + M (fun ~ok ~ko -> function ModeOutput -> ok | _ -> ko ())); + ] +} |> CConv.(!<) + + (*****************************************************************************) (*****************************************************************************) (*****************************************************************************) @@ -1828,6 +1846,40 @@ NParams can always be omitted, since it is inferred. with Not_found -> !: [])), DocAbove); + LPDoc "-- Coq's Hint DB -------------------------------------"; + + MLData mode; + + MLCode(Pred("coq.hints.add-mode", + In(gref, "GR", + In(B.string, "DB", + In(B.list mode, "Mode", + Full(global, {|Adds a mode declaration to DB about GR. +Supported attributes: +- @local! (default: false)|})))), + (fun gr db mode ~depth:_ {options} _ -> on_global_state "coq.hints.add-mode" (fun state -> + let open Goptions in + let locality = if options.local = Some true then OptLocal else OptExport in + Hints.add_hints ~locality [db] (Hints.HintsModeEntry(gr,mode)); + state, (), [] + ))), + DocAbove); + + MLCode(Pred("coq.hints.modes", + In(gref, "GR", + In(B.string, "DB", + Out(B.list (B.list mode), "Modes", + Easy {|Gets all the mode declarations in DB about GR|}))), + (fun gr db _ ~depth:_ -> + try + let db = Hints.searchtable_map db in + let modes = Hints.Hint_db.modes db in + !: (List.map (fun a -> Array.to_list a) @@ GlobRef.Map.find gr modes) + with Not_found -> + !: [] + )), + DocAbove); + LPDoc "-- Coq's notational mechanisms -------------------------------------"; MLData implicit_kind; diff --git a/tests/test_API2.v b/tests/test_API2.v index 7dbba9db5..bab927678 100644 --- a/tests/test_API2.v +++ b/tests/test_API2.v @@ -50,3 +50,13 @@ Elpi Query lp:{{ coq.strategy.get X3 (level 123). }}. + +Axiom P : nat -> Prop. + +Elpi Command mode. +Elpi Query lp:{{ + coq.hints.add-mode {{:gref P }} "core" [mode-input], + coq.hints.add-mode {{:gref P }} "core" [mode-ground], + coq.hints.modes {{:gref P }} "core" M, + std.assert! (M = [[mode-ground],[mode-input]]) "wrong modes" +}}. From f2e23d93dbd72a1c15d69352abb50f4167526616 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 18:30:20 +0200 Subject: [PATCH 12/22] API coq.TC.declare-class --- Changelog.md | 1 + coq-builtin.elpi | 3 +++ src/coq_elpi_builtins.ml | 10 +++++++++- tests/test_API.v | 8 ++++++++ 4 files changed, 21 insertions(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index 52a59ba2b..20ffd0916 100644 --- a/Changelog.md +++ b/Changelog.md @@ -13,6 +13,7 @@ Requires Elpi 1.13.6 and Coq 8.13. and similar - New `coq.hints.add-mode` like the `Hint Mode` vernacular - New `coq.hints.modes` +- New `coq.TC.declare-class` ## [1.10.3] - 18-06-2021 diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 688ed5700..c1cb35855 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -797,6 +797,9 @@ external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance. external pred coq.CS.canonical-projections i:inductive, o:list (option constant). +% [coq.TC.declare-class GR] Declare GR as a type class +external pred coq.TC.declare-class i:gref. + % Type class instance with priority kind tc-instance type. type tc-instance gref -> int -> tc-instance. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index d6f2047b0..f43fac0be 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1750,8 +1750,16 @@ Supported attributes: CList.map (Option.map (fun x -> Constant x))))), DocAbove); - MLData tc_instance; + MLCode(Pred("coq.TC.declare-class", + In(gref, "GR", + Full(global, {|Declare GR as a type class|})), + (fun gr ~depth { options } _ -> on_global_state "coq.TC.declare-class" (fun state -> + Record.declare_existing_class gr; + state, (), []))), + DocAbove); + MLData tc_instance; + MLCode(Pred("coq.TC.declare-instance", In(gref, "GR", In(int, "Priority", diff --git a/tests/test_API.v b/tests/test_API.v index 32f52330f..7edfd070e 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -578,6 +578,14 @@ Elpi Query lp:{{coq.locate "RewriteRelation" GR, coq.TC.db-for GR L}}. Elpi Query lp:{{coq.locate "RewriteRelation" GR, coq.TC.class? GR}}. Elpi Query lp:{{coq.locate "True" GR, not(coq.TC.class? GR)}}. +Axiom C : Type -> Type. + +Elpi Query lp:{{ coq.TC.declare-class {{:gref C }} }}. + +Axiom c : C nat. + +Instance foox : C nat := c. + (****** CS **********************************) Structure eq := mk_eq { carrier : Type; eq_op : carrier -> carrier -> bool; _ : nat }. From c4d6395de6fe9d4c4317a2e4caf1a528ee555312 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 19:09:18 +0200 Subject: [PATCH 13/22] spring cleanup --- Changelog.md | 2 ++ _CoqProject | 3 ++- _CoqProject.test | 2 ++ coq-builtin.elpi | 28 +++++++++++++++++++++------- elpi/elpi-reduction.elpi | 2 +- src/coq_elpi_builtins.ml | 26 ++++++++++++++++++++------ src/coq_elpi_glob_quotation.ml | 2 +- src/coq_elpi_utils.ml | 2 +- tests/test_API.v | 4 ++-- 9 files changed, 52 insertions(+), 19 deletions(-) diff --git a/Changelog.md b/Changelog.md index 20ffd0916..e68d33ba2 100644 --- a/Changelog.md +++ b/Changelog.md @@ -14,6 +14,8 @@ Requires Elpi 1.13.6 and Coq 8.13. - New `coq.hints.add-mode` like the `Hint Mode` vernacular - New `coq.hints.modes` - New `coq.TC.declare-class` +- Deprecate `coq.env.const-opaque?` -> `coq.env.opaque?` +- Deprecate `coq.env.const-primitive?` -> `coq.env.primitive?` ## [1.10.3] - 18-06-2021 diff --git a/_CoqProject b/_CoqProject index 839d76c7f..e92d66812 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,4 @@ --arg -w -arg +elpi.add-const-for-axiom-or-sectionvar +-arg -w -arg +elpi.deprecated -R theories elpi -Q examples elpi.examples @@ -39,3 +39,4 @@ src/coq_elpi_builtins.mli src/coq_elpi_config.ml src/elpi_plugin.mlpack + diff --git a/_CoqProject.test b/_CoqProject.test index 84c236c41..0ffafbc79 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -1,3 +1,5 @@ +-arg -w -arg +elpi.deprecated + -Q theories elpi -Q examples elpi.examples -Q tests elpi.tests diff --git a/coq-builtin.elpi b/coq-builtin.elpi index c1cb35855..4d47a7f1b 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -587,8 +587,8 @@ external pred coq.env.record? i:inductive, o:bool. % [coq.env.recursive? Ind] checks if Ind is recursive external pred coq.env.recursive? i:inductive. -% [coq.env.const-opaque? GR] checks if GR is an opaque constant -external pred coq.env.const-opaque? i:constant. +% [coq.env.opaque? GR] checks if GR is an opaque constant +external pred coq.env.opaque? i:constant. % [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant GR. % Opaque constants have Bo = none. @@ -598,9 +598,9 @@ external pred coq.env.const i:constant, o:option term, o:term. % opaque. If such body is none, then the constant is a true axiom external pred coq.env.const-body i:constant, o:option term. -% [coq.env.const-primitive? GR] tests if GR is a primitive constant (like -% uin63 addition) -external pred coq.env.const-primitive? i:constant. +% [coq.env.primitive? GR] tests if GR is a primitive constant (like uin63 +% addition) +external pred coq.env.primitive? i:constant. % [coq.locate-module ModName ModPath] locates a module. It's a fatal error % if ModName cannot be located. *E* @@ -625,6 +625,20 @@ external pred coq.env.section o:list constant. % [coq.env.current-path Path] lists the current module path external pred coq.env.current-path o:list string. +% Deprecated, use coq.env.opaque? + pred coq.env.const-opaque? i:constant. + coq.env.const-opaque? C :- + coq.warning "elpi.deprecated" "elpi.const-opaque" "use coq.env.opaque? in place of coq.env.const-opaque?", + coq.env.opaque? C. + + +% Deprecated, use coq.env.primitive? + pred coq.env.const-primitive? i:constant. + coq.env.const-primitive? C :- + coq.warning "elpi.deprecated" "elpi.const-primitive" "use coq.env.primitive? in place of coq.env.const-primitive?", + coq.env.primitive? C. + + % -- Environment: write ----------------------------------------------- % Note: universe constraints are taken from ELPI's constraints store. Use @@ -1059,14 +1073,14 @@ external pred coq.reduction.native.available? . % Deprecated, use coq.reduction.cbv.norm pred coq.reduction.cbv.whd_all i:term, o:term. coq.reduction.cbv.whd_all T R :- - coq.warning "elpi" "deprecated-reduction" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all", + coq.warning "elpi.deprecated" "elpi.cbv-whd-all" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all", coq.reduction.cbv.norm T R. % Deprecated, use coq.reduction.vm.norm pred coq.reduction.vm.whd_all i:term, i:term, o:term. coq.reduction.vm.whd_all T TY R :- - coq.warning "elpi" "deprecated-reduction" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all", + coq.warning "elpi.deprecated" "elpi.vm-whd-all" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all", coq.reduction.vm.norm T TY R. diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi index 099176a5a..e23136b00 100644 --- a/elpi/elpi-reduction.elpi +++ b/elpi/elpi-reduction.elpi @@ -34,7 +34,7 @@ whd (fun N T F) [B|C] X XC :- !, whd (let N T B F) C X XC :- !, (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B. whd (global (const GR)) C X XC :- unfold GR C D DC, !, whd D DC X XC. -whd (global (const GR) as HD) C X XC :- coq.env.const-primitive? GR, !, +whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !, unwind HD C Orig, coq.reduction.lazy.whd_all Orig R, if (same_term Orig R) (X = HD, XC = C) (whd R [] X XC). diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index f43fac0be..d319bf7ed 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -826,7 +826,7 @@ let ppboxes = let open Conv in let open Pp in let open API.AlgebraicData in decl let warn_deprecated_add_axiom = CWarnings.create ~name:"elpi.add-const-for-axiom-or-sectionvar" - ~category:"deprecated" + ~category:"elpi.deprecated" Pp.(fun () -> strbrk ("elpi: Using coq.env.add-const for declaring axioms or " ^ "section variables is deprecated. Use coq.env.add-axiom or " ^ @@ -1213,7 +1213,7 @@ It's a fatal error if Name cannot be located.|})), )), DocAbove); - MLCode(Pred("coq.env.const-opaque?", + MLCode(Pred("coq.env.opaque?", In(constant, "GR", Read(global, "checks if GR is an opaque constant")), (fun c ~depth {env} _ state -> @@ -1228,7 +1228,7 @@ It's a fatal error if Name cannot be located.|})), | Context.Named.Declaration.LocalDef _ -> raise Pred.No_clause | Context.Named.Declaration.LocalAssum _ -> ())), DocAbove); - + MLCode(Pred("coq.env.const", In(constant, "GR", COut(!>> option closed_ground_term, "Bo", @@ -1272,7 +1272,7 @@ It's a fatal error if Name cannot be located.|})), end, [])), DocAbove); - MLCode(Pred("coq.env.const-primitive?", + MLCode(Pred("coq.env.primitive?", In(constant, "GR", Read (global,"tests if GR is a primitive constant (like uin63 addition)")), (fun c ~depth {env} _ state -> @@ -1341,6 +1341,20 @@ It's a fatal error if Name cannot be located.|})), (fun _ ~depth _ _ state -> !: (mp2path (Safe_typing.current_modpath (Global.safe_env ()))))), DocAbove); + LPCode {|% Deprecated, use coq.env.opaque? + pred coq.env.const-opaque? i:constant. + coq.env.const-opaque? C :- + coq.warning "elpi.deprecated" "elpi.const-opaque" "use coq.env.opaque? in place of coq.env.const-opaque?", + coq.env.opaque? C. + |}; + + LPCode {|% Deprecated, use coq.env.primitive? + pred coq.env.const-primitive? i:constant. + coq.env.const-primitive? C :- + coq.warning "elpi.deprecated" "elpi.const-primitive" "use coq.env.primitive? in place of coq.env.const-primitive?", + coq.env.primitive? C. + |}; + LPDoc "-- Environment: write -----------------------------------------------"; LPDoc ("Note: universe constraints are taken from ELPI's constraints "^ @@ -2434,14 +2448,14 @@ hole. Similarly universe levels present in T are disregarded.|}))))), LPCode {|% Deprecated, use coq.reduction.cbv.norm pred coq.reduction.cbv.whd_all i:term, o:term. coq.reduction.cbv.whd_all T R :- - coq.warning "elpi" "deprecated-reduction" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all", + coq.warning "elpi.deprecated" "elpi.cbv-whd-all" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all", coq.reduction.cbv.norm T R. |}; LPCode {|% Deprecated, use coq.reduction.vm.norm pred coq.reduction.vm.whd_all i:term, i:term, o:term. coq.reduction.vm.whd_all T TY R :- - coq.warning "elpi" "deprecated-reduction" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all", + coq.warning "elpi.deprecated" "elpi.vm-whd-all" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all", coq.reduction.vm.norm T TY R. |}; diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 65c155927..ddd18655f 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -169,7 +169,7 @@ let rec gterm2lp ~depth state x = Id.Map.bindings ctx.name2db |> List.filter (fun (n,_) -> not(is_restricted_name n)) |> List.map snd |> - List.sort Pervasives.compare |> + List.sort Stdlib.compare |> List.map E.mkBound in state, E.mkUnifVar uv ~args state diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index a33124787..061f7da73 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -210,7 +210,7 @@ let detype_closed_glob env sigma closure = fix_detype gbody type qualified_name = string list -let compare_qualified_name = Pervasives.compare +let compare_qualified_name = Stdlib.compare let pr_qualified_name = Pp.prlist_with_sep (fun () -> Pp.str".") Pp.str let show_qualified_name = String.concat "." let pp_qualified_name fmt l = Format.fprintf fmt "%s" (String.concat "." l) diff --git a/tests/test_API.v b/tests/test_API.v index 7edfd070e..dc4e6a33e 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -248,7 +248,7 @@ Elpi Query lp:{{ coq.gref->id (const GR) S, Name is S ^ "_equal", coq.env.add-const Name BO TY @opaque! NGR, - coq.env.const-opaque? NGR, + coq.env.opaque? NGR, coq.env.const NGR none _, coq.say {coq.gref->id (const NGR)}, coq.env.const-body NGR (some BO), rex_match "add_equal" {coq.gref->id (const NGR)}. @@ -261,7 +261,7 @@ About add_equal. Elpi Query lp:{{ coq.locate "False" F, coq.env.add-axiom "myfalse" (global F) GR, - coq.env.const-opaque? GR, + coq.env.opaque? GR, coq.env.const GR none _, coq.env.const-body GR none, coq.say GR. From e6a3e19adfe24662c25589e582e2e0a12ff6de24 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 19:13:47 +0200 Subject: [PATCH 14/22] fix opam --- coq-elpi.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/coq-elpi.opam b/coq-elpi.opam index 61f929d40..e277b92b2 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -13,6 +13,7 @@ build: [ [ make "build" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAML ] install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] depends: [ + "stdlib-shims" "elpi" {>= "1.13.6" & < "1.14.0~"} "coq" {>= "8.13" & < "8.14~" } ] From 2b6c271421fc6231ded57ef4c4707cb1e2ae265e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 19:25:01 +0200 Subject: [PATCH 15/22] fix docker action --- .github/workflows/main.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index dad8d2f31..0bbffe49f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -18,7 +18,8 @@ jobs: coq_version: - '8.13' ocaml_version: - - 'minimal' + - '4.07-flambda' + - '4.11-flambda' steps: - uses: actions/checkout@v2 - uses: coq-community/docker-coq-action@v1 From 587008e770689b72a58665c0b16b793fa665b8ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Jun 2021 19:25:46 +0200 Subject: [PATCH 16/22] bump date --- Changelog.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index e68d33ba2..701f3ce81 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,6 +1,6 @@ # Changelog -## [1.10.4] - 23-06-2021 +## [1.10.4] - 28-06-2021 Requires Elpi 1.13.6 and Coq 8.13. From 7c40b7405a6c80df6a7a3842f04fe27d8f74454c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Jun 2021 18:25:14 +0200 Subject: [PATCH 17/22] primitive (proj P N) (fix #259) --- Changelog.md | 4 ++++ apps/derive/tests/test_lens.v | 2 +- coq-builtin.elpi | 5 +++++ elpi/coq-HOAS.elpi | 2 ++ elpi/elpi-reduction.elpi | 7 ++++++ src/coq_elpi_HOAS.ml | 40 ++++++++++++++++++++++++++-------- src/coq_elpi_HOAS.mli | 1 + src/coq_elpi_builtins.ml | 4 +++- src/coq_elpi_builtins_HOAS.ml | 2 ++ src/coq_elpi_glob_quotation.ml | 25 ++++++++++++++++----- src/coq_elpi_utils.ml | 12 ++++++++++ src/coq_elpi_utils.mli | 1 + tests/test_API.v | 4 ++-- tests/test_HOAS.v | 27 +++++++++++++++++++++++ 14 files changed, 118 insertions(+), 18 deletions(-) diff --git a/Changelog.md b/Changelog.md index 701f3ce81..e17e3da20 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,10 @@ Requires Elpi 1.13.6 and Coq 8.13. +### HOAS +- New node `proj : primitive-value` holding the projection name (a Coq detail) + and the number of the field it projects (0 based), eg: `primitive (proj P N)`. + ### API - New `coq.notation.add-abbreviation-for-tactic` to add a parsing rule for a tactic-in-term, along the lines of diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v index 7526dde4b..bf7da076c 100644 --- a/apps/derive/tests/test_lens.v +++ b/apps/derive/tests/test_lens.v @@ -21,7 +21,7 @@ Check @_pf4 : forall A, Lens (pr_record A) (pr_record A) A A. Goal forall A x, x = @_pf3 A. intros; unfold _pf3. match goal with -| |- x = {| over := fun f r => {| pf3 := f (pf3 A r); pf4 := pf4 A r |} ; +| |- x = {| over := fun f r => {| pf3 := f (_ r); pf4 := _ r |} ; view := _ |} => idtac "ok" | |- _ => fail "not primitive" diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 4d47a7f1b..956f0036a 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -89,6 +89,8 @@ type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo kind primitive-value type. type uint63 uint63 -> primitive-value. type float64 float64 -> primitive-value. +type proj projection -> int -> primitive-value. + type primitive primitive-value -> term. @@ -534,6 +536,9 @@ typeabbrev modpath (ctype "modpath"). typeabbrev modtypath (ctype "modtypath"). +typeabbrev projection (ctype "projection"). + + % -- Environment: read ------------------------------------------------ % Note: The type [term] is defined in coq-HOAS.elpi diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index dd4b1bc92..214b24d35 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -74,6 +74,8 @@ type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo kind primitive-value type. type uint63 uint63 -> primitive-value. type float64 float64 -> primitive-value. +type proj projection -> int -> primitive-value. + type primitive primitive-value -> term. diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi index e23136b00..5202b1ac1 100644 --- a/elpi/elpi-reduction.elpi +++ b/elpi/elpi-reduction.elpi @@ -34,6 +34,8 @@ whd (fun N T F) [B|C] X XC :- !, whd (let N T B F) C X XC :- !, (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B. whd (global (const GR)) C X XC :- unfold GR C D DC, !, whd D DC X XC. +whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A GR KA, !, + whd {proj-red GR KA N C} X XC. whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !, unwind HD C Orig, coq.reduction.lazy.whd_all Orig R, @@ -61,6 +63,11 @@ match-red GR KArgs BL C X XC :- drop Lno KArgs Args, nth Ki BL Bi, hd-beta {coq.mk-app Bi Args} C X XC. +pred proj-red i:constructor, i:list term, i:int, i:stack, o:term, o:stack. +proj-red GR KArgs FieldNo C V C :- + coq.env.indc GR Lno _ _ _, + drop Lno KArgs Args, + nth FieldNo Args V. % iota step pred fix-red diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 4e02bce46..cde5dd6ee 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -385,6 +385,7 @@ let in_elpi_fix name rno ty bo = let primitivec = E.Constants.declare_global_symbol "primitive" let uint63c = E.Constants.declare_global_symbol "uint63" let float64c = E.Constants.declare_global_symbol "float64" +let projc = E.Constants.declare_global_symbol "proj" let in_elpi_uint63 ~depth state i = let state, i, _ = Coq_elpi_utils.uint63.API.Conversion.embed ~depth state i in @@ -394,6 +395,11 @@ let in_elpi_float64 ~depth state f = let state, f, _ = Coq_elpi_utils.float64.API.Conversion.embed ~depth state f in state, E.mkApp primitivec (E.mkApp float64c f []) [] +let in_elpi_proj ~depth state c x = + let n = Names.Projection.arg c in + let state, p, _ = Coq_elpi_utils.projection.API.Conversion.embed ~depth state c in + state, in_elpi_appl ~depth (E.mkApp primitivec (E.mkApp projc p [CD.of_int n]) []) [x] + (* ********************************* }}} ********************************** *) (* {{{ HOAS : Evd.evar_map -> elpi *************************************** *) @@ -891,8 +897,8 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = let state, bo = aux ~depth:(depth+1) env state bo in state, in_elpi_fix name.Context.binder_name rarg typ bo | C.Proj(p,t) -> - let t = Retyping.expand_projection env sigma p t [] in - aux ~depth env state t + let state, t = aux ~depth env state t in + in_elpi_proj ~depth state p t | C.Fix _ -> nYI "HOAS for mutual fix" | C.CoFix _ -> nYI "HOAS for cofix" | C.Int i -> in_elpi_uint63 ~depth state i @@ -1229,13 +1235,26 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals err Pp.(str"wrong constant:" ++ str (E.Constants.show n)) (* app *) - | E.App(c,x,[]) when appc == c -> - (match U.lp_list_to_list ~depth x with - | x :: xs -> - let state, x, gl1 = aux ~depth state x in - let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in - state, EC.mkApp (x, Array.of_list xs), gl1 @ gl2 - | _ -> assert false) (* TODO *) + | E.App(c,x,[]) when appc == c -> begin + match U.lp_list_to_list ~depth x with + | x :: xs -> begin + match E.look ~depth x, xs with + | E.App(c,p,[]), i :: xs when primitivec == c -> + begin match E.look ~depth p with + | E.App(c,p,[_]) when projc == c -> + let state, p, gls = Coq_elpi_utils.projection.API.Conversion.readback ~depth state p in + let state, i, gl1 = aux ~depth state i in + let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in + state, EC.mkApp (EC.mkProj (p,i),Array.of_list xs), gls @ gl1 @ gl2 + | _ -> err Pp.(str"not a primitive projection:" ++ str (E.Constants.show c)) + end + | x, _ -> + let state, x, gl1 = aux ~depth state (E.kool x) in + let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in + state, EC.mkApp (x, Array.of_list xs), gl1 @ gl2 + end + | _ -> assert false (* TODO *) + end (* match *) | E.App(c,t,[rt;bs]) when matchc == c -> @@ -1297,6 +1316,9 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | E.App(c,f,[]) when float64c == c -> let state, f, gls = Coq_elpi_utils.float64.API.Conversion.readback ~depth state f in state, EC.mkFloat f, gls + | E.App(c,p,[_]) when projc == c -> + let state, p, gls = Coq_elpi_utils.projection.API.Conversion.readback ~depth state p in + state, EC.mkConst (Names.Projection.constant p), gls | _ -> err Pp.(str"Not a HOAS primitive value:" ++ str (P.Debug.show_term t)) end diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index c63b10234..8a38148fe 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -124,6 +124,7 @@ val in_elpi_match : term -> term -> term list -> term val in_elpi_fix : Name.t -> int -> term -> term -> term val in_elpi_uint63 : depth:int -> state -> Uint63.t -> state * term val in_elpi_float64 : depth:int -> state -> Float64.t -> state * term +val in_elpi_proj : depth:int -> state -> Projection.t -> term -> state * term val in_elpi_name : Name.t -> term diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index d319bf7ed..340a0be58 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1070,7 +1070,9 @@ Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@b MLData gref; MLData id; MLData modpath; - MLData modtypath; ] @ + MLData modtypath; + MLData projection; + ] @ [ LPDoc "-- Environment: read ------------------------------------------------"; diff --git a/src/coq_elpi_builtins_HOAS.ml b/src/coq_elpi_builtins_HOAS.ml index 533953889..d62d7a8ae 100644 --- a/src/coq_elpi_builtins_HOAS.ml +++ b/src/coq_elpi_builtins_HOAS.ml @@ -76,6 +76,8 @@ type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo kind primitive-value type. type uint63 uint63 -> primitive-value. type float64 float64 -> primitive-value. +type proj projection -> int -> primitive-value. + type primitive primitive-value -> term. diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index ddd18655f..9105ae844 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -185,12 +185,27 @@ let rec gterm2lp ~depth state x = | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar" | GPatVar _ -> nYI "(glob)HOAS for GPatVar" -(* | GProj _ -> nYI "(glob)HOAS for GProj" *) - | GApp(hd,args) -> - let state, hd = gterm2lp ~depth state hd in - let state, args = CList.fold_left_map (gterm2lp ~depth) state args in - state, in_elpi_appl ~depth hd args + | GApp(hd,args) -> begin + match DAst.get hd with + | GRef(GlobRef.ConstRef p,_ul) when Recordops.is_primitive_projection p -> + let p = Option.get @@ Recordops.find_primitive_projection p in + let p = Projection.make p false in + let npars = Projection.npars p in + begin match CList.skipn npars args with + | i :: args -> + let state, i = gterm2lp ~depth state i in + let state, args = CList.fold_left_map (gterm2lp ~depth) state args in + let state, p = in_elpi_proj ~depth state p i in + state, in_elpi_appl ~depth p args + | [] -> CErrors.user_err ~hdr:"elpi quotation" + Pp.(str"Coq primitive projection " ++ Projection.print p ++ str " has not enough arguments"); + end + | _ -> + let state, hd = gterm2lp ~depth state hd in + let state, args = CList.fold_left_map (gterm2lp ~depth) state args in + state, in_elpi_appl ~depth hd args + end | GLetTuple(kargs,(as_name,oty),t,b) -> let state, t = gterm2lp ~depth state t in diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 061f7da73..1c621d0b4 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -170,6 +170,18 @@ let float64 : Float64.t Elpi.API.Conversion.t = constants = []; } + let projection : Names.Projection.t Elpi.API.Conversion.t = + let open Elpi.API.OpaqueData in + declare { + name = "projection"; + doc = ""; + pp = (fun fmt i -> Format.fprintf fmt "%s" (Names.Projection.to_string i)); + compare = Names.Projection.CanOrd.compare; + hash = Names.Projection.CanOrd.hash; + hconsed = false; + constants = []; + } + let fold_elpi_term f acc ~depth t = let module E = Elpi.API.RawData in match t with diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index 403936ac3..e5a944150 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -32,6 +32,7 @@ val fold_elpi_term : val uint63 : Uint63.t Elpi.API.Conversion.t val float64 : Float64.t Elpi.API.Conversion.t +val projection : Names.Projection.t Elpi.API.Conversion.t type clause_scope = Local | Regular | Global | SuperGlobal val pp_scope : Format.formatter -> clause_scope -> unit diff --git a/tests/test_API.v b/tests/test_API.v index dc4e6a33e..c0b559124 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -316,12 +316,12 @@ Definition pc (r : prim_eq_class nat) := r.(prim_eq_f). Elpi Query lp:{{ coq.locate "pc" (const C), - coq.env.const C (some (fun _ _ r\ app[global _, _, r])) _ + coq.env.const C (some (fun _ _ r\ app[primitive _, r])) _ }}. Elpi Command primp. Elpi Accumulate lp:{{ - main [const-decl _ (some (fun _ _ r\ app[global _, _, r])) _]. + main [const-decl _ (some (fun _ _ r\ app[primitive _, r])) _]. }}. Elpi primp Definition pc (r : prim_eq_class nat) := r.(prim_eq_f). diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index ad7b0d496..5071bb91f 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -242,6 +242,33 @@ From Coq Require Import PrimFloat. Open Scope float_scope. Elpi primitive (2.4e13 + 1). +Module P. +Set Primitive Projections. + +Record foo (A : Type) := { p1 : nat; p2 : A }. +Definition x : foo bool := {| p1 := 3; p2 := false |}. + +Unset Primitive Projections. +End P. + +Elpi Command primitive_proj. +Elpi Accumulate lp:{{ + main [trm T, int N] :- + coq.say T, + T = app[primitive (proj P N),A], + coq.say P N A, + coq.say {coq.term->string T}, + coq.say {coq.term->string (primitive (proj P N))}, + {{:gref P.p1 }} = const C, + coq.env.const C BO _, + coq.say BO, + coq.say {whd T []}. +}}. +Elpi Typecheck. + +Elpi primitive_proj (P.p1 _ P.x) 0. +Elpi primitive_proj (P.p2 _ P.x) 1. + (* glob of ifte *) Elpi Command ifte. From ff07b45920bafaea3c3c2bf52a4c26cb37257d5c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Jun 2021 19:16:05 +0200 Subject: [PATCH 18/22] proj carries the real field number --- Changelog.md | 6 ++++-- elpi/elpi-reduction.elpi | 10 ++++------ src/coq_elpi_HOAS.ml | 5 +++-- tests/test_HOAS.v | 8 ++++---- 4 files changed, 15 insertions(+), 14 deletions(-) diff --git a/Changelog.md b/Changelog.md index e17e3da20..d31677597 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,8 +5,10 @@ Requires Elpi 1.13.6 and Coq 8.13. ### HOAS -- New node `proj : primitive-value` holding the projection name (a Coq detail) - and the number of the field it projects (0 based), eg: `primitive (proj P N)`. +- New node `proj` of type `projection -> int -> primitive-value` holding the + projection name (a Coq detail) and the number of the field it projects (0 + based), eg: `primitive (proj _ N)` stands for the projection for the Nth + constructor field counting parameters. ### API - New `coq.notation.add-abbreviation-for-tactic` to add a parsing rule diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi index 5202b1ac1..7f5485741 100644 --- a/elpi/elpi-reduction.elpi +++ b/elpi/elpi-reduction.elpi @@ -34,8 +34,8 @@ whd (fun N T F) [B|C] X XC :- !, whd (let N T B F) C X XC :- !, (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B. whd (global (const GR)) C X XC :- unfold GR C D DC, !, whd D DC X XC. -whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A GR KA, !, - whd {proj-red GR KA N C} X XC. +whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A _ KA, !, + whd {proj-red KA N C} X XC. whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !, unwind HD C Orig, coq.reduction.lazy.whd_all Orig R, @@ -63,10 +63,8 @@ match-red GR KArgs BL C X XC :- drop Lno KArgs Args, nth Ki BL Bi, hd-beta {coq.mk-app Bi Args} C X XC. -pred proj-red i:constructor, i:list term, i:int, i:stack, o:term, o:stack. -proj-red GR KArgs FieldNo C V C :- - coq.env.indc GR Lno _ _ _, - drop Lno KArgs Args, +pred proj-red i:list term, i:int, i:stack, o:term, o:stack. +proj-red Args FieldNo C V C :- nth FieldNo Args V. % iota step diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index cde5dd6ee..d949b2038 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -396,9 +396,10 @@ let in_elpi_float64 ~depth state f = state, E.mkApp primitivec (E.mkApp float64c f []) [] let in_elpi_proj ~depth state c x = - let n = Names.Projection.arg c in + let np = Names.Projection.npars c in + let na = Names.Projection.arg c in let state, p, _ = Coq_elpi_utils.projection.API.Conversion.embed ~depth state c in - state, in_elpi_appl ~depth (E.mkApp primitivec (E.mkApp projc p [CD.of_int n]) []) [x] + state, in_elpi_appl ~depth (E.mkApp primitivec (E.mkApp projc p [CD.of_int @@ np + na]) []) [x] (* ********************************* }}} ********************************** *) diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 5071bb91f..1cb8e1098 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -253,7 +253,7 @@ End P. Elpi Command primitive_proj. Elpi Accumulate lp:{{ - main [trm T, int N] :- + main [trm T, int N, trm V] :- coq.say T, T = app[primitive (proj P N),A], coq.say P N A, @@ -262,12 +262,12 @@ Elpi Accumulate lp:{{ {{:gref P.p1 }} = const C, coq.env.const C BO _, coq.say BO, - coq.say {whd T []}. + std.assert! (unwind {whd T []} V) "wrong value". }}. Elpi Typecheck. -Elpi primitive_proj (P.p1 _ P.x) 0. -Elpi primitive_proj (P.p2 _ P.x) 1. +Elpi primitive_proj (P.p1 _ P.x) 1 (3%nat). +Elpi primitive_proj (P.p2 _ P.x) 2 (false). (* glob of ifte *) From a1755e53e359dd4e722a75d6c70265010fc835ac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Jun 2021 20:36:13 +0200 Subject: [PATCH 19/22] deprecate coq.CS.canonical-projections --- Changelog.md | 2 ++ coq-builtin.elpi | 21 +++++++++++---- examples/example_import_projections.v | 2 +- examples/example_record_expansion.v | 2 +- src/coq_elpi_builtins.ml | 39 ++++++++++++++++++++------- tests/test_API.v | 4 +-- tests/test_HOAS.v | 11 ++++---- 7 files changed, 58 insertions(+), 23 deletions(-) diff --git a/Changelog.md b/Changelog.md index d31677597..e7e27e146 100644 --- a/Changelog.md +++ b/Changelog.md @@ -22,6 +22,8 @@ Requires Elpi 1.13.6 and Coq 8.13. - New `coq.TC.declare-class` - Deprecate `coq.env.const-opaque?` -> `coq.env.opaque?` - Deprecate `coq.env.const-primitive?` -> `coq.env.primitive?` +- Deprecate `coq.CS.canonical-projections` -> `coq.env.projections` +- New `coq.env.primitive-projections` ## [1.10.3] - 18-06-2021 diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 956f0036a..d5ab376f3 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -734,6 +734,15 @@ external pred coq.env.begin-section i:id. % [coq.env.end-section] end the current section *E* external pred coq.env.end-section . +% [coq.env.projections StructureName Projections] given a record +% StructureName lists all projections +external pred coq.env.projections i:inductive, o:list (option constant). + +% [coq.env.primitive-projections StructureName Projections] given a record +% StructureName lists all primitive projections +external pred coq.env.primitive-projections i:inductive, + o:list (option (pair projection int)). + % -- Universes -------------------------------------------------------- % Univ.Universe.t @@ -811,11 +820,6 @@ external pred coq.CS.db o:list cs-instance. % or canonical Value, or both external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance. -% [coq.CS.canonical-projections StructureName Projections] given a record -% StructureName lists all projections -external pred coq.CS.canonical-projections i:inductive, - o:list (option constant). - % [coq.TC.declare-class GR] Declare GR as a type class external pred coq.TC.declare-class i:gref. @@ -864,6 +868,13 @@ external pred coq.coercion.db o:list coercion. external pred coq.coercion.db-for i:class, i:class, o:list (pair gref int). +% Deprecated, use coq.env.projections +pred coq.CS.canonical-projections i:inductive, o:list (option constant). +coq.CS.canonical-projections I L :- + coq.warning "elpi.deprecated" "elpi.canonical-projections" "use coq.env.projections in place of coq.CS.canonical-projections", + coq.env.projections I L. + + % -- Coq's Hint DB ------------------------------------- % Hint Mode diff --git a/examples/example_import_projections.v b/examples/example_import_projections.v index 86a5f9273..20d874944 100644 --- a/examples/example_import_projections.v +++ b/examples/example_import_projections.v @@ -19,7 +19,7 @@ main-import-projections T Ty :- std.assert! (coq.env.record? I PrimProjs) "not a record", coq.env.indt I _ _ NParams _ _ _, std.assert! (std.length Args NParams) "the record is not fully appplied", - coq.CS.canonical-projections I Ps, % get the projections generated by Coq + coq.env.projections I Ps, % get the projections generated by Coq if (PrimProjs = tt) (std.forall Ps (declare-abbrev {std.append {coq.mk-n-holes NParams} [T]})) (std.forall Ps (declare-abbrev {std.append Args [T]})). diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index f0a465b8a..64e192b3b 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -145,7 +145,7 @@ expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :- pred expand i:inductive, i:gref, i:gref, i:term, o:term, o:prop. expand R GR NGR X Y Clause :- std.assert! (coq.env.indt R tt 0 0 _ [K] [KTY]) "record is too complex for this example", - coq.CS.canonical-projections R Projs, + coq.env.projections R Projs, expand-spine (info R GR NGR Projs K KTY) X Y [] [] [] Clause. % This simply dispatches between global references ---------------------------- diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 340a0be58..e7d2a2dd7 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1619,6 +1619,29 @@ denote the same x as before.|}; state, (), []))), DocAbove); + MLCode(Pred("coq.env.projections", + In(inductive, "StructureName", + Out(list (option constant), "Projections", + Easy "given a record StructureName lists all projections")), + (fun i _ ~depth -> + !: (Recordops.lookup_projections i |> + CList.map (Option.map (fun x -> Constant x))))), + DocAbove); + + MLCode(Pred("coq.env.primitive-projections", + In(inductive, "StructureName", + Out(list (option (pair projection int)), "Projections", + Easy "given a record StructureName lists all primitive projections")), + (fun i _ ~depth -> + !: (Recordops.lookup_projections i |> + CList.map (fun o -> Option.bind o (fun x -> + Option.bind (Recordops.find_primitive_projection x) (fun c -> + let c = Names.Projection.make c false in + let np = Names.Projection.npars c in + let na = Names.Projection.arg c in + Some (c, np + na))))))), + DocAbove); + LPDoc "-- Universes --------------------------------------------------------"; @@ -1757,15 +1780,6 @@ Supported attributes: !: (try [(p,v),snd @@ Recordops.lookup_canonical_conversion env (p,v)] with Not_found -> []))), DocAbove); - MLCode(Pred("coq.CS.canonical-projections", - In(inductive, "StructureName", - Out(list (option constant), "Projections", - Easy "given a record StructureName lists all projections")), - (fun i _ ~depth -> - !: (Recordops.lookup_projections i |> - CList.map (Option.map (fun x -> Constant x))))), - DocAbove); - MLCode(Pred("coq.TC.declare-class", In(gref, "GR", Full(global, {|Declare GR as a type class|})), @@ -1870,6 +1884,13 @@ NParams can always be omitted, since it is inferred. with Not_found -> !: [])), DocAbove); + LPCode {|% Deprecated, use coq.env.projections +pred coq.CS.canonical-projections i:inductive, o:list (option constant). +coq.CS.canonical-projections I L :- + coq.warning "elpi.deprecated" "elpi.canonical-projections" "use coq.env.projections in place of coq.CS.canonical-projections", + coq.env.projections I L. +|}; + LPDoc "-- Coq's Hint DB -------------------------------------"; MLData mode; diff --git a/tests/test_API.v b/tests/test_API.v index c0b559124..10b9968af 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -299,7 +299,7 @@ Elpi Query lp:{{ field _ "prim_eq_proof" {{lp:f = lp:f :> bool}} _\ end-record)), @primitive! => coq.env.add-indt DECL GR, - coq.CS.canonical-projections GR [some _, some _]. + coq.env.projections GR [some _, some _]. }}. (* primitive records have eta *) @@ -606,7 +606,7 @@ Elpi Query lp:{{ coq.CS.db L }}. Elpi Query lp:{{ coq.locate "eq" (indt I), - coq.CS.canonical-projections I [some P1, some P2, none], + coq.env.projections I [some P1, some P2, none], coq.locate "carrier" (const P1), coq.locate "eq_op" (const P2) }}. diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 1cb8e1098..37a92645f 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -88,7 +88,7 @@ Record foo A (B : A) : Type := { Elpi Query lp:{{ coq.locate "foo" (indt I), - coq.CS.canonical-projections I [some _, some _, some _]. + coq.env.projections I [some _, some _, some _]. }}. End record_attributes. @@ -253,8 +253,9 @@ End P. Elpi Command primitive_proj. Elpi Accumulate lp:{{ - main [trm T, int N, trm V] :- - coq.say T, + main [trm (global (indt I)), trm T, int N, trm V] :- + coq.env.projections I [_,_], + coq.env.primitive-projections I [some (pr _ 1), some (pr _ 2)], T = app[primitive (proj P N),A], coq.say P N A, coq.say {coq.term->string T}, @@ -266,8 +267,8 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. -Elpi primitive_proj (P.p1 _ P.x) 1 (3%nat). -Elpi primitive_proj (P.p2 _ P.x) 2 (false). +Elpi primitive_proj (P.foo) (P.p1 _ P.x) 1 (3%nat). +Elpi primitive_proj (P.foo) (P.p2 _ P.x) 2 (false). (* glob of ifte *) From 1a44f9b5cace279892b177f7d1b0cee277712a59 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Jun 2021 22:45:07 +0200 Subject: [PATCH 20/22] cleanup --- coq-builtin.elpi | 12 +++--- elpi/coq-HOAS.elpi | 5 --- src/coq_elpi_HOAS.ml | 78 +++++++++++++++++++--------------- src/coq_elpi_HOAS.mli | 10 +++-- src/coq_elpi_builtins.ml | 1 + src/coq_elpi_builtins_HOAS.ml | 5 --- src/coq_elpi_glob_quotation.ml | 9 ++-- 7 files changed, 63 insertions(+), 57 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index d5ab376f3..1d0c4b335 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -86,11 +86,6 @@ type app list term -> term. % app [hd|args] type match term -> term -> list term -> term. % match t p [branch]) type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo -kind primitive-value type. -type uint63 uint63 -> primitive-value. -type float64 float64 -> primitive-value. -type proj projection -> int -> primitive-value. - type primitive primitive-value -> term. @@ -743,6 +738,13 @@ external pred coq.env.projections i:inductive, o:list (option constant). external pred coq.env.primitive-projections i:inductive, o:list (option (pair projection int)). +% Primitive values +kind primitive-value type. +type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits +type float64 float64 -> + primitive-value. % double precision foalting points +type proj projection -> int -> primitive-value. % primitive projection + % -- Universes -------------------------------------------------------- % Univ.Universe.t diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 214b24d35..02947f7ea 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -71,11 +71,6 @@ type app list term -> term. % app [hd|args] type match term -> term -> list term -> term. % match t p [branch]) type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo -kind primitive-value type. -type uint63 uint63 -> primitive-value. -type float64 float64 -> primitive-value. -type proj projection -> int -> primitive-value. - type primitive primitive-value -> term. diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index d949b2038..bd5955bad 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -383,23 +383,38 @@ let in_elpi_fix name rno ty bo = E.mkApp fixc (in_elpi_name name) [CD.of_int rno; ty; E.mkLam bo] let primitivec = E.Constants.declare_global_symbol "primitive" -let uint63c = E.Constants.declare_global_symbol "uint63" -let float64c = E.Constants.declare_global_symbol "float64" -let projc = E.Constants.declare_global_symbol "proj" -let in_elpi_uint63 ~depth state i = - let state, i, _ = Coq_elpi_utils.uint63.API.Conversion.embed ~depth state i in - state, E.mkApp primitivec (E.mkApp uint63c i []) [] +type primitive_value = + | Uint63 of Uint63.t + | Float64 of Float64.t + | Projection of Projection.t -let in_elpi_float64 ~depth state f = - let state, f, _ = Coq_elpi_utils.float64.API.Conversion.embed ~depth state f in - state, E.mkApp primitivec (E.mkApp float64c f []) [] - -let in_elpi_proj ~depth state c x = - let np = Names.Projection.npars c in - let na = Names.Projection.arg c in - let state, p, _ = Coq_elpi_utils.projection.API.Conversion.embed ~depth state c in - state, in_elpi_appl ~depth (E.mkApp primitivec (E.mkApp projc p [CD.of_int @@ np + na]) []) [x] +let primitive_value : primitive_value API.Conversion.t = + let module B = Coq_elpi_utils in + let open API.AlgebraicData in declare { + ty = API.Conversion.TyName "primitive-value"; + doc = "Primitive values"; + pp = (fun fmt -> function + | Uint63 i -> Format.fprintf fmt "Type" + | Float64 f -> Format.fprintf fmt "Set" + | Projection p -> Format.fprintf fmt ""); + constructors = [ + K("uint63","unsigned integers over 63 bits",A(B.uint63,N), + B (fun x -> Uint63 x), + M (fun ~ok ~ko -> function Uint63 x -> ok x | _ -> ko ())); + K("float64","double precision foalting points",A(B.float64,N), + B (fun x -> Float64 x), + M (fun ~ok ~ko -> function Float64 x -> ok x | _ -> ko ())); + K("proj","primitive projection",A(B.projection,A(API.BuiltInData.int,N)), + B (fun p n -> Projection p), + M (fun ~ok ~ko -> function Projection p -> ok p Names.Projection.(arg p + npars p) | _ -> ko ())); + ] +} |> API.ContextualConversion.(!<) + +let in_elpi_primitive ~depth state i = + let state, i, _ = primitive_value.API.Conversion.embed ~depth state i in + state, E.mkApp primitivec i [] + (* ********************************* }}} ********************************** *) @@ -899,11 +914,12 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = state, in_elpi_fix name.Context.binder_name rarg typ bo | C.Proj(p,t) -> let state, t = aux ~depth env state t in - in_elpi_proj ~depth state p t + let state, p = in_elpi_primitive ~depth state (Projection p) in + state, in_elpi_app ~depth p [|t|] | C.Fix _ -> nYI "HOAS for mutual fix" | C.CoFix _ -> nYI "HOAS for cofix" - | C.Int i -> in_elpi_uint63 ~depth state i - | C.Float f -> in_elpi_float64 ~depth state f + | C.Int i -> in_elpi_primitive ~depth state (Uint63 i) + | C.Float f -> in_elpi_primitive ~depth state (Float64 f) | C.Array _ -> nYI "HOAS for persistent arrays" in if debug () then @@ -1241,9 +1257,9 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | x :: xs -> begin match E.look ~depth x, xs with | E.App(c,p,[]), i :: xs when primitivec == c -> - begin match E.look ~depth p with - | E.App(c,p,[_]) when projc == c -> - let state, p, gls = Coq_elpi_utils.projection.API.Conversion.readback ~depth state p in + let state, p, gls = primitive_value.API.Conversion.readback ~depth state p in + begin match p with + | Projection p -> let state, i, gl1 = aux ~depth state i in let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in state, EC.mkApp (EC.mkProj (p,i),Array.of_list xs), gls @ gl1 @ gl2 @@ -1309,19 +1325,13 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | _ -> err Pp.(str"Not an int: " ++ str (P.Debug.show_term rno)) in state, EC.mkFix (([|rno|],0),([|name|],[|ty|],[|bo|])), gl1 @ gl2 - | E.App(c,v,[]) when primitivec == c -> begin - match E.look ~depth v with - | E.App(c,i,[]) when uint63c == c -> - let state, i, gls = Coq_elpi_utils.uint63.API.Conversion.readback ~depth state i in - state, EC.mkInt i, gls - | E.App(c,f,[]) when float64c == c -> - let state, f, gls = Coq_elpi_utils.float64.API.Conversion.readback ~depth state f in - state, EC.mkFloat f, gls - | E.App(c,p,[_]) when projc == c -> - let state, p, gls = Coq_elpi_utils.projection.API.Conversion.readback ~depth state p in - state, EC.mkConst (Names.Projection.constant p), gls - | _ -> err Pp.(str"Not a HOAS primitive value:" ++ str (P.Debug.show_term t)) - end + | E.App(c,v,[]) when primitivec == c -> + let state, v, gls = primitive_value.API.Conversion.readback ~depth state v in + begin match v with + | Uint63 i -> state, EC.mkInt i, gls + | Float64 f -> state, EC.mkFloat f, gls + | Projection p -> state, EC.mkConst (Names.Projection.constant p), gls + end (* evar *) | E.UnifVar (elpi_evk,args) as x -> diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index 8a38148fe..fc562b962 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -122,9 +122,7 @@ val in_elpi_let : Name.t -> term -> term -> term -> term val in_elpi_appl : depth:int -> term -> term list -> term val in_elpi_match : term -> term -> term list -> term val in_elpi_fix : Name.t -> int -> term -> term -> term -val in_elpi_uint63 : depth:int -> state -> Uint63.t -> state * term -val in_elpi_float64 : depth:int -> state -> Float64.t -> state * term -val in_elpi_proj : depth:int -> state -> Projection.t -> term -> state * term + val in_elpi_name : Name.t -> term @@ -147,6 +145,12 @@ val global_constant_of_globref : Names.GlobRef.t -> global_constant val abbreviation : Globnames.syndef_name Conversion.t val implicit_kind : Glob_term.binding_kind Conversion.t val collect_term_variables : depth:int -> term -> Names.Id.t list +type primitive_value = + | Uint63 of Uint63.t + | Float64 of Float64.t + | Projection of Projection.t +val primitive_value : primitive_value Conversion.t +val in_elpi_primitive : depth:int -> state -> primitive_value -> state * term module GRMap : Elpi.API.Utils.Map.S with type key = Names.GlobRef.t module GRSet : Elpi.API.Utils.Set.S with type elt = Names.GlobRef.t diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index e7d2a2dd7..7b3c68df8 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1642,6 +1642,7 @@ denote the same x as before.|}; Some (c, np + na))))))), DocAbove); + MLData primitive_value; LPDoc "-- Universes --------------------------------------------------------"; diff --git a/src/coq_elpi_builtins_HOAS.ml b/src/coq_elpi_builtins_HOAS.ml index d62d7a8ae..f898f025f 100644 --- a/src/coq_elpi_builtins_HOAS.ml +++ b/src/coq_elpi_builtins_HOAS.ml @@ -73,11 +73,6 @@ type app list term -> term. % app [hd|args] type match term -> term -> list term -> term. % match t p [branch]) type fix name -> int -> term -> (term -> term) -> term. % fix name rno ty bo -kind primitive-value type. -type uint63 uint63 -> primitive-value. -type float64 float64 -> primitive-value. -type proj projection -> int -> primitive-value. - type primitive primitive-value -> term. diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 9105ae844..e604bd72b 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -193,10 +193,9 @@ let rec gterm2lp ~depth state x = let p = Projection.make p false in let npars = Projection.npars p in begin match CList.skipn npars args with - | i :: args -> - let state, i = gterm2lp ~depth state i in + | _ :: _ as args -> let state, args = CList.fold_left_map (gterm2lp ~depth) state args in - let state, p = in_elpi_proj ~depth state p i in + let state, p = in_elpi_primitive ~depth state (Projection p) in state, in_elpi_appl ~depth p args | [] -> CErrors.user_err ~hdr:"elpi quotation" Pp.(str"Coq primitive projection " ++ Projection.print p ++ str " has not enough arguments"); @@ -315,8 +314,8 @@ let rec gterm2lp ~depth state x = let state, bo = under_ctx (Name name) ty None gterm2lp ~depth state bo in state, in_elpi_fix (Name name) rno ty bo | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix" - | GInt i -> in_elpi_uint63 ~depth state i - | GFloat f -> in_elpi_float64 ~depth state f + | GInt i -> in_elpi_primitive ~depth state (Uint63 i) + | GFloat f -> in_elpi_primitive ~depth state (Float64 f) | GArray _ -> nYI "(glob)HOAS persistent arrays" ;; From 8ef6766e869cead5ab7e2a8f5445699cff55806b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jun 2021 10:02:53 +0200 Subject: [PATCH 21/22] cleanup warnings --- Changelog.md | 1 + examples/example_import_projections.v | 3 ++- tests/test_API.v | 17 +++++++++++++++-- tests/test_HOAS.v | 5 +++-- tests/test_quotation.v | 5 +++-- tests/test_tactic.v | 1 + 6 files changed, 25 insertions(+), 7 deletions(-) diff --git a/Changelog.md b/Changelog.md index e7e27e146..01a2f5112 100644 --- a/Changelog.md +++ b/Changelog.md @@ -24,6 +24,7 @@ Requires Elpi 1.13.6 and Coq 8.13. - Deprecate `coq.env.const-primitive?` -> `coq.env.primitive?` - Deprecate `coq.CS.canonical-projections` -> `coq.env.projections` - New `coq.env.primitive-projections` +- Change `coq.warning` emits the same warning only once ## [1.10.3] - 18-06-2021 diff --git a/examples/example_import_projections.v b/examples/example_import_projections.v index 20d874944..5f44e339f 100644 --- a/examples/example_import_projections.v +++ b/examples/example_import_projections.v @@ -59,7 +59,8 @@ Check refl_equal _ : p1 = 3. (* check the value of p1 is 3 *) End test. Set Primitive Projections. -Record r1 (A : Type) := { +Unset Auto Template Polymorphism. +Record r1 (A : Type) : Type := { f1 : A; f2 : nat; }. diff --git a/tests/test_API.v b/tests/test_API.v index 10b9968af..f6713544d 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -107,7 +107,7 @@ Elpi Accumulate lp:{{ main [indt-decl D] :- std.assert-ok! (coq.elaborate-indt-decl-skeleton D D1) "illtyped", coq.env.add-indt D1 _. - main [const-decl N (some BO) TYA] :- std.spy-do! [ + main [const-decl N (some BO) TYA] :- std.do! [ coq.arity->term TYA TY, std.assert-ok! (coq.elaborate-ty-skeleton TY _ TY1) "illtyped", std.assert-ok! (coq.elaborate-skeleton BO TY1 BO1) "illtyped", @@ -168,10 +168,21 @@ Elpi Query lp:{{ coq.say "hello world" }}. +Set Warnings "-elpi,-category". +Elpi Query lp:{{ + coq.warn "this is a generic warning". +}}. Elpi Query lp:{{ - coq.warn "this is a generic warning", coq.warning "category" "name" "this is a warning with a name an category". }}. +Set Warnings "+category". +Elpi Query lp:{{ + coq.warning "category" "name" "this is a warning with a name an category". +}}. +Fail Elpi Query lp:{{ + coq.warning "category" "name" "this is another warning with a name an category". +}}. +Set Warnings "elpi,category". (****** locate **********************************) @@ -401,6 +412,7 @@ Elpi Query lp:{{ Elpi Query lp:{{ coq.locate-module "Datatypes" MP, coq.env.module MP L }}. Module X. + Unset Auto Template Polymorphism. Inductive i := . Definition d := i. Module Y. @@ -480,6 +492,7 @@ Print ITA. (* section *) Section SA. +Unset Auto Template Polymorphism. Variable a : nat. Inductive ind := K. Section SB. diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 37a92645f..d2182b16f 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -24,7 +24,7 @@ Ltac foobar x := idtac x; eapply x. Elpi Tactic test2. Elpi Accumulate lp:{{ -solve (goal [decl T A B | _ ] _ _ _ _ as G) GS :- +solve (goal [decl T _ _ | _ ] _ _ _ _ as G) GS :- coq.ltac.call "foobar" [trm T] G GS, coq.say GS. @@ -103,7 +103,7 @@ Print foo1. Check foo1 _ _ _ _ : Type. Fail Check (foo1 _ _ _ _ _). Check a_k1 _ _ _ 3 _ : foo1 _ _ _ 3. - +Unset Auto Template Polymorphism. Inductive r (A : Type) (a : A) := R { f :> A -> A; g : A; p : a = g }. End inductive_nup. @@ -245,6 +245,7 @@ Elpi primitive (2.4e13 + 1). Module P. Set Primitive Projections. +Unset Auto Template Polymorphism. Record foo (A : Type) := { p1 : nat; p2 : A }. Definition x : foo bool := {| p1 := 3; p2 := false |}. diff --git a/tests/test_quotation.v b/tests/test_quotation.v index 83bb2defd..dfdd0efc3 100644 --- a/tests/test_quotation.v +++ b/tests/test_quotation.v @@ -56,6 +56,7 @@ X = {{ fun (r : nat) (p : forall y : nat, y = 0 :> nat) (q : bool) => lp:{{ {of Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). +Unset Auto Template Polymorphism. Record is_SUB (T : Type) (P : T -> bool) (sub_sort : Type) := SubType { val : sub_sort -> T; Sub : forall x, P x = true -> sub_sort; @@ -68,7 +69,7 @@ Structure ord u := Ord { oval : nat; prop : leq oval u = true }. Check fun u => SubType _ _ _ (oval u) _ inlined_sub_rect. -Elpi Query lp:{{ std.spy-do! [ +Elpi Query lp:{{ std.do! [ T = {{ fun u => SubType _ _ _ (oval u) _ inlined_sub_rect }}, std.assert-ok! (coq.elaborate-skeleton T _ T1) "does not typecheck", T1 = {{ fun u => SubType _ _ _ _ (lp:K u) _ }}, @@ -77,7 +78,7 @@ Elpi Query lp:{{ std.spy-do! [ }}. (* unfortunately the error message does not mention "unknown_inductive" *) -Fail Elpi Query lp:{{ std.spy-do! [ +Fail Elpi Query lp:{{ std.do! [ T = {{ fun u => SubType _ _ _ (oval u) _ inlined_sub_rect }}, std.assert-ok! (coq.typecheck T _) "does not typecheck", ] diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 16f5a809c..ba29cda69 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -320,6 +320,7 @@ split; intro x. all: exact (test.m (@eq_refl _ x)). Qed. +Set Warnings "-non-reversible-notation". Notation Foo pp := ltac:(elpi test.m (pp)). Goal (forall x : nat, x = x) /\ (forall x : bool, x = x). From 55871ccca40cae07eac95e8e7f359aaad2b83551 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jun 2021 10:03:16 +0200 Subject: [PATCH 22/22] cs-instance as in 8.14 --- Changelog.md | 3 ++- coq-builtin.elpi | 22 +++++++++++----------- src/coq_elpi_builtins.ml | 38 ++++++++++++++++++++++++++++++-------- tests/test_API.v | 2 +- 4 files changed, 44 insertions(+), 21 deletions(-) diff --git a/Changelog.md b/Changelog.md index 01a2f5112..28d728054 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,6 +1,6 @@ # Changelog -## [1.10.4] - 28-06-2021 +## [1.11.0] - 30-06-2021 Requires Elpi 1.13.6 and Coq 8.13. @@ -9,6 +9,7 @@ Requires Elpi 1.13.6 and Coq 8.13. projection name (a Coq detail) and the number of the field it projects (0 based), eg: `primitive (proj _ N)` stands for the projection for the Nth constructor field counting parameters. +- Change `cs-instance` carries a `gref` ### API - New `coq.notation.add-abbreviation-for-tactic` to add a parsing rule diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 1d0c4b335..ee89c8673 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -531,9 +531,6 @@ typeabbrev modpath (ctype "modpath"). typeabbrev modtypath (ctype "modtypath"). -typeabbrev projection (ctype "projection"). - - % -- Environment: read ------------------------------------------------ % Note: The type [term] is defined in coq-HOAS.elpi @@ -738,13 +735,6 @@ external pred coq.env.projections i:inductive, o:list (option constant). external pred coq.env.primitive-projections i:inductive, o:list (option (pair projection int)). -% Primitive values -kind primitive-value type. -type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits -type float64 float64 -> - primitive-value. % double precision foalting points -type proj projection -> int -> primitive-value. % primitive projection - % -- Universes -------------------------------------------------------- % Univ.Universe.t @@ -791,6 +781,16 @@ typeabbrev uint63 (ctype "uint63"). typeabbrev float64 (ctype "float64"). +typeabbrev projection (ctype "projection"). + + +% Primitive values +kind primitive-value type. +type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits +type float64 float64 -> + primitive-value. % double precision foalting points +type proj projection -> int -> primitive-value. % primitive projection + % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % API for extra logical objects @@ -807,7 +807,7 @@ type cs-sort universe -> cs-pattern. % Canonical Structure instances: (cs-instance Proj ValPat Inst) kind cs-instance type. -type cs-instance gref -> cs-pattern -> term -> cs-instance. +type cs-instance gref -> cs-pattern -> gref -> cs-instance. % [coq.CS.declare-instance GR] Declares GR as a canonical structure % instance. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 7b3c68df8..d6f8670de 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -447,7 +447,7 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Record doc = "Canonical Structure instances: (cs-instance Proj ValPat Inst)"; pp = (fun fmt (_,{ o_DEF }) -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((Printer.pr_constr_env (Global.env()) Evd.empty o_DEF))); constructors = [ - K("cs-instance","",A(gref,A(cs_pattern,CA(closed_ground_term,N))), (* XXX should be a gref *) + K("cs-instance","",A(gref,A(cs_pattern,A(gref,N))), B (fun p v i -> assert false), M (fun ~ok ~ko ((proj_gr,patt), { o_DEF = solution; (* c *) @@ -456,7 +456,7 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Record o_TABS = types; (* b1 .. bk *) o_TPARAMS = params; (* p1 .. pm *) o_NPARAMS = nparams; (* m *) - o_TCOMPS = cval_args }) -> ok proj_gr patt (EConstr.of_constr solution))) + o_TCOMPS = cval_args }) -> ok proj_gr patt (fst @@ Constr.destRef solution))) ] } @@ -942,8 +942,30 @@ let mode = let open API.AlgebraicData in let open Hints in declare { M (fun ~ok ~ko -> function ModeOutput -> ok | _ -> ko ())); ] } |> CConv.(!<) - - + +module WMsg = Set.Make(struct + type t = Loc.t option * string + let compare = Stdlib.compare +end) + +let coq_warning_cache : WMsg.t API.Data.StrMap.t ref = + ref API.Data.StrMap.empty +let coq_warning_cache category name loc txt = + let key = category ^ " " ^ name in + let msg = loc, txt in + try + let s = API.Data.StrMap.find key !coq_warning_cache in + if WMsg.mem msg s then false + else + let s = WMsg.add msg s in + coq_warning_cache := API.Data.StrMap.add key s !coq_warning_cache; + true + with + Not_found -> + coq_warning_cache := API.Data.StrMap.add key (WMsg.singleton msg) !coq_warning_cache; + true + + (*****************************************************************************) (*****************************************************************************) (*****************************************************************************) @@ -1034,7 +1056,8 @@ line option|}))), Some (Coq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args | _ -> None, x :: args in - warning ?loc (pp2string (P.list ~boxed:true pp " ") args); + let txt = pp2string (P.list ~boxed:true pp " ") args in + if coq_warning_cache category name loc txt then warning ?loc txt; state, ())), DocAbove); @@ -1071,7 +1094,6 @@ Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@b MLData id; MLData modpath; MLData modtypath; - MLData projection; ] @ [ @@ -1642,8 +1664,6 @@ denote the same x as before.|}; Some (c, np + na))))))), DocAbove); - MLData primitive_value; - LPDoc "-- Universes --------------------------------------------------------"; MLData univ; @@ -1727,6 +1747,8 @@ denote the same x as before.|}; MLData Coq_elpi_utils.uint63; MLData Coq_elpi_utils.float64; + MLData Coq_elpi_utils.projection; + MLData primitive_value; LPCode {| % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/tests/test_API.v b/tests/test_API.v index f6713544d..1667282f0 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -639,7 +639,7 @@ Elpi Query lp:{{ coq.locate "eq_op" P, coq.CS.db-for P _ [_,_] }}. Elpi Query lp:{{ coq.locate "W" W, coq.CS.db-for _ (cs-gref W) [_] }}. -Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "Z1" W, coq.CS.db-for P (cs-gref W) L, coq.say L, L = [cs-instance P (cs-gref W) {{myc1}}] }}. +Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "Z1" W, coq.CS.db-for P (cs-gref W) L, coq.say L, L = [cs-instance P (cs-gref W) {{:gref myc1}}] }}. Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "nat" W, coq.CS.db-for P (cs-gref W) [] }}.