Exposing structure of the entries to tactic notation printers.

This allows a proper printing of tactic notations with special tokens
such as separators.

1 files changed, 80 insertions, 66 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 9ab6895f3b..44c832bd7a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -27,7 +27,11 @@ open Printer
 
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
-type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
 type pp_tactic = {
   pptac_level : int;
@@ -335,51 +339,23 @@ module Make
         try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
         with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
 
-  let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) =
-    match wit with
-      | ListArg wit ->
-        let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
-        let ans = pr_sequence map x in
-        hov_if_not_empty 0 ans
-      | OptArg wit ->
-        let ans = match x with
-          | None -> mt ()
-          | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
-        in
-        hov_if_not_empty 0 ans
-      | PairArg (wit1, wit2) ->
-        let p, q = x in
-        let p = in_gen (topwit wit1) p in
-        let q = in_gen (topwit wit2) q in
-        let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in
-        hov_if_not_empty 0 ans
-      | ExtraArg s ->
-        try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x)
-        with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x)
-
   let rec tacarg_using_rule_token pr_gen = function
-    | 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"
-
-  let filter_arg = function
-  | Egramml.GramTerminal _ -> None
-  | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t)
+    | [] -> []
+    | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
+    | TacNonTerm (_, (symb, arg), _) :: l  ->
+      pr_gen symb arg :: tacarg_using_rule_token pr_gen l
 
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
-    | (Egramml.GramTerminal s :: l, al) ->
+    | TacTerm s :: l ->
       (** 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))
+      primitive s :: tacarg_using_rule_token pr_gen l
     | _ -> tacarg_using_rule_token pr_gen l
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
+  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
         str "@" ++ int i
@@ -390,31 +366,82 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
-  let pr_alias_gen check pr_gen lev key l =
+  let pr_alias_gen pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
-      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
+      let rec pack prods args = match prods, args with
+      | [], [] -> []
+      | TacTerm s :: prods, args -> TacTerm s :: pack prods args
+      | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
+        TacNonTerm (loc, (symb, arg), id) :: pack prods args
+      | _ -> raise Not_found
+      in
+      let prods = pack pp.pptac_prods l in
+      let p = pr_tacarg_using_rule pr_gen prods 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)
-  | _ -> argument_type_eq t (ArgumentType wit_tactic)
+      let pr arg = str "_" in
+      KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
 
   let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
 
+  let is_genarg tag wit =
+    let ArgT.Any tag = tag in
+    argument_type_eq (ArgumentType (ExtraArg tag)) wit
+
+  let get_list : type l. l generic_argument -> l generic_argument list option =
+  function (GenArg (wit, arg)) -> match wit with
+  | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg)
+  | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg)
+  | _ -> None
+
+  let get_opt : type l. l generic_argument -> l generic_argument option option =
+  function (GenArg (wit, arg)) -> match wit with
+  | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg)
+  | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
+  | _ -> None
+
+  let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+  fun prtac symb arg -> match symb with
+  | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+  | Extend.Ulist1 s | Extend.Ulist0 s ->
+    begin match get_list arg with
+    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | Some l -> pr_sequence (pr_any_arg prtac s) l
+    end
+  | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
+    begin match get_list arg with
+    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
+    end
+  | Extend.Uopt s ->
+    begin match get_opt arg with
+    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | Some l -> pr_opt (pr_any_arg prtac s) l
+    end
+  | Extend.Uentry _ | Extend.Uentryl _ ->
+    str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+  let rec pr_targ prtac symb arg = match symb with
+  | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
+    prtac (1, Any) arg
+  | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+  | _ ->
+    match arg with
+    | TacGeneric arg ->
+      let pr l arg = prtac l (TacGeneric arg) in
+      pr_any_arg pr symb arg
+    | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
   let pr_raw_extend_rec prc prlc prtac prpat =
-    pr_extend_gen check_type (pr_farg prtac)
+    pr_extend_gen (pr_farg prtac)
   let pr_glob_extend_rec prc prlc prtac prpat =
-    pr_extend_gen check_type (pr_farg prtac)
+    pr_extend_gen (pr_farg prtac)
 
-  let pr_raw_alias prc prlc prtac prpat =
-    pr_alias_gen check_type (pr_farg prtac)
-  let pr_glob_alias prc prlc prtac prpat =
-    pr_alias_gen check_type (pr_farg prtac)
+  let pr_raw_alias prc prlc prtac prpat lev key args =
+    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+  let pr_glob_alias prc prlc prtac prpat lev key args =
+    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -1278,10 +1305,6 @@ module Make
     (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
     (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
 
-  let pr_top_generic env = pr_top_generic_rec
-    (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-    pr_value pr_constr_pattern
-
   let pr_raw_extend env = pr_raw_extend_rec
     pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
 
@@ -1289,20 +1312,11 @@ module Make
     (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
     (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
 
-  let check_val_type t arg =
-    let ArgumentType t = t in
-(*     let t = Genarg.val_tag (Obj.magic t) in *)
-(*     let Val.Dyn (t', _) = arg in *)
-(*     match Genarg.Val.eq t t' with *)
-(*     | None -> false *)
-(*     | Some _ -> true *)
-    true (** FIXME *)
-
   let pr_alias pr lev key args =
-    pr_alias_gen check_val_type pr lev key args
+    pr_alias_gen (fun _ arg -> pr arg) lev key args
 
   let pr_extend pr lev ml args =
-    pr_extend_gen check_val_type pr lev ml args
+    pr_extend_gen pr lev ml args
 
   let pr_atomic_tactic env = pr_atomic_tactic_level env ltop