Quelques modifications autour du filtrage Ltac:

- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
  où c'est le n-ième sous-termes qui finalement réussit (passage à une
  complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
  dans le type des let (puisque ce n'est pas cencé être une
  information utilisateur) mais rajout de la recherche dans le champ
  cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
  filtrées (dans matches/sub_match) et utilisation de ces noms dans
  ltac (utile pour récupérer x dans "exists x, P x");



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

2 files changed, 170 insertions, 141 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 5162113506..6b3b4e1751 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -44,15 +44,37 @@ open Pattern
 
  *)
 
+type bound_ident_map = (identifier * identifier) list
+
 exception PatternMatchingFailure
 
-let constrain (n,m) sigma =
-  if List.mem_assoc n sigma then
-    if eq_constr m (List.assoc n sigma) then sigma
+let constrain (n,m) (names,terms as subst) =
+  try
+    if eq_constr m (List.assoc n terms) then subst
     else raise PatternMatchingFailure
-  else 
-    (n,m)::sigma
-    
+  with
+      Not_found ->
+        if List.mem_assoc n names then
+          Flags.if_verbose Pp.warning
+              ("Collision between bound variable "^string_of_id n^
+                 " and a metavariable of same name.");
+        (names,(n,m)::terms)
+
+let add_binders na1 na2 (names,terms as subst) =
+  match na1, na2 with
+  | Name id1, Name id2 ->
+      if List.mem_assoc id1 names then
+        (Flags.if_verbose Pp.warning
+          ("Collision between bound variables of name"^string_of_id id1);
+         (names,terms))
+      else
+        (if List.mem_assoc id1 terms then
+            Flags.if_verbose Pp.warning
+              ("Collision between bound variable "^string_of_id id1^
+                  " and another bound variable of same name.");
+         ((id1,id2)::names,terms));
+  | _ -> subst
+
 let build_lambda toabstract stk (m : constr) = 
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
@@ -77,7 +99,10 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   | None -> cs1 = ci2.ci_cstr_nargs
 
 let matches_core convert allow_partial_app pat c = 
-  let rec sorec stk sigma p t =
+  let conv = match convert with
+    | None -> eq_constr
+    | Some (env,sigma) -> is_conv env sigma in
+  let rec sorec stk subst p t =
     let cT = strip_outer_cast t in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
@@ -89,7 +114,7 @@ let matches_core convert allow_partial_app pat c =
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
-	    constrain (n,build_lambda relargs stk cT) sigma
+	    constrain (n,build_lambda relargs stk cT) subst
 	  else
 	    raise PatternMatchingFailure
 
@@ -97,66 +122,63 @@ let matches_core convert allow_partial_app pat c =
 	  let depth = List.length stk in
           if depth = 0 then
             (* Optimisation *)
-            constrain (n,cT) sigma
+            constrain (n,cT) subst
           else
 	    let frels = Intset.elements (free_rels cT) in
             if List.for_all (fun i -> i > depth) frels then
-	      constrain (n,lift (-depth) cT) sigma
+	      constrain (n,lift (-depth) cT) subst
             else 
 	      raise PatternMatchingFailure
 
-      | PMeta None, m -> sigma
+      | PMeta None, m -> subst
 
-      | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma
+      | PRef (VarRef v1), Var v2 when v1 = v2 -> subst
 
-      | PVar v1, Var v2 when v1 = v2 -> sigma
+      | PVar v1, Var v2 when v1 = v2 -> subst
 
-      | PRef ref, _ when constr_of_global ref = cT -> sigma
+      | PRef ref, _ when conv (constr_of_global ref) cT -> subst
 
-      | PRel n1, Rel n2 when n1 = n2 -> sigma
+      | PRel n1, Rel n2 when n1 = n2 -> subst
 
-      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma
+      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst
 
-      | PSort (RType _), Sort (Type _) -> sigma
+      | PSort (RType _), Sort (Type _) -> subst
 
-      | PApp (p, [||]), _ -> sorec stk sigma p t
+      | PApp (p, [||]), _ -> sorec stk subst p t
 
       | PApp (PApp (h, a1), a2), _ ->
-          sorec stk sigma (PApp(h,Array.append a1 a2)) t
+          sorec stk subst (PApp(h,Array.append a1 a2)) t
 
       | 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 subst =
 	      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
+	        constrain (n,lift (-depth) c) subst
               else
 	        raise PatternMatchingFailure in
-            array_fold_left2 (sorec stk) sigma args1 args22
+            array_fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
       | PApp (c1,arg1), App (c2,arg2) ->
-        (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
+        (try array_fold_left2 (sorec stk) (sorec stk subst 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
+	  sorec ((na2,c2)::stk)
+            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
+	  sorec ((na2,c2)::stk)
+            (add_binders na1 na2 (sorec stk subst 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) = Option.get convert in
-	  let c = constr_of_global ref in
-	  if is_conv env evars c cT then sigma
-	  else raise PatternMatchingFailure
+	  sorec ((na2,t2)::stk)
+            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
 	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in
@@ -167,140 +189,129 @@ let matches_core convert allow_partial_app pat c =
 	    let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
 	    let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
-  	    sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
+  	    sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
 
       | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
 	  if same_case_structure ci1 ci2 br1 br2 then
   	    array_fold_left2 (sorec stk) 
-	      (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+	      (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2
           else
             raise PatternMatchingFailure
 
-      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
-      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
+      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
+      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
       | _ -> raise PatternMatchingFailure
 
-  in 
-  Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
+  in
+  let names,terms = sorec [] ([],[]) pat c in
+  (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
 
-let matches = matches_core None false
+let extended_matches = matches_core None false
 
-let pmatches = matches_core None true
+let matches c p = snd (matches_core None false c p)
 
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
+let pmatches c p = snd (matches_core None true c p)
+
+let special_meta = (-1)
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ nocc mres =
-  if not (List.for_all (fun (_,c) -> closed0 c) (fst mres)) then
+let authorized_occ sigma mk_ctx next =
+  if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then
     raise PatternMatchingFailure;
-  if nocc = 0 then mres
-  else raise (NextOccurrence nocc)
-
-let special_meta = (-1)
+  sigma, mk_ctx (mkMeta special_meta), next
 
 (* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match ?(partial_app=false) nocc pat c =
+let rec sub_match ?(partial_app=false) pat c =
+  let rec aux c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,mkCast (List.hd lc, k,c2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,mkCast (List.hd lc, k,c2)))
- | Lambda (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+      let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
+      try_aux [c1] mk_ctx next)
+  | Lambda (x,c1,c2) ->
+    (try authorized_occ (extended_matches pat c) mk_ctx next 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)))
+      let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+      try_aux [c1;c2] mk_ctx next)
   | Prod (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next 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 special_meta) with
+      let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+      try_aux [c1;c2] mk_ctx next)
+  | LetIn (x,c1,t1,c2) ->
+    (try authorized_occ (extended_matches pat c) mk_ctx next 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)))
+      let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t1,c2) | _ -> assert false
+      in try_aux [c1;c2] mk_ctx next)
   | App (c1,lc) ->
-      let rec aux nocc app args =
-	match args with
-	| [] -> 
-	    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)))
-	| arg :: args ->
-	    let app = mkApp (app, [|arg|]) in
-	      try let (lm,ce) = sub_match nocc pat app in
-		    (lm,mkApp (ce, Array.of_list args))
-	      with NextOccurrence nocc ->
-		aux nocc app args
-      in
-	(try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
-	| PatternMatchingFailure ->
-	    if partial_app then
-	      aux nocc c1 (Array.to_list lc)
-	    else
-	      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 ->
-	    if partial_app then
-	      aux nocc c1 (Array.to_list lc)
-	    else
-	      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))))
+      (try authorized_occ (extended_matches pat c) mk_ctx next with
+      | PatternMatchingFailure ->
+          let topdown = true in
+	  if partial_app then
+            if topdown then
+              let lc1 = Array.sub lc 0 (Array.length lc - 1) in
+              let app = mkApp (c1,lc1) in
+              let mk_ctx = function 
+                | [app';c] -> mk_ctx (mkApp (app',[|c|]))
+                | _ -> assert false in
+	      try_aux [app;array_last lc] mk_ctx next
+            else
+              let rec aux2 app args next =
+                match args with
+                | [] ->
+                  let mk_ctx le =
+                    mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+	          try_aux (c1::Array.to_list lc) mk_ctx next
+	        | arg :: args ->
+                  let app = mkApp (app,[|arg|]) in
+                  let next () = aux2 app args next in
+                  let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
+                  aux app mk_ctx next in
+              aux2 c1 (Array.to_list lc) next
+          else
+            let mk_ctx le =
+              mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+	    try_aux (c1::Array.to_list lc) mk_ctx next)
   | Case (ci,hd,c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next 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))))
+      let mk_ctx le = 
+        mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in
+      try_aux (c1::Array.to_list lc) mk_ctx next)
   | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
   | Rel _|Meta _|Var _|Sort _ ->
-    (try authorized_occ nocc ((matches pat c),mkMeta special_meta) 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 match_subterm nocc pat c =
-  try sub_match nocc pat c
-  with NextOccurrence _ -> raise PatternMatchingFailure
-
-let match_appsubterm nocc pat c =
-  try sub_match ~partial_app:true nocc pat c
-  with NextOccurrence _ -> raise PatternMatchingFailure
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
+    | PatternMatchingFailure -> next ())
+
+  (* Tries [sub_match] for all terms in the list *)
+  and try_aux lc mk_ctx next =
+    let rec try_sub_match_rec lacc = function
+      | [] -> next ()
+      | c::tl ->
+          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
+          let next () = try_sub_match_rec (c::lacc) tl in
+          aux c mk_ctx next in
+    try_sub_match_rec [] lc in
+  aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
+
+type subterm_matching_result =
+    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
+let match_subterm pat c = sub_match pat c
+
+let match_appsubterm pat c = sub_match ~partial_app:true pat c
+
+let match_subterm_gen app pat c = sub_match ~partial_app:app pat c
 
 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 matches_conv env sigma c p =
+  snd (matches_core (Some (env,sigma)) false c p)
 
 let is_matching_conv env sigma pat n =
   try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 42f9eab122..574a4bbd23 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -22,36 +22,54 @@ exception PatternMatchingFailure
 
 val special_meta : metavariable
 
+type bound_ident_map = (identifier * identifier) list
+
 (* [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 -> patvar_map
 
-(* [is_matching pat c] just tells if [c] matches against [pat] *)
+(* [extended_matches pat c] also returns the names of bound variables
+   in [c] that matches the bound variables in [pat]; if several bound
+   variables or metavariables have the same name, the metavariable,
+   or else the rightmost bound variable, takes precedence *)
+val extended_matches : 
+  constr_pattern -> constr -> bound_ident_map * patvar_map
 
+(* [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 -> patvar_map
 
+(* The type of subterm matching results: a substitution + a context
+   (whose hole is denoted with [special_meta]) + a continuation that
+   either returns the next matching subterm or raise PatternMatchingFailure *)
+type subterm_matching_result =
+    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
 (* [match_subterm n pat c] returns the substitution and the context
-   corresponding to the [n+1]th **closed** subterm of [c] matching [pat];
-   It raises PatternMatchingFailure if no such matching exists *)
-val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
+   corresponding to the first **closed** subterm of [c] matching [pat], and
+   a continuation that looks for the next matching subterm.
+   It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_subterm : constr_pattern -> constr -> subterm_matching_result
+
+(* [match_appsubterm pat c] returns the substitution and the context
+   corresponding to the first **closed** subterm of [c] matching [pat], 
+   considering application contexts as well. It also returns a
+   continuation that looks for the next matching subterm.
+   It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
 
-(* [match_appsubterm n pat c] returns the substitution and the context
-   corresponding to the [n+1]th **closed** subterm of [c] matching [pat], 
-   considering application contexts as well;
-   It raises PatternMatchingFailure if no such matching exists *)
-val match_appsubterm : int -> constr_pattern -> constr -> patvar_map * constr
+(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
+val match_subterm_gen : bool (* true = with app context *) -> 
+   constr_pattern -> constr -> subterm_matching_result
 
 (* [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