Exposing structure of the entries to tactic notation printers.

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

5 files changed, 154 insertions, 133 deletions

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 2cc1b7b1c..f1b8eee5e 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Libobject
 open Genarg
+open Extend
 open Pcoq
 open Egramml
 open Egramcoq
@@ -19,7 +20,7 @@ open Vernacexpr
 open Libnames
 open Nameops
 
-type 'a grammar_tactic_prod_item_expr =
+type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
 | TacNonTerm of Loc.t * 'a * Names.Id.t
 
@@ -42,7 +43,6 @@ let coincide s pat off =
   !break
 
 let atactic n =
-  let open Extend in
   if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
   else Aentryl (name_of_entry Tactic.tactic_expr, n)
 
@@ -51,7 +51,6 @@ type entry_name = EntryName :
 
 (** Quite ad-hoc *)
 let get_tacentry n m =
-  let open Extend in
   let check_lvl n =
     Int.equal m n
     && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
@@ -66,7 +65,6 @@ let get_separator = function
 | Some sep -> sep
 
 let rec parse_user_entry s sep =
-  let open Extend in
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
     let entry = parse_user_entry (String.sub s 3 (l-8)) None in
@@ -94,25 +92,14 @@ let arg_list = function Rawwit t -> Rawwit (ListArg t)
 let arg_opt = function Rawwit t -> Rawwit (OptArg t)
 
 let interp_entry_name interp symb =
-  let open Extend in
   let rec eval = function
-  | Ulist1 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1 g)
-  | Ulist1sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist1sep (g, sep))
-  | Ulist0 e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0 g)
-  | Ulist0sep (e, sep) ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Alist0sep (g, sep))
-  | Uopt e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_opt t, Aopt g)
-  | Uentry s -> interp s None
-  | Uentryl (s, n) -> interp s (Some n)
+  | Ulist1 e -> Ulist1 (eval e)
+  | Ulist1sep (e, sep) -> Ulist1sep (eval e, sep)
+  | Ulist0 e -> Ulist0 (eval e)
+  | Ulist0sep (e, sep) -> Ulist0sep (eval e, sep)
+  | Uopt e -> Uopt (eval e)
+  | Uentry s -> Uentry (interp s None)
+  | Uentryl (s, n) -> Uentryl (interp s (Some n), n)
   in
   eval symb
 
@@ -134,15 +121,40 @@ let get_tactic_entry n =
 
 type tactic_grammar = {
   tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
+  tacgram_prods : Pptactic.grammar_terminals;
 }
 
 (* Declaration of the tactic grammar rule *)
 
 let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
+| TacTerm _ :: _ -> true
 | _ -> false
 
+let rec prod_item_of_symbol lev = function
+| Extend.Ulist1 s ->
+  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
+  EntryName (Rawwit (ListArg typ), Alist1 e)
+| Extend.Ulist0 s ->
+  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
+  EntryName (Rawwit (ListArg typ), Alist0 e)
+| Extend.Ulist1sep (s, sep) ->
+  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
+  EntryName (Rawwit (ListArg typ), Alist1sep (e, sep))
+| Extend.Ulist0sep (s, sep) ->
+  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
+  EntryName (Rawwit (ListArg typ), Alist0sep (e, sep))
+| Extend.Uopt s ->
+  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
+  EntryName (Rawwit (OptArg typ), Aopt e)
+| Extend.Uentry arg ->
+  let ArgT.Any tag = arg in
+  let wit = ExtraArg tag in
+  EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+| Extend.Uentryl (s, n) ->
+  let ArgT.Any tag = s in
+  assert (coincide (ArgT.repr tag) "tactic" 0);
+  get_tacentry n lev
+
 (** Tactic grammar extensions *)
 
 let add_tactic_entry (kn, ml, tg) =
@@ -164,7 +176,14 @@ let add_tactic_entry (kn, ml, tg) =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
       error "Notation for simple tactic must start with an identifier."
   in
-  let rules = make_rule mkact tg.tacgram_prods in
+  let map = function
+  | TacTerm s -> GramTerminal s
+  | TacNonTerm (loc, s, _) ->
+    let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
+    GramNonTerminal (loc, typ, e)
+  in
+  let prods = List.map map tg.tacgram_prods in
+  let rules = make_rule mkact prods in
   synchronize_level_positions ();
   grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
   1
@@ -186,28 +205,27 @@ let register_tactic_notation_entry name entry =
   in
   entry_names := String.Map.add name entry !entry_names
 
-let interp_prod_item lev = function
-  | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, (nt, sep), _) ->
+let interp_prod_item = function
+  | TacTerm s -> TacTerm s
+  | TacNonTerm (loc, (nt, sep), id) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
-      let ArgT.Any arg =
-        if String.Map.mem s !entry_names then
-          String.Map.find s !entry_names
-        else match ArgT.name s with
-        | None -> error ("Unknown entry "^s^".")
-        | Some arg -> arg
-      in
-      let wit = ExtraArg arg in
-      EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+      if String.Map.mem s !entry_names then String.Map.find s !entry_names
+      else begin match ArgT.name s with
+      | None -> error ("Unknown entry "^s^".")
+      | Some arg -> arg
+      end
     | Some n ->
       (** FIXME: do better someday *)
       assert (String.equal s "tactic");
-      get_tacentry n lev
+      begin match Constrarg.wit_tactic with
+      | ExtraArg tag -> ArgT.Any tag
+      | _ -> assert false
+      end
     in
-    let EntryName (etyp, e) = interp_entry_name interp symbol in
-    GramNonTerminal (loc, etyp, e)
+    let symbol = interp_entry_name interp symbol in
+    TacNonTerm (loc, symbol, id)
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -300,7 +318,7 @@ let add_glob_tactic_notation local n prods forml ids tac =
 
 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 prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   add_glob_tactic_notation local n prods false ids tac
 
@@ -315,12 +333,13 @@ let extend_atomic_tactic name entries =
   let open Tacexpr in
   let map_prod prods =
     let (hd, rem) = match prods with
-    | GramTerminal s :: rem -> (s, rem)
+    | TacTerm s :: rem -> (s, rem)
     | _ -> assert false (** Not handled by the ML extension syntax *)
     in
     let empty_value = function
-    | GramTerminal s -> raise NonEmptyArgument
-    | GramNonTerminal (_, typ, e) ->
+    | TacTerm s -> raise NonEmptyArgument
+    | TacNonTerm (_, symb, _) ->
+      let EntryName (typ, e) = prod_item_of_symbol 0 symb in
       let Genarg.Rawwit wit = typ in
       let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
       let default = epsilon_value inj e in
@@ -342,33 +361,21 @@ let extend_atomic_tactic name entries =
   List.iteri add_atomic entries
 
 let add_ml_tactic_notation name prods =
-  let interp_prods = function
-  | TacTerm s -> None, GramTerminal s
-  | TacNonTerm (loc, symb, id) ->
-    let interp (ArgT.Any tag) lev = match lev with
-    | None ->
-      let wit = ExtraArg tag in
-      EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit)))
-    | Some lev ->
-      assert (coincide (ArgT.repr tag) "tactic" 0);
-      EntryName (Rawwit Constrarg.wit_tactic, atactic lev)
-    in
-    let EntryName (etyp, e) = interp_entry_name interp symb in
-    Some id, GramNonTerminal (loc, etyp, e)
-  in
-  let prods = List.map (fun p -> List.map interp_prods p) prods in
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
-    let (ids, prods) = List.split prods in
-    let ids = List.map_filter (fun x -> x) ids in
+    let get_id = function
+    | TacTerm s -> None
+    | TacNonTerm (_, _, id) -> Some id
+    in
+    let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
     let tac = TacML (Loc.ghost, entry, List.map map ids) in
     add_glob_tactic_notation false 0 prods true ids tac
   in
   List.iteri iter (List.rev prods);
-  extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods)
+  extend_atomic_tactic name prods
 
 (**********************************************************************)
 (** Ltac quotations                                                   *)
@@ -376,7 +383,6 @@ let add_ml_tactic_notation name prods =
 let ltac_quotations = ref String.Set.empty
 
 let create_ltac_quotation name cast (e, l) =
-  let open Extend in
   let () =
     if String.Set.mem name !ltac_quotations then
       failwith ("Ltac quotation " ^ name ^ " already registered")
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 7586bff92..402cb2fc9 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -18,7 +18,7 @@ val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit
 
 (** {5 Tactic Notations} *)
 
-type 'a grammar_tactic_prod_item_expr =
+type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
 | TacNonTerm of Loc.t * 'a * Names.Id.t
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 9ab6895f3..44c832bd7 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
 
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index b1e650b87..86e3ea548 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -17,6 +17,9 @@ open Constrexpr
 open Tacexpr
 open Ppextend
 
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
@@ -42,7 +45,7 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
-type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
 type pp_tactic = {
   pptac_level : int;
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index d49bef1fd..4ef2ea918 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -36,8 +36,6 @@ module type Pp = sig
 
   val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
 
-  val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
-
   val pr_raw_extend: env -> int ->
     ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds