Splitting ML tactics in one function per grammar entry.

Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.

7 files changed, 35 insertions, 26 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e91e66696..5cf23067a 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -75,7 +75,8 @@ let make_clause (pt,_,e) =
 
 let make_fun_clauses loc s l =
   check_unicity s l;
-  Compat.make_fun loc (List.map make_clause l)
+  let map c = Compat.make_fun loc [make_clause c] in
+  mlexpr_of_list map l
 
 let rec make_args = function
   | [] -> <:expr< [] >>
@@ -110,14 +111,14 @@ let rec make_tags loc = function
       <:expr< [ $t$ :: $l$ ] >>
   | _::l -> make_tags loc l
 
-let make_one_printing_rule se (pt,_,e) =
+let make_one_printing_rule (pt,_,e) =
   let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
   let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
-  <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$;
-            pptac_prods = ($level$, $prods$) }) >>
+  <:expr< { Pptactic.pptac_args = $make_tags loc pt$;
+            pptac_prods = ($level$, $prods$) } >>
 
-let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
+let make_printing_rule = mlexpr_of_list make_one_printing_rule
 
 let make_empty_check = function
 | GramNonTerminal(_, t, e, _)->
@@ -207,7 +208,7 @@ let declare_tactic loc s c cl = match cl with
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac True False $name$ $body$ in
       try do {
-        Tacenv.register_ml_tactic $se$ $tac$;
+        Tacenv.register_ml_tactic $se$ [|$tac$|];
         Mltop.declare_cache_obj obj $plugin_name$; }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
@@ -220,7 +221,7 @@ let declare_tactic loc s c cl = match cl with
       TacML tactic. *)
   let entry = mlexpr_of_string s in
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let pp = make_printing_rule se cl in
+  let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let atom =
     mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
@@ -229,9 +230,9 @@ let declare_tactic loc s c cl = match cl with
   declare_str_items loc
     [ <:str_item< do {
       try do {
-        Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
+        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
         Mltop.declare_cache_obj $obj$ $plugin_name$;
-        List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
+        Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); }
       with [ e when Errors.noncritical e ->
         Pp.msg_warning
           (Pp.app
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index bc837d81d..a76d73006 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -34,13 +34,14 @@ type pp_tactic = {
 }
 
 (* ML Extensions *)
-let prtac_tab = Hashtbl.create 17
+let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
+  Hashtbl.create 17
 
 (* Tactic notations *)
 let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
 
 let declare_ml_tactic_pprule key pt =
-  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+  Hashtbl.add prtac_tab key pt
 
 let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -414,14 +415,18 @@ module Make
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev s l =
+  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
     try
-      let tags = List.map genarg_tag l in
-      let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+      let pp_rules = Hashtbl.find prtac_tab s in
+      let pp = pp_rules.(i) in
+      let (lev', pl) = pp.pptac_prods in
       let p = pr_tacarg_using_rule pr_gen (pl,l) in
       if lev' > lev then surround p else p
     with Not_found ->
-      let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+      let name =
+        str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
+        str "@" ++ int i
+      in
       let args = match l with
         | [] -> mt ()
         | _ -> spc() ++ pr_sequence pr_gen l
@@ -756,7 +761,7 @@ module Make
     pr_reference : 'ref -> std_ppcmds;
     pr_name      : 'nam -> std_ppcmds;
     pr_generic   : 'lev generic_argument -> std_ppcmds;
-    pr_extend    : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
+    pr_extend    : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
     pr_alias     : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
   }
 
@@ -1250,7 +1255,7 @@ module Make
             | TacArg (_,a) ->
               pr_tacarg a, latom
             | TacML (loc,s,l) ->
-              pr_with_comments loc (pr.pr_extend 1 s.mltac_name l), lcall
+              pr_with_comments loc (pr.pr_extend 1 s l), lcall
             | TacAlias (loc,kn,l) ->
               pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
           )
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 284237f01..50cc4e2bc 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -50,7 +50,7 @@ type pp_tactic = {
   pptac_prods : int * grammar_terminals;
 }
 
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit
+val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 98b5757da..ee1669f7f 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -60,19 +60,19 @@ module type Pp = sig
     (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
     (tolerability -> raw_tactic_expr -> std_ppcmds) ->
     (constr_expr -> std_ppcmds) -> int ->
-    ml_tactic_name -> raw_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
 
   val pr_glob_extend:
     (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
-    ml_tactic_name -> glob_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
 
   val pr_extend :
     (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     (constr_pattern -> std_ppcmds) -> int ->
-    ml_tactic_name -> typed_generic_argument list -> std_ppcmds
+    ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
 
   val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
 
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 9d8b9a9d5..1bffa9f60 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -47,7 +47,7 @@ let pr_tacname t =
 
 let tac_tab = ref MLTacMap.empty
 
-let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
+let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
   let () =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
@@ -58,9 +58,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
-let interp_ml_tactic { mltac_name = s } =
+let interp_ml_tactic { mltac_name = s; mltac_index = i } =
   try
-    MLTacMap.find s !tac_tab
+    let tacs = MLTacMap.find s !tac_tab in
+    let () = if Array.length tacs <= i then raise Not_found in
+    tacs.(i)
   with Not_found ->
     Errors.errorlabstrm ""
       (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 72b1ca90f..424bb142c 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -48,7 +48,7 @@ type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
 (** Type of external tactics, used by [TacML]. *)
 
-val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
+val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit
 (** Register an external tactic. *)
 
 val interp_ml_tactic : ml_tactic_entry -> ml_tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 8de804d6d..e6f33a47b 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -159,7 +159,8 @@ let flatten_contravariant_conj flags ist =
 
 let constructor i =
   let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
-  let name = { Tacexpr.mltac_name = name; mltac_index = 0 } in
+  (** Take care of the index: this is the second entry in constructor. *)
+  let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
   let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
   Tacexpr.TacML (Loc.ghost, name, [i])