From d66fe71c93bc06f6006c64118deb1d5b01bf7487 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:01:23 +0100 Subject: Adding a universe argument to Pcoq.create_generic_entry. --- grammar/argextend.ml4 | 4 ++-- parsing/pcoq.ml | 2 +- parsing/pcoq.mli | 4 ++-- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/funind/g_indfun.ml4 | 2 +- tactics/g_rewrite.ml4 | 2 +- toplevel/g_obligations.ml4 | 2 +- 7 files changed, 9 insertions(+), 9 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 46c68ecc3a..57ae357dec 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -147,7 +147,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; <:str_item< do { Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule @@ -170,7 +170,7 @@ let declare_vernac_argument loc s pr cl = value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; <:str_item< do { Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 52437e3867..e150578196 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -251,7 +251,7 @@ let create_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.ent let create_constr_entry s = create_entry uconstr s (rawwit wit_constr) -let create_generic_entry s wit = create_entry utactic s wit +let create_generic_entry = create_entry (* [make_gen_entry] builds entries extensible by giving its name (a string) *) (* For entries extensible only via the ML name, Gram.entry_create is enough *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7e0c89fd12..625f0370e6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -162,8 +162,8 @@ val uvernac : gram_universe val get_entry : gram_universe -> string -> typed_entry -val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> - 'a Gram.entry +val create_generic_entry : gram_universe -> string -> + ('a, rlevel) abstract_argument_type -> 'a Gram.entry module Prim : sig diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 2d096a1081..2afbaca2c8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry = Gram.entry_create "vernac:proof_command" (* Auxiliary grammar entry. *) let proof_instr : raw_proof_instr Gram.entry = - Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr) + Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr) let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61ada5cc8c..dbcdeb83ad 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -149,7 +149,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) GEXTEND Gram GLOBAL: function_rec_definition_loc ; diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 8b012aa88e..0ce886373f 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -186,7 +186,7 @@ type binders_argtype = local_binder list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) -let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders) +let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) open Pcoq diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 32ccf21d2b..2a5676525a 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -34,7 +34,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = Genarg.create_arg "withtac" -let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac) +let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) GEXTEND Gram GLOBAL: withtac; -- cgit v1.2.3 From 4d13842869647790c9bd3084dce672fee7b648a1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:23:59 +0100 Subject: Code factorization in Pcoq. --- parsing/pcoq.ml | 37 +++++++++---------------------------- 1 file changed, 9 insertions(+), 28 deletions(-) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index e150578196..1b1ecaf910 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -200,8 +200,6 @@ let parse_string f x = type gram_universe = Entry.universe -let trace = ref false - let uprim = Entry.uprim let uconstr = Entry.uconstr let utactic = Entry.utactic @@ -231,38 +229,21 @@ let get_typed_entry e = let new_entry etyp u s = let utab = get_utable u in let uname = Entry.univ_name u in - if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" uname s; flush stderr); let _ = Entry.create u s in let ename = uname ^ ":" ^ s in let e = Gram.entry_create ename in Hashtbl.add utab s (TypedEntry (etyp, e)); e -let create_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = +let make_gen_entry u rawwit s = new_entry rawwit u s + +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = let utab = get_utable u in - try - let TypedEntry (typ, e) = Hashtbl.find utab s in - match abstract_argument_type_eq typ etyp with - | None -> - let u = Entry.univ_name u in - failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); - | Some Refl -> e - with Not_found -> + if Hashtbl.mem utab s then + let u = Entry.univ_name u in + failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists"); + else new_entry etyp u s -let create_constr_entry s = create_entry uconstr s (rawwit wit_constr) - -let create_generic_entry = create_entry - -(* [make_gen_entry] builds entries extensible by giving its name (a string) *) -(* For entries extensible only via the ML name, Gram.entry_create is enough *) - -let make_gen_entry u rawwit s = - let univ = get_utable u in - let uname = Entry.univ_name u in - let e = Gram.entry_create (uname ^ ":" ^ s) in - let _ = Entry.create u s in - Hashtbl.add univ s (TypedEntry (rawwit, e)); e - (* Initial grammar entries *) module Prim = @@ -312,7 +293,7 @@ module Constr = let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr let lconstr = gec_constr "lconstr" - let binder_constr = create_constr_entry "binder_constr" + let binder_constr = gec_constr "binder_constr" let ident = make_gen_entry uconstr (rawwit wit_ident) "ident" let global = make_gen_entry uconstr (rawwit wit_ref) "global" let sort = make_gen_entry uconstr (rawwit wit_sort) "sort" @@ -612,7 +593,7 @@ let compute_entry allow_create adjust forpat = function try get_entry u n with Not_found when allow_create -> let wit = rawwit wit_constr in - TypedEntry (wit, create_entry u n wit) + TypedEntry (wit, create_generic_entry u n wit) in object_of_typed_entry e, None, true -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- grammar/argextend.ml4 | 7 +------ grammar/q_util.ml4 | 15 +-------------- interp/constrarg.ml | 10 ++++++++++ interp/constrarg.mli | 12 ++++++++++++ interp/stdarg.ml | 5 +++++ interp/stdarg.mli | 5 +++++ plugins/cc/g_congruence.ml4 | 4 ++++ plugins/derive/g_derive.ml4 | 4 ++++ plugins/extraction/g_extraction.ml4 | 4 ++++ plugins/firstorder/g_ground.ml4 | 4 ++++ plugins/funind/g_indfun.ml4 | 4 ++++ plugins/micromega/g_micromega.ml4 | 4 ++++ plugins/omega/g_omega.ml4 | 2 ++ plugins/quote/g_quote.ml4 | 4 ++++ plugins/romega/g_romega.ml4 | 2 ++ plugins/setoid_ring/g_newring.ml4 | 5 +++++ tactics/coretactics.ml4 | 7 ++++++- tactics/extraargs.ml4 | 4 ++++ tactics/extraargs.mli | 1 - tactics/extratactics.ml4 | 7 +++++++ tactics/g_auto.ml4 | 7 ++++++- tactics/g_class.ml4 | 5 +++++ tactics/g_rewrite.ml4 | 5 +++++ toplevel/g_obligations.ml4 | 6 ++++++ 24 files changed, 110 insertions(+), 23 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 57ae357dec..41e94914ee 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -23,12 +23,7 @@ let qualified_name loc s = let (name, path) = CList.sep_last path in qualified_name loc path name -let mk_extraarg loc s = - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> +let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 1848bf85f1..3946d5d2b9 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -47,15 +47,6 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let repr_entry e = - let entry u = - let _ = Pcoq.get_entry u e in - Some (Entry.univ_name u, e) - in - try entry Pcoq.uprim with Not_found -> - try entry Pcoq.uconstr with Not_found -> - try entry Pcoq.utactic with Not_found -> None - let rec mlexpr_of_prod_entry_key = function | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> @@ -63,11 +54,7 @@ let rec mlexpr_of_prod_entry_key = function | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Uentry e -> - begin match repr_entry e with - | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> - | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >> - end + | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ead4e39692..20ee7aa4fb 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -82,3 +82,13 @@ let () = register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; register_name0 wit_bindings "Constrarg.wit_bindings"; register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; + () + +(** Aliases *) + +let wit_reference = wit_ref +let wit_global = wit_ref +let wit_clause = wit_clause_dft_concl +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern +let wit_redexpr = wit_red_expr diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 5c26af3c2a..1197b85a25 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -72,3 +72,15 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) 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 + +(** 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_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, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 56b995e537..e497c996f7 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool" let () = register_name0 wit_int "Stdarg.wit_int" let () = register_name0 wit_string "Stdarg.wit_string" let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" + +(** Aliases for compatibility *) + +let wit_integer = wit_int +let wit_preident = wit_pre_ident diff --git a/interp/stdarg.mli b/interp/stdarg.mli index d8904dab87..e1f648d7fc 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type val wit_string : string uniform_genarg_type val wit_pre_ident : string uniform_genarg_type + +(** Aliases for compatibility *) + +val wit_integer : int uniform_genarg_type +val wit_preident : string uniform_genarg_type diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 5dbc340caa..9a53e2e16a 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -9,6 +9,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Cctac +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr DECLARE PLUGIN "cc_plugin" diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 18570a6846..35a5a7616c 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Constrarg +open Pcoq.Prim +open Pcoq.Constr + (*i camlp4deps: "grammar/grammar.cma" i*) let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index aec9586895..7bd07f6255 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -11,6 +11,10 @@ (* ML names *) open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr open Pp open Names open Nameops diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3e8be36993..587d10d1cc 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,6 +15,10 @@ open Goptions open Tacticals open Tacinterp open Libnames +open Constrarg +open Stdarg +open Pcoq.Prim +open Pcoq.Tactic DECLARE PLUGIN "ground_plugin" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index dbcdeb83ad..4bd69b9fe7 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -16,8 +16,12 @@ open Constrexpr open Indfun_common open Indfun open Genarg +open Constrarg open Tacticals open Misctypes +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "recdef_plugin" diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index bfc9c727d5..bca1c2febd 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -18,6 +18,10 @@ open Errors open Misctypes +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Tactic DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 04c62eb487..b314e0d85f 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin" open Names open Coq_omega +open Constrarg +open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 7a3d7936a6..a15b0eb05a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,6 +13,10 @@ open Misctypes open Tacexpr open Geninterp open Quote +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "quote_plugin" diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 6b2b2bbfaf..61efa9f545 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega +open Constrarg +open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 856ec0db5f..cd1d704dde 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -14,6 +14,11 @@ open Libnames open Printer open Newring_ast open Newring +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "newring_plugin" diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 7da6df717e..73b7bde9d7 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -13,6 +13,11 @@ open Names open Locus open Misctypes open Genredexpr +open Stdarg +open Constrarg +open Pcoq.Constr +open Pcoq.Prim +open Pcoq.Tactic open Proofview.Notations open Sigma.Notations @@ -143,7 +148,7 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ] +| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 98868e8f91..8215e785ab 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -10,6 +10,10 @@ open Pp open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr open Names open Tacexpr open Taccoerce diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 7df845e4bd..f7b379e69e 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -53,7 +53,6 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds - (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ae8b83b95e..52419497d1 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -10,7 +10,12 @@ open Pp open Genarg +open Stdarg +open Constrarg open Extraargs +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic open Mod_subst open Names open Tacexpr @@ -49,6 +54,8 @@ 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 + TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4 index f4fae763fd..788443944f 100644 --- a/tactics/g_auto.ml4 +++ b/tactics/g_auto.ml4 @@ -10,6 +10,11 @@ open Pp open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic open Tacexpr DECLARE PLUGIN "g_auto" @@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto END TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ] +| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ] END TACTIC EXTEND autounfold_one diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 766593543c..9ef1545416 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -10,6 +10,11 @@ open Misctypes open Class_tactics +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic +open Stdarg +open Constrarg DECLARE PLUGIN "g_class" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 0ce886373f..c4ef1f297e 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -20,6 +20,11 @@ open Extraargs open Tacmach open Tacticals open Rewrite +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "g_rewrite" diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 2a5676525a..dd11efebd8 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -16,6 +16,12 @@ open Libnames open Constrexpr open Constrexpr_ops +open Stdarg +open Constrarg +open Extraargs +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac. -- cgit v1.2.3 From 36e865119e5bb5fbaed14428fc89ecd4e96fb7be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 18:27:39 +0100 Subject: Removing the special status of generic arguments defined by Coq itself. This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. --- grammar/argextend.ml4 | 11 ++-- grammar/q_util.ml4 | 26 +++----- grammar/q_util.mli | 2 +- grammar/tacextend.ml4 | 3 +- grammar/vernacextend.ml4 | 8 +-- parsing/highparsing.mllib | 1 - parsing/pcoq.ml | 51 ++++++++++++++-- parsing/pcoq.mli | 2 + plugins/funind/g_indfun.ml4 | 2 +- tactics/coretactics.ml4 | 1 + tactics/extraargs.ml4 | 18 ++++++ tactics/extraargs.mli | 7 +++ tactics/extratactics.ml4 | 12 ++-- tactics/g_obligations.ml4 | 141 ++++++++++++++++++++++++++++++++++++++++++++ tactics/hightactics.mllib | 1 + toplevel/g_obligations.ml4 | 141 -------------------------------------------- 16 files changed, 244 insertions(+), 183 deletions(-) create mode 100644 tactics/g_obligations.ml4 delete mode 100644 toplevel/g_obligations.ml4 diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 41e94914ee..82bc09519b 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -46,18 +46,16 @@ let has_extraarg l = let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (t, _, p) :: tl -> - <:expr< - (fun $lid:p$ -> - let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) - >> + | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g + | ExtNonTerminal (_, g, _) -> + let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in + mlexpr_of_prod_entry_key base g let rec make_prod = function | [] -> <:expr< Extend.Stop >> @@ -174,7 +172,6 @@ let declare_vernac_argument loc s pr cl = (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] -open Pcoq open Pcaml open PcamlSig (* necessary for camlp4 *) diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 3946d5d2b9..c43ce15be2 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -47,31 +47,23 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let rec mlexpr_of_prod_entry_key = function - | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> - | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> +let rec mlexpr_of_prod_entry_key f = function + | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >> + | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> -let type_entry u e = - let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in - Genarg.unquote t - let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> Genarg.ListArgType (type_of_user_symbol s) | Uopt s -> Genarg.OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> - try type_entry Pcoq.uprim e with Not_found -> - try type_entry Pcoq.uconstr e with Not_found -> - try type_entry Pcoq.utactic e with Not_found -> - Genarg.ExtraArgType e +| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 837ec6fb02..712aa8509d 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -28,6 +28,6 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr val mlexpr_of_ident : string -> MLast.expr -val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index c35fa00d2e..8c85d01629 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -85,8 +85,9 @@ let make_fun_clauses loc s l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (nt, g, id) -> + let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key g$ >> + $mlexpr_of_prod_entry_key base g$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3bb1e09076..d8c8850884 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -42,7 +42,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let e pt) (* To avoid warnings *) @@ -58,11 +58,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr c) pt)), + vala None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr cg) pt)), + vala None, <:expr< fun () -> $cg$ $str:s$ >>) | None, None -> msg_warning (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ @@ -85,7 +85,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = strbrk("Specific classifiers have precedence over global "^ "classifiers. Only one classifier is called.")++fnl()); (make_patt pt, - vala (Some (make_when loc pt)), + vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 13ed804641..eed6caea30 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,4 +4,3 @@ G_prim G_proofs G_tactic G_ltac -G_obligations diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 1b1ecaf910..05fd9f9d8c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -229,12 +229,23 @@ let get_typed_entry e = let new_entry etyp u s = let utab = get_utable u in let uname = Entry.univ_name u in - let _ = Entry.create u s in + let entry = Entry.create u s in let ename = uname ^ ":" ^ s in let e = Gram.entry_create ename in - Hashtbl.add utab s (TypedEntry (etyp, e)); e + Hashtbl.add utab s (TypedEntry (etyp, e)); (entry, e) -let make_gen_entry u rawwit s = new_entry rawwit u s +let make_gen_entry u rawwit s = snd (new_entry rawwit u s) + +module GrammarObj = +struct + type ('r, _, _) obj = 'r Entry.t + let name = "grammar" + let default _ = None +end + +module Grammar = Register(GrammarObj) + +let genarg_grammar wit = Grammar.obj wit let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = let utab = get_utable u in @@ -242,7 +253,10 @@ let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a let u = Entry.univ_name u in failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists"); else - new_entry etyp u s + let (entry, e) = new_entry etyp u s in + let Rawwit t = etyp in + let () = Grammar.register0 t entry in + e (* Initial grammar entries *) @@ -841,3 +855,32 @@ let epsilon_value f e = let entry = G.entry_create "epsilon" in let () = maybe_uncurry (Gram.extend entry) ext in try Some (parse_string entry "") with _ -> None + +(** Registering grammar of generic arguments *) + +let () = + let open Stdarg in + let open Constrarg in +(* Grammar.register0 wit_unit; *) +(* Grammar.register0 wit_bool; *) + Grammar.register0 wit_int (name_of_entry Prim.integer); + Grammar.register0 wit_string (name_of_entry Prim.string); + Grammar.register0 wit_pre_ident (name_of_entry Prim.preident); + Grammar.register0 wit_int_or_var (name_of_entry Tactic.int_or_var); + Grammar.register0 wit_intro_pattern (name_of_entry Tactic.simple_intropattern); + Grammar.register0 wit_ident (name_of_entry Prim.ident); + Grammar.register0 wit_var (name_of_entry Prim.var); + Grammar.register0 wit_ref (name_of_entry Prim.reference); + Grammar.register0 wit_quant_hyp (name_of_entry Tactic.quantified_hypothesis); + Grammar.register0 wit_sort (name_of_entry Constr.sort); + Grammar.register0 wit_constr (name_of_entry Constr.constr); + Grammar.register0 wit_constr_may_eval (name_of_entry Tactic.constr_may_eval); + Grammar.register0 wit_uconstr (name_of_entry Tactic.uconstr); + Grammar.register0 wit_open_constr (name_of_entry Tactic.open_constr); + Grammar.register0 wit_constr_with_bindings (name_of_entry Tactic.constr_with_bindings); + Grammar.register0 wit_bindings (name_of_entry Tactic.bindings); +(* Grammar.register0 wit_hyp_location_flag; *) + Grammar.register0 wit_red_expr (name_of_entry Tactic.red_expr); + Grammar.register0 wit_tactic (name_of_entry Tactic.tactic); + Grammar.register0 wit_clause_dft_concl (name_of_entry Tactic.clause_dft_concl); + () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 625f0370e6..b1353ef8ad 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -160,6 +160,8 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t + val get_entry : gram_universe -> string -> typed_entry val create_generic_entry : gram_universe -> string -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4bd69b9fe7..e93c395e3d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -94,7 +94,7 @@ let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." -ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 73b7bde9d7..6c02a7202f 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -15,6 +15,7 @@ open Misctypes open Genredexpr open Stdarg open Constrarg +open Extraargs open Pcoq.Constr open Pcoq.Prim open Pcoq.Tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 8215e785ab..d33ec91f9d 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -55,6 +55,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ ] -> [ true ] END +let pr_int _ _ _ i = Pp.int i + +let _natural = Pcoq.Prim.natural + +ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int +| [ _natural(i) ] -> [ i ] +END + let pr_orient = pr_orient () () () @@ -122,6 +130,8 @@ let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) let glob_glob = Tacintern.intern_constr +let pr_lconstr _ prc _ c = prc c + let subst_glob = Tacsubst.subst_glob_constr_and_expr ARGUMENT EXTEND glob @@ -139,6 +149,14 @@ ARGUMENT EXTEND glob [ constr(c) ] -> [ c ] END +let l_constr = Pcoq.Constr.lconstr + +ARGUMENT EXTEND lconstr + TYPED AS constr + PRINTED BY pr_lconstr + [ l_constr(c) ] -> [ c ] +END + ARGUMENT EXTEND lglob PRINTED BY pr_globc diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index f7b379e69e..14aa69875f 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg val pr_occurrences : int list or_var -> Pp.std_ppcmds val occurrences_of : int list -> Locus.occurrences +val wit_natural : int Genarg.uniform_genarg_type + val wit_glob : (constr_expr, Tacexpr.glob_constr_and_expr, @@ -31,6 +33,11 @@ val wit_lglob : Tacexpr.glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type +val wit_lconstr : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Constr.t) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 52419497d1..0cc796886c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -154,23 +154,23 @@ TACTIC EXTEND einjection | [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND injection_as_main -| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> +| [ "injection" constr_with_bindings(c) "as" intropattern_list(ipat)] -> [ elimOnConstrWithHoles (injClause (Some ipat)) false c ] END TACTIC EXTEND injection_as -| [ "injection" "as" simple_intropattern_list(ipat)] -> +| [ "injection" "as" intropattern_list(ipat)] -> [ injClause (Some ipat) false None ] -| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> +| [ "injection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] -> [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND einjection_as_main -| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> +| [ "einjection" constr_with_bindings(c) "as" intropattern_list(ipat)] -> [ elimOnConstrWithHoles (injClause (Some ipat)) true c ] END TACTIC EXTEND einjection_as -| [ "einjection" "as" simple_intropattern_list(ipat)] -> +| [ "einjection" "as" intropattern_list(ipat)] -> [ injClause (Some ipat) true None ] -| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> +| [ "einjection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] -> [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ] END diff --git a/tactics/g_obligations.ml4 b/tactics/g_obligations.ml4 new file mode 100644 index 0000000000..e67d701218 --- /dev/null +++ b/tactics/g_obligations.ml4 @@ -0,0 +1,141 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + *) + +module Gram = Pcoq.Gram +module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic + +open Pcoq + +let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) + +type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type + +let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = + Genarg.create_arg "withtac" + +let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) + +GEXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> Some t + | -> None ] ] + ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [LocalRawAssum ([id], default_binder_kind, typ)] + ] ]; + + END + +open Obligations + +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> + [ obligation (num, Some name, Some t) tac ] +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> + [ obligation (num, Some name, None) tac ] +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> + [ obligation (num, None, Some t) tac ] +| [ "Obligation" integer(num) withtac(tac) ] -> + [ obligation (num, None, None) tac ] +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> + [ next_obligation (Some name) tac ] +| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] +END + +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF +| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> + [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] +END + +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" "with" tactic(t) ] -> + [ try_solve_obligations None (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" ] -> + [ try_solve_obligations None None ] +END + +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> + [ solve_all_obligations (Some (Tacinterp.interp t)) ] +| [ "Solve" "All" "Obligations" ] -> + [ solve_all_obligations None ] +END + +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF +| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] +| [ "Admit" "Obligations" ] -> [ admit_obligations None ] +END + +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ + set_default_tactic + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) + (Tacintern.glob_tactic t) ] +END + +open Pp + +VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY +| [ "Show" "Obligation" "Tactic" ] -> [ + msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] +END + +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY +| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] +| [ "Obligations" ] -> [ show_obligations None ] +END + +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY +| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] +| [ "Preterm" ] -> [ msg_info (show_term None) ] +END + +open Pp + +(* Declare a printer for the content of Program tactics *) +let () = + let printer _ _ _ = function + | None -> mt () + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac + in + (* should not happen *) + let dummy _ _ _ expr = assert false in + Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 73f11d0be0..5c59465429 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,4 +1,5 @@ Extraargs +G_obligations Coretactics Autorewrite Extratactics diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 deleted file mode 100644 index dd11efebd8..0000000000 --- a/toplevel/g_obligations.ml4 +++ /dev/null @@ -1,141 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -open Pcoq - -let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg "withtac" - -let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) - -GEXTEND Gram - GLOBAL: withtac; - - withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] - ] ]; - - END - -open Obligations - -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) - -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] -END - -VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] -END - -VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] -END - -VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] -END - -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY -| [ "Show" "Obligation" "Tactic" ] -> [ - msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] -END - -VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ msg_info (show_term None) ] -END - -open Pp - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac - in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy -- cgit v1.2.3 From b5f6eb57a480d705be9362067e2fb887533c822c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 23:49:40 +0100 Subject: ARGUMENT EXTEND made of only one entry share the same grammar. This fixes parsing conflicts with the [fix ... with] tactic. --- grammar/argextend.ml4 | 33 ++++++++++++++++++++++---------- grammar/tacextend.ml4 | 2 +- parsing/pcoq.ml | 53 ++++++++++++++++++++++++++------------------------- parsing/pcoq.mli | 3 ++- 4 files changed, 53 insertions(+), 38 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 82bc09519b..f26a66a12b 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -64,6 +64,27 @@ let rec make_prod = function let make_rule loc (prods,act) = <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> +let is_ident x = function +| <:expr< $lid:s$ >> -> CString.equal s x +| _ -> false + +let make_extend loc s cl wit = match cl with +| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act -> + (** Special handling of identity arguments by not redeclaring an entry *) + <:str_item< + value $lid:s$ = + let () = Pcoq.register_grammar $wit$ $lid:e$ in + $lid:e$ + >> +| _ -> + let se = mlexpr_of_string s in + let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + <:str_item< + value $lid:s$ = + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + $lid:s$ >> + let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr = match typ with | `Uniform typ -> @@ -129,8 +150,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = @@ -139,10 +158,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; Egramcoq.create_ltac_quotation $se$ @@ -153,8 +170,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in @@ -162,10 +177,8 @@ let declare_vernac_argument loc s pr cl = [ <:str_item< value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8c85d01629..a18dfa5096 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -85,7 +85,7 @@ let make_fun_clauses loc s l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (nt, g, id) -> - let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in + let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ $mlexpr_of_prod_entry_key base g$ >> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 05fd9f9d8c..b769a3cbc4 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -229,23 +229,24 @@ let get_typed_entry e = let new_entry etyp u s = let utab = get_utable u in let uname = Entry.univ_name u in - let entry = Entry.create u s in + let _ = Entry.create u s in let ename = uname ^ ":" ^ s in let e = Gram.entry_create ename in - Hashtbl.add utab s (TypedEntry (etyp, e)); (entry, e) + Hashtbl.add utab s (TypedEntry (etyp, e)); e -let make_gen_entry u rawwit s = snd (new_entry rawwit u s) +let make_gen_entry u rawwit s = new_entry rawwit u s module GrammarObj = struct - type ('r, _, _) obj = 'r Entry.t + type ('r, _, _) obj = 'r Gram.entry let name = "grammar" let default _ = None end module Grammar = Register(GrammarObj) -let genarg_grammar wit = Grammar.obj wit +let register_grammar = Grammar.register0 +let genarg_grammar = Grammar.obj let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = let utab = get_utable u in @@ -253,9 +254,9 @@ let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a let u = Entry.univ_name u in failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists"); else - let (entry, e) = new_entry etyp u s in + let e = new_entry etyp u s in let Rawwit t = etyp in - let () = Grammar.register0 t entry in + let () = Grammar.register0 t e in e (* Initial grammar entries *) @@ -863,24 +864,24 @@ let () = let open Constrarg in (* Grammar.register0 wit_unit; *) (* Grammar.register0 wit_bool; *) - Grammar.register0 wit_int (name_of_entry Prim.integer); - Grammar.register0 wit_string (name_of_entry Prim.string); - Grammar.register0 wit_pre_ident (name_of_entry Prim.preident); - Grammar.register0 wit_int_or_var (name_of_entry Tactic.int_or_var); - Grammar.register0 wit_intro_pattern (name_of_entry Tactic.simple_intropattern); - Grammar.register0 wit_ident (name_of_entry Prim.ident); - Grammar.register0 wit_var (name_of_entry Prim.var); - Grammar.register0 wit_ref (name_of_entry Prim.reference); - Grammar.register0 wit_quant_hyp (name_of_entry Tactic.quantified_hypothesis); - Grammar.register0 wit_sort (name_of_entry Constr.sort); - Grammar.register0 wit_constr (name_of_entry Constr.constr); - Grammar.register0 wit_constr_may_eval (name_of_entry Tactic.constr_may_eval); - Grammar.register0 wit_uconstr (name_of_entry Tactic.uconstr); - Grammar.register0 wit_open_constr (name_of_entry Tactic.open_constr); - Grammar.register0 wit_constr_with_bindings (name_of_entry Tactic.constr_with_bindings); - Grammar.register0 wit_bindings (name_of_entry Tactic.bindings); + 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_sort (Constr.sort); + Grammar.register0 wit_constr (Constr.constr); + Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval); + 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 (name_of_entry Tactic.red_expr); - Grammar.register0 wit_tactic (name_of_entry Tactic.tactic); - Grammar.register0 wit_clause_dft_concl (name_of_entry Tactic.clause_dft_concl); + Grammar.register0 wit_red_expr (Tactic.red_expr); + Grammar.register0 wit_tactic (Tactic.tactic); + Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index b1353ef8ad..64f6f720c2 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -160,7 +160,8 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t +val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry val get_entry : gram_universe -> string -> typed_entry -- cgit v1.2.3 From 1730369cd4f7b62a076c93b2a0ece190ee08f7eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Mar 2016 00:32:02 +0100 Subject: Making the EXTEND macros almost self-contained. --- grammar/argextend.ml4 | 16 ++-------------- grammar/grammar.mllib | 24 ------------------------ grammar/q_util.ml4 | 40 ++++++++++++++++++++++++++++++++++++++++ grammar/q_util.mli | 2 ++ grammar/tacextend.ml4 | 27 ++------------------------- grammar/vernacextend.ml4 | 41 ++++++++++++++++++----------------------- parsing/lexer.ml4 | 2 +- 7 files changed, 65 insertions(+), 87 deletions(-) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index f26a66a12b..5bf7b65d77 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -10,10 +10,8 @@ open Genarg open Q_util -open Egramml open Compat open Extend -open Pcoq let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> @@ -36,17 +34,10 @@ let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> -let has_extraarg l = - let check = function - | ExtNonTerminal(ExtraArgType _, _, _) -> true - | _ -> false - in - List.exists check l - let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) @@ -241,10 +232,7 @@ EXTEND | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) - | s = STRING -> - if String.length s > 0 && Util.is_letter s.[0] then - Lexer.add_keyword s; - ExtTerminal s + | s = STRING -> ExtTerminal s ] ] ; entry_name: diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 6a265bf4a8..ae18925ead 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,46 +1,22 @@ Coq_config -Hook -Terminal Hashset Hashcons -CSet CMap Int -Dyn -HMap Option Store Exninfo -Backtrace -Pp_control -Flags Loc CList CString -Serialize -Stateid -Feedback -Pp -CArray -CStack -Util -Ppstyle -Errors Segmenttree Unicodetable Unicode -Genarg - -Stdarg -Constrarg Tok Compat -Lexer -Entry -Pcoq Q_util Argextend diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index c43ce15be2..4160d03c5c 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -67,3 +67,43 @@ let rec type_of_user_symbol = function | Uopt s -> Genarg.OptArgType (type_of_user_symbol s) | Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e + +let coincide s pat off = + let len = String.length pat in + let break = ref true in + let i = ref 0 in + while !break && !i < len do + let c = Char.code s.[off + !i] in + let d = Char.code pat.[!i] in + break := Int.equal c d; + incr i + done; + !break + +let rec parse_user_entry s sep = + let l = String.length s in + if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then + let entry = parse_user_entry (String.sub s 3 (l-8)) "" in + Ulist1 entry + else if l > 12 && coincide s "ne_" 0 && + coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 3 (l-12)) "" in + Ulist1sep (entry, sep) + else if l > 5 && coincide s "_list" (l-5) then + let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + Ulist0 entry + else if l > 9 && coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 0 (l-9)) "" in + Ulist0sep (entry, sep) + else if l > 4 && coincide s "_opt" (l-4) then + let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + Uopt entry + else if l > 5 && coincide s "_mods" (l-5) then + let entry = parse_user_entry (String.sub s 0 (l-1)) "" in + Umodifiers entry + else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then + let n = Char.code s.[6] - 48 in + Uentryl ("tactic", n) + else + let s = match s with "hyp" -> "var" | _ -> s in + Uentry s diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 712aa8509d..5f292baf32 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -31,3 +31,5 @@ val mlexpr_of_ident : string -> MLast.expr val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type + +val parse_user_entry : string -> string -> Extend.user_symbol diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index a18dfa5096..1951b8b452 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -10,14 +10,8 @@ (** Implementation of the TACTIC EXTEND macro. *) -open Util -open Pp -open Names -open Genarg open Q_util open Argextend -open Pcoq -open Egramml open Compat let dloc = <:expr< Loc.ghost >> @@ -39,14 +33,6 @@ let rec mlexpr_of_argtype loc = function <:expr< Genarg.PairArgType $t1$ $t2$ >> | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> -let rec make_when loc = function - | [] -> <:expr< True >> - | ExtNonTerminal (t, _, p) :: l -> - let l = make_when loc l in - let t = mlexpr_of_argtype loc t in - <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >> - | _::l -> make_when loc l - let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> | ExtNonTerminal (t, _, p) :: l -> @@ -64,21 +50,12 @@ let rec extract_signature = function | _::l -> extract_signature l - -let check_unicity s l = - let l' = List.map (fun (l,_,_) -> extract_signature l) l in - if not (Util.List.distinct l') then - Pp.msg_warning - (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^ - "non-terminals in the same order: put them in distinct tactic entries")) - let make_clause (pt,_,e) = (make_patt pt, vala None, make_let false e pt) let make_fun_clauses loc s l = - check_unicity s l; let map c = Compat.make_fun loc [make_clause c] in mlexpr_of_list map l @@ -126,7 +103,7 @@ let declare_tactic loc s c cl = match cl with (** Special handling of tactics without arguments: such tactics do not do a Proofview.Goal.nf_enter to compute their arguments. It matters for some whole-prof tactics like [shelve_unifiable]. *) - if List.is_empty rem then + if CList.is_empty rem then <:expr< fun _ $lid:"ist"$ -> $tac$ >> else let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in @@ -201,7 +178,7 @@ EXTEND let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> - if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); + let () = if CString.is_empty s then failwith "Empty terminal." in ExtTerminal s ] ] ; diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index d8c8850884..453907689e 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -10,13 +10,9 @@ (** Implementation of the VERNAC EXTEND macro. *) -open Pp -open Util open Q_util open Argextend open Tacextend -open Pcoq -open Egramml open Compat type rule = { @@ -64,26 +60,26 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = (make_patt pt, vala None, <:expr< fun () -> $cg$ $str:s$ >>) - | None, None -> msg_warning - (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ + | None, None -> prerr_endline + (("Vernac entry \""^s^"\" misses a classifier. "^ "A classifier is a function that returns an expression "^ - "of type vernac_classification (see Vernacexpr). You can: ")++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ - "new vernacular command does not alter the system state;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "of type vernac_classification (see Vernacexpr). You can: ") ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ + "new vernacular command does not alter the system state;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ "new vernacular command alters the system state but not the "^ - "parser nor it starts a proof or ends one;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "parser nor it starts a proof or ends one;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ "a global function f. The function f will be called passing "^ - "\""^s^"\" as the only argument;")) ++fnl()++ - str"- "++hov 0 ( - strbrk"Add a specific classifier in each clause using the syntax:" - ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++ - strbrk("Specific classifiers have precedence over global "^ - "classifiers. Only one classifier is called.")++fnl()); + "\""^s^"\" as the only argument;")) ^ "\n" ^ + "- " ^ ( + "Add a specific classifier in each clause using the syntax:" + ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ + ("Specific classifiers have precedence over global "^ + "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) @@ -164,8 +160,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - if String.is_empty s then - Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty."); + let () = if CString.is_empty s then failwith "Command name is empty." in let b = <:expr< fun () -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 232e9aee3f..8b8b38c34b 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -724,7 +724,7 @@ let strip s = let terminal s = let s = strip s in - let () = match s with "" -> Errors.error "empty token." | _ -> () in + let () = match s with "" -> failwith "empty token." | _ -> () in if is_ident_not_keyword s then IDENT s else if is_number s then INT s else KEYWORD s -- cgit v1.2.3 From f8f1f9d38bf2d35b0dc69fbf2e8ebbfc04b1a82d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Mar 2016 01:36:39 +0100 Subject: Documenting the change of EXTEND macros. --- dev/doc/changes.txt | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 0581a5f850..1f5ba7862f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -66,6 +66,15 @@ Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t +- The various EXTEND macros do not handle specially the Coq-defined entries + anymore. Instead, they just output a name that have to exist in the scope + of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for + variables "$name" of type Gram.entry, while the parsing rules of + (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will + look for variables "wit_$name" of type Genarg.genarg_type. The small DSL + for constructing compound entries still works over this scheme. Note that in + the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound + in the parsing rules, so beware of recursive calls. ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = -- cgit v1.2.3