Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic

tactic arguments of ltac functions).

Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.

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

12 files changed, 60 insertions, 32 deletions

diff --git a/interp/genarg.mli b/interp/genarg.mli
index 43cd73aedb..540fc400c6 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -257,7 +257,7 @@ val app_pair :
 
 (** create a new generic type of argument: force to associate
    unique ML types at each of the three levels *)
-val create_arg : 'globa option ->
+val create_arg : 'rawa option ->
     string ->
       ('a,tlevel) abstract_argument_type
       * ('globa,glevel) abstract_argument_type
@@ -314,4 +314,4 @@ type an_arg_of_this_type
 val in_generic :
   argument_type -> an_arg_of_this_type -> 'co generic_argument
 
-val default_empty_value : ('a,glevel) abstract_argument_type -> 'a option
+val default_empty_value : ('a,rlevel) abstract_argument_type -> 'a option
diff --git a/interp/notation.ml b/interp/notation.ml
index 96de08da3a..397f46fc42 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -818,3 +818,8 @@ let _ =
     { freeze_function = freeze;
       unfreeze_function = unfreeze;
       init_function = init }
+
+let with_notation_protection f x =
+  let fs = freeze () in
+  try let a = f x in unfreeze fs; a
+  with e -> unfreeze fs; raise e
diff --git a/interp/notation.mli b/interp/notation.mli
index 25ea594190..de14c95155 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -178,3 +178,5 @@ val declare_notation_printing_rule : notation -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 
 (** Rem: printing rules for primitive token are canonical *)
+
+val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index e8d72740f3..ac5aef8d42 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -107,28 +107,17 @@ 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,_) =
+let statically_known_possibly_empty s (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 *)
+    | GramNonTerminal(_,ExtraArgType s',_,_) ->
+        (* For ExtraArg we don't know (we'll have to test dynamically) *)
+        (* unless it is a recursive call *)
+        s <> s'
+    | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) ->
+        (* Opt and List0 parses the empty string *)
         true
     | _ ->
         (* This consumes a token for sure *) false)
@@ -140,7 +129,7 @@ let possibly_empty_subentries loc (prods,act) =
     | Some id ->
         let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
   let rec aux = function
-    | [] -> <:expr< $act$ >>
+    | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >>
     | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
         bind_name p <:expr< None >> (aux tl)
     | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
@@ -148,19 +137,22 @@ let possibly_empty_subentries loc (prods,act) =
     | 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
+        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit 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 ] >>)
+    (* Needs a dynamic check; catch all exceptions if ever some rhs raises *)
+    (* an exception rather than returning a value; *)
+    (* declares loc because some code can refer to it; *)
+    (* ensures loc is used to avoid "unused variable" warning *)
+    (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
   else
     (* Static optimisation *)
     (false, aux prods)
 
-let make_possibly_empty_subentries loc cl =
-  let cl = List.filter statically_known_possibly_empty cl in
+let make_possibly_empty_subentries loc s cl =
+  let cl = List.filter (statically_known_possibly_empty s) cl in
   if cl = [] then
     <:expr< None >>
   else
@@ -226,7 +218,7 @@ 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
+  let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index f30e061ff0..ecd7a1acc4 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -350,3 +350,8 @@ let _ =
     { freeze_function = freeze;
       unfreeze_function = unfreeze;
       init_function = init }
+
+let with_grammar_rule_protection f x =
+  let fs = freeze () in
+  try let a = f x in unfreeze fs; a
+  with e -> unfreeze fs; raise e
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 4a5f3c4c65..c9f92b7294 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -72,3 +72,5 @@ val get_extend_vernac_grammars :
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) ->
   notation_var_internalization_type list * notation_grammar
+
+val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 95f916f551..c7a646ac49 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -132,10 +132,12 @@ let rec possibly_empty_subentries loc = function
                              OptArgType _|
                              ExtraArgType _ as t),_,_)->
             (* This possibly parses epsilon *)
-            let globwit = make_globwit loc t in
-            <:expr< match Genarg.default_empty_value $globwit$ with
+            let rawwit = make_rawwit loc t in
+            <:expr< match Genarg.default_empty_value $rawwit$ with
                     [ None -> failwith ""
-                    | Some v -> Genarg.in_gen $globwit$ v ] >>
+                    | Some v ->
+                        Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign
+                          (Genarg.in_gen $rawwit$ v) ] >>
         | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
             (* This does not parse epsilon (this Exit is static time) *)
              raise Exit) prods in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a1e8f9bd1d..9da816d908 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2487,6 +2487,10 @@ let make_empty_glob_sign () =
   { ltacvars = ([],[]); ltacrecvars = [];
     gsigma = Evd.empty; genv = Global.env() }
 
+let fully_empty_glob_sign =
+  { ltacvars = ([],[]); ltacrecvars = [];
+    gsigma = Evd.empty; genv = Environ.empty_env }
+
 (* Initial call for interpretation *)
 let interp_tac_gen lfun avoid_ids debug t gl =
   interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 4d01e5ad97..eff48b1004 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -78,6 +78,8 @@ type glob_sign = {
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
+val fully_empty_glob_sign : glob_sign
+
 val add_interp_genarg :
   string ->
     (glob_sign -> raw_generic_argument -> glob_generic_argument) *
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3657c5d5af..8bb875ffb5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -273,7 +273,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
-    States.with_state_protection (fun () ->
+    Metasyntax.with_syntax_protection (fun () ->
      (* Temporary declaration of notations and scopes *)
      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      (* Interpret the constructor types *)
@@ -753,7 +753,7 @@ let interp_recursive isfix fixl notations =
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
-    States.with_state_protection (fun () ->
+    Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 76326f51ff..8415f0bcc9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -987,6 +987,18 @@ let inNotation : notation_obj -> obj =
        classify_function = classify_notation}
 
 (**********************************************************************)
+
+let with_lib_stk_protection f x =
+  let fs = Lib.freeze () in
+  try let a = f x in Lib.unfreeze fs; a
+  with e -> Lib.unfreeze fs; raise e
+
+let with_syntax_protection f x =
+  with_lib_stk_protection
+    (with_grammar_rule_protection
+       (with_notation_protection f)) x
+
+(**********************************************************************)
 (* Recovering existing syntax                                         *)
 
 let contract_notation ntn =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 74a8e0fe9c..e228b829ac 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -62,3 +62,5 @@ val add_syntactic_definition : identifier -> identifier list * constr_expr ->
 val print_grammar : string -> unit
 
 val check_infix_modifiers : syntax_modifier list -> unit
+
+val with_syntax_protection : ('a -> 'b) -> 'a -> 'b