From 7f39d17e7c1d7655be595ccbe741a15ba780b785 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Oct 2018 15:15:38 +0200
Subject: Providing a centralized API for ARGUMENT EXTEND.

We chose to stick to the most general possible API, even though the macro
will not make full use of the possibilities. It makes explicit the various
data expected to be provided in an orthogonal way.
---
 vernac/vernacentries.ml  | 27 +++++++++++++++++++++++++++
 vernac/vernacentries.mli | 18 ++++++++++++++++++
 2 files changed, 45 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 32c61378db..48d4165830 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2613,3 +2613,30 @@ let vernac_extend ~command ?classifier ?entry ext =
   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 34f6029e78..0c4630e45f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -63,6 +63,24 @@ val vernac_extend :
   ?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 :
-- 
cgit v1.2.3