4 files changed, 96 insertions, 9 deletions
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 048d4d93a0..c5dedc880e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -64,6 +64,15 @@ let make_rule f prod =
   let act = ty_eval ty_rule f in
   Extend.Rule (symb, act)
 
+let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
+| TUentry a -> ExtraArg a
+| TUentryl (a,l) -> ExtraArg a
+| TUopt(o) -> OptArg (proj_symbol o)
+| TUlist1 l -> ListArg (proj_symbol l)
+| TUlist1sep (l,_) -> ListArg (proj_symbol l)
+| TUlist0 l -> ListArg (proj_symbol l)
+| TUlist0sep (l,_) -> ListArg (proj_symbol l)
+
 (** Vernac grammar extensions *)
 
 let vernac_exts = ref []
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a5ee036db5..c4f4fcfaa4 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -26,6 +26,8 @@ val extend_vernac_command_grammar :
 
 val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
 
+val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
+
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 08dd6bec18..653f8b26e0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2437,8 +2437,75 @@ let interp ?verbosely ?proof ~st cmd =
     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:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+  string option * ('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 (id, tu, ty) ->
+  let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id 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 =
@@ -2448,8 +2515,8 @@ 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
+  let get_classifier (TyML (_, ty, _, cl)) = match cl with
+  | Some cl -> untype_classifier ty cl
   | None ->
     match classifier with
     | Some cl -> fun _ -> cl command
@@ -2478,9 +2545,11 @@ let vernac_extend ~command ?classifier ?entry ext =
       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
+  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
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 102f996cf2..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -47,15 +47,22 @@ val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool o
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+  string option *
+  ('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 ->
-  (bool *
-    Vernacinterp.plugin_args Vernacinterp.vernac_command *
-    classifier option *
-    Vernacexpr.vernac_expr Egramml.grammar_prod_item list) list -> unit
+  ty_ml list -> unit
 
 (** {5 STM classifiers} *)