Problème de désynchronisation des variables du type et du corps d'un point-fixe

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

3 files changed, 51 insertions, 5 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 86bca87ebc..8943109dcf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -236,7 +236,15 @@ let rec detype tenv avoid env t =
 	let indsp = annot.ci_ind in
         let considl = annot.ci_pp_info.cnames in
         let k = annot.ci_pp_info.ind_nargs in
-	let consnargsl = mis_constr_nargs_env tenv indsp in
+
+        (* Find constructors arity *)
+        let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in
+        let get_consnarg j = 
+          let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in
+          let l,_ = decompose_prod_assum typi in
+          List.length l - mip.mind_nparams in
+        let consnargsl =
+          Array.init (Array.length mip.mind_consnames) get_consnarg in
 	let pred = 
 	  if synth_type & computable p k & considl <> [||] then
 	    None
@@ -272,20 +280,49 @@ let rec detype tenv avoid env t =
 	  let bl = array_map2 remove_type consnargsl bl in
 	  ROrderedCase (dummy_loc,tag,pred,tomatch,bl)
 	
-    | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef
-    | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef
+    | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef
+    | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef
 
-and detype_fix tenv avoid env fixkind (names,tys,bodies) =
+and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) =
+  let def_avoid, def_env, lfi =
+    Array.fold_left
+      (fun (avoid, env, l) na ->
+	 let id = next_name_away na avoid in 
+	 (id::avoid, add_name (Name id) env, id::l))
+      (avoid, env, []) names in
+ (* Be sure that bodies and types share the same names *)
+  let rec share_names n l avoid env c t =
+    if n = 0 then
+      let c = detype tenv avoid env c in
+      let t = detype tenv avoid env t in
+      List.fold_left (fun c (na,t) -> RLambda (dummy_loc,na,t,c)) c l,
+      List.fold_left (fun c (na,t) -> RProd (dummy_loc,na,t,c)) t l
+    else match kind_of_term c, kind_of_term t with
+      | Lambda (na,t,c), Prod (_,t',c') ->
+          let t = detype tenv avoid env t in
+	  let id = next_name_away na avoid in 
+          let avoid = id::avoid and env = add_name (Name id) env in
+          share_names (n-1) ((na,t)::l) avoid env c c'
+      | _ -> anomaly "Detype: wrong fix" in
+  let n = Array.length tys in
+  let v = array_map3
+    (fun c t i -> share_names (i+1) [] def_avoid def_env c (lift n t))
+    bodies tys vn in
+  RRec(dummy_loc,RFix nvn,Array.of_list (List.rev lfi),
+       Array.map snd v, Array.map fst v)
+
+and detype_cofix tenv avoid env n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left
       (fun (avoid, env, l) na ->
 	 let id = next_name_away na avoid in 
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
-  RRec(dummy_loc,fixkind,Array.of_list (List.rev lfi),
+  RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi),
        Array.map (detype tenv avoid env) tys,
        Array.map (detype tenv def_avoid def_env) bodies)
 
+  
 
 and detype_eqn tenv avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
new file mode 100644
index 0000000000..5f13caafc4
--- /dev/null
+++ b/test-suite/output/Cases.out
@@ -0,0 +1,4 @@
+t_rect = 
+[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))]
+ Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end}
+     : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t)
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
new file mode 100644
index 0000000000..7483e8c40d
--- /dev/null
+++ b/test-suite/output/Cases.v
@@ -0,0 +1,5 @@
+(* Cases with let-in in constructors types *)
+
+Inductive t : Set := k : [x:=t]x -> x.
+
+Print t_rect.