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

6 files changed, 197 insertions, 70 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 2c0285ed24..ddfe5dd076 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -46,9 +46,10 @@ type bound_ident_map = (identifier * identifier) list
 
 exception PatternMatchingFailure
 
-let constrain (n,m) (names,terms as subst) =
+let constrain (n,(ids,m as x)) (names,terms as subst) =
   try
-    if eq_constr m (List.assoc n terms) then subst
+    let (ids',m') = List.assoc n terms in
+    if ids = ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with
       Not_found ->
@@ -56,7 +57,7 @@ let constrain (n,m) (names,terms as subst) =
           Flags.if_verbose Pp.warning
               ("Collision between bound variable "^string_of_id n^
                  " and a metavariable of same name.");
-        (names,(n,m)::terms)
+        (names,(n,x)::terms)
 
 let add_binders na1 na2 (names,terms as subst) =
   match na1, na2 with
@@ -76,7 +77,7 @@ let add_binders na1 na2 (names,terms as subst) =
 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) ->
+    | (n, (_,na,t)::tl) ->
 	if List.mem n toabstract then
           buildrec (mkLambda (na,t,m)) (n+1) tl
         else
@@ -96,7 +97,58 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   | Some ind -> ind = ci2.ci_ind
   | None -> cs1 = ci2.ci_cstr_ndecls
 
-let matches_core convert allow_partial_app pat c =
+let rec list_insert f a = function
+  | [] -> [a]
+  | b::l when f a b -> a::b::l
+  | b::l when a = b -> raise PatternMatchingFailure
+  | b::l -> b :: list_insert f a l
+
+let extract_bound_vars =
+  let rec aux k = function
+  | ([],_) -> []
+  | (n::l,(na1,na2,_)::stk) when k = n ->
+      begin match na1,na2 with
+      | Name id1,Name _ -> list_insert (<) id1 (aux (k+1) (l,stk))
+      | Name _,Anonymous -> anomaly "Unnamed bound variable"
+      | Anonymous,_ -> raise PatternMatchingFailure
+      end
+  | (l,_::stk) -> aux (k+1) (l,stk)
+  | (_,[]) -> assert false
+  in aux 1
+
+let dummy_constr = mkProp
+
+let rec make_renaming ids = function
+  | (Name id,Name _,_)::stk ->
+      let renaming = make_renaming ids stk in
+      (try mkRel (list_index id ids) :: renaming
+       with Not_found -> dummy_constr :: renaming)
+  | (_,_,_)::stk ->
+      dummy_constr :: make_renaming ids stk
+  | [] ->
+      []
+
+let merge_binding allow_bound_rels stk n cT subst =
+  let depth = List.length stk in
+  let c =
+    if depth = 0 then
+      (* Optimization *)
+      ([],cT)
+    else
+      let frels = Intset.elements (free_rels cT) in
+      let frels = List.filter (fun i -> i <= depth) frels in
+      if allow_bound_rels then
+	let frels = Sort.list (<) frels in
+	let canonically_ordered_vars = extract_bound_vars (frels,stk) in
+	let renaming = make_renaming canonically_ordered_vars stk in
+	(canonically_ordered_vars, substl renaming cT)
+      else if frels = [] then
+	([],lift (-depth) cT)
+      else
+	raise PatternMatchingFailure in
+  constrain (n,c) subst
+
+let matches_core convert allow_partial_app allow_bound_rels pat c =
   let conv = match convert with
     | None -> eq_constr
     | Some (env,sigma) -> is_conv env sigma in
@@ -112,21 +164,11 @@ 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) subst
+	    constrain (n,([],build_lambda relargs stk cT)) subst
 	  else
 	    raise PatternMatchingFailure
 
-      | PMeta (Some n), m ->
-	  let depth = List.length stk in
-          if depth = 0 then
-            (* Optimisation *)
-            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) subst
-            else
-	      raise PatternMatchingFailure
+      | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
 
       | PMeta None, m -> subst
 
@@ -151,14 +193,8 @@ let matches_core convert allow_partial_app pat c =
           let p = Array.length args2 - Array.length args1 in
           if p>=0 then
             let args21, args22 = array_chop p args2 in
-            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) subst
-              else
-	        raise PatternMatchingFailure in
+	    let c = mkApp(c2,args21) in
+            let subst = merge_binding allow_bound_rels stk n c subst in
             array_fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
@@ -167,15 +203,15 @@ let matches_core convert allow_partial_app pat c =
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk)
+	  sorec ((na1,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 ((na1,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 ((na1,na2,t2)::stk)
             (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -184,8 +220,10 @@ let matches_core convert allow_partial_app pat c =
 	  let n = rel_context_length ctx in
           let n' = rel_context_length ctx' in
 	  if noccur_between 1 n b2 & noccur_between 1 n' b2' then
-	    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 s =
+	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
+	    let s' =
+	      List.fold_left (fun l (na,_,t) -> (Anonymous,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 subst a1 a2) b1 b2) b1' b2'
           else
@@ -206,16 +244,20 @@ let matches_core convert allow_partial_app pat c =
   let names,terms = sorec [] ([],[]) pat c in
   (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
 
-let extended_matches = matches_core None true
+let matches_core_closed convert allow_partial_app pat c =
+  let names,subst = matches_core convert allow_partial_app false pat c in
+  (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+
+let extended_matches = matches_core None true true
 
-let matches c p = snd (matches_core None true c p)
+let matches c p = snd (matches_core_closed None true c p)
 
 let special_meta = (-1)
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
-    let sigma = matches_core None partial_app pat c in
+    let sigma = matches_core_closed None partial_app pat c in
     if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
     then next ()
     else sigma, mk_ctx (mkMeta special_meta), next
@@ -308,7 +350,7 @@ let is_matching_appsubterm ?(closed=true) pat c =
   with PatternMatchingFailure -> false
 
 let matches_conv env sigma c p =
-  snd (matches_core (Some (env,sigma)) false c p)
+  snd (matches_core_closed (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 95314054e5..eb9c8fc8c6 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,18 +6,25 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This module implements pattern-matching on terms *)
+
 open Names
 open Term
 open Environ
 open Pattern
 open Termops
 
-(** {6 This modules implements pattern-matching on terms } *)
-
+(** [PatternMatchingFailure] is the exception raised when pattern
+  matching fails *)
 exception PatternMatchingFailure
 
+(** [special_meta] is the default name of the meta holding the
+   surrounding context in subterm matching *)
 val special_meta : metavariable
 
+(** [bound_ident_map] represents the result of matching binding
+   identifiers of the pattern with the binding identifiers of the term
+   matched *)
 type bound_ident_map = (identifier * identifier) list
 
 (** [matches pat c] matches [c] against [pat] and returns the resulting
@@ -31,7 +38,7 @@ val matches : constr_pattern -> constr -> patvar_map
    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
+  constr_pattern -> constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : constr_pattern -> constr -> bool
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 48218f47f2..59f3cde88a 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
 
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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 71a21f6c88..e63b9a234f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,8 +45,10 @@ open Evarconv
 open Pattern
 
 type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -131,7 +133,7 @@ sig
   *)
 
   val understand_ltac :
-    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -162,18 +164,15 @@ sig
    *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+    ltac_var_map -> rawconstr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_type_judgment
+    ltac_var_map -> rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    var_map * (identifier * identifier option) list ->
-    typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> rawconstr -> constr
 
     (*i*)
 end
@@ -225,7 +224,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let check_branches_message loc env evdref c (explft,lft) =
     for i = 0 to Array.length explft - 1 do
       if not (e_cumul env evdref lft.(i) explft.(i)) then
-	let sigma =  !evdref in
+	let sigma = !evdref in
 	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
     done
 
@@ -243,7 +242,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | Anonymous -> name'
     | _ -> name
 
-  let pretype_id loc env (lvar,unbndltacvars) id =
+  let invert_ltac_bound_name env id0 id =
+    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    with Not_found ->
+      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+	str " depends on pattern variable name " ++ pr_id id ++
+	str " which is not bound in current context.")
+
+  let pretype_id loc env sigma (lvar,unbndltacvars) id =
     (* Look for the binder of [id] *)
     try
       let (n,_,typ) = lookup_rel_id id (rel_context env) in
@@ -251,7 +257,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     with Not_found ->
     (* Check if [id] is an ltac variable *)
     try
-      List.assoc id lvar
+      let (ids,c) = List.assoc id lvar in
+      let subst = List.map (invert_ltac_bound_name env id) ids in
+      let c = substl subst c in
+      { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
     with Not_found ->
     (* Check if [id] is a section or goal variable *)
     try
@@ -295,7 +304,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
     | RVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_id loc env lvar id)
+	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
     | REvar (loc, evk, instopt) ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18a6b03a71..00eb613abc 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,6 +6,12 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This file implements type inference. It maps [rawconstr]
+   (i.e. untyped terms whose names are located) to [constr]. In
+   particular, it drives complex pattern-matching problems ("match")
+   into elementary ones, insertion of coercions and resolution of
+   implicit arguments. *)
+
 open Names
 open Sign
 open Term
@@ -21,8 +27,10 @@ val search_guard :
 
 type typing_constraint = OfType of types option | IsType
 
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
 
 module type S =
 sig
@@ -56,7 +64,7 @@ sig
   *)
 
   val understand_ltac :
-    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (** Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -84,18 +92,15 @@ sig
   (** Internal of Pretyping... *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+    ltac_var_map -> rawconstr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_type_judgment
+    ltac_var_map -> rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    var_map * (identifier * identifier option) list ->
-    typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> rawconstr -> constr
 
   (**/**)