Improved the inference of the return predicate in dependent pattern-matching.

More precisely, the mecanism used to automatically infer return
predicates of the form

"as x in I y1..yn match y1..yn x with u1(z1)..un(zn) => P(z1..zn) | _ => ID end"

now computes the dependencies in the types of y1..yn and x. This
allows it to benefit of the generalisation mechanism of the
pattern-matching compilation algorithm ("Abstract") and to infer more
sophisticated return predicates (e.g. when working with "vector").

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

1 files changed, 19 insertions, 18 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 540db1c81..aa0f4843f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1299,20 +1299,13 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
     let (p,_,_) = lookup_rel_id x (rel_context extenv) in
-    let rec aux n (_,b,ty) =
-      match b with
-      | Some c ->
-	  assert (isRel c);
-	  let p = n + destRel c in aux p (lookup_rel p extenv)
-      | None ->
-	  (n,ty) in
-    let (p,ty) = aux p (lookup_rel p extenv) in
-    if noccur_between_without_evar 1 (n'-p-n+1) ty
-    then
-      let u = lift (n'-n) u in
-      (p,u,(expand_vars_in_term extenv u,lift p ty))
-    else
-      failwith "") subst in
+    let rec traverse_local_defs p =
+      match pi2 (lookup_rel p extenv) with
+      | Some c -> assert (isRel c); traverse_local_defs (p + destRel c)
+      | None -> p in
+    let p = traverse_local_defs p in
+    let u = lift (n'-n) u in
+    (p,u,expand_vars_in_term extenv u)) subst in
   let t0 = lift (n'-n) t in
   (subst0,t0)
 
@@ -1349,7 +1342,8 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
     else
     let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
     if good <> [] then
-      let (u,ty) = pi3 (List.hd good) in
+      let u = pi3 (List.hd good) in
+      let ty = aux x (get_type_of env sigma t) in
       let vl = List.map pi1 good in
       let inst =
 	list_map_i
@@ -1432,16 +1426,23 @@ let build_inversion_problem loc env sigma tms t =
      problem have to be abstracted *)
   let patl,sign,(subst,avoid) = aux 0 env [] tms ([],avoid0) in
   let n = List.length sign in
+
+  let decls = List.rev sign in
+  let dep_sign = find_dependencies_signature (list_make n true) decls in
+
   let (pb_env,_),sub_tms =
-    list_fold_map (fun (env,i) (na,b,t as d) ->
+    list_fold_map (fun (env,i) (deps,(na,b,t as d)) ->
       let typ =
 	if b<>None then NotInd(None,t) else
 	  try try_find_ind env sigma t None
 	  with Not_found -> NotInd (None,t) in
       let ty = lift_tomatch_type (n-i) typ in
-      let tm = Pushed ((mkRel (n-i),ty),[],(Anonymous,KnownNotDep)) in
+      let na_dep =
+	if deps = [] then (Anonymous,KnownNotDep) else (force_name na,KnownDep)
+      in
+      let tm = Pushed ((mkRel (n-i),ty),deps,na_dep) in
       ((push_rel d env,i+1),tm))
-      (env,0) (List.rev sign) in
+      (env,0) (List.combine dep_sign decls) in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
   (* [eqn1] is the first clause of the auxiliary pattern-matching that
      serves as skeleton for the return type: [patl] is the