diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 16:09:17 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 16:33:00 +0200 |
commit | 975e7cd2ad032668c7df690c9bdaa8cdbb196569 (patch) | |
tree | d7c511f083288601aa3fee1032b76834f28913d8 | |
parent | 21dc493a93853525c5d9c33c0c7558909ce5e79d (diff) |
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
-rw-r--r-- | grammar/tacextend.mlp | 2 | ||||
-rw-r--r-- | interp/constrarg.ml | 11 | ||||
-rw-r--r-- | interp/constrarg.mli | 35 | ||||
-rw-r--r-- | ltac/extraargs.ml4 | 1 | ||||
-rw-r--r-- | ltac/extratactics.ml4 | 1 | ||||
-rw-r--r-- | ltac/g_class.ml4 | 1 | ||||
-rw-r--r-- | ltac/g_ltac.ml4 | 5 | ||||
-rw-r--r-- | ltac/g_obligations.ml4 | 1 | ||||
-rw-r--r-- | ltac/ltac.mllib | 1 | ||||
-rw-r--r-- | ltac/pltac.ml | 1 | ||||
-rw-r--r-- | ltac/pptactic.ml | 3 | ||||
-rw-r--r-- | ltac/tacarg.ml | 26 | ||||
-rw-r--r-- | ltac/tacarg.mli | 27 | ||||
-rw-r--r-- | ltac/tacentries.ml | 10 | ||||
-rw-r--r-- | ltac/tacintern.ml | 1 | ||||
-rw-r--r-- | ltac/tacinterp.ml | 1 | ||||
-rw-r--r-- | ltac/tacsubst.ml | 1 | ||||
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 1 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 1 | ||||
-rw-r--r-- | plugins/quote/g_quote.ml4 | 1 | ||||
-rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 1 | ||||
-rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 1 |
22 files changed, 90 insertions, 43 deletions
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/interp/constrarg.ml b/interp/constrarg.ml index ca828102b..aaf33a956 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -7,7 +7,6 @@ (************************************************************************) open Loc -open Tacexpr open Misctypes open Genarg open Geninterp @@ -27,14 +26,9 @@ let loc_of_or_by_notation f = function let wit_int_or_var = make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "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 = +let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.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 +55,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..32f2dc6f3 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -17,7 +17,6 @@ open Globnames open Genredexpr open Pattern open Constrexpr -open Tacexpr open Misctypes open Genarg @@ -28,7 +27,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type val wit_ident : Id.t uniform_genarg_type @@ -38,50 +37,38 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type +val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type -val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type +val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (constr_expr, glob_constr_and_expr, constr) genarg_type + (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type + Tacexpr.glob_constr_and_expr with_bindings, + constr with_bindings Pretyping.delayed_open) genarg_type val wit_bindings : (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type + Tacexpr.glob_constr_and_expr bindings, + constr bindings Pretyping.delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.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 val wit_global : (reference, global_reference located or_var, global_reference) genarg_type val wit_clause : (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_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index c32f757d9..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 diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d16ed84a2..de701bb23 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -12,6 +12,7 @@ open Pp open Genarg open Stdarg open Constrarg +open Tacarg open Extraargs open Pcoq.Prim open Pltac diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 3cdb3a6c7..b662057ba 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -13,6 +13,7 @@ open Class_tactics 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 f17cbc9a3..cce068910 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -34,7 +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 Constrarg.wit_ltac) tac +let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) @@ -348,12 +348,13 @@ GEXTEND Gram ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in + 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 df0b3e855..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) = diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index b9b63be3a..029dfd393 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Tacarg Pptactic Pltac Taccoerce diff --git a/ltac/pltac.ml b/ltac/pltac.ml index 148867aac..94bf32d1d 100644 --- a/ltac/pltac.ml +++ b/ltac/pltac.ml @@ -50,6 +50,7 @@ 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); diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index a4222ae2c..dc2676bf4 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -16,6 +16,7 @@ open Tacexpr open Genarg open Geninterp open Constrarg +open Tacarg open Libnames open Ppextend open Misctypes @@ -1305,7 +1306,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)); 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 fcdb1875d..2e2b55be7 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -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." @@ -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 diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index b1de30893..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 diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 9e502682b..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 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/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/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 1a0020031..13e225404 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -16,6 +16,7 @@ open Newring_ast open Newring open Stdarg open Constrarg +open Tacarg open Pcoq.Constr open Pltac diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 150be9d72..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 |