diff options
| -rw-r--r-- | coqpp/coqpp_main.ml | 20 | ||||
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 46 | ||||
| -rw-r--r-- | grammar/argextend.mlp | 10 | ||||
| -rw-r--r-- | grammar/dune | 5 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 10 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 147 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 47 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 211 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 60 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 77 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 21 |
16 files changed, 315 insertions, 353 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 7cecff9d75..ba3b9bcbbf 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -357,15 +357,15 @@ let print_body fmt r = print_binders r.vernac_toks print_atts_right r.vernac_atts let rec print_sig fmt = function -| [] -> fprintf fmt "@[Vernacentries.TyNil@]" +| [] -> fprintf fmt "@[Vernacextend.TyNil@]" | ExtTerminal s :: rem -> - fprintf fmt "@[Vernacentries.TyTerminal (\"%s\", %a)@]" s print_sig rem + fprintf fmt "@[Vernacextend.TyTerminal (\"%s\", %a)@]" s print_sig rem | ExtNonTerminal (symb, _) :: rem -> - fprintf fmt "@[Vernacentries.TyNonTerminal (%a, %a)@]" + fprintf fmt "@[Vernacextend.TyNonTerminal (%a, %a)@]" print_symbol symb print_sig rem let print_rule fmt r = - fprintf fmt "Vernacentries.TyML (%b, %a, %a, %a)" + fprintf fmt "Vernacextend.TyML (%b, %a, %a, %a)" r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r let print_rules fmt rules = @@ -386,7 +386,7 @@ let print_entry fmt = function let print_ast fmt ext = let pr fmt () = - fprintf fmt "Vernacentries.vernac_extend ~command:\"%s\" %a ?entry:%a %a" + fprintf fmt "Vernacextend.vernac_extend ~command:\"%s\" %a ?entry:%a %a" ext.vernacext_name print_classifier ext.vernacext_class print_entry ext.vernacext_entry print_rules ext.vernacext_rules in @@ -481,8 +481,8 @@ let print_rules fmt (name, rules) = factorization of parsing rules. It allows to recognize rules of the form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and reuse the same entry directly. *) - fprintf fmt "@[Vernacentries.Arg_alias (%s)@]" e - | _ -> fprintf fmt "@[Vernacentries.Arg_rules (%a)@]" pr rules + fprintf fmt "@[Vernacextend.Arg_alias (%s)@]" e + | _ -> fprintf fmt "@[Vernacextend.Arg_rules (%a)@]" pr rules let print_printer fmt = function | None -> fprintf fmt "@[fun _ -> Pp.str \"missing printer\"@]" @@ -491,9 +491,9 @@ let print_printer fmt = function let print_ast fmt arg = let name = arg.vernacargext_name in let pr fmt () = - fprintf fmt "Vernacentries.vernac_argument_extend ~name:%a @[{@\n\ - Vernacentries.arg_parsing = %a;@\n\ - Vernacentries.arg_printer = %a;@\n}@]" + fprintf fmt "Vernacextend.vernac_argument_extend ~name:%a @[{@\n\ + Vernacextend.arg_parsing = %a;@\n\ + Vernacextend.arg_printer = %a;@\n}@]" print_string name print_rules (name, arg.vernacargext_rules) print_printer arg.vernacargext_printer in diff --git a/dev/base_include b/dev/base_include index 67a7e87d78..0e12b57b36 100644 --- a/dev/base_include +++ b/dev/base_include @@ -176,7 +176,7 @@ open Mltop open Record open Coqloop open Vernacentries -open Vernacinterp +open Vernacextend open Vernac (* Various utilities *) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fd08f9ffe8..f94e9acb72 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -509,41 +509,23 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Genarg -open Stdarg -open Egramml - let _ = - try - Vernacinterp.vinterp_add false ("PrintConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context econstr_display c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintConstr", 0) None - [GramTerminal "PrintConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintConstr" [cmd] let _ = - try - Vernacinterp.vinterp_add false ("PrintPureConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context print_pure_econstr c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintPureConstr", 0) None - [GramTerminal "PrintPureConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index b882d2164f..715b8cd23f 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -75,9 +75,9 @@ let is_ident x = function let make_extend loc self cl = match cl with | [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> (** Special handling of identity arguments by not redeclaring an entry *) - <:expr< Vernacentries.Arg_alias $lid:e$ >> + <:expr< Vernacextend.Arg_alias $lid:e$ >> | _ -> - <:expr< Vernacentries.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> + <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> let warning_deprecated prefix s = function | None -> () @@ -144,9 +144,9 @@ let declare_vernac_argument loc s pr cl = let pr_rules = match pr with | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< $lid:pr$ >> in - declare_arg loc s <:expr< Vernacentries.vernac_argument_extend ~{ name = $se$ } { - Vernacentries.arg_printer = $pr_rules$; - Vernacentries.arg_parsing = $make_extend loc s cl$ + declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } { + Vernacextend.arg_printer = $pr_rules$; + Vernacextend.arg_parsing = $make_extend loc s cl$ } >> open Pcaml diff --git a/grammar/dune b/grammar/dune index f03fe07607..78df2826d6 100644 --- a/grammar/dune +++ b/grammar/dune @@ -1,8 +1,7 @@ (library - (name grammar) + (name grammar5) (synopsis "Coq Camlp5 Grammar Extensions for Plugins") (public_name coq.grammar) - (wrapped false) (flags (:standard -w -58)) (libraries camlp5)) @@ -14,7 +13,7 @@ (rule (targets coqp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5))) + (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5))) (install (section bin) diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 3c401e827e..d44eeef670 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -25,24 +25,24 @@ type rule = { } let rec mlexpr_of_clause = function -| [] -> <:expr< Vernacentries.TyNil >> -| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> +| [] -> <:expr< Vernacextend.TyNil >> +| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal (g, id) :: cl -> - <:expr< Vernacentries.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> + <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> let make_rule r = let ty = mlexpr_of_clause r.r_patt in let cmd = binders_of_tokens r.r_branch r.r_patt in let make_classifier c = binders_of_tokens c r.r_patt in let classif = mlexpr_of_option make_classifier r.r_class in - <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> + <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> let declare_command loc s c nt cl = let se = mlexpr_of_string s in let c = mlexpr_of_option (fun x -> x) c in let rules = mlexpr_of_list make_rule cl in declare_str_items loc - [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] + [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] open Pcaml diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0f88734caf..1b212334ce 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -700,7 +700,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; @@ -751,10 +751,10 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = in let () = register_interp0 wit (interp_fun name arg tag) in let entry = match arg.arg_parsing with - | Vernacentries.Arg_alias e -> + | Vernacextend.Arg_alias e -> let () = Pcoq.register_grammar wit e in e - | Vernacentries.Arg_rules rules -> + | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in e diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index c93d6251e0..79f9e093fb 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -128,7 +128,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Geninterp.Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c93487d377..4db86817c9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -189,7 +189,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try Vernacentries.get_vernac_classifier s l + try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier = function diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 30fae756e9..ce93a8baaf 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -8,7 +8,7 @@ Himsg ExplainErr Locality Egramml -Vernacinterp +Vernacextend Ppvernac Proof_using Lemmas diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 74423d482e..1fab35b650 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -30,7 +30,6 @@ open Constrexpr open Redexpr open Lemmas open Locality -open Vernacinterp open Attributes module NamedDecl = Context.Named.Declaration @@ -2268,7 +2267,7 @@ let interp ?proof ~atts ~st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in + let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in () (** A global default timeout, controlled by option "Set Default Timeout n". @@ -2400,147 +2399,3 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn - -(** VERNAC EXTEND registering *) - -open Genarg -open Extend - -type classifier = Genarg.raw_generic_argument list -> vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") - -let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_classifier ty (f v) args - end - -(** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_command ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_command ty (f v) args - end - -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function -| TUlist1 l -> Alist1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUlist0 l -> Alist0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUopt o -> Aopt (untype_user_symbol o) -| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) -| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) - -let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function -| TyNil -> [] -| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty -| TyNonTerminal (tu, ty) -> - let t = rawwit (Egramml.proj_symbol tu) in - let symb = untype_user_symbol tu in - Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty - -let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol - -let classifiers : classifier array String.Map.t ref = ref String.Map.empty - -let get_vernac_classifier (name, i) args = - (String.Map.find name !classifiers).(i) args - -let declare_vernac_classifier name f = - classifiers := String.Map.add name f !classifiers - -let vernac_extend ~command ?classifier ?entry ext = - let get_classifier (TyML (_, ty, _, cl)) = match cl with - | Some cl -> untype_classifier ty cl - | None -> - match classifier with - | Some cl -> fun _ -> cl command - | None -> - let e = match entry with - | None -> "COMMAND" - | Some e -> Pcoq.Gram.Entry.name e - in - let msg = Printf.sprintf "\ - Vernac entry \"%s\" misses a classifier. \ - A classifier is a function that returns an expression \ - of type vernac_classification (see Vernacexpr). You can: \n\ - - 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;\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;\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." - command e e e command - in - CErrors.user_err (Pp.strbrk msg) - in - let cl = Array.map_of_list get_classifier ext in - let iter i (TyML (depr, ty, f, _)) = - let f = untype_command ty f in - let r = untype_grammar ty in - let () = vinterp_add depr (command, i) f in - Egramml.extend_vernac_command_grammar (command, i) entry r - in - let () = declare_vernac_classifier command cl in - List.iteri iter ext - -(** VERNAC ARGUMENT EXTEND registering *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Extend.production_rule list - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -let vernac_argument_extend ~name arg = - let wit = Genarg.create_arg name in - let entry = match arg.arg_parsing with - | Arg_alias e -> - let () = Pcoq.register_grammar wit e in - e - | Arg_rules rules -> - let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in - e - in - let pr = arg.arg_printer in - let pr x = Genprint.PrinterBasic (fun () -> pr x) in - let () = Genprint.register_vernac_print0 wit pr in - (wit, entry) diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 8ccd121b8f..8d8d7cfcf0 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -36,50 +36,3 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t - -(** {5 VERNAC EXTEND} *) - -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : - ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> - ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -(** Wrapper to dynamically extend vernacular commands. *) -val vernac_extend : - command:string -> - ?classifier:(string -> Vernacexpr.vernac_classification) -> - ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> - ty_ml list -> unit - -(** {5 VERNAC ARGUMENT EXTEND} *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t - (** This is used because CAMLP5 parser can be dumb about rule factorization, - which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list - (** There is a discrepancy here as we use directly extension rules and thus - entries instead of ty_user_symbol and thus arguments as roots. *) - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -val vernac_argument_extend : name:string -> 'a vernac_argument -> - ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t - -(** {5 STM classifiers} *) - -val get_vernac_classifier : - Vernacexpr.extend_name -> classifier - -(** Low-level API, not for casual user. *) -val declare_vernac_classifier : - string -> classifier array -> unit diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml new file mode 100644 index 0000000000..5fba586298 --- /dev/null +++ b/vernac/vernacextend.ml @@ -0,0 +1,211 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Pp +open CErrors + +type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +(* Table of vernac entries *) +let vernac_tab = + (Hashtbl.create 211 : + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + +let vinterp_add depr s f = + try + Hashtbl.add vernac_tab s (depr, f) + with Failure _ -> + user_err ~hdr:"vinterp_add" + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") + +let vinterp_map s = + try + Hashtbl.find vernac_tab s + with Failure _ | Not_found -> + user_err ~hdr:"Vernac Interpreter" + (str"Cannot find vernac command " ++ str (fst s) ++ str".") + +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + +(* Interpretation of a vernac command *) + +let call opn converted_args ~atts ~st = + let phase = ref "Looking up command" in + try + let depr, callback = vinterp_map opn in + let () = if depr then + let rules = Egramml.get_extend_vernac_rule opn in + let pr_gram = function + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" + in + let pr = pr_sequence pr_gram rules in + warn_deprecated_command pr; + in + phase := "Checking arguments"; + let hunk = callback converted_args in + phase := "Executing command"; + hunk ~atts ~st + with + | reraise -> + let reraise = CErrors.push reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); + iraise reraise + +(** VERNAC EXTEND registering *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = + let open Extend in function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (tu, ty) -> + let t = Genarg.rawwit (Egramml.proj_symbol tu) in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol + +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - 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;\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;\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." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext + +(** VERNAC ARGUMENT EXTEND registering *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t +| Arg_rules of 'a Extend.production_rule list + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +let vernac_argument_extend ~name arg = + let wit = Genarg.create_arg name in + let entry = match arg.arg_parsing with + | Arg_alias e -> + let () = Pcoq.register_grammar wit e in + e + | Arg_rules rules -> + let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + e + in + let pr = arg.arg_printer in + let pr x = Genprint.PrinterBasic (fun () -> pr x) in + let () = Genprint.register_vernac_print0 wit pr in + (wit, entry) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli new file mode 100644 index 0000000000..bb94f3a6a9 --- /dev/null +++ b/vernac/vernacextend.mli @@ -0,0 +1,60 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Interpretation of extended vernac phrases. *) + +type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +(** {5 VERNAC EXTEND} *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> + ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +(** Wrapper to dynamically extend vernacular commands. *) +val vernac_extend : + command:string -> + ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> + ty_ml list -> unit + +(** {5 VERNAC ARGUMENT EXTEND} *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t + (** This is used because CAMLP5 parser can be dumb about rule factorization, + which sometimes requires two entries to be the same. *) +| Arg_rules of 'a Extend.production_rule list + (** There is a discrepancy here as we use directly extension rules and thus + entries instead of ty_user_symbol and thus arguments as roots. *) + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +val vernac_argument_extend : name:string -> 'a vernac_argument -> + ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t + +(** {5 STM classifiers} *) + +val get_vernac_classifier : + Vernacexpr.extend_name -> classifier diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml deleted file mode 100644 index eb4282705e..0000000000 --- a/vernac/vernacinterp.ml +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Pp -open CErrors - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -(* Table of vernac entries *) -let vernac_tab = - (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) - -let vinterp_add depr s f = - try - Hashtbl.add vernac_tab s (depr, f) - with Failure _ -> - user_err ~hdr:"vinterp_add" - (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") - -let overwriting_vinterp_add s f = - begin - try - let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s - with Not_found -> () - end; - Hashtbl.add vernac_tab s (false, f) - -let vinterp_map s = - try - Hashtbl.find vernac_tab s - with Failure _ | Not_found -> - user_err ~hdr:"Vernac Interpreter" - (str"Cannot find vernac command " ++ str (fst s) ++ str".") - -let vinterp_init () = Hashtbl.clear vernac_tab - -let warn_deprecated_command = - let open CWarnings in - create ~name:"deprecated-command" ~category:"deprecated" - (fun pr -> str "Deprecated vernacular command: " ++ pr) - -(* Interpretation of a vernac command *) - -let call opn converted_args ~atts ~st = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then - let rules = Egramml.get_extend_vernac_rule opn in - let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" - in - let pr = pr_sequence pr_gram rules in - warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts ~st - with - | reraise -> - let reraise = CErrors.push reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - iraise reraise diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli deleted file mode 100644 index 0fc02c6915..0000000000 --- a/vernac/vernacinterp.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Interpretation of extended vernac phrases. *) - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -val vinterp_init : unit -> unit -val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit -val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit - -val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t |