Added support for Ltac-matching terms with variables bound in the pattern

- Instances found by matching.ml now collect the set of bound
  variables they possibly depend on in the pattern (see type
  Pattern.extended_patvar_map); the variables names are canonically
  ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
  tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
  is that we may have to re-type several times the same term but it is
  necessary for considering terms with locally bound variables of which
  we do not keep the type (and if even we had kept the type, we would have
  to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
  and I hope I did not break some intended existing behavior.

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

1 files changed, 33 insertions, 9 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 48218f47f..59f3cde88 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -19,8 +19,10 @@ open Mod_subst
 
 (* Metavariables *)
 
+type constr_under_binders = identifier list * constr
+
 type patvar_map = (patvar * constr) list
-let pr_patvar = pr_id
+type extended_patvar_map = (patvar * constr_under_binders) list
 
 (* Patterns *)
 
@@ -143,9 +145,9 @@ let pattern_of_constr sigma t =
 let map_pattern_with_binders g f l = function
   | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
   | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
-  | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
-  | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
-  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+  | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
+  | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
+  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
   (* Non recursive *)
@@ -153,18 +155,40 @@ let map_pattern_with_binders g f l = function
   (* Bound to terms *)
   | PFix _ | PCoFix _ as x) -> x
 
-let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
+
+let error_instantiate_pattern id l =
+  let is = if List.length l = 1 then "is" else "are" in
+  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+    ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+    ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
-let rec instantiate_pattern lvar = function
-  | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
+let instantiate_pattern lvar c =
+  let rec aux vars = function
+  | PVar id as x ->
+      (try
+	let ctx,c = List.assoc id lvar in
+	try
+	  let inst =
+	    List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+	  let c = substl inst c in
+	  snd (pattern_of_constr Evd.empty c)
+	with Not_found (* list_index failed *) ->
+	  let vars =
+	    list_map_filter (function Name id -> Some id | _ -> None) vars in
+	  error_instantiate_pattern id (list_subtract ctx vars)
+       with Not_found (* List.assoc failed *) ->
+	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
-  | c -> map_pattern (instantiate_pattern lvar) c
+  | c ->
+      map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
+  aux [] c
 
 let rec liftn_pattern k n = function
   | PRel i as x -> if i >= n then PRel (i+k) else x
   | PFix x -> PFix (destFix (liftn k n (mkFix x)))
   | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
-  | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+  | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
 
 let lift_pattern k = liftn_pattern k 1