Globalisation des noms de tactiques dans les définitions de tactiques

pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).


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

4 files changed, 74 insertions, 111 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b476320150..641ccf7fc5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -90,6 +90,10 @@ let explain_internalisation_error = function
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
   | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
 
+let error_unbound_metanum loc n =
+  user_err_loc
+    (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound")
+
 (**********************************************************************)
 (* Dump of globalization (to be used by coqdoc)                       *)
 
@@ -453,8 +457,13 @@ let internalise isarity sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern false env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
-    | CMeta (loc, n) when n >=0 or allow_soapp ->
+    | CMeta (loc, n) when allow_soapp = None or !interning_grammar ->
 	RMeta (loc, n)
+    | CMeta (loc, n) when n >=0 ->
+        if List.mem n (out_some allow_soapp) then 
+	  RMeta (loc, n)
+        else 
+          error_unbound_metanum loc n
     | CMeta (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
     | CSort (loc, s) ->
@@ -559,20 +568,20 @@ let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c =
     allow_soapp (ltacvar,Environ.named_context env, []) c
 
 let interp_rawconstr sigma env c =
-  interp_rawconstr_gen false sigma env [] false ([],[]) c
+  interp_rawconstr_gen false sigma env [] (Some []) ([],[]) c
 
 let interp_rawtype sigma env c =
-  interp_rawconstr_gen true sigma env [] false ([],[]) c
+  interp_rawconstr_gen true sigma env [] (Some []) ([],[]) c
 
 let interp_rawtype_with_implicits sigma env impls c =
-  interp_rawconstr_gen true sigma env impls false ([],[]) c
+  interp_rawconstr_gen true sigma env impls (Some []) ([],[]) c
 
 (*
 (* The same as interp_rawconstr but with a list of variables which must not be
    globalized *)
 
 let interp_rawconstr_wo_glob sigma env lvar c =
-  interp_rawconstr_gen sigma env [] false lvar c
+  interp_rawconstr_gen sigma env [] (Some []) lvar c
 *)
 
 (*********************************************************************)
@@ -621,7 +630,7 @@ type ltac_env =
 (* of instantiations (variables and metas)    *)
 (* Note: typ is retyped *)
 let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] false 
+  let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta))
     (List.map fst ltacvar,unbndltacvar) c
   and rtype lst = retype_list sigma env lst in
   understand_gen sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
@@ -629,7 +638,7 @@ let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
 let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
-  let c = interp_rawconstr_gen false sigma env [] false
+  let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta))
     (List.map fst ltacvar,unbndltacvar) c
   and rtype lst = retype_list sigma env lst in
   understand_gen_tcc sigma env (rtype ltacvar) (rtype lmeta) exptyp c;;
@@ -637,86 +646,10 @@ let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp =
 let interp_casted_constr sigma env c typ = 
   understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
 
-(* To process patterns, we need a translation without typing at all. *)
-
-let rec pat_of_raw metas vars lvar = function
-  | RVar (_,id) ->
-      (try PRel (list_index (Name id) vars)
-       with Not_found ->
-       try List.assoc id lvar
-       with Not_found -> PVar id)
-  | RMeta (_,n) ->
-      metas := n::!metas; PMeta (Some n)
-  | RRef (_,r) ->
-      PRef r
-  (* Hack pour ne pas réécrire une interprétation complète des patterns*)
-  | RApp (_, RMeta (_,n), cl) when n<0 ->
-      PSoApp (- n, List.map (pat_of_raw metas vars lvar) cl)
-  | RApp (_,c,cl) -> 
-      PApp (pat_of_raw metas vars lvar c,
-	    Array.of_list (List.map (pat_of_raw metas vars lvar) cl))
-  | RLambda (_,na,c1,c2) ->
-      PLambda (na, pat_of_raw metas vars lvar c1,
-	       pat_of_raw metas (na::vars) lvar c2)
-  | RProd (_,na,c1,c2) ->
-      PProd (na, pat_of_raw metas vars lvar c1,
-	       pat_of_raw metas (na::vars) lvar c2)
-  | RLetIn (_,na,c1,c2) ->
-      PLetIn (na, pat_of_raw metas vars lvar c1,
-	       pat_of_raw metas (na::vars) lvar c2)
-  | RSort (_,s) ->
-      PSort s
-  | RHole _ ->
-      PMeta None
-  | RCast (_,c,t) ->
-      if_verbose warning "Cast not taken into account in constr pattern";
-      pat_of_raw metas vars lvar c
-  | ROrderedCase (_,st,po,c,br) ->
-      PCase (st,option_app (pat_of_raw metas vars lvar) po,
-             pat_of_raw metas vars lvar c,
-             Array.map (pat_of_raw metas vars lvar) br)
-  | RCases (loc,po,[c],br) ->
-      PCase (Term.RegularStyle,option_app (pat_of_raw metas vars lvar) po,
-             pat_of_raw metas vars lvar c,
-             Array.init (List.length br)
-               (pat_of_raw_branch loc metas vars lvar br))
-  | r ->
-      let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", str "Not supported pattern")
-
-and pat_of_raw_branch loc metas vars lvar brs i =
-  let bri = List.filter
-    (function
-        (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
-      | (loc,_,_,_) ->
-          user_err_loc (loc,"pattern_of_rawconstr",
-                        str "Not supported pattern")) brs in
-  match bri with
-      [(_,_,[PatCstr(_,_,lv,_)],br)] ->
-        let lna =
-          List.map
-            (function PatVar(_,na) -> na
-              | PatCstr(loc,_,_,_) ->
-                  user_err_loc (loc,"pattern_of_rawconstr",
-                                str "Not supported pattern")) lv in
-        let vars' = List.rev lna @ vars in 
-        List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna
-          (pat_of_raw metas vars' lvar br)
-    | _ -> user_err_loc (loc,"pattern_of_rawconstr",
-                         str "No unique branch for " ++ int (i+1) ++
-                         str"-th constructor")
-
-
-let pattern_of_rawconstr lvar c =
-  let metas = ref [] in
-  let p = pat_of_raw metas [] lvar c in
-  (!metas,p)
-
 let interp_constrpattern_gen sigma env (ltacvar,unbndltacvar) c =
-  let c = interp_rawconstr_gen false sigma env [] true
+  let c = interp_rawconstr_gen false sigma env [] None
     (List.map fst ltacvar,unbndltacvar) c in
-  let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) ltacvar in
-  pattern_of_rawconstr nlvar c
+  pattern_of_rawconstr c
 
 let interp_constrpattern sigma env c =
   interp_constrpattern_gen sigma env ([],[]) c
@@ -726,7 +659,7 @@ let interp_aconstr vars a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
-    false (([],[]),Environ.named_context env,vl)) a in
+    (Some []) (([],[]),Environ.named_context env,vl)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 5d66424c24..99e7d68bbc 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -43,7 +43,7 @@ type ltac_env =
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
 val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> 
-    bool -> ltac_sign -> constr_expr -> rawconstr
+    int list option -> ltac_sign -> constr_expr -> rawconstr
 
 (*s Composing the translation with typing *)
 val interp_constr        : evar_map -> env -> constr_expr -> constr
diff --git a/interp/genarg.ml b/interp/genarg.ml
index b25908b42e..0f2e031cc7 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -39,6 +39,9 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+type 'a or_metanum = AN of 'a | MetaNum of int located
+type 'a and_short_name = 'a * identifier option
+type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
 
@@ -53,57 +56,72 @@ let create_arg s =
     anomaly ("Genarg.create: already declared generic argument " ^ s);
   dyntab := s :: !dyntab;
   let t = ExtraArgType s in
-  (t,t)
+  (t,t,t)
 
 let exists_argtype s = List.mem s !dyntab
 
 type open_constr = Evd.evar_map * Term.constr
-(*type open_rawconstr = Coqast.t*)
-type open_rawconstr = constr_expr
+type open_constr_expr = constr_expr
+type open_rawconstr = rawconstr_and_expr
 
 let rawwit_bool = BoolArgType
+let globwit_bool = BoolArgType
 let wit_bool = BoolArgType
 
 let rawwit_int = IntArgType
+let globwit_int = IntArgType
 let wit_int = IntArgType
 
 let rawwit_int_or_var = IntOrVarArgType
+let globwit_int_or_var = IntOrVarArgType
 let wit_int_or_var = IntOrVarArgType
 
 let rawwit_string = StringArgType
+let globwit_string = StringArgType
 let wit_string = StringArgType
 
 let rawwit_ident = IdentArgType
+let globwit_ident = IdentArgType
 let wit_ident = IdentArgType
 
 let rawwit_pre_ident = PreIdentArgType
+let globwit_pre_ident = PreIdentArgType
 let wit_pre_ident = PreIdentArgType
 
 let rawwit_ref = RefArgType
+let globwit_ref = RefArgType
 let wit_ref = RefArgType
 
 let rawwit_quant_hyp = QuantHypArgType
+let globwit_quant_hyp = QuantHypArgType
 let wit_quant_hyp = QuantHypArgType
 
 let rawwit_sort = SortArgType
+let globwit_sort = SortArgType
 let wit_sort = SortArgType
 
 let rawwit_constr = ConstrArgType
+let globwit_constr = ConstrArgType
 let wit_constr = ConstrArgType
 
 let rawwit_constr_may_eval = ConstrMayEvalArgType
+let globwit_constr_may_eval = ConstrMayEvalArgType
 let wit_constr_may_eval = ConstrMayEvalArgType
 
 let rawwit_tactic = TacticArgType
+let globwit_tactic = TacticArgType
 let wit_tactic = TacticArgType
 
 let rawwit_casted_open_constr = CastedOpenConstrArgType
+let globwit_casted_open_constr = CastedOpenConstrArgType
 let wit_casted_open_constr = CastedOpenConstrArgType
 
 let rawwit_constr_with_bindings = ConstrWithBindingsArgType
+let globwit_constr_with_bindings = ConstrWithBindingsArgType
 let wit_constr_with_bindings = ConstrWithBindingsArgType
 
 let rawwit_red_expr = RedExprArgType
+let globwit_red_expr = RedExprArgType
 let wit_red_expr = RedExprArgType
 
 let wit_list0 t = List0ArgType t
@@ -167,17 +185,6 @@ let app_pair f1 f2 = function
       (u, Obj.repr (o1,o2))
   | _ -> failwith "Genarg: not a pair"
 
-let or_var_app f = function
-  | ArgArg x -> ArgArg (f x)
-  | ArgVar _ as x -> x
-
-let smash_var_app t f g = function
-  | ArgArg x -> f x
-  | ArgVar (_,id) ->
-      let (u, _ as x) = g id in
-      if t <> u then failwith "Genarg: a variable bound to a wrong type";
-      x
-
 let unquote x = x
 
 type an_arg_of_this_type = Obj.t
diff --git a/interp/genarg.mli b/interp/genarg.mli
index f1246b2cc6..c938d4c516 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -16,10 +16,17 @@ open Rawterm
 open Topconstr
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+type 'a or_metanum = AN of 'a | MetaNum of int located
+type 'a and_short_name = 'a * identifier option
 
-type open_constr = Evd.evar_map * Term.constr
-type open_rawconstr = constr_expr
+(* In globalize tactics, we need to keep the initial constr_expr to recompute*)
+(* in the environment by the effective calls to Intro, Inversion, etc *)
+(* The constr_expr field is None in TacDef though *)
+type rawconstr_and_expr = rawconstr * constr_expr option
 
+type open_constr = Evd.evar_map * Term.constr
+type open_constr_expr = constr_expr
+type open_rawconstr = rawconstr_and_expr
 
 (* The route of a generic argument, from parsing to evaluation
 
@@ -47,12 +54,12 @@ IntOrVarArgType                int or_var               int
 StringArgType                  string (parsed w/ "")    string
 IdentArgType                   identifier               identifier         
 PreIdentArgType                string (parsed w/o "")   string
-RefArgType                     reference           global_reference
-ConstrArgType                  constr_expr               constr
-ConstrMayEvalArgType               constr_expr may_eval      constr
+RefArgType                     reference                global_reference
+ConstrArgType                  constr_expr              constr
+ConstrMayEvalArgType           constr_expr may_eval     constr
 QuantHypArgType                quantified_hypothesis    quantified_hypothesis
 TacticArgType                  raw_tactic_expr          tactic
-CastedOpenConstrArgType        constr_expr               open_constr
+CastedOpenConstrArgType        constr_expr              open_constr
 ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
 List0ArgType of argument_type
 List1ArgType of argument_type
@@ -63,49 +70,64 @@ ExtraArgType of string         '_a                      '_b
 type ('a,'co,'ta) abstract_argument_type
 
 val rawwit_bool : (bool,'co,'ta) abstract_argument_type
+val globwit_bool : (bool,'co,'ta) abstract_argument_type
 val wit_bool : (bool,'co,'ta) abstract_argument_type
 
 val rawwit_int : (int,'co,'ta) abstract_argument_type
+val globwit_int : (int,'co,'ta) abstract_argument_type
 val wit_int : (int,'co,'ta) abstract_argument_type
 
 val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
 val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
 
 val rawwit_string : (string,'co,'ta) abstract_argument_type
+val globwit_string : (string,'co,'ta) abstract_argument_type
 val wit_string : (string,'co,'ta) abstract_argument_type
 
 val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
+val globwit_ident : (identifier,'co,'ta) abstract_argument_type
 val wit_ident : (identifier,'co,'ta) abstract_argument_type
 
 val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
+val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
 val wit_pre_ident : (string,'co,'ta) abstract_argument_type
 
 val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
+val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_ref : (global_reference,constr,'ta) abstract_argument_type
 
 val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
 val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
 
 val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type
+val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_sort : (sorts,constr,'ta) abstract_argument_type
 
 val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr : (constr,constr,'ta) abstract_argument_type
 
-val rawwit_constr_may_eval : (constr_expr may_eval,constr_expr,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference or_metanum) may_eval,constr_expr,'ta) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
 
-val rawwit_casted_open_constr : (open_rawconstr,constr_expr,'ta) abstract_argument_type
+val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
 
 val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
 
 val rawwit_red_expr : ((constr_expr,reference or_metanum) red_expr_gen,constr_expr,'ta) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
 
 (* TODO: transformer tactic en extra arg *)
 val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type
+val globwit_tactic : ('ta,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_tactic : ('ta,constr,'ta) abstract_argument_type
 
 val wit_list0 :
@@ -159,8 +181,9 @@ val app_pair :
    polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
    de create *)
 val create_arg : string ->
-      ('rawa,'rawco,'rawta) abstract_argument_type
-      * ('a,'co,'ta) abstract_argument_type
+      ('a,'co,'ta) abstract_argument_type
+      * ('globa,'globco,'globta) abstract_argument_type
+      * ('rawa,'rawco,'rawta) abstract_argument_type
 
 val exists_argtype : string -> bool