From 4aa99307874c59f97570f624a06463aaa8115ec5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 6 Nov 2018 14:25:33 +0100 Subject: [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. --- vernac/vernac.mllib | 2 +- vernac/vernacentries.ml | 147 +-------------------------------- vernac/vernacentries.mli | 47 ----------- vernac/vernacextend.ml | 211 +++++++++++++++++++++++++++++++++++++++++++++++ vernac/vernacextend.mli | 60 ++++++++++++++ vernac/vernacinterp.ml | 77 ----------------- vernac/vernacinterp.mli | 21 ----- 7 files changed, 273 insertions(+), 292 deletions(-) create mode 100644 vernac/vernacextend.ml create mode 100644 vernac/vernacextend.mli delete mode 100644 vernac/vernacinterp.ml delete mode 100644 vernac/vernacinterp.mli (limited to 'vernac') 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 *) +(* ('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 *) +(* ('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 *) -(*