Make most of TACTIC EXTEND macros runtime calls.

Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.

PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.

2 files changed, 44 insertions, 114 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 6c072e36a..525be6432 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -13,15 +13,6 @@
 open Q_util
 open Argextend
 
-(** Quotation difference for match clauses *)
-
-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 plugin_name = <:expr< __coq_plugin_name >>
 
 let mlexpr_of_ident id =
@@ -29,112 +20,33 @@ let mlexpr_of_ident id =
   let id = "$" ^ id in
   <:expr< Names.Id.of_string_soft $str:id$ >>
 
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, Some p) :: l ->
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_let raw e = function
-  | [] -> <:expr< fun $lid:"ist"$ -> $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 raw e l in
-      let v =
-        if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
-               else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
-      <:expr< let $lid:p$ = $v$ in $e$ >>
-  | _::l -> make_let raw e l
-
-let make_clause (pt,e) =
-  (make_patt pt,
-   ploc_vala None,
-   make_let false e pt)
-
-let make_fun_clauses loc s l =
-  let map c = make_fun loc [make_clause c] in
-  mlexpr_of_list map l
-
-let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
-
 let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| 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 arg = get_argt <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
 | Uentryl (e, l) ->
   assert (e = "tactic");
-  let arg = get_argt <:expr< Tacarg.wit_tactic >> in
-  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
-
-let make_prod_item = function
-  | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
-  | ExtNonTerminal (g, id) ->
-    <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >>
-
-let mlexpr_of_clause cl =
-  mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl
-
-(** Special treatment of constr entries *)
-let is_constr_gram = function
-| ExtTerminal _ -> false
-| ExtNonTerminal (Uentry "constr", _) -> true
-| _ -> false
-
-let make_var = function
-  | ExtNonTerminal (_, p) -> p
-  | _ -> assert false
-
-let declare_tactic loc tacname ~level clause = match clause with
-| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem ->
-  (** The extension is only made of a name followed by constr entries: we do not
-      add any grammar nor printing rule and add it as a true Ltac definition. *)
-  let patt = make_patt rem in
-  let vars = List.map make_var rem in
-  let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
-  let entry = mlexpr_of_string tacname in
-  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
-  let name = mlexpr_of_string name in
-  let tac = match rem with
-  | [] ->
-    (** Special handling of tactics without arguments: such tactics do not do
-        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
-        whole-prof tactics like [shelve_unifiable]. *)
-      <:expr< fun _ $lid:"ist"$ -> $tac$ >>
-  | _ ->
-      let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
-      <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
-  in
-  (** Arguments are not passed directly to the ML tactic in the TacML node,
-      the ML tactic retrieves its arguments in the [ist] environment instead.
-      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
-  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in
-  let name = <:expr< Names.Id.of_string $name$ >> in
-  declare_str_items loc
-    [ <:str_item< do {
-      let obj () = Tacenv.register_ltac True False $name$ $body$ in
-      let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in
-      Mltop.declare_cache_obj obj $plugin_name$ } >>
-    ]
-| _ ->
-  (** Otherwise we add parsing and printing rules to generate a call to a
-      TacML tactic. *)
-  let entry = mlexpr_of_string tacname in
-  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let gl = mlexpr_of_clause clause in
-  let level = mlexpr_of_int level in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
-  declare_str_items loc
-    [ <:str_item< do {
-        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
-    ]
+  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$) >>
+| ExtNonTerminal(g,None) :: cl ->
+  <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
+| ExtNonTerminal(g,Some id) :: cl ->
+  <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>
+
+let rec binders_of_clause e = function
+| [] -> <:expr< fun ist -> $e$ >>
+| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
+| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
+| _ :: cl -> binders_of_clause e cl
 
 open Pcaml
 
@@ -146,13 +58,17 @@ EXTEND
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
-         declare_tactic loc s ~level l ] ]
+        let level = mlexpr_of_int level in
+        let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
+        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
-        "->"; "["; e = Pcaml.expr; "]" -> (l,e)
+        "->"; "["; e = Pcaml.expr; "]" ->
+         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
     ] ]
   ;
+
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 24ee0042b..a2872d07f 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -12,7 +12,6 @@
 
 open Q_util
 open Argextend
-open Tacextend
 
 type rule = {
   r_head : string option;
@@ -27,6 +26,21 @@ type rule = {
   (** Whether this entry is deprecated *)
 }
 
+(** Quotation difference for match clauses *)
+
+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 ->