Merge PR#633: An extension of EXTEND and notations to make standard parsing tricks available to users

9 files changed, 45 insertions, 27 deletions

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432..ec3a49df4 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
 | [ in_clause'(cl) ] -> [ cl ]
 END
 
+let local_test_lpar_id_colon =
+  let err () = raise Stream.Failure in
+  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Util.stream_nth 0 strm with
+        | Tok.KEYWORD "(" ->
+            (match Util.stream_nth 1 strm with
+              | Tok.IDENT _ ->
+                  (match Util.stream_nth 2 strm with
+                    | Tok.KEYWORD ":" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfad..9b4167512 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e6ccaf84..bd48614db 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c2..d717ed0a5 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
 
 let pr_ltac_production_item = function
 | Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, sep), id) ->
+| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
+| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
+| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
   let sep = match sep with
   | None -> mt ()
   | Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
 | [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+| [ ident(nt) ] ->
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af..e33c25cf8 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
         | _ -> err ())
 
 (* idem for (x:t) *)
-let test_lpar_id_colon =
-  Gram.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b73b66e56..a61957559 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
       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
+      | TacNonTerm (_, _, None) :: prods, args -> pack prods args
+      | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
+        TacNonTerm (loc, (symb, arg), ido) :: pack prods args
       | _ -> raise Not_found
       in
       let prods = pack pp.pptac_prods l in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 729338fb9..433f342c4 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 32750383b..91262f6fd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
 
 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
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 type argument = Genarg.ArgT.any Extend.user_symbol
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let map = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, s, _) ->
+  | TacNonTerm (loc, s, ido) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (loc, typ, e)
+    GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
 
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
-  | TacNonTerm (loc, (nt, sep), id) ->
+  | TacNonTerm (loc, (nt, sep), ido) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
       end
     in
     let symbol = interp_entry_name interp symbol in
-    TacNonTerm (loc, symbol, id)
+    TacNonTerm (loc, symbol, ido)
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, _, id) -> Some id
+| TacNonTerm (_, _, ido) -> ido
 
 let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
@@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
     let open Tacexpr in
     let get_id = function
     | TacTerm s -> None
-    | TacNonTerm (_, _, id) -> Some id
+    | TacNonTerm (_, _, ido) -> ido
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 069504473..dac62dad3 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
 
 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
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 (** An argument type as provided in Tactic notations, i.e. a string like