diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-16 13:54:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-16 13:54:13 +0200 |
| commit | 978dd21af8467aa483bce551b3d5df8895cfff0f (patch) | |
| tree | 41f473bddf855d3daf179c83ed63166834ae3240 | |
| parent | 89f7bc53fbd558e3b5ff2ce1d1693f570afcc536 (diff) | |
| parent | 7bd00a63015c4017d8209a4d495b9683d33d1d53 (diff) | |
Make the Coq codebase independent from Ltac-related code.
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
94 files changed, 769 insertions, 519 deletions
diff --git a/dev/base_include b/dev/base_include index b09b6df2d..0abcefc38 100644 --- a/dev/base_include +++ b/dev/base_include @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; +let parse_tac = Pcoq.parse_string Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index fb1e805c1..00078c69f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,8 @@ = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= +* ML API * + We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr @@ -21,7 +23,18 @@ The following type aliases where removed Context.section_context ... it was just an alias for "Context.Named.t" which is still available -* ML API * +** Ltac API ** + +Many Ltac specific API has been moved in its own ltac/ folder. Amongst other +important things: + +- Pcoq.Tactic -> Pltac +- Constrarg.wit_tactic -> Tacarg.wit_tactic +- Constrarg.wit_ltac -> Tacarg.wit_ltac +- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument + instead +- Some printing functions were moved from Pptactic to Pputils +- A part of Tacexpr has been moved to Tactypes ** Error handling ** diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 2d5c40894..919ca3ad7 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -70,8 +70,8 @@ let rec mlexpr_of_prod_entry_key f = function | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >> - else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry (Pltac.binder_tactic) >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index a1b3f4f25..175853d50 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -61,7 +61,7 @@ let rec mlexpr_of_symbol = function <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> | Uentryl (e, l) -> assert (e = "tactic"); - let arg = get_argt <:expr< Constrarg.wit_tactic >> in + let arg = get_argt <:expr< Tacarg.wit_tactic >> in <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> let make_prod_item = function diff --git a/ide/richprinter.ml b/ide/richprinter.ml index 5f39f36ea..995cef1ac 100644 --- a/ide/richprinter.ml +++ b/ide/richprinter.ml @@ -2,7 +2,6 @@ open Richpp module RichppConstr = Ppconstr.Richpp module RichppVernac = Ppvernac.Richpp -module RichppTactic = Pptactic.Richpp type rich_pp = Ppannotation.t Richpp.located Xml_datatype.gxml diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008a..328ddd0cd 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -127,10 +127,6 @@ let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] [] let xmlProof loc xml = xmlWithLoc loc "proof" [] xml -let xmlRawTactic name rtac = - Element("rawtactic", ["name",name], - [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))]) - let xmlSectionSubsetDescr name ssd = Element("sectionsubsetdescr",["name",name], [PCData (Proof_using.to_string ssd)]) @@ -742,7 +738,7 @@ let rec tmpp v loc = | VernacShow _ as x -> xmlTODO loc x | VernacCheckGuard as x -> xmlTODO loc x | VernacProof (tac,using) -> - let tac = Option.map (xmlRawTactic "closingtactic") tac in + let tac = None (** FIXME *) in let using = Option.map (xmlSectionSubsetDescr "using") using in xmlProof loc (Option.List.(cons tac (cons using []))) | VernacProofMode name -> xmlProofMode loc name diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ca828102b..b8baa6401 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -7,8 +7,8 @@ (************************************************************************) open Loc -open Tacexpr open Misctypes +open Tactypes open Genarg open Geninterp @@ -30,11 +30,6 @@ let wit_int_or_var = let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = make0 "intropattern" -let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - make0 "tactic" - -let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" - let wit_ident = make0 "ident" @@ -61,9 +56,6 @@ let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = make0 "clause_dft_concl" -let wit_destruction_arg = - make0 "destruction_arg" - (** Aliases *) let wit_reference = wit_ref diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 6ccd944d4..4b542675b 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -17,8 +17,8 @@ open Globnames open Genredexpr open Pattern open Constrexpr -open Tacexpr open Misctypes +open Tactypes open Genarg (** FIXME: nothing to do there. *) @@ -60,20 +60,8 @@ val wit_red_expr : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type - -(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their - toplevel interpretation. The one of [wit_ltac] forces the tactic and - discards the result. *) -val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type - val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type -val wit_destruction_arg : - (constr_expr with_bindings destruction_arg, - glob_constr_and_expr with_bindings destruction_arg, - delayed_open_constr_with_bindings destruction_arg) genarg_type - (** Aliases for compatibility *) val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 630f8d140..fb11359e3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -660,23 +660,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let open Tacexpr in - let open Genarg in - let wit = glbwit Constrarg.wit_tactic in - let body = - if has_type arg wit then out_gen wit arg - else assert false (** FIXME *) - in - let mk_env id (c, (tmp_scope, subscopes)) accu = + let mk_env (c, (tmp_scope, subscopes)) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in let gc = intern nenv c in - let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in - ((loc, id), c) :: accu + (gc, Some c) in - let bindings = Id.Map.fold mk_env terms [] in - let tac = TacLetIn (false, bindings, body) in - let arg = in_gen wit tac in - Some arg + let bindings = Id.Map.map mk_env terms in + Some (Genintern.generic_substitute_notation bindings arg) in GHole (loc, knd, naming, arg) | NBinderList (x,y,iter,terminator) -> diff --git a/interp/genintern.ml b/interp/genintern.ml index d6bfd347f..be7abfa99 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -16,6 +16,7 @@ type glob_sign = { type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct @@ -31,8 +32,16 @@ struct let default _ = None end +module NtnSubstObj = +struct + type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun + let name = "notation_subst" + let default _ = None +end + module Intern = Register (InternObj) module Subst = Register (SubstObj) +module NtnSubst = Register (NtnSubstObj) let intern = Intern.obj let register_intern0 = Intern.register0 @@ -50,3 +59,12 @@ let generic_substitute subs (GenArg (Glbwit wit, v)) = in_gen (glbwit wit) (substitute wit subs v) let () = Hook.set Detyping.subst_genarg_hook generic_substitute + +(** Notation substitution *) + +let substitute_notation = NtnSubst.obj +let register_ntn_subst0 = NtnSubst.register0 + +let generic_substitute_notation env (GenArg (Glbwit wit, v)) = + let v = substitute_notation wit env v in + in_gen (glbwit wit) v diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b244b38d..4b0354be3 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun val generic_substitute : glob_generic_argument subst_fun +(** {5 Notation functions} *) + +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb + +val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun + +val generic_substitute_notation : glob_generic_argument ntn_subst_fun + (** Registering functions *) val register_intern0 : ('raw, 'glb, 'top) genarg_type -> @@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type -> val register_subst0 : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun -> unit + +val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb ntn_subst_fun -> unit diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 2df79673a..16f0c0c92 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -8,6 +8,8 @@ (** Reduction expressions *) +open Names + (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -50,5 +52,15 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (Loc.t * Names.Id.t) * 'a + | ConstrContext of (Loc.t * Id.t) * 'a | ConstrTypeOf of 'a + +open Libnames +open Constrexpr +open Misctypes + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 1452bbc34..e4f595ac4 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -108,3 +108,31 @@ type 'a or_by_notation = (** Kinds of modules *) type module_kind = Module | ModType | ModAny + +(** Various flags *) + +type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type letin_flag = bool (* true = use local def false = use Leibniz *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of Id.t Loc.located + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear diff --git a/intf/tactypes.mli b/intf/tactypes.mli new file mode 100644 index 000000000..b96cb67df --- /dev/null +++ b/intf/tactypes.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Tactic-related types that are not totally Ltac specific and still used in + lower API. It's not clear whether this is a temporary API or if this is + meant to stay. *) + +open Loc +open Names +open Constrexpr +open Glob_term +open Pattern +open Misctypes + +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern + +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } + +type delayed_open_constr = Term.constr delayed_open +type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open + +type intro_pattern = delayed_open_constr intro_pattern_expr located +type intro_patterns = delayed_open_constr intro_pattern_expr located list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located +type intro_pattern_naming = intro_pattern_naming_expr located diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df..5713b2ee6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -8,7 +8,6 @@ open Loc open Names -open Tacexpr open Misctypes open Constrexpr open Decl_kinds @@ -27,7 +26,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation to print a goal that is out of focus (or already solved) it doesn't make sense to apply a tactic to it. Hence it the types may look very similar, they do not seem to mean the same thing. *) -type goal_selector = Tacexpr.goal_selector = +type goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -130,7 +129,7 @@ type hints_expr = | HintsTransparency of reference list * bool | HintsMode of reference * hint_mode list | HintsConstructors of reference list - | HintsExtern of int * constr_expr option * raw_tactic_expr + | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument type search_restriction = | SearchInside of reference list @@ -171,7 +170,7 @@ type sort_expr = glob_sort type definition_expr = | ProveBody of local_binder list * constr_expr - | DefineBody of local_binder list * raw_red_expr option * constr_expr + | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type fixpoint_expr = @@ -432,9 +431,9 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * raw_red_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable | VernacSearch of searchable * int option * search_restriction | VernacLocate of locatable @@ -460,7 +459,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_expr option + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -473,10 +472,6 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) - (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or diff --git a/lib/future.mli b/lib/future.mli index 114c59176..c780faf32 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -87,7 +87,7 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation the value is not just the 'a but also the global system state *) val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation -(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook. +(* To get the fix_exn of a computation and build a Lemmas.declaration_hook. * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the * same state id that corresponds to the future computation end. I.e. Qed diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index c6d72e03e..1176772cd 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -12,6 +12,7 @@ open Pp open Genarg open Stdarg open Constrarg +open Tacarg open Pcoq.Prim open Pcoq.Constr open Names @@ -35,11 +36,11 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr -let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Constrarg.wit_intro_pattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520b..de701bb23 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -12,9 +12,10 @@ open Pp open Genarg open Stdarg open Constrarg +open Tacarg open Extraargs open Pcoq.Prim -open Pcoq.Tactic +open Pltac open Mod_subst open Names open Tacexpr @@ -53,7 +54,7 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) -let clause = Pcoq.Tactic.clause_dft_concl +let clause = Pltac.clause_dft_concl TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] @@ -983,7 +984,7 @@ let pr_cmp' _prc _prlc _prt = pr_cmp let pr_test_gen f (Test(c,x,y)) = Pp.(f x ++ pr_cmp c ++ f y) -let pr_test = pr_test_gen (Pptactic.pr_or_var Pp.int) +let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) let pr_test' _prc _prlc _prt = pr_test diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 8bc2ffd65..2165e826e 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -14,7 +14,8 @@ open Stdarg open Constrarg open Pcoq.Prim open Pcoq.Constr -open Pcoq.Tactic +open Pltac +open Hints open Tacexpr DECLARE PLUGIN "g_auto" diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index eaa6aad4f..b662057ba 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -10,9 +10,10 @@ open Misctypes open Class_tactics -open Pcoq.Tactic +open Pltac open Stdarg open Constrarg +open Tacarg DECLARE PLUGIN "g_class" diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c67af33e2..cce068910 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -19,8 +19,10 @@ open Genredexpr open Tok (* necessary for camlp4 *) open Pcoq +open Pcoq.Constr +open Pcoq.Vernac_ open Pcoq.Prim -open Pcoq.Tactic +open Pltac let fail_default_value = ArgArg 0 @@ -32,6 +34,7 @@ let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c +let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) @@ -72,14 +75,17 @@ let test_bracket_ident = (* Tactics grammar rules *) +let hint = G_proofs.hint + let warn_deprecated_appcontext = CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" (fun () -> strbrk "appcontext is deprecated and will be removed " ++ strbrk "in a future version") GEXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - tactic_mode constr_may_eval constr_eval selector toplevel_selector; + GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + tactic_mode constr_may_eval constr_eval selector toplevel_selector + operconstr; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -287,15 +293,15 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, TacFun (it, body)) + Tacexpr.TacticDefinition (id, TacFun (it, body)) | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, body) + if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, body) + Tacexpr.TacticDefinition (id, body) ] ] ; tactic: @@ -327,9 +333,28 @@ GEXTEND Gram tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] ; + command: + [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; + l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> + Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l) + | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; + ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> + Vernacexpr.VernacProof (ta,Some l) ] ] + ; + hint: + [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; + tac = Pltac.tactic -> + Vernacexpr.HintsExtern (n,c, in_tac tac) ] ] + ; + operconstr: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in + CHole (!@loc, None, IntroAnonymous, Some arg) ] ] + ; END open Constrarg +open Tacarg open Vernacexpr open Vernac_classifier open Goptions diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 987b9d538..fd531ca69 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -18,6 +18,7 @@ open Constrexpr open Constrexpr_ops open Stdarg open Constrarg +open Tacarg open Extraargs let (set_default_tactic, get_default_tactic, print_default_tactic) = @@ -30,12 +31,23 @@ let () = end in Obligations.default_tactic := tac +let with_tac f tac = + let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let tac = match tac with + | None -> None + | Some tac -> + let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in + let _, tac = Genintern.generic_intern env tac in + Some tac + in + f tac + (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac.<foo> *) module Gram = Pcoq.Gram -module Tactic = Pcoq.Tactic +module Tactic = Pltac open Pcoq @@ -66,6 +78,9 @@ GEXTEND Gram open Obligations +let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac + let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index 82b79c883..cdcbfdb7c 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -22,9 +22,10 @@ open Tacticals open Rewrite open Stdarg open Constrarg +open Pcoq.Vernac_ open Pcoq.Prim open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "g_rewrite" diff --git a/parsing/g_tactic.ml4 b/ltac/g_tactic.ml4 index 3c2c45c72..4e657fe83 100644 --- a/parsing/g_tactic.ml4 +++ b/ltac/g_tactic.ml4 @@ -120,7 +120,7 @@ let lookup_at_as_comma = open Constr open Prim -open Tactic +open Pltac let mk_fix_tac (loc,id,bl,ann,ty) = let n = @@ -217,6 +217,8 @@ let warn_deprecated_eqn_syntax = (* Auxiliary grammar rules *) +open Vernac_ + GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index fc51e48ae..af1c7149d 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,6 @@ +Tacarg +Pptactic +Pltac Taccoerce Tacsubst Tacenv @@ -5,6 +8,7 @@ Tactic_debug Tacintern Tacentries Profile_ltac +Tactic_matching Tacinterp Evar_tactics Tactic_option @@ -19,4 +23,5 @@ Rewrite G_rewrite Tauto G_eqdecide +G_tactic G_ltac diff --git a/ltac/pltac.ml b/ltac/pltac.ml new file mode 100644 index 000000000..94bf32d1d --- /dev/null +++ b/ltac/pltac.ml @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Pcoq + +(* Main entry for extensions *) +let simple_tactic = Gram.entry_create "tactic:simple_tactic" + +let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name) + +(* Entries that can be referred via the string -> Gram.entry table *) +(* Typically for tactic user extensions *) +let open_constr = + make_gen_entry utactic "open_constr" +let constr_with_bindings = + make_gen_entry utactic "constr_with_bindings" +let bindings = + make_gen_entry utactic "bindings" +let hypident = Gram.entry_create "hypident" +let constr_may_eval = make_gen_entry utactic "constr_may_eval" +let constr_eval = make_gen_entry utactic "constr_eval" +let uconstr = + make_gen_entry utactic "uconstr" +let quantified_hypothesis = + make_gen_entry utactic "quantified_hypothesis" +let destruction_arg = make_gen_entry utactic "destruction_arg" +let int_or_var = make_gen_entry utactic "int_or_var" +let simple_intropattern = + make_gen_entry utactic "simple_intropattern" +let clause_dft_concl = + make_gen_entry utactic "clause" + + +(* Main entries for ltac *) +let tactic_arg = Gram.entry_create "tactic:tactic_arg" +let tactic_expr = make_gen_entry utactic "tactic_expr" +let binder_tactic = make_gen_entry utactic "binder_tactic" + +let tactic = make_gen_entry utactic "tactic" + +(* Main entry for quotations *) +let tactic_eoi = eoi_entry tactic + +let () = + let open Stdarg in + let open Constrarg in + let open Tacarg in + register_grammar wit_int_or_var (int_or_var); + register_grammar wit_intro_pattern (simple_intropattern); + register_grammar wit_quant_hyp (quantified_hypothesis); + register_grammar wit_uconstr (uconstr); + register_grammar wit_open_constr (open_constr); + register_grammar wit_constr_with_bindings (constr_with_bindings); + register_grammar wit_bindings (bindings); + register_grammar wit_tactic (tactic); + register_grammar wit_ltac (tactic); + register_grammar wit_clause_dft_concl (clause_dft_concl); + register_grammar wit_destruction_arg (destruction_arg); + () diff --git a/ltac/pltac.mli b/ltac/pltac.mli new file mode 100644 index 000000000..27eb9f280 --- /dev/null +++ b/ltac/pltac.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Ltac parsing entries *) + +open Loc +open Names +open Pcoq +open Libnames +open Constrexpr +open Tacexpr +open Genredexpr +open Misctypes + +val open_constr : constr_expr Gram.entry +val constr_with_bindings : constr_expr with_bindings Gram.entry +val bindings : constr_expr bindings Gram.entry +val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry +val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry +val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry +val uconstr : constr_expr Gram.entry +val quantified_hypothesis : quantified_hypothesis Gram.entry +val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry +val int_or_var : int or_var Gram.entry +val simple_tactic : raw_tactic_expr Gram.entry +val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry +val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry +val tactic_arg : raw_tactic_arg Gram.entry +val tactic_expr : raw_tactic_expr Gram.entry +val binder_tactic : raw_tactic_expr Gram.entry +val tactic : raw_tactic_expr Gram.entry +val tactic_eoi : raw_tactic_expr Gram.entry diff --git a/printing/pptactic.ml b/ltac/pptactic.ml index e2c78a507..f738d2150 100644 --- a/printing/pptactic.ml +++ b/ltac/pptactic.ml @@ -16,12 +16,14 @@ open Tacexpr open Genarg open Geninterp open Constrarg +open Tacarg open Libnames open Ppextend open Misctypes open Locus open Decl_kinds open Genredexpr +open Pputils open Ppconstr open Printer @@ -62,19 +64,6 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds -let genarg_pprule = ref String.Map.empty - -let declare_extra_genarg_pprule wit f g h = - let s = match wit with - | ExtraArg s -> ArgT.repr s - | _ -> error - "Can declare a pretty-printing rule only for extra argument types." - in - let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in - let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in - let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in - genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule - module Make (Ppconstr : Ppconstrsig.Pp) (Taggers : sig @@ -135,80 +124,8 @@ module Make end | _ -> default - let pr_with_occurrences pr (occs,c) = - match occs with - | AllOccurrences -> - pr c - | NoOccurrences -> - failwith "pr_with_occurrences: no occurrences" - | OnlyOccurrences nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - | AllOccurrencesBut nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - - exception ComplexRedFlag - - let pr_short_red_flag pr r = - if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then - raise ComplexRedFlag - else if List.is_empty r.rConst then - if r.rDelta then mt () else raise ComplexRedFlag - else (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") - - let pr_red_flag pr r = - try pr_short_red_flag pr r - with complexRedFlags -> - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else - (if r.rMatch then pr_arg str "match" else mt ()) ++ - (if r.rFix then pr_arg str "fix" else mt ()) ++ - (if r.rCofix then pr_arg str "cofix" else mt ())) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - - let pr_union pr1 pr2 = function - | Inl a -> pr1 a - | Inr b -> pr2 b - - let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function - | Red false -> keyword "red" - | Hnf -> keyword "hnf" - | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) - ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o - | Cbv f -> - if f.rBeta && f.rMatch && f.rFix && f.rCofix && - f.rZeta && f.rDelta && List.is_empty f.rConst then - keyword "compute" - else - hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> - hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) - | Cbn f -> - hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) - | Unfold l -> - hov 1 (keyword "unfold" ++ spc() ++ - prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l) - | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> - hov 1 (keyword "pattern" ++ - pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l) - - | Red true -> - error "Shouldn't be accessible from user." - | ExtraRedExpr s -> - str s - | CbvVm o -> - keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o - | CbvNative o -> - keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o + let pr_with_occurrences pr c = pr_with_occurrences pr keyword c + let pr_red_expr pr c = pr_red_expr pr keyword c let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> @@ -232,10 +149,6 @@ module Make let pr_arg pr x = spc () ++ pr x - let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar (_,s) -> pr_id s - let pr_and_short_name pr (c,_) = pr c let pr_or_by_notation f = function @@ -300,52 +213,6 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let hov_if_not_empty n p = if Pp.ismt p then p else hov n p - - let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = - match wit with - | ListArg wit -> - let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - let ans = pr_sequence map x in - hov_if_not_empty 0 ans - | OptArg wit -> - let ans = match x with - | None -> mt () - | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) - in - hov_if_not_empty 0 ans - | PairArg (wit1, wit2) -> - let p, q = x in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - hov_if_not_empty 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) - | ExtraArg s -> - try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x) - with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x) - - - let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) = - match wit with - | ListArg wit -> - let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - let ans = pr_sequence map x in - hov_if_not_empty 0 ans - | OptArg wit -> - let ans = match x with - | None -> mt () - | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) - in - hov_if_not_empty 0 ans - | PairArg (wit1, wit2) -> - let p, q = x in - let p = in_gen (glbwit wit1) p in - let q = in_gen (glbwit wit2) q in - let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in - hov_if_not_empty 0 ans - | ExtraArg s -> - try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) - with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) - let rec tacarg_using_rule_token pr_gen = function | [] -> [] | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l @@ -1232,7 +1099,7 @@ module Make pr_constant = pr_or_by_notation pr_reference; pr_reference = pr_reference; pr_name = pr_lident; - pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference; + pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in @@ -1262,9 +1129,7 @@ module Make pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; - pr_generic = pr_glb_generic_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg); pr_extend = pr_glob_extend_rec (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); @@ -1312,12 +1177,9 @@ module Make in prtac n t - let pr_raw_generic env = pr_raw_generic_rec - pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference + let pr_raw_generic = Pputils.pr_raw_generic - let pr_glb_generic env = pr_glb_generic_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + let pr_glb_generic = Pputils.pr_glb_generic let pr_raw_extend env = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr @@ -1365,6 +1227,26 @@ include Make (Ppconstr) (struct let tag_atomic_tactic_expr = do_not_tag end) +let declare_extra_genarg_pprule wit + (f : 'a raw_extra_genarg_printer) + (g : 'b glob_extra_genarg_printer) + (h : 'c extra_genarg_printer) = + let s = match wit with + | ExtraArg s -> ArgT.repr s + | _ -> error + "Can declare a pretty-printing rule only for extra argument types." + in + let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let g x = + let env = Global.env () in + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + in + let h x = + let env = Global.env () in + h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + in + Genprint.register_print0 wit f g h + (** Registering *) let run_delayed c = @@ -1418,7 +1300,7 @@ let () = ; Genprint.register_print0 Constrarg.wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 Constrarg.wit_bindings @@ -1429,7 +1311,7 @@ let () = (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it))); - Genprint.register_print0 Constrarg.wit_destruction_arg + Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it)); @@ -1452,16 +1334,17 @@ module Richpp = struct include Make (Ppconstr.Richpp) (struct open Ppannotation + open Genarg let do_not_tag _ x = x let tag e s = Pp.tag (Pp.Tag.inj e tag) s let tag_keyword = tag AKeyword let tag_primitive = tag AKeyword let tag_string = do_not_tag () - let tag_glob_tactic_expr e = tag (AGlobTacticExpr e) - let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a) - let tag_raw_tactic_expr e = tag (ARawTacticExpr e) - let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a) - let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a) + let tag_glob_tactic_expr e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e)) + let tag_glob_atomic_tactic_expr = do_not_tag + let tag_raw_tactic_expr e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e)) + let tag_raw_atomic_tactic_expr = do_not_tag + let tag_atomic_tactic_expr = do_not_tag end) end diff --git a/printing/pptactic.mli b/ltac/pptactic.mli index 86e3ea548..86e3ea548 100644 --- a/printing/pptactic.mli +++ b/ltac/pptactic.mli diff --git a/printing/pptacticsig.mli b/ltac/pptacticsig.mli index c08d6044d..455cc1be1 100644 --- a/printing/pptacticsig.mli +++ b/ltac/pptacticsig.mli @@ -25,9 +25,7 @@ module type Pp = sig ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds - val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds - val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds val pr_clauses : bool option -> ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds diff --git a/ltac/tacarg.ml b/ltac/tacarg.ml new file mode 100644 index 000000000..42552c484 --- /dev/null +++ b/ltac/tacarg.ml @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Generic arguments based on Ltac. *) + +open Genarg +open Geninterp +open Tacexpr + +let make0 ?dyn name = + let wit = Genarg.make0 name in + let () = Geninterp.register_val0 wit dyn in + wit + +let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = + make0 "tactic" + +let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" + +let wit_destruction_arg = + make0 "destruction_arg" diff --git a/ltac/tacarg.mli b/ltac/tacarg.mli new file mode 100644 index 000000000..bfa423db2 --- /dev/null +++ b/ltac/tacarg.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Genarg +open Tacexpr +open Constrexpr +open Misctypes + +(** Generic arguments based on Ltac. *) + +val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type + +(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their + toplevel interpretation. The one of [wit_ltac] forces the tactic and + discards the result. *) +val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type + +val wit_destruction_arg : + (constr_expr with_bindings Tacexpr.destruction_arg, + glob_constr_and_expr with_bindings Tacexpr.destruction_arg, + delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type + diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2fed0e14f..2e2b55be7 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -43,8 +43,8 @@ let coincide s pat off = !break let atactic n = - if n = 5 then Aentry Tactic.binder_tactic - else Aentryl (Tactic.tactic_expr, n) + if n = 5 then Aentry Pltac.binder_tactic + else Aentryl (Pltac.tactic_expr, n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name @@ -56,9 +56,9 @@ let get_tacentry n m = && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) in - if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself) - else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext) - else EntryName (rawwit Constrarg.wit_tactic, atactic n) + if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself) + else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext) + else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function | None -> error "Missing separator." @@ -108,11 +108,11 @@ let interp_entry_name interp symb = let get_tactic_entry n = if Int.equal n 0 then - Tactic.simple_tactic, None + Pltac.simple_tactic, None else if Int.equal n 5 then - Tactic.binder_tactic, None + Pltac.binder_tactic, None else if 1<=n && n<5 then - Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -163,7 +163,7 @@ let add_tactic_entry (kn, ml, tg) state = let mkact loc l = let map arg = (** HACK to handle especially the tactic(...) entry *) - let wit = Genarg.rawwit Constrarg.wit_tactic in + let wit = Genarg.rawwit Tacarg.wit_tactic in if Genarg.has_type arg wit && not ml then Tacexp (Genarg.out_gen wit arg) else @@ -218,7 +218,7 @@ let interp_prod_item = function | Some n -> (** FIXME: do better someday *) assert (String.equal s "tactic"); - begin match Constrarg.wit_tactic with + begin match Tacarg.wit_tactic with | ExtraArg tag -> ArgT.Any tag | _ -> assert false end @@ -405,7 +405,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) (** Command *) @@ -425,7 +425,7 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then @@ -434,14 +434,14 @@ let register_ltac local tacl = in let is_shadowed = try - match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with + match Pcoq.parse_string Pltac.tactic (Id.to_string id) with | Tacexpr.TacArg _ -> false | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) @@ -511,3 +511,15 @@ let print_ltacs () = hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) + +(** Grammar *) + +let () = + let open Metasyntax in + let entries = [ + AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.binder_tactic; + AnyEntry Pltac.simple_tactic; + AnyEntry Pltac.tactic_arg; + ] in + register_grammar "tactic" entries diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 27df819ee..969c118fb 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -13,7 +13,7 @@ open Tacexpr (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) diff --git a/intf/tacexpr.mli b/ltac/tacexpr.mli index 5b5957bef..9c25a1645 100644 --- a/intf/tacexpr.mli +++ b/ltac/tacexpr.mli @@ -32,15 +32,13 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) - -type goal_selector = +type goal_selector = Vernacexpr.goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll -type 'a core_destruction_arg = +type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of Id.t located | ElimOnAnonHyp of int @@ -48,7 +46,7 @@ type 'a core_destruction_arg = type 'a destruction_arg = clear_flag * 'a core_destruction_arg -type inversion_kind = +type inversion_kind = Misctypes.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear @@ -79,12 +77,6 @@ type ('constr,'dconstr,'id) induction_clause_list = type 'a with_bindings_arg = clear_flag * 'a with_bindings -type multi = - | Precisely of int - | UpTo of int - | RepeatStar - | RepeatPlus - (* Type of patterns *) type 'a match_pattern = | Term of 'a @@ -117,18 +109,15 @@ type ml_tactic_entry = { (** Composite types *) -(** In globalize tactics, we need to keep the initial [constr_expr] to recompute - in the environment by the effective calls to Intro, Inversion, etc - The [constr_expr] field is [None] in TacDef though *) -type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option +type glob_constr_and_expr = Tactypes.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr -type binding_bound_vars = Id.Set.t +type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = 'a Pretyping.delayed_open = +type 'a delayed_open = 'a Tactypes.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open @@ -401,3 +390,7 @@ type ltac_call_kind = | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map type ltac_trace = (Loc.t * ltac_call_kind) list + +type tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index cd791398d..b0b4dc357 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -24,6 +24,7 @@ open Termops open Tacexpr open Genarg open Constrarg +open Tacarg open Misctypes open Locus @@ -775,13 +776,16 @@ let intern_ident' ist id = let lf = ref Id.Set.empty in (ist, intern_ident lf ist id) +let intern_ltac ist tac = + Flags.with_option strict_check (fun () -> intern_pure_tactic ist tac) () + let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); - Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg); + Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); @@ -792,15 +796,17 @@ let () = Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg); () -(***************************************************************************) -(* Backwarding recursive needs of tactic glob/interp/eval functions *) +(** Substitution for notations containing tactic-in-terms *) -let _ = - let f l = - let ltacvars = - List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l - in - Flags.with_option strict_check - (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) +let notation_subst bindings tac = + let fold id c accu = + let loc = Glob_ops.loc_of_glob_constr (fst c) in + let c = ConstrMayEval (ConstrTerm c) in + ((loc, id), c) :: accu in - Hook.set Hints.extern_intern_tac f + let bindings = Id.Map.fold fold bindings [] in + (** This is theoretically not correct due to potential variable capture, but + Ltac has no true variables so one cannot simply substitute *) + TacLetIn (false, bindings, tac) + +let () = Genintern.register_ntn_subst0 wit_tactic notation_subst diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 177867abd..a65e58ddb 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -32,6 +32,7 @@ open Genarg open Geninterp open Stdarg open Constrarg +open Tacarg open Printer open Pretyping open Misctypes @@ -1969,7 +1970,6 @@ let interp_tac_gen lfun avoid_ids debug t = end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t -let _ = Proof_global.set_interp_tac interp (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index cce4382c2..e0fdc4e5a 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -11,6 +11,7 @@ open Tacexpr open Mod_subst open Genarg open Constrarg +open Tacarg open Misctypes open Globnames open Term diff --git a/tactics/tactic_matching.ml b/ltac/tactic_matching.ml index ef45ee47e..ef45ee47e 100644 --- a/tactics/tactic_matching.ml +++ b/ltac/tactic_matching.ml diff --git a/tactics/tactic_matching.mli b/ltac/tactic_matching.mli index 090207bcc..090207bcc 100644 --- a/tactics/tactic_matching.mli +++ b/ltac/tactic_matching.mli diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7021e5270..ccc7c55a8 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -215,9 +215,6 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in - CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; record_declaration: diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1e3c4b880..2adbf300e 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -13,7 +13,6 @@ open Misctypes open Tok open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ @@ -26,9 +25,11 @@ let hint_proof_using e = function | None -> None | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) +let hint = Gram.entry_create "hint" + (* Proof commands *) GEXTEND Gram - GLOBAL: command; + GLOBAL: hint command; opt_hintbases: [ [ -> [] @@ -39,12 +40,6 @@ GEXTEND Gram | IDENT "Proof" -> VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn - | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = tactic -> ta ] -> - VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll @@ -124,10 +119,7 @@ GEXTEND Gram | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid - | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc - | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; - tac = tactic -> - HintsExtern (n,c,tac) ] ] + | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ] ; constr_body: [ [ ":="; c = lconstr -> c diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7cb897cf7..51c4733aa 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -260,7 +260,7 @@ GEXTEND Gram ProveBody (bl, t) ] ] ; reduce: - [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r + [ [ IDENT "Eval"; r = red_expr; "in" -> Some r | -> None ] ] ; one_decl_notation: @@ -867,7 +867,7 @@ GEXTEND Gram VernacRemoveOption ([table], v) ]] ; query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Compute"; c = lconstr -> fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) @@ -1024,7 +1024,7 @@ GEXTEND Gram (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; - r = Tactic.red_expr -> + r = red_expr -> VernacDeclareReduction (s,r) ] ]; diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 8df519b56..05e2911c2 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -2,4 +2,3 @@ G_constr G_vernac G_prim G_proofs -G_tactic diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 714e25f85..e3a66dc11 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -324,47 +324,6 @@ module Module = let module_type = Gram.entry_create "module_type" end -module Tactic = - struct - (* Main entry for extensions *) - let simple_tactic = Gram.entry_create "tactic:simple_tactic" - - (* Entries that can be referred via the string -> Gram.entry table *) - (* Typically for tactic user extensions *) - let open_constr = - make_gen_entry utactic "open_constr" - let constr_with_bindings = - make_gen_entry utactic "constr_with_bindings" - let bindings = - make_gen_entry utactic "bindings" - let hypident = Gram.entry_create "hypident" - let constr_may_eval = make_gen_entry utactic "constr_may_eval" - let constr_eval = make_gen_entry utactic "constr_eval" - let uconstr = - make_gen_entry utactic "uconstr" - let quantified_hypothesis = - make_gen_entry utactic "quantified_hypothesis" - let destruction_arg = make_gen_entry utactic "destruction_arg" - let int_or_var = make_gen_entry utactic "int_or_var" - let red_expr = make_gen_entry utactic "red_expr" - let simple_intropattern = - make_gen_entry utactic "simple_intropattern" - let clause_dft_concl = - make_gen_entry utactic "clause" - - - (* Main entries for ltac *) - let tactic_arg = Gram.entry_create "tactic:tactic_arg" - let tactic_expr = make_gen_entry utactic "tactic_expr" - let binder_tactic = make_gen_entry utactic "binder_tactic" - - let tactic = make_gen_entry utactic "tactic" - - (* Main entry for quotations *) - let tactic_eoi = eoi_entry tactic - - end - module Vernac_ = struct let gec_vernac s = Gram.entry_create ("vernac:" ^ s) @@ -377,6 +336,7 @@ module Vernac_ = let vernac = gec_vernac "Vernac.vernac" let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" + let red_expr = make_gen_entry utactic "red_expr" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" let noedit_mode = gec_vernac "noedit_command" @@ -499,26 +459,12 @@ let with_grammar_rule_protection f x = let () = let open Stdarg in let open Constrarg in -(* Grammar.register0 wit_unit; *) -(* Grammar.register0 wit_bool; *) Grammar.register0 wit_int (Prim.integer); Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); - Grammar.register0 wit_int_or_var (Tactic.int_or_var); - Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern); Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); - Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_uconstr (Tactic.uconstr); - Grammar.register0 wit_open_constr (Tactic.open_constr); - Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); - Grammar.register0 wit_bindings (Tactic.bindings); -(* Grammar.register0 wit_hyp_location_flag; *) - Grammar.register0 wit_red_expr (Tactic.red_expr); - Grammar.register0 wit_tactic (Tactic.tactic); - Grammar.register0 wit_ltac (Tactic.tactic); - Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); - Grammar.register0 wit_destruction_arg (Tactic.destruction_arg); + Grammar.register0 wit_red_expr (Vernac_.red_expr); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 635b0170a..82ec49417 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -12,7 +12,6 @@ open Extend open Vernacexpr open Genarg open Constrexpr -open Tacexpr open Libnames open Misctypes open Genredexpr @@ -177,29 +176,6 @@ module Module : val module_type : module_ast Gram.entry end -module Tactic : - sig - val open_constr : constr_expr Gram.entry - val constr_with_bindings : constr_expr with_bindings Gram.entry - val bindings : constr_expr bindings Gram.entry - val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry - val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry - val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry - val uconstr : constr_expr Gram.entry - val quantified_hypothesis : quantified_hypothesis Gram.entry - val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry - val int_or_var : int or_var Gram.entry - val red_expr : raw_red_expr Gram.entry - val simple_tactic : raw_tactic_expr Gram.entry - val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry - val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry - val tactic_arg : raw_tactic_arg Gram.entry - val tactic_expr : raw_tactic_expr Gram.entry - val binder_tactic : raw_tactic_expr Gram.entry - val tactic : raw_tactic_expr Gram.entry - val tactic_eoi : raw_tactic_expr Gram.entry - end - module Vernac_ : sig val gallina : vernac_expr Gram.entry @@ -211,6 +187,7 @@ module Vernac_ : val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry + val red_expr : raw_red_expr Gram.entry end (** The main entry: reads an optional vernac command *) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 6c17dcc4f..18a35c6cf 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,7 +19,7 @@ open Vernacexpr open Tok (* necessary for camlp4 *) open Pcoq.Constr -open Pcoq.Tactic +open Pltac open Ppdecl_proof let pr_goal gs = diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 95095b09c..487162687 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -16,6 +16,7 @@ open Tacticals open Tacinterp open Libnames open Constrarg +open Tacarg open Stdarg open Pcoq.Prim diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 42e490315..6368c2536 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -18,7 +18,7 @@ open Constrarg open Misctypes open Pcoq.Prim open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "recdef_plugin" @@ -143,7 +143,7 @@ END module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic +module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 027f690fc..aadcf060e 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -17,6 +17,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Constrarg +open Tacarg DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index fd87d5b7d..ebd19428f 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -14,6 +14,7 @@ open Tacexpr open Geninterp open Quote open Constrarg +open Tacarg DECLARE PLUGIN "quote_plugin" diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 216eb8b37..13e225404 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -16,8 +16,9 @@ open Newring_ast open Newring open Stdarg open Constrarg +open Tacarg open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "newring_plugin" diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 5fb0bb664..099918c35 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -20,6 +20,7 @@ open Pp open Pcoq open Genarg open Constrarg +open Tacarg open Term open Vars open Topconstr @@ -41,7 +42,7 @@ open Proofview.Notations open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886a98263..5ec44a68d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -45,6 +45,7 @@ open Context.Rel.Declaration *) +type binding_bound_vars = Id.Set.t type bound_ident_map = Id.t Id.Map.t exception PatternMatchingFailure diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 8d8166f22..ee6c5141b 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -13,6 +13,8 @@ open Term open Environ open Pattern +type binding_bound_vars = Id.Set.t + (** [PatternMatchingFailure] is the exception raised when pattern matching fails *) exception PatternMatchingFailure @@ -41,7 +43,7 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map variables or metavariables have the same name, the metavariable, or else the rightmost bound variable, takes precedence *) val extended_matches : - env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern -> + env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> bound_ident_map * extended_patvar_map (** [is_matching pat c] just tells if [c] matches against [pat] *) @@ -75,7 +77,7 @@ val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matchi (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) -> - Tacexpr.binding_bound_vars * constr_pattern -> constr -> + binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 13e5ea97a..aee3405f0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_ops open Evarconv open Pattern open Misctypes +open Tactypes open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -59,8 +60,6 @@ type ltac_var_map = { } type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } (************************************************************************) (* This concerns Cases *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 824bb11aa..f015813af 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -55,9 +55,6 @@ type inference_flags = { expand_evars : bool } -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } - val default_inference_flags : bool -> inference_flags val no_classes_no_fail_inference_flags : inference_flags @@ -120,7 +117,7 @@ val understand_judgment_tcc : env -> evar_map ref -> val type_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver diff --git a/printing/genprint.ml b/printing/genprint.ml index 0ec35e07b..6505a8f82 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -9,15 +9,17 @@ open Pp open Genarg -type ('raw, 'glb, 'top) printer = { - raw : 'raw -> std_ppcmds; - glb : 'glb -> std_ppcmds; - top : 'top -> std_ppcmds; +type 'a printer = 'a -> std_ppcmds + +type ('raw, 'glb, 'top) genprinter = { + raw : 'raw printer; + glb : 'glb printer; + top : 'top printer; } module PrintObj = struct - type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer + type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter let name = "printer" let default wit = match wit with | ExtraArg tag -> diff --git a/printing/genprint.mli b/printing/genprint.mli index 6e6626f2f..5381fc5bd 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -11,6 +11,8 @@ open Pp open Genarg +type 'a printer = 'a -> std_ppcmds + val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds (** Printer for raw level generic arguments. *) @@ -20,9 +22,9 @@ val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds (** Printer for top level generic arguments. *) -val generic_raw_print : rlevel generic_argument -> std_ppcmds -val generic_glb_print : glevel generic_argument -> std_ppcmds -val generic_top_print : tlevel generic_argument -> std_ppcmds +val generic_raw_print : rlevel generic_argument printer +val generic_glb_print : glevel generic_argument printer +val generic_top_print : tlevel generic_argument printer val register_print0 : ('raw, 'glb, 'top) genarg_type -> - ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit + 'raw printer -> 'glb printer -> 'top printer -> unit diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml index 511f93569..24b4c1515 100644 --- a/printing/ppannotation.ml +++ b/printing/ppannotation.ml @@ -10,28 +10,23 @@ open Ppextend open Constrexpr open Vernacexpr open Tacexpr +open Genarg type t = | AKeyword | AUnparsing of unparsing | AConstrExpr of constr_expr | AVernac of vernac_expr - | AGlobTacticExpr of glob_tactic_expr - | AGlobAtomicTacticExpr of glob_atomic_tactic_expr - | ARawTacticExpr of raw_tactic_expr - | ARawAtomicTacticExpr of raw_atomic_tactic_expr - | AAtomicTacticExpr of atomic_tactic_expr + | AGlbGenArg of glob_generic_argument + | ARawGenArg of raw_generic_argument let tag_of_annotation = function | AKeyword -> "keyword" | AUnparsing _ -> "unparsing" | AConstrExpr _ -> "constr_expr" | AVernac _ -> "vernac_expr" - | AGlobTacticExpr _ -> "glob_tactic_expr" - | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr" - | ARawTacticExpr _ -> "raw_tactic_expr" - | ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr" - | AAtomicTacticExpr _ -> "atomic_tactic_expr" + | AGlbGenArg _ -> "glob_generic_argument" + | ARawGenArg _ -> "raw_generic_argument" let attributes_of_annotation a = [] diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index a0fef1a75..b0e0facef 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -12,18 +12,15 @@ open Ppextend open Constrexpr open Vernacexpr -open Tacexpr +open Genarg type t = | AKeyword | AUnparsing of unparsing | AConstrExpr of constr_expr | AVernac of vernac_expr - | AGlobTacticExpr of glob_tactic_expr - | AGlobAtomicTacticExpr of glob_atomic_tactic_expr - | ARawTacticExpr of raw_tactic_expr - | ARawAtomicTacticExpr of raw_atomic_tactic_expr - | AAtomicTacticExpr of atomic_tactic_expr + | AGlbGenArg of glob_generic_argument + | ARawGenArg of raw_generic_argument val tag_of_annotation : t -> string diff --git a/printing/pputils.ml b/printing/pputils.ml index 906b463a8..33382fe83 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -6,10 +6,143 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp +open Genarg +open Nameops +open Misctypes +open Locus +open Genredexpr let pr_located pr (loc, x) = if Flags.do_beautify () && loc <> Loc.ghost then let (b, e) = Loc.unloc loc in Pp.comment b ++ pr x ++ Pp.comment e else pr x + +let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar (_,s) -> pr_id s + +let pr_with_occurrences pr keyword (occs,c) = + match occs with + | AllOccurrences -> + pr c + | NoOccurrences -> + failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + +exception ComplexRedFlag + +let pr_short_red_flag pr r = + if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then + raise ComplexRedFlag + else if List.is_empty r.rConst then + if r.rDelta then mt () else raise ComplexRedFlag + else (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") + +let pr_red_flag pr r = + try pr_short_red_flag pr r + with complexRedFlags -> + (if r.rBeta then pr_arg str "beta" else mt ()) ++ + (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else + (if r.rMatch then pr_arg str "match" else mt ()) ++ + (if r.rFix then pr_arg str "fix" else mt ()) ++ + (if r.rCofix then pr_arg str "cofix" else mt ())) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then + if r.rDelta then pr_arg str "delta" + else mt () + else + pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) + +let pr_union pr1 pr2 = function + | Inl a -> pr1 a + | Inr b -> pr2 b + +let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function + | Red false -> keyword "red" + | Hnf -> keyword "hnf" + | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) + ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + | Cbv f -> + if f.rBeta && f.rMatch && f.rFix && f.rCofix && + f.rZeta && f.rDelta && List.is_empty f.rConst then + keyword "compute" + else + hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) + | Lazy f -> + hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) + | Cbn f -> + hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) + | Unfold l -> + hov 1 (keyword "unfold" ++ spc() ++ + prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l) + | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) + | Pattern l -> + hov 1 (keyword "pattern" ++ + pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) + + | Red true -> + CErrors.error "Shouldn't be accessible from user." + | ExtraRedExpr s -> + str s + | CbvVm o -> + keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + | CbvNative o -> + keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + +let pr_or_by_notation f = function + | AN v -> f v + | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + +let hov_if_not_empty n p = if Pp.ismt p then p else hov n p + +let rec pr_raw_generic env (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_raw_generic env (in_gen (rawwit wit) x) in + let ans = pr_sequence map x in + hov_if_not_empty 0 ans + | OptArg wit -> + let ans = match x with + | None -> mt () + | Some x -> pr_raw_generic env (in_gen (rawwit wit) x) + in + hov_if_not_empty 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q]) + | ExtraArg s -> + Genprint.generic_raw_print (in_gen (rawwit wit) x) + + +let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_glb_generic env (in_gen (glbwit wit) x) in + let ans = pr_sequence map x in + hov_if_not_empty 0 ans + | OptArg wit -> + let ans = match x with + | None -> mt () + | Some x -> pr_glb_generic env (in_gen (glbwit wit) x) + in + hov_if_not_empty 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic env) [p; q] in + hov_if_not_empty 0 ans + | ExtraArg s -> + Genprint.generic_glb_print (in_gen (glbwit wit) x) diff --git a/printing/pputils.mli b/printing/pputils.mli index a0f2c7728..b236fed70 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -7,7 +7,25 @@ (************************************************************************) open Pp +open Genarg +open Misctypes +open Locus +open Genredexpr val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds (** Prints an object surrounded by its commented location *) +val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds +val pr_with_occurrences : + ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds + +val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds +val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds +val pr_red_expr : + ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> + (string -> std_ppcmds) -> + ('a,'b,'c) red_expr_gen -> std_ppcmds + +val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds +val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0..51fc289b4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -21,7 +21,6 @@ open Decl_kinds module Make (Ppconstr : Ppconstrsig.Pp) - (Pptactic : Pptacticsig.Pp) (Taggers : sig val tag_keyword : std_ppcmds -> std_ppcmds val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds @@ -30,7 +29,6 @@ module Make open Taggers open Ppconstr - open Pptactic let keyword s = tag_keyword (str s) @@ -67,7 +65,7 @@ module Make | (loc,Name id) -> pr_lident (loc,id) | lna -> pr_located pr_name lna - let pr_smart_global = pr_or_by_notation pr_reference + let pr_smart_global = Pputils.pr_or_by_notation pr_reference let pr_ltac_ref = Libnames.pr_reference @@ -81,7 +79,7 @@ module Make | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = pr_raw_generic (Global.env ()) t + let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() @@ -195,7 +193,7 @@ module Make | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ - spc() ++ pr_raw_tactic tac + spc() ++ Pputils.pr_raw_generic (Global.env ()) tac in hov 2 (keyword "Hint "++ pph ++ opth) @@ -703,7 +701,7 @@ module Make | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1127,7 +1125,7 @@ module Make let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1138,7 +1136,7 @@ module Make | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) @@ -1179,12 +1177,12 @@ module Make return (keyword "Proof " ++ spc () ++ keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) + return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te) | VernacProof (Some te, Some e) -> return ( keyword "Proof" ++ spc () ++ keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++pr_raw_tactic te + keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te ) | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) @@ -1223,7 +1221,7 @@ module Make end -include Make (Ppconstr) (Pptactic) (struct +include Make (Ppconstr) (struct let do_not_tag _ x = x let tag_keyword = do_not_tag () let tag_vernac = do_not_tag @@ -1233,7 +1231,6 @@ module Richpp = struct include Make (Ppconstr.Richpp) - (Pptactic.Richpp) (struct open Ppannotation let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s diff --git a/printing/printing.mllib b/printing/printing.mllib index bc8f0750e..b0141b6d3 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -3,7 +3,6 @@ Pputils Ppannotation Ppconstr Printer -Pptactic Printmod Prettyp Ppvernac diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index aa091aecd..8a096b645 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -10,8 +10,8 @@ open Term open Clenv -open Tacexpr open Unification +open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9b0200039..f2f4b11ed 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -124,7 +124,7 @@ val get_all_proof_names : unit -> Id.t list (** [set_end_tac tac] applies tactic [tac] to all subgoal generate by [solve] *) -val set_end_tac : Tacexpr.raw_tactic_expr -> unit +val set_end_tac : Genarg.glob_generic_argument -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f3ca19a90..2956d623f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -90,7 +90,7 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; terminator : proof_terminator CEphemeron.key; - endline_tactic : Tacexpr.raw_tactic_expr option; + endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; proof : Proof.proof; strength : Decl_kinds.goal_kind; @@ -148,9 +148,6 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let get_current_proof_name () = (cur_pstate ()).pid -let interp_tac = ref (fun _ -> assert false) -let set_interp_tac f = interp_tac := f - let with_current_proof f = match !pstates with | [] -> raise NoCurrentProof @@ -158,7 +155,13 @@ let with_current_proof f = let et = match p.endline_tactic with | None -> Proofview.tclUNIT () - | Some tac -> !interp_tac tac in + | Some tac -> + let open Geninterp in + let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in + let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in + let tac = Geninterp.interp tag ist tac in + Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) + in let (newpr,ret) = f et p.proof in let p = { p with proof = newpr } in pstates := p :: rest; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 86fc1deff..97a21cf22 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -134,10 +134,7 @@ val simple_with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit -val set_interp_tac : - (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) - -> unit +val set_endline_tactic : Genarg.glob_generic_argument -> unit (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) + a list of diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f7798a0ed..ff60ae5bf 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,7 +11,6 @@ open Evd open Names open Term -open Tacexpr open Glob_term open Nametab open Misctypes diff --git a/tactics/auto.ml b/tactics/auto.ml index 962af4b5c..b85328402 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -20,7 +20,6 @@ open Genredexpr open Tactics open Tacticals open Clenv -open Tacexpr open Locus open Proofview.Notations open Hints diff --git a/tactics/auto.mli b/tactics/auto.mli index 1608a0ea6..1689bd73c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -14,6 +14,7 @@ open Clenv open Pattern open Decl_kinds open Hints +open Tactypes val priority : ('a * full_hint) list -> ('a * full_hint) list @@ -39,45 +40,45 @@ val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argume (** The use of the "core" database can be de-activated by passing "nocore" amongst the databases. *) -val auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val auto : ?debug:debug -> + int -> delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic (** Auto with more delta. *) -val new_auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val new_auto : ?debug:debug -> + int -> delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic (** auto with default search depth and with the hint database "core" *) val default_auto : unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database *) -val full_auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic +val full_auto : ?debug:debug -> + int -> delayed_open_constr list -> unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database and doing delta *) -val new_full_auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic +val new_full_auto : ?debug:debug -> + int -> delayed_open_constr list -> unit Proofview.tactic (** auto with default search depth and with all hint databases except the "v62" compatibility database *) val default_full_auto : unit Proofview.tactic (** The generic form of auto (second arg [None] means all bases) *) -val gen_auto : ?debug:Tacexpr.debug -> - int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val gen_auto : ?debug:debug -> + int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic (** The hidden version of auto *) -val h_auto : ?debug:Tacexpr.debug -> - int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val h_auto : ?debug:debug -> + int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic (** Trivial *) -val trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic -val gen_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic -val full_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> unit Proofview.tactic -val h_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val trivial : ?debug:debug -> + delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val gen_trivial : ?debug:debug -> + delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val full_trivial : ?debug:debug -> + delayed_open_constr list -> unit Proofview.tactic +val h_trivial : ?debug:debug -> + delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 7628b7885..dae1cc9f1 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -83,7 +83,7 @@ let print_rewrite_hintdb bas = str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ - Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) + Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 070657179..49e8588da 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -9,7 +9,6 @@ (** This files implements the autorewrite tactic. *) open Term -open Tacexpr open Equality (** Rewriting rules before tactic interpretation *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index ba2195070..bac4d27c3 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -20,7 +20,7 @@ open Tactics open Clenv open Auto open Genredexpr -open Tacexpr +open Tactypes open Locus open Locusops open Hints @@ -203,7 +203,7 @@ type search_state = { dblist : hint_db list; localdb : hint_db list; prev : prev_search_state; - local_lemmas : Tacexpr.delayed_open_constr list; + local_lemmas : delayed_open_constr list; } and prev_search_state = (* for info eauto *) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 8812093d5..1f69e4ab3 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -9,6 +9,7 @@ open Term open Proof_type open Hints +open Tactypes val e_assumption : unit Proofview.tactic @@ -16,15 +17,15 @@ val registered_e_assumption : unit Proofview.tactic val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic -val prolog_tac : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic +val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic -val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list -> +val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic val eauto_with_bases : - ?debug:Tacexpr.debug -> + ?debug:debug -> bool * int -> - Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic + delayed_open_constr list -> hint_db list -> Proof_type.tactic val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic diff --git a/tactics/elim.mli b/tactics/elim.mli index ae9cf85f3..29c441463 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -10,11 +10,12 @@ open Names open Term open Tacticals open Misctypes +open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : Tacexpr.evars_flag -> - (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> +val introCaseAssumsThen : evars_flag -> + (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index b1d3290aa..1a67bedc2 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -22,6 +22,7 @@ open Tacticals.New open Auto open Constr_matching open Misctypes +open Tactypes open Hipattern open Pretyping open Tacmach.New @@ -73,7 +74,7 @@ let mkBranches c1 c2 = let discrHyp id = let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in - let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in + let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac let solveNoteqBranch side = @@ -121,7 +122,7 @@ let eqCase tac = let injHyp id = let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in - let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in + let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac let diseqCase hyps eqonleft = diff --git a/tactics/equality.ml b/tactics/equality.ml index d4b372837..b525b3ab5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -26,7 +26,6 @@ open Retyping open Tacmach.New open Logic open Hipattern -open Tacexpr open Tacticals.New open Tactics open Tacred diff --git a/tactics/equality.mli b/tactics/equality.mli index 47cb6b82f..6a4a8126e 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -11,10 +11,10 @@ open Names open Term open Evd open Environ -open Tacexpr open Ind_tables open Locus open Misctypes +open Tactypes (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 4b43a9e69..ac945de3c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -20,11 +20,11 @@ open Namegen open Libnames open Smartlocate open Misctypes +open Tactypes open Evd open Termops open Inductiveops open Typing -open Tacexpr open Decl_kinds open Pattern open Patternops @@ -41,6 +41,8 @@ module NamedDecl = Context.Named.Declaration (* General functions *) (****************************************) +type debug = Debug | Info | Off + exception Bound let head_constr_bound t = @@ -803,7 +805,6 @@ let make_unfold eref = code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = - let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri = pri; @@ -1081,8 +1082,6 @@ let add_trivials env sigma l local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let (forward_intern_tac, extern_intern_tac) = Hook.make () - type hnf = bool type hints_entry = @@ -1093,7 +1092,7 @@ type hints_entry = | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list | HintsExternEntry of - int * (patvar list * constr_pattern) option * glob_tactic_expr + int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" @@ -1183,7 +1182,9 @@ let interp_hints poly = | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in let l = match pat with None -> [] | Some (l, _) -> l in - let tacexp = Hook.get forward_intern_tac l tacexp in + let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in + let env = Genintern.({ genv = env; ltacvars }) in + let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry (pri, pat, tacexp) let add_hints local dbnames0 h = @@ -1276,7 +1277,7 @@ let pr_hint h = match h.obj with env with e when CErrors.noncritical e -> Global.env () in - (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) + (str "(*external*) " ++ Pputils.pr_glb_generic env tac) let pr_id_hint (id, v) = (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) diff --git a/tactics/hints.mli b/tactics/hints.mli index 6f5ee8ba5..9a3817203 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -15,6 +15,7 @@ open Globnames open Decl_kinds open Evd open Misctypes +open Tactypes open Clenv open Pattern open Vernacexpr @@ -25,6 +26,8 @@ exception Bound val decompose_app_bound : constr -> global_reference * constr array +type debug = Debug | Info | Off + (** Pre-created hint databases *) type 'a hint_ast = @@ -132,7 +135,7 @@ type hints_entry = | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list | HintsExternEntry of - int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr + int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -199,7 +202,7 @@ val make_resolve_hyp : (** [make_extern pri pattern tactic_expr] *) val make_extern : - int -> constr_pattern option -> Tacexpr.glob_tactic_expr + int -> constr_pattern option -> Genarg.glob_generic_argument -> hint_entry val run_hint : hint -> @@ -209,14 +212,11 @@ val run_hint : hint -> written code. *) val repr_hint : hint -> (raw_hint * clausenv) hint_ast -val extern_intern_tac : - (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t - (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> Tacexpr.delayed_open_constr list -> hint_db +val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> delayed_open_constr list -> hint_db val make_db_list : hint_db_name list -> hint_db list diff --git a/tactics/inv.ml b/tactics/inv.ml index 291bc0965..e7d8249e4 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -25,7 +25,6 @@ open Tactics open Elim open Equality open Misctypes -open Tacexpr open Sigma.Notations open Proofview.Notations @@ -497,8 +496,6 @@ let inversion inv_kind status names id = let inv_gen thin status names = try_intros_until (inversion thin status names) -open Tacexpr - let inv k = inv_gen k NoDep let inv_tac id = inv FullInversion None (NamedHyp id) diff --git a/tactics/inv.mli b/tactics/inv.mli index af1cb996a..df629e7c9 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -9,7 +9,7 @@ open Names open Term open Misctypes -open Tacexpr +open Tactypes type inversion_status = Dep of constr option | NoDep diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 203d97542..f739488aa 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -15,6 +15,7 @@ open Termops open Declarations open Tacmach open Clenv +open Tactypes open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -152,7 +153,7 @@ type branch_args = { nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. true=assumption, false=let-in *) - branchnames : Tacexpr.intro_patterns} + branchnames : intro_patterns} type branch_assumptions = { ba : branch_args; (* the branch args *) @@ -479,10 +480,10 @@ module New = struct (* Select a subset of the goals *) let tclSELECT = function - | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Tacexpr.SelectId id -> Proofview.tclFOCUSID id - | Tacexpr.SelectAll -> fun tac -> tac + | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i + | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l + | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id + | Vernacexpr.SelectAll -> fun tac -> tac (* Check that holes in arguments have been resolved *) @@ -533,7 +534,7 @@ module New = struct Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let Sigma (x, sigma, _) = x.Tacexpr.delayed env sigma in + let Sigma (x, sigma, _) = x.delayed env sigma in tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma) end } diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cfdc2cffd..18cf03c51 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -11,9 +11,9 @@ open Names open Term open Tacmach open Proof_type -open Tacexpr open Locus open Misctypes +open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) @@ -221,7 +221,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 85b6e8de9..9d0e9f084 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -32,7 +32,6 @@ open Refiner open Tacticals open Hipattern open Coqlib -open Tacexpr open Decl_kinds open Evarutil open Indrec @@ -41,6 +40,7 @@ open Unification open Locus open Locusops open Misctypes +open Tactypes open Proofview.Notations open Sigma.Notations open Context.Named.Declaration @@ -871,7 +871,11 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = - let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in + let trace () = + let open Printer in + let pr = (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern) in + Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) + in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter { enter = begin fun gl -> let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index fb033363e..7acfb6286 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -15,10 +15,10 @@ open Evd open Clenv open Redexpr open Globnames -open Tacexpr open Pattern open Unification open Misctypes +open Tactypes open Locus (** Main tactics defined in ML. This file is huge and should probably be split diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 093302608..f54ad86a3 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -16,7 +16,6 @@ Hints Auto Eauto Class_tactics -Tactic_matching Term_dnet Eqdecide Autorewrite diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index cd244bf63..bbec5b72d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -46,12 +46,30 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s) let entry_buf = Buffer.create 64 +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +let grammars : any_entry list String.Map.t ref = ref String.Map.empty + +let register_grammar name grams = + grammars := String.Map.add name grams !grammars + let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in let () = Gram.entry_print ft e in str (Buffer.contents entry_buf) +let pr_registered_grammar name = + let gram = try Some (String.Map.find name !grammars) with Not_found -> None in + match gram with + | None -> error "Unknown or unprintable grammar entry." + | Some entries -> + let pr_one (AnyEntry e) = + str "Entry " ++ str (Gram.Entry.name e) ++ str " is" ++ fnl () ++ + pr_entry e + in + prlist pr_one entries + let pr_grammar = function | "constr" | "operconstr" | "binder_constr" -> str "Entry constr is" ++ fnl () ++ @@ -64,15 +82,6 @@ let pr_grammar = function pr_entry Pcoq.Constr.operconstr | "pattern" -> pr_entry Pcoq.Constr.pattern - | "tactic" -> - str "Entry tactic_expr is" ++ fnl () ++ - pr_entry Pcoq.Tactic.tactic_expr ++ - str "Entry binder_tactic is" ++ fnl () ++ - pr_entry Pcoq.Tactic.binder_tactic ++ - str "Entry simple_tactic is" ++ fnl () ++ - pr_entry Pcoq.Tactic.simple_tactic ++ - str "Entry tactic_arg is" ++ fnl () ++ - pr_entry Pcoq.Tactic.tactic_arg | "vernac" -> str "Entry vernac is" ++ fnl () ++ pr_entry Pcoq.Vernac_.vernac ++ @@ -84,7 +93,7 @@ let pr_grammar = function pr_entry Pcoq.Vernac_.gallina ++ str "Entry gallina_ext is" ++ fnl () ++ pr_entry Pcoq.Vernac_.gallina_ext - | _ -> error "Unknown or unprintable grammar entry." + | name -> pr_registered_grammar name (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 085cc87c8..57c120402 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Tacexpr open Vernacexpr open Notation open Constrexpr @@ -55,6 +54,10 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> val pr_grammar : string -> Pp.std_ppcmds +type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry + +val register_grammar : string -> any_entry list -> unit + val check_infix_modifiers : syntax_modifier list -> unit val with_syntax_protection : ('a -> 'b) -> 'a -> 'b diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 69d206961..80b689144 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -87,9 +87,9 @@ val add_mutual_definitions : fixpoint_kind -> unit val obligation : int * Names.Id.t option * Constrexpr.constr_expr option -> - Tacexpr.raw_tactic_expr option -> unit + Genarg.glob_generic_argument option -> unit -val next_obligation : Names.Id.t option -> Tacexpr.raw_tactic_expr option -> unit +val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress (* Number of remaining obligations to be solved for this program *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index eebc9ff66..14d9a55c6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -844,11 +844,12 @@ let focus_command_cond = Proof.no_cond command_focus let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = + let open Genintern in + let env = { genv = Global.env (); ltacvars = Id.Set.empty } in + let _, tac = Genintern.generic_intern env tac in if not (refining ()) then error "Unknown command of the non proof-editing mode."; - match tac with - | Tacexpr.TacId [] -> () - | _ -> set_end_tac tac + set_end_tac tac (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 4e7fa4a08..7cdc8dd06 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -62,5 +62,5 @@ val with_fail : bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind -val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr -> +val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t |