Export a wrapper simplifying the registration of vernacular commands.

5 files changed, 95 insertions, 71 deletions

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index a2872d07f6..f344f3c573 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -66,54 +66,13 @@ let mk_ignore c pt =
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
 
-let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
-  match c ,cg with
-  | Some c, _ ->
-     (make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)
-  | None, Some cg ->
-     (make_patt pt,
-      ploc_vala None,
-      <:expr< fun loc -> $cg$ $str:s$ >>)
-  | 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: ") ^
-       "- " ^ (
-        ("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.") ^ "\n");
-    (make_patt pt,
-      ploc_vala None,
-      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
-
-let make_fun_clauses loc s l =
+let make_clause_classifier { r_patt = pt; r_class = c; } =
   let map c =
-    let depr = match c.r_depr with
-    | None -> false
-    | Some () -> true
-    in
-    let cl = make_fun loc [make_clause c] in
-    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
+    make_fun loc [(make_patt pt,
+      ploc_vala None,
+      make_let (mk_ignore c pt) pt)]
   in
-  mlexpr_of_list map l
-
-let make_fun_classifiers loc s c l =
-  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
-  mlexpr_of_list (fun x -> x) cl
+  mlexpr_of_option map c
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
@@ -124,23 +83,28 @@ let make_prod_item = function
       <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
       $mlexpr_of_prod_entry_key base g$ ) ) >>
 
-let mlexpr_of_clause cl =
-  let mkexpr { r_head = a; r_patt = b; } = match a with
-  | None -> mlexpr_of_list make_prod_item b
-  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
+| None -> mlexpr_of_list make_prod_item b
+| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+
+let make_rule r =
+  let depr = match r.r_depr with
+  | None -> false
+  | Some () -> true
   in
-  mlexpr_of_list mkexpr cl
+  let gram = mlexpr_of_clause r in
+  let cmd = make_fun loc [make_clause r] in
+  let classif = make_clause_classifier r in
+  <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
-  let gl = mlexpr_of_clause cl in
-  let funcl = make_fun_clauses loc s cl in
-  let classl = make_fun_classifiers loc s c cl 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< do {
-        CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
-        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
-	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
+        Vernacentries.vernac_extend ?{ classifier = $c$ }
+          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
       } >> ]
 
 open Pcaml
@@ -207,7 +171,7 @@ EXTEND
     ] ]
   ;
   classifier:
-    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 6be80d29a5..eca0c6674b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -42,13 +42,6 @@ let string_of_vernac_when = function
 let string_of_vernac_classification (t,w) =
   string_of_vernac_type t ^ " " ^ string_of_vernac_when w
 
-let classifiers = ref []
-let declare_vernac_classifier
-  (s : Vernacexpr.extend_name)
-  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
-=
-  classifiers := !classifiers @ [s,f]
-
 let idents_of_name : Names.Name.t -> Names.Id.t list =
   function
   | Names.Anonymous -> []
@@ -194,7 +187,7 @@ let classify_vernac e =
     | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
-        try List.assoc s !classifiers l ()
+        try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier ~poly = function
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 45fbfb42af..e82b191418 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -9,17 +9,12 @@
 (************************************************************************)
 
 open Vernacexpr
-open Genarg
 
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
 val classify_vernac : vernac_control -> vernac_classification
 
-(** Install a vernacular classifier for VernacExtend *)
-val declare_vernac_classifier :
-  Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
-
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
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