Export a wrapper simplifying the registration of vernacular commands.

2 files changed, 72 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6bc76a2ed..08dd6bec18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2436,3 +2436,52 @@ let interp ?verbosely ?proof ~st cmd =
     let exn = CErrors.push exn in
     Vernacstate.invalidate_cache ();
     iraise exn
+
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+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 = function
+  | Some cl -> 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 (fun (_, _, cl, _) -> get_classifier cl) ext in
+  let iter i (depr, f, cl, r) =
+    let () = Vernacinterp.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
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9c05ad8..102f996cf2 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,3 +42,26 @@ val universe_polymorphism_option_name : string list
 (** Elaborate a [atts] record out of a list of flags.
     Also returns whether polymorphism is explicitly (un)set. *)
 val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+(** Wrapper to dynamically extend vernacular commands. *)
+val vernac_extend :
+  command:string ->
+  ?classifier:(string -> Vernacexpr.vernac_classification) ->
+  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
+  (bool *
+    Vernacinterp.plugin_args Vernacinterp.vernac_command *
+    classifier option *
+    Vernacexpr.vernac_expr Egramml.grammar_prod_item list) list -> unit
+
+(** {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