Fixing bug #2732 (anomaly when using the tolerance for writing

"f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an
Ltac function - see Tacinterp.add_primitive_tactic).

More precisely, when parsing "f ref" and "ref" is recognized as the
name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic
(like "eauto", "firstorder", "discriminate", ...), the code was
correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END'
was given (where "foo" has no arguments in the rule) but not when a rule
of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given
(where "foo" had an optional argument in the rule). In particular,
"firstorder" was in this case.

More generally, if, for an extra argument able to parse the empty string, a rule
`TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given,
then "foo" was not recognized as parseable as an atomic string (this
happened e.g. for "eauto").  This is now also fixed.

There was also another bug when the internal name of tactic was not
the same as the user-level name of the tactic. This is the reason why
"congruence" was not recognized when given as argument of an ltac (its
internal name is "cc").

Incidentally removed the redundant last line in the parsing rule for
"firstorder".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 103 insertions, 25 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 788e664e2..d890be142 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -107,6 +107,72 @@ let rec make_wit loc = function
         value wit = $lid:"wit_"^s$;
       end in WIT.wit >>
 
+let possibly_empty_subentries prods =
+  try
+    Some (List.fold_right (fun e l -> match e with
+    | GramNonTerminal(_,(List0ArgType _| OptArgType _),_,_) ->
+        (* This parses epsilon *) l
+    | GramNonTerminal(_,ExtraArgType s,_,_) ->
+        (* This parses epsilon if s parses it *) s::l
+    | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+        (* This does not parse epsilon *)
+        (* Not meaningful to have Pair in prods nor to have empty *)
+        (* entries in Lst1 productions *)
+        raise Exit) prods [])
+  with Exit -> None
+
+let has_extraarg =
+  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+
+let statically_known_possibly_empty (prods,_) =
+  List.for_all (function
+    | GramNonTerminal(_,(OptArgType _|List0ArgType _|ExtraArgType _),_,_) ->
+        (* Opt and List0 parses the empty string and for ExtraArg we don't know *)
+        (* (we'll have to test dynamically *)
+        true
+    | _ ->
+        (* This consumes a token for sure *) false)
+      prods
+
+let possibly_empty_subentries loc (prods,act) =
+  let bind_name p v e = match p with
+    | None -> e
+    | Some id ->
+        let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+  let rec aux = function
+    | [] -> <:expr< $act$ >>
+    | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
+        bind_name p <:expr< None >> (aux tl)
+    | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
+        bind_name p <:expr< [] >> (aux tl)
+    | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
+        (* We check at runtime if extraarg s parses "epsilon" *)
+        let s = match p with None -> "_" | Some id -> Names.string_of_id id in
+        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_globwit loc t$ with
+          [ None -> raise Exit
+          | Some v -> v ] in $aux tl$ >>
+    | _ -> assert false (* already filtered out *) in
+  if has_extraarg prods then
+    (* Needs a dynamic check *)
+    (true, <:expr< try Some $aux prods$ with Exit -> None >>)
+  else
+    (* Static optimisation *)
+    (false, aux prods)
+
+let make_possibly_empty_subentries loc cl =
+  let cl = List.filter statically_known_possibly_empty cl in
+  if cl = [] then
+    <:expr< None >>
+  else
+    let rec aux = function
+    | (true, e) :: l ->
+        <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
+    | (false, e) :: _ ->
+        <:expr< Some $e$ >>
+    | [] ->
+        <:expr< None >> in
+    aux (List.map (possibly_empty_subentries loc) cl)
+
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
@@ -160,10 +226,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
   let globwit = <:expr< $lid:"globwit_"^s$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  let default_value = <:expr< $make_possibly_empty_subentries loc cl$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
-      Genarg.create_arg $se$ >>;
+      Genarg.create_arg $default_value$ $se$>>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
      <:str_item< do {
@@ -195,7 +262,7 @@ let declare_vernac_argument loc s pr cl =
    [ <:str_item<
       value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
              ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
-              $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>;
+              $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
     <:str_item< do {
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index cc5b58ee7..a660f910e 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -16,12 +16,12 @@ open Genarg
 
 let tactic_main_level = 5
 
-let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
-let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
-let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
-let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
-let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
-let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg None "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg None "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg None "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg None "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg None "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg None "tactic5"
 
 let wit_tactic = function
   | 0 -> wit_tactic0
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 838c771c6..b7364efc1 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -120,19 +120,27 @@ let make_one_printing_rule se (pt,e) =
 
 let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
 
-let rec contains_epsilon = function
-  | List0ArgType _ -> true
-  | List1ArgType t -> contains_epsilon t
-  | OptArgType _ -> true
-  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
-  | ExtraArgType("hintbases") -> true
-  | _ -> false
-let is_atomic = function
-  | GramTerminal s :: l when
-      List.for_all (function
-          GramTerminal _ -> false
-	| GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
-	-> [s]
+let possibly_empty_subentries loc s prods =
+  try
+    let l = List.map (function
+    | GramNonTerminal(_,(List0ArgType _|OptArgType _|ExtraArgType _ as t),_,_)->
+        (* This possibly parses epsilon *)
+        let globwit = make_globwit loc t in
+        <:expr< match Genarg.default_empty_value $globwit$ with
+                [ None -> failwith ""
+                | Some v -> Genarg.in_gen $globwit$ v ] >>
+    | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+        (* This does not parse epsilon (this Exit is static time) *)
+        raise Exit) prods in
+    if has_extraarg prods then
+      [s, <:expr< try Some $mlexpr_of_list (fun x -> x) l$
+                  with Failure "" -> None >>]
+    else
+      [s, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>]
+  with Exit -> []
+
+let possibly_atomic loc = function
+  | GramTerminal s :: l -> possibly_empty_subentries loc s l
   | _ -> []
 
 let declare_tactic loc s cl =
@@ -152,17 +160,20 @@ let declare_tactic loc s cl =
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
   let atomic_tactics =
-    mlexpr_of_list mlexpr_of_string
-      (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
+    mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
+      (List.flatten (List.map (fun (al,_) -> possibly_atomic loc al) cl)) in
   declare_str_items loc
    (hidden @
     [ <:str_item< do {
       try
         let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
         List.iter
-          (fun s -> Tacinterp.add_primitive_tactic s
+          (fun (s,l) -> match l with
+           [ Some l ->
+              Tacinterp.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
-                 Tacexpr.TacExtend($default_loc$,s,[]))))
+                 Tacexpr.TacExtend($default_loc$,$se$,l)))
+           | None -> () ])
           $atomic_tactics$
       with e -> Pp.pp (Errors.print e);
       Egrammar.extend_tactic_grammar $se$ $gl$;