Discarding let-ins from the instances of the evars in the

pattern-unification test. They were tolerated up to r14539.  Also
expanded the let-ins not bound to rel or var in the right-hand side of
a term for which pattern-unification is tested (this expansion can
refer to a non-let variable that has to be taken into account in the
pattern-unification test).

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

5 files changed, 84 insertions, 31 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ec581eaf1..91b0eacc4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -228,7 +228,7 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-          match is_unification_pattern_evar env ev1 l1 (applist appr2) with
+          match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with
           | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
@@ -261,7 +261,7 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-	  match is_unification_pattern_evar env ev2 l2 (applist appr1) with
+	  match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with
           | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
@@ -361,7 +361,7 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, (Rigid _ | PseudoRigid _) ->
-	(match is_unification_pattern_evar env ev1 l1 (applist appr2) with
+	(match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with
         | Some l1 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
@@ -375,7 +375,7 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
 	  true)
 
     | (Rigid _ | PseudoRigid _), Flexible ev2 ->
-	(match is_unification_pattern_evar env ev2 l2 (applist appr1) with
+	(match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with
         | Some l2 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fd07680b5..57a6426ab 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -171,7 +171,8 @@ let compute_var_aliases sign =
             let aliases_of_id =
               try Idmap.find id' aliases with Not_found -> [] in
             Idmap.add id (aliases_of_id@[t]) aliases
-	| _ -> aliases)
+	| _ ->
+            Idmap.add id [t] aliases)
     | None -> aliases)
     sign Idmap.empty
 
@@ -190,7 +191,7 @@ let compute_rel_aliases var_aliases rels =
                try Intmap.find (p+n) aliases with Not_found -> [] in
              Intmap.add n (aliases_of_n@[mkRel (p+n)]) aliases
          | _ ->
-           aliases)
+             Intmap.add n [lift n t] aliases)
      | None -> aliases))
          rels (List.length rels,Intmap.empty))
 
@@ -208,7 +209,9 @@ let get_alias_chain_of aliases x = match kind_of_term x with
 let normalize_alias_opt aliases x =
   match get_alias_chain_of aliases x with
   | []  -> None
-  | a::_ -> Some a
+  | a::_ when isRel a or isVar a -> Some a
+  | [_] -> None
+  | _::a::_ -> Some a
 
 let normalize_alias aliases x =
   match normalize_alias_opt aliases x with
@@ -235,12 +238,20 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
               try Intmap.find (p+1) rel_aliases with Not_found -> [] in
 	    Intmap.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
         | _ ->
-          rel_aliases)
+            Intmap.add 1 [lift 1 t] rel_aliases)
     | None -> rel_aliases in
   (var_aliases, rel_aliases)
 
 let rec expansions_of_var aliases x =
-  x :: List.rev (get_alias_chain_of aliases x)
+  match get_alias_chain_of aliases x with
+  | [] -> [x]
+  | a::_ as l when isRel a || isVar a -> x :: List.rev l
+  | _::l -> x :: List.rev l
+
+let expansion_of_var aliases x =
+  match get_alias_chain_of aliases x with
+  | [] -> x
+  | a::_ -> a
 
 let rec expand_vars_in_term_using aliases t = match kind_of_term t with
   | Rel _ | Var _ ->
@@ -255,7 +266,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
   let rec frec (aliases,depth) c = match kind_of_term c with
     | Rel _ | Var _ ->
-      let c = normalize_alias aliases c in
+      let c = expansion_of_var aliases c in
         (match kind_of_term c with
         | Var id -> acc2 := Idset.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
@@ -402,17 +413,6 @@ let generalize_evar_over_rels sigma (ev,args) =
  * operations on the evar constraints *
  *------------------------------------*)
 
-(* Pb: defined Rels and Vars should not be considered as a pattern... *)
-(*
-let is_pattern inst =
-  let rec is_hopat l = function
-      [] -> true
-    | t :: tl ->
-        (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in
-  is_hopat [] (Array.to_list inst)
-*)
-
-
 exception IllTypedFilter
 
 let check_restricted_occur evd refine env filter constr =
@@ -1333,6 +1333,15 @@ let get_actual_deps aliases l t =
       | Rel n -> Intset.mem n fv_rels
       | _ -> assert false) l
 
+let remove_instance_local_defs evd evk args =
+  let evi = Evd.find evd evk in
+  let rec aux = function
+  | (_,Some _,_)::sign, a::args -> aux (sign,args)
+  | (_,None,_)::sign, a::args -> a::aux (sign,args)
+  | [], [] -> []
+  | _ -> assert false in
+  aux (evar_filtered_context evi, args)
+
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
 let find_unification_pattern_args env l t =
@@ -1354,19 +1363,20 @@ let is_unification_pattern_meta env nb m l t =
   else
     None
 
-let is_unification_pattern_evar env (evk,args) l t =
+let is_unification_pattern_evar env evd (evk,args) l t =
   if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
-    let n = Array.length args in
-    match find_unification_pattern_args env (Array.to_list args @ l) t with
+    let args = remove_instance_local_defs evd evk (Array.to_list args) in
+    let n = List.length args in
+    match find_unification_pattern_args env (args @ l) t with
     | Some l when not (occur_evar evk t) -> Some (list_skipn n l)
     | _ -> None
   else
     None
 
-let is_unification_pattern (env,nb) f l t =
+let is_unification_pattern (env,nb) evd f l t =
   match kind_of_term f with
   | Meta m -> is_unification_pattern_meta env nb m l t
-  | Evar ev -> is_unification_pattern_evar env ev l t
+  | Evar ev -> is_unification_pattern_evar env evd ev l t
   | _ -> None
 
 (* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
@@ -1383,7 +1393,7 @@ let solve_pattern_eqn env l c =
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let d = map_rel_declaration (lift n) (lookup_rel n env) in
-          mkLambda_or_LetIn  d c'
+          mkLambda_or_LetIn d c'
       | Var id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
       | _ -> assert false)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 36e64c9ad..78898aaa7 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -96,10 +96,10 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
 
-val is_unification_pattern_evar : env -> existential -> constr list ->
+val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> constr list option
 
-val is_unification_pattern : env * int -> constr -> constr list ->
+val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
   constr -> constr list option
 
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 187533ad3..78f62a5ab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -443,13 +443,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| App (f1,l1), _ when
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
              || use_evars_pattern_unification flags && isAllowedEvar flags f1) &
-	    store whenmem (is_unification_pattern curenvnb f1 (Array.to_list l1) cN) ->
+	    store whenmem (is_unification_pattern curenvnb sigma f1 (Array.to_list l1) cN) ->
 	      solve_pattern_eqn_array curenvnb f1 (restore whenmem) cN substn
 
 	| _, App (f2,l2) when
 	    (isMeta f2 && use_metas_pattern_unification flags nb l2
              || use_evars_pattern_unification flags && isAllowedEvar flags f2) &
-	    store whenmem (is_unification_pattern curenvnb f2 (Array.to_list l2) cM) ->
+	    store whenmem (is_unification_pattern curenvnb sigma f2 (Array.to_list l2) cM) ->
 	      solve_pattern_eqn_array curenvnb f2 (restore whenmem) cM substn
 
 	| App (f1,l1), App (f2,l2) ->
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ba8da1a4f..2f1ec7571 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -266,3 +266,46 @@ Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
 intros.
 refine ((fun H => conj (proj1 H) (proj2 H)) _).
 Abort.
+
+(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *)
+(* r14753 after the restrictions made on detecting Miller's pattern in the *)
+(* presence of alias, only the second-order unification procedure was *)
+(* able to solve this problem but it was deactivated for 8.4 in r14219 *)
+
+Definition k0
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) o :=
+ match o with (* note: match introduces an alias! *)
+ | Some a => e _ (j a)
+ | None => O
+ end.
+
+Definition k1
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a).
+
+Definition k2
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* Other examples about aliases involved in pattern unification *)
+
+Definition k3
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b).
+
+Definition k4
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b).
+
+Definition k5
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b).
+
+Definition k6
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b).
+
+Definition k7
+  (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).