Fixing postprocessing bugs in pattern-matching compilation.

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

2 files changed, 51 insertions, 9 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 119167cadf..453e8ecaca 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1002,23 +1002,43 @@ let mkSpecialLetIn orig (na,b,t) isdeppred c =
 (* Remove commutative cuts that turn out to be non-dependent after
    some evars have been instantiated *)
 
-let ungeneralize_branch n (sign,body) cs =
+let rec ungeneralize n ng body =
   match kind_of_term body with
-  | Lambda (_,_,c) | LetIn (_,_,_,c) ->
-      (sign,subst1 (mkRel (n+cs.cs_nargs)) c)
-  | Case _ ->
-      (* Typically case of a match *)
-      (* Not clear what to do; is it avoidable? should we go down the match? *)
-      (sign,applist (body,[mkRel (n+cs.cs_nargs)]))
+  | Lambda (_,_,c) when ng = 0 ->
+      subst1 (mkRel n) c
+  | Lambda (na,t,c) ->
+      (* We traverse an inner generalization *)
+      mkLambda (na,t,ungeneralize (n+1) (ng-1) c)
+  | LetIn (na,b,t,c) ->
+      (* We traverse an alias *)
+      mkLetIn (na,b,t,ungeneralize (n+1) ng c)
+  | Case (ci,p,c,brs) ->
+      (* We traverse a split *)
+      let p =
+        let sign,p = decompose_lam_assum p in
+        let sign2,p = decompose_prod_n_assum ng p in
+        let p = prod_applist p [mkRel (n+List.length sign+ng)] in
+        it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
+      mkCase (ci,p,c,array_map2 (fun q c ->
+        let sign,b = decompose_lam_n_assum q c in
+        it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
+        ci.ci_cstr_ndecls brs)
+  | App (f,args) ->
+      (* We traverse an inner generalization *)
+      assert (isCase f);
+      mkApp (ungeneralize n (ng+Array.length args) f,args)
   | _ -> assert false
 
+let ungeneralize_branch n (sign,body) cs =
+  (sign,ungeneralize (n+cs.cs_nargs) 0 body)
+
 let postprocess_dependencies evd current brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
   | [], _ -> brs,tomatch,pred,[]
   | n::deps, Abstract (i,d) :: tomatch ->
       let d = map_rel_declaration (nf_evar evd) d in
-      if List.exists (fun c -> dependent_decl (lift k c) d) tocheck then
-        (* The dependency is real *)
+      if List.exists (fun c -> dependent_decl (lift k c) d) tocheck || pi2 d <> None then
+        (* Dependency in the current term to match and its dependencies is real *)
         let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in
         let inst = if pi2 d = None then mkRel n::inst else inst in
         brs, Abstract (i,d) :: tomatch, pred, inst
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 8fde93c1ba..05554bed7b 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -26,6 +26,28 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
   end.
 End Folding.
 
+(** Testing post-processing of nested dependencies *)
+
+Check fun x:{x|x=0}*nat+nat => match x with
+      | inl ((exist 0 eq_refl),0) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
 (* -------------------------------------------------------------------- *)
 (*   Example to test patterns matching on dependent families            *)
 (* This exemple extracted from the developement done by Nacira Chabane  *)