Tactic notation printing accesses all the token data.

4 files changed, 32 insertions, 35 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index bf0c4fc21..a870722fd 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -86,10 +86,6 @@ let rec make_args = function
       <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
   | _::l -> make_args l
 
-let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
-  | ExtTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
-  | ExtNonTerminal _ -> <:expr< None >>
-
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (EntryName (nt, g), id) ->
@@ -98,7 +94,7 @@ let make_prod_item = function
       $mlexpr_of_prod_entry_key g$ >>
 
 let mlexpr_of_clause cl =
-  mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) cl
+  mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
 
 let rec make_tags loc = function
   | [] -> <:expr< [] >>
@@ -112,9 +108,9 @@ let rec make_tags loc = function
 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< { Pptactic.pptac_args = $make_tags loc pt$;
-            pptac_prods = ($level$, $prods$) } >>
+  let prods = mlexpr_of_list make_prod_item pt in
+  <:expr< { Pptactic.pptac_level = $level$;
+            pptac_prods = $prods$ } >>
 
 let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a8fa8313f..5bc242b2b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -26,11 +26,11 @@ open Printer
 
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 (* ML Extensions *)
@@ -345,16 +345,22 @@ module Make
         with Not_found -> Genprint.generic_top_print x
 
   let rec tacarg_using_rule_token pr_gen = function
-    | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
-    | None :: l, a :: al ->
+    | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
+    | Egramml.GramNonTerminal _ :: l, a :: al ->
       let r = tacarg_using_rule_token pr_gen (l,al) in
       pr_gen a :: r
     | [], [] -> []
     | _ -> failwith "Inconsistent arguments of extended tactic"
 
+  type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg
+
+  let filter_arg = function
+  | Egramml.GramTerminal _ -> None
+  | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t)
+
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
-    | (Some s :: l, al) ->
+    | (Egramml.GramTerminal s :: l, al) ->
       (** First terminal token should be considered as the name of the tactic,
           so we tag it differently than the other terminal tokens. *)
       primitive s :: (tacarg_using_rule_token pr_gen (l, al))
@@ -366,10 +372,10 @@ module Make
     try
       let pp_rules = Hashtbl.find prtac_tab s in
       let pp = pp_rules.(i) in
-      let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found 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
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
@@ -384,15 +390,15 @@ module Make
   let pr_alias_gen check pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
-      let (lev', pl) = pp.pptac_prods in
-      let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
-      let p = pr_tacarg_using_rule pr_gen (pl, l) in
-      if lev' > lev then surround p else p
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
       KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
-  let check_type t arg = match arg with
-  | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+  let check_type t arg = match t, arg with
+  | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg)
   | _ -> false
 
   let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
@@ -1347,6 +1353,7 @@ module Make
     (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
 
   let check_val_type t arg =
+    let AnyArg t = t in
     let t = Genarg.val_tag (Obj.magic t) in (** FIXME *)
     let Val.Dyn (t', _) = arg in
     match Genarg.Val.eq t t' with
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 30b9483db..57c7f67fd 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -41,11 +41,11 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6ba5f4f87..6919729fe 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -55,11 +55,6 @@ let make_terminal_status = function
   | GramTerminal s -> Some s
   | GramNonTerminal _ -> None
 
-let rec make_tags = function
-  | GramTerminal s :: l -> make_tags l
-  | GramNonTerminal (loc, etyp, _) :: l -> Genarg.unquote etyp :: make_tags l
-  | [] -> []
-
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
   fun () ->
@@ -133,10 +128,9 @@ let cons_production_parameter = function
 let add_tactic_notation (local,n,prods,e) =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map (interp_prod_item n) prods in
-  let tags = make_tags prods in
   let pprule = {
-    Pptactic.pptac_args = tags;
-    pptac_prods = (n, List.map make_terminal_status prods);
+    Pptactic.pptac_level = n;
+    pptac_prods = prods;
   } in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   let parule = {