Statically typecheck the VERNAC EXTEND wrapper.

This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.

9 files changed, 140 insertions, 129 deletions

diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 323a12357d..f3af318b60 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -48,3 +48,5 @@ val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.ex
 val type_of_user_symbol : user_symbol -> argument_type
 
 val parse_user_entry : string -> string -> user_symbol
+
+val mlexpr_of_symbol : user_symbol -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0b8d7fda7a..0e2bf55d86 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -128,3 +128,17 @@ let rec parse_user_entry s sep =
     let s = match s with "hyp" -> "var" | _ -> s in
     check_separator sep;
     Uentry s
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed599..07a9a76139 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -15,20 +15,6 @@ open Argextend
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
-let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
-| Uentry e ->
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f344f3c573..f30c96a7f5 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -14,98 +14,42 @@ open Q_util
 open Argextend
 
 type rule = {
-  r_head : string option;
-  (** The first terminal grammar token *)
   r_patt : extend_token list;
   (** The remaining tokens of the parsing rule *)
   r_class : MLast.expr option;
   (** An optional classifier for the STM *)
   r_branch : MLast.expr;
   (** The action performed by this rule. *)
-  r_depr : unit option;
+  r_depr : bool;
   (** Whether this entry is deprecated *)
 }
 
-(** Quotation difference for match clauses *)
+let rec make_patt r = function
+| [] -> r
+| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
+| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
+| ExtTerminal _ :: l -> make_patt r l
 
-let default_patt loc =
-  (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, ploc_vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, Some p) :: l ->
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_let e = function
-  | [] -> e
-  | ExtNonTerminal (g, Some p) :: l ->
-      let t = type_of_user_symbol g in
-      let loc = MLast.loc_of_expr e in
-      let e = make_let e l in
-      <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
-  | _::l -> make_let e l
-
-let make_clause { r_patt = pt; r_branch = e; } =
-  (make_patt pt,
-   ploc_vala None,
-   make_let e pt)
-
-(* To avoid warnings *)
-let mk_ignore c pt =
-  let fold accu = function
-  | ExtNonTerminal (_, Some p) -> p :: accu
-  | _ -> accu
-  in
-  let names = List.fold_left fold [] pt in
-  let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
-  let names = List.fold_left fold <:expr< () >> names in
-  <:expr< do { let _ = $names$ in $c$ } >>
-
-let make_clause_classifier { r_patt = pt; r_class = c; } =
-  let map c =
-    make_fun loc [(make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)]
-  in
-  mlexpr_of_option map c
-
-let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (g, ido) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-    let typ = match ido with None -> None | Some _ -> Some nt in
-      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
-      $mlexpr_of_prod_entry_key base g$ ) ) >>
-
-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 rec mlexpr_of_clause = function
+| [] -> <:expr< Vernacentries.TyNil >>
+| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
+| ExtNonTerminal (g, id) :: cl ->
+  let id = mlexpr_of_option mlexpr_of_string id in
+  <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 let make_rule r =
-  let depr = match r.r_depr with
-  | None -> false
-  | Some () -> true
-  in
-  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 ty = mlexpr_of_clause r.r_patt in
+  let cmd = make_patt r.r_branch r.r_patt in
+  let make_classifier c = make_patt c r.r_patt in
+  let classif = mlexpr_of_option make_classifier r.r_class in
+  <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s 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 {
-        Vernacentries.vernac_extend ?{ classifier = $c$ }
-          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
-      } >> ]
+  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
 
 open Pcaml
 
@@ -140,34 +84,21 @@ EXTEND
     ] ]
   ;
   deprecation:
-    [ [ "DEPRECATED" -> () ] ]
+    [ [ -> false | "DEPRECATED" -> true ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string
-      (which otherwise could have been another argument) is not passed
-      to the VernacExtend interpreter function to discriminate between
-      the clauses. *)
   rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+      { r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
+  (** The [OPT "-"] argument serves no purpose nowadays, it is left here for
+      backward compatibility. *)
   fun_rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< $e$ >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< $e$ >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      { r_patt = l; r_class = c; r_branch = e; r_depr = d; }
     ] ]
   ;
   classifier:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a628..463d8633cf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -592,15 +592,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
 let clause_of_ty_ml = function
   | TyML (t,_) -> clause_of_sign t
 
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
-  | TUentry a -> ExtraArg a
-  | TUentryl (a,l) -> ExtraArg a
-  | TUopt(o) -> OptArg (prj o)
-  | TUlist1 l -> ListArg (prj l)
-  | TUlist1sep (l,_) -> ListArg (prj l)
-  | TUlist0 l -> ListArg (prj l)
-  | TUlist0sep (l,_) -> ListArg (prj l)
-
 let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
   fun sign tac ->
     match sign with
@@ -615,7 +606,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
       begin fun tac vals ist -> match vals with
       | [] -> assert false
       | v :: vals ->
-        let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+        let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
         f (tac v') vals ist
       end tac
     | TyAnonArg (a, sig') -> eval_sign sig' tac
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} *)