New strategy to infer return predicate of match construct when

external type has evars. We now create a new ad hoc evar instead of
having evars as arguments of evars and use filters to resolved them as
was done since about r10124. In particular, this completes the
resolution of bug 2615.

Evar filters for occurrences might be obsolete as a consequence of
this commit.

Also, abstract_tycon, evar_define, second_order_matching which all
implement some form of second_order_matching should eventually be
merged (abstract_tycon looks for subterms up to delta while
second_order_matching currently looks for syntactic equal subterms,
evar_define doesn't consider the possible dependencies in
non-variables-nor-constructors subterms but has a better handling of
aliases, ...).

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

4 files changed, 56 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b104db0267..6559084578 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1298,6 +1298,10 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
 let push_binder d (k,env,subst) =
   (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
 
+let rec list_assoc_in_triple x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
+
 (* Let vijk and ti be a set of dependent terms and T a type, all
  * defined in some environment env. The vijk and ti are supposed to be
  * instances for variables aijk and bi.
@@ -1323,20 +1327,33 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
      by an evar that may depend (and only depend) on the corresponding
      convertible subterms of the substitution *)
   let rec aux (k,env,subst as x) t =
-    if isRel t && pi2 (lookup_rel (destRel t) env) <> None then
-      map_constr_with_full_binders push_binder aux x t
-    else
+    let t = whd_evar !evdref t in match kind_of_term t with
+    | Rel n when pi2 (lookup_rel n env) <> None ->
+        map_constr_with_full_binders push_binder aux x t
+    | Evar ev ->
+        let ty = get_type_of env sigma t in
+        let inst =
+	  list_map_i
+	    (fun i _ ->
+              try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
+              1 (rel_context env) in
+        let ev = e_new_evar evdref env ~src:(loc, CasesType) ty in
+        evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref;
+        ev
+    | _ ->
     let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
     if good <> [] then
-      let u = pi3 (List.hd good) in
-      let ty = aux x (get_type_of env sigma t) in
+      let u = pi3 (List.hd good) in (* u is in extenv *)
       let vl = List.map pi1 good in
+      let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
+      let depvl = free_rels ty in
       let inst =
 	list_map_i
 	  (fun i _ -> if List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
-	List.map (fun a -> not (isRel a) or dependent a u) inst in
+	List.map (fun a -> not (isRel a) || dependent a u
+                           || Intset.mem (destRel a) depvl) inst in
       let named_filter =
 	List.map (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
@@ -1350,17 +1367,22 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
   aux (0,extenv,subst0) t0
 
 let build_tycon loc env tycon_env subst tycon extenv evdref t =
-  let t = match t with
+  let t,tt = match t with
     | None ->
 	(* This is the situation we are building a return predicate and
            we are in an impossible branch *)
 	let n = rel_context_length (rel_context env) in
 	let n' = rel_context_length (rel_context tycon_env) in
+        let tt = new_Type () in
 	let impossible_case_type =
-	  e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in
-	lift (n'-n) impossible_case_type
-    | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in
-  get_judgment_of extenv !evdref t
+	  e_new_evar evdref env ~src:(loc,ImpossibleCase) tt in
+	(lift (n'-n) impossible_case_type, tt)
+    | Some t ->
+        let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
+        let evd,tt = Typing.e_type_of extenv !evdref t in
+        evdref := evd;
+        (t,tt) in
+  { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 993cb3a850..7683778938 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -464,11 +464,8 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in
  * substitution u1..uq.
  *)
 
-let materialize_evar define_fun env evd k (evk1,args1) ty =
-  let evi1 = Evd.find_undefined evd evk1 in
+let materialize_evar_from_sign define_fun env evd k sign1 filter1 args1 ty =
   let env1,rel_sign = env_rel_context_chop k env in
-  let sign1 = evar_hyps evi1 in
-  let filter1 = evar_filter evi1 in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
   let inst_in_sign =
     List.map mkVar (snd (list_filter2 (fun b id -> b) (filter1,ids1))) in
@@ -487,7 +484,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty =
           (sign,filter,inst_in_env,inst_in_sign,
            push_rel d env,evd,avoid))
       rel_sign
-      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
+      (sign1,filter1,args1,inst_in_sign,env1,evd,ids1)
   in
   let evd,ev2ty_in_sign =
     define_evar_from_virtual_equation define_fun env evd ty
@@ -497,6 +494,11 @@ let materialize_evar define_fun env evd k (evk1,args1) ty =
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
+let materialize_evar define_fun env evd k (evk1,args1) ty =
+  let evi1 = Evd.find_undefined evd evk1 in
+  materialize_evar_from_sign define_fun env evd k
+    (evar_hyps evi1) (evar_filter evi1) (Array.to_list args1) ty
+
 let subfilter env ccl filter newfilter args =
   let vars = collect_vars ccl in
   let (filter, _, _, newargs) =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3652768531..54fc072659 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -62,6 +62,16 @@ type conv_fun =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   existential -> constr -> evar_map
 
+val materialize_evar_from_sign :
+  (env -> evar_map -> existential -> constr -> evar_map) ->
+  env -> evar_map -> int ->
+  named_context_val -> bool list -> constr list -> types ->
+  evar_map * constr * existential
+
+val solve_evar_evar :
+  (env -> evar_map -> existential -> constr -> evar_map) ->
+  env -> evar_map -> existential -> existential -> evar_map
+
 (** {6 Evars/Metas switching...} *)
 
 (** [evars_to_metas] generates new metavariables for each non dependent
diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v
index 005491637d..54e1a07cc8 100644
--- a/test-suite/bugs/closed/shouldsucceed/2615.v
+++ b/test-suite/bugs/closed/shouldsucceed/2615.v
@@ -6,3 +6,9 @@ Inductive foo : forall A, A -> Prop :=
 Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
 Fail induction 1.
 
+(* Whether these examples should succeed with a non-dependent return predicate 
+   or fail because there is well-typed return predicate dependent in f 
+   is questionable. As of 25 oct 2011, they succeed *)
+refine (fun p => match p with _ => _ end).
+Undo.
+refine (fun p => match p with foo_intro _ _ => _ end).