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, 44 insertions, 4 deletions

diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index d805730e97..3b61c1e437 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,6 +6,9 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This module defines the type of pattern used for pattern-matching
+    terms in tatics *)
+
 open Pp
 open Names
 open Sign
@@ -16,12 +19,46 @@ open Nametab
 open Rawterm
 open Mod_subst
 
-(** Pattern variables *)
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+    of a matching. Matching can return terms defined in a some context
+    of named binders; in the context, variable names are ordered by
+    (<) and referred to by index in the term Thanks to the canonical
+    ordering, a matching problem like
+
+    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+    will be accepted. Thanks to the reference by index, a matching
+    problem like
+
+    [match ... with [(fun x => ?p)] => [forall x => p]]
+
+    will work even if [x] is also the name of an existing goal
+    variable.
+
+    Note: we do not keep types in the signature. Besides simplicity,
+    the main reason is that it would force to close the signature over
+    binders that occur only in the types of effective binders but not
+    in the term itself (e.g. for a term [f x] with [f:A -> True] and
+    [x:A]).
+
+    On the opposite side, by not keeping the types, we loose
+    opportunity to propagate type informations which otherwise would
+    not be inferable, as e.g. when matching [forall x, x = 0] with
+    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+    expression [forall x, h = x] where nothing tells how the type of x
+    could be inferred. We also loose the ability of typing ltac
+    variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = identifier list * constr
+
+(** Types of substitutions with or w/o bound variables *)
 
 type patvar_map = (patvar * constr) list
-val pr_patvar : patvar -> std_ppcmds
+type extended_patvar_map = (patvar * constr_under_binders) list
 
-(** Patterns *)
+(** {5 Patterns} *)
 
 type constr_pattern =
   | PRef of global_reference
@@ -41,6 +78,8 @@ type constr_pattern =
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
+(** {5 Functions on patterns} *)
+
 val occur_meta_pattern : constr_pattern -> bool
 
 val subst_pattern : substitution -> constr_pattern -> constr_pattern
@@ -72,6 +111,7 @@ val pattern_of_rawconstr : rawconstr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern
+  (identifier * (identifier list * constr)) list ->
+  constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern