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, 102 insertions, 277 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7af3a75dc8..9dafda587a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -13,11 +13,10 @@ open Names
 open Libnames
 open Nameops
 open Term
-open Termops
-open Reductionops
 open Rawterm
 open Environ
 open Nametab
+open Pp
 
 type constr_pattern =
   | PRef of global_reference
@@ -149,234 +148,6 @@ let head_of_constr_reference c = match kind_of_term c with
   | Var id -> VarNode id
   | _ -> anomaly "Not a rigid reference"
 
-
-(* Second part : Given a term with second-order variables in it,
-   represented by Meta's, and possibly applied using [SOAPP] to
-   terms, this function will perform second-order, binding-preserving,
-   matching, in the case where the pattern is a pattern in the sense
-   of Dale Miller.
-
-   ALGORITHM:
-
-   Given a pattern, we decompose it, flattening Cast's and apply's,
-   recursing on all operators, and pushing the name of the binder each
-   time we descend a binder.
-
-   When we reach a first-order variable, we ask that the corresponding
-   term's free-rels all be higher than the depth of the current stack.
-
-   When we reach a second-order application, we ask that the
-   intersection of the free-rels of the term and the current stack be
-   contained in the arguments of the application, and in that case, we
-   construct a LAMBDA with the names on the stack.
-
- *)
-
-exception PatternMatchingFailure
-
-let constrain ((n : int),(m : constr)) sigma =
-  if List.mem_assoc n sigma then
-    if eq_constr m (List.assoc n sigma) then sigma
-    else raise PatternMatchingFailure
-  else 
-    (n,m)::sigma
-    
-let build_lambda toabstract stk (m : constr) = 
-  let rec buildrec m p_0 p_1 = match p_0,p_1 with 
-    | (_, []) -> m
-    | (n, (na,t)::tl) -> 
-	if List.mem n toabstract then
-          buildrec (mkLambda (na,t,m)) (n+1) tl
-        else 
-	  buildrec (pop m) (n+1) tl
-  in 
-  buildrec m 1 stk
-
-let memb_metavars m n =
-  match (m,n) with
-    | (None, _)     -> true
-    | (Some mvs, n) -> List.mem n mvs
-
-let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
-
-let matches_core convert allow_partial_app pat c = 
-  let rec sorec stk sigma p t =
-    let cT = strip_outer_cast t in
-    match p,kind_of_term cT with
-      | PSoApp (n,args),m ->
-	  let relargs =
-	    List.map
-	      (function
-		 | PRel n -> n
-		 | _ -> error "Only bound indices are currently allowed in second order pattern matching")
-	      args in
-	  let frels = Intset.elements (free_rels cT) in
-	  if list_subset frels relargs then
-	    constrain (n,build_lambda relargs stk cT) sigma
-	  else
-	    raise PatternMatchingFailure
-
-      | PMeta (Some n), m ->
-	  let depth = List.length stk in
-	  let frels = Intset.elements (free_rels cT) in
-          if List.for_all (fun i -> i > depth) frels then
-	    constrain (n,lift (-depth) cT) sigma
-          else 
-	    raise PatternMatchingFailure
-
-      | PMeta None, m -> sigma
-
-      | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma
-
-      | PVar v1, Var v2 when v1 = v2 -> sigma
-
-      | PRef ref, _ when constr_of_reference ref = cT -> sigma
-
-      | PRel n1, Rel n2 when n1 = n2 -> sigma
-
-      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma
-
-      | PSort (RType _), Sort (Type _) -> sigma
-
-      | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
-          let p = Array.length args2 - Array.length args1 in
-          if p>=0 then
-            let args21, args22 = array_chop p args2 in
-            let sigma =
-	      let depth = List.length stk in
-              let c = mkApp(c2,args21) in
-	      let frels = Intset.elements (free_rels c) in
-              if List.for_all (fun i -> i > depth) frels then
-	        constrain (n,lift (-depth) c) sigma
-              else
-	        raise PatternMatchingFailure in
-            array_fold_left2 (sorec stk) sigma args1 args22
-          else raise PatternMatchingFailure
-
-      | PApp (c1,arg1), App (c2,arg2) ->
-        (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
-         with Invalid_argument _ -> raise PatternMatchingFailure)
-
-      | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PRef (ConstRef _ as ref), _ when convert <> None ->
-	  let (env,evars) = out_some convert in
-	  let c = constr_of_reference ref in
-	  if is_conv env evars c cT then sigma
-	  else raise PatternMatchingFailure
-
-      | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
-	  (* On ne teste pas le prédicat *)
-          if (Array.length br1) = (Array.length br2) then
-  	    array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
-          else
-            raise PatternMatchingFailure
-      (* À faire *)
-      |	PFix f0, Fix f1 when f0 = f1 -> sigma
-      |	PCoFix c0, CoFix c1 when c0 = c1 -> sigma
-      | _ -> raise PatternMatchingFailure
-
-  in 
-  Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
-
-let matches = matches_core None false
-
-let pmatches = matches_core None true
-
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
-
-(* Tells if it is an authorized occurrence *)
-let authorized_occ nocc mres =
-  if nocc = 0 then mres
-  else raise (NextOccurrence nocc)
-
-(* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match nocc pat c =
-  match kind_of_term c with
-  | Cast (c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,mkCast (List.hd lc, c2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,mkCast (List.hd lc, c2)))
-  | Lambda (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
-  | Prod (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1)))
-  | LetIn (x,c1,t2,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
-  | App (c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
-  | Case (ci,hd,c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
-      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
-      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))))
-  | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
-  | Rel _|Meta _|Var _|Sort _ ->
-    (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
-    | PatternMatchingFailure -> raise (NextOccurrence nocc)
-    | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
-
-(* Tries [sub_match] for all terms in the list *)
-and try_sub_match nocc pat lc =
-  let rec try_sub_match_rec nocc pat lacc = function
-    | [] -> raise (NextOccurrence nocc)
-    | c::tl ->
-      (try 
-         let (lm,ce) = sub_match nocc pat c in
-         (lm,lacc@(ce::tl))
-       with
-      | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
-  try_sub_match_rec nocc pat [] lc
-
-let is_matching pat n =
-  try let _ = matches pat n in true
-  with PatternMatchingFailure -> false
-
-let matches_conv env sigma = matches_core (Some (env,sigma)) false
-
-let is_matching_conv env sigma pat n =
-  try let _ = matches_conv env sigma pat n in true
-  with PatternMatchingFailure -> false
-
 let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -402,3 +173,93 @@ let rec pattern_of_constr t =
     | Fix f -> PFix f
     | CoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
+
+(* To process patterns, we need a translation without typing at all. *)
+
+let rec inst lvar = function
+  | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
+  | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
+  | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl)
+  | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b)
+  | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
+  | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
+  | PCase (c,po,p,pl) ->
+      PCase (c,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
+  (* Non recursive *)
+  | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
+  (* Bound to terms *)
+  | (PFix _ | PCoFix _ as r) ->
+      error ("Not instantiable pattern")
+
+let instantiate_pattern = inst
+
+let rec pat_of_raw metas vars = function
+  | RVar (_,id) ->
+      (try PRel (list_index (Name id) vars)
+       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) cl)
+  | RApp (_,c,cl) -> 
+      PApp (pat_of_raw metas vars c,
+	    Array.of_list (List.map (pat_of_raw metas vars) cl))
+  | RLambda (_,na,c1,c2) ->
+      PLambda (na, pat_of_raw metas vars c1,
+	       pat_of_raw metas (na::vars) c2)
+  | RProd (_,na,c1,c2) ->
+      PProd (na, pat_of_raw metas vars c1,
+	       pat_of_raw metas (na::vars) c2)
+  | RLetIn (_,na,c1,c2) ->
+      PLetIn (na, pat_of_raw metas vars c1,
+	       pat_of_raw metas (na::vars) c2)
+  | RSort (_,s) ->
+      PSort s
+  | RHole _ ->
+      PMeta None
+  | RCast (_,c,t) ->
+      Options.if_verbose
+        Pp.warning "Cast not taken into account in constr pattern";
+      pat_of_raw metas vars c
+  | ROrderedCase (_,st,po,c,br) ->
+      PCase (st,option_app (pat_of_raw metas vars) po,
+             pat_of_raw metas vars c,
+             Array.map (pat_of_raw metas vars) br)
+  | RCases (loc,po,[c],br) ->
+      PCase (Term.RegularStyle,option_app (pat_of_raw metas vars) po,
+             pat_of_raw metas vars c,
+             Array.init (List.length br)
+               (pat_of_raw_branch loc metas vars br))
+  | r ->
+      let loc = loc_of_rawconstr r in
+      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")
+
+and pat_of_raw_branch loc metas vars brs i =
+  let bri = List.filter
+    (function
+        (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
+      | (loc,_,_,_) ->
+          user_err_loc (loc,"pattern_of_rawconstr",
+                        Pp.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",
+                                Pp.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' br)
+    | _ -> user_err_loc (loc,"pattern_of_rawconstr",
+                         str "No unique branch for " ++ int (i+1) ++
+                         str"-th constructor")
+
+let pattern_of_rawconstr c =
+  let metas = ref [] in
+  let p = pat_of_raw metas [] c in
+  (!metas,p)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 4b8c0aa8dd..11821a6a8f 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -67,38 +67,11 @@ val head_of_constr_reference : Term.constr -> constr_label
 
 val pattern_of_constr : constr -> constr_pattern
 
+(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
+   a pattern; variables bound in [l] are replaced by the pattern to which they
+    are bound *)
 
-exception PatternMatchingFailure
+val pattern_of_rawconstr : Rawterm.rawconstr -> int list * constr_pattern
 
-(* [matches pat c] matches [c] against [pat] and returns the resulting
-   assignment of metavariables; it raises [PatternMatchingFailure] if
-   not matchable; bindings are given in increasing order based on the
-   numbers given in the pattern *)
-val matches      :
-  constr_pattern -> constr -> (int * constr) list
-
-(* [is_matching pat c] just tells if [c] matches against [pat] *)
-
-val is_matching      :
-  constr_pattern -> constr -> bool
-
-(* [matches_conv env sigma] matches up to conversion in environment
-   [(env,sigma)] when constants in pattern are concerned; it raises
-   [PatternMatchingFailure] if not matchable; bindings are given in
-   increasing order based on the numbers given in the pattern *)
-
-val matches_conv :
-  env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
-
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
-
-(* Tries to match a subterm of [c] with [pat] *)
-val sub_match :
-  int -> constr_pattern -> constr -> ((int * constr) list * constr)
-
-(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
-   up to conversion for constants in patterns *)
-
-val is_matching_conv :
-  env -> Evd.evar_map -> constr_pattern -> constr -> bool
+val instantiate_pattern :
+  (identifier * constr_pattern) list -> constr_pattern -> constr_pattern
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0075be7d82..0dcf901882 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -159,7 +159,6 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
-(*
 let rec subst_pat subst pat = 
   match pat with
   | PatVar _ -> pat
@@ -168,8 +167,7 @@ let rec subst_pat subst pat =
       and cpl' = list_smartmap (subst_pat subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
-*)	
-(*
+
 let rec subst_raw subst raw = 
   match raw with
   | RRef (loc,ref) -> 
@@ -244,7 +242,6 @@ let rec subst_raw subst raw =
 	  RCast (loc,r1',r2')
 
   | RDynamic _ -> raw
-*)
 
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
@@ -284,10 +281,8 @@ type ('a,'b) red_expr_gen =
   | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
-type 'a or_metanum = AN of 'a | MetaNum of int located
-
-type 'a may_eval =
+type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a
+  | ConstrEval of ('a, 'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 7ac8a15b7f..293667aed9 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -98,9 +98,7 @@ val map_rawconstr_with_binders_loc : loc ->
 
 val loc_of_rawconstr : rawconstr -> loc
 
-(*
 val subst_raw : Names.substitution -> rawconstr -> rawconstr
-*)
 
 type 'a raw_red_flag = {
   rBeta : bool;
@@ -123,10 +121,8 @@ type ('a,'b) red_expr_gen =
   | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
-type 'a or_metanum = AN of 'a | MetaNum of int located
-
-type 'a may_eval =
+type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a
+  | ConstrEval of ('a, 'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a