modif des fixpoints pour que si on donne une notation au produit, les pts fixes s'affichent correctement

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

4 files changed, 120 insertions, 62 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ffd2fad54a..e1f0da13b5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -358,45 +358,14 @@ and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) =
 	 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,typ) (na,body,t) -> match body with
-	| None -> (RLambda (dummy_loc,na,t,c),RProd (dummy_loc,na,t,typ))
-	| Some b -> (RLetIn (dummy_loc,na,b,c),RLetIn (dummy_loc,na,b,typ)))
-	(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) ((Name id,None,t)::l) avoid env c c'
-      (* May occur for fix built interactively *)
-      | LetIn (na,b,t',c), _ ->
-          let t' = detype tenv avoid env t' in
-          let b = detype tenv avoid env b in
-	  let id = next_name_away na avoid in 
-          let avoid = id::avoid and env = add_name (Name id) env in
-          share_names n ((Name id,Some b,t')::l) avoid env c t
-      (* Only if built with the f/n notation or w/o let-expansion in types *)
-      | _, LetIn (_,b,_,t) ->
-	  share_names n l avoid env c (subst1 b t)
-      (* If it is an open proof: we cheat and eta-expand *)
-      | _, Prod (na',t',c') ->
-          let t' = detype tenv avoid env t' in
-          let avoid = name_cons na' avoid and env = add_name na' env in
-          let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-          share_names (n-1) ((na',None,t')::l) avoid env appc c'
-      (* If built with the f/n notation: we renounce to share names *)
-      | _ -> share_names 0 l avoid env c t 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))
+    (fun c t i -> share_names tenv (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)
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
 
 and detype_cofix tenv avoid env n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
@@ -405,9 +374,53 @@ and detype_cofix tenv avoid env n (names,tys,bodies) =
 	 let id = next_name_away na avoid in 
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
+  let n = Array.length tys in
+  let v = array_map2
+    (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift n t))
+    bodies tys in
   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)
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
+and share_names tenv n l avoid env c t =
+  if !Options.v7 && n=0 then
+    let c = detype tenv avoid env c in
+    let t = detype tenv avoid env t in
+    (l,c,t)
+  else
+  match kind_of_term c, kind_of_term t with
+    | Lambda (na,t,c), Prod (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in 
+        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 tenv (n-1) ((Name id,None,t)::l) avoid env c c'
+    (* May occur for fix built interactively *)
+    | LetIn (na,b,t',c), _ ->
+        let t' = detype tenv avoid env t' in
+        let b = detype tenv avoid env b in
+	let id = next_name_away na avoid in 
+        let avoid = id::avoid and env = add_name (Name id) env in
+        share_names tenv n ((Name id,Some b,t')::l) avoid env c t
+    (* Only if built with the f/n notation or w/o let-expansion in types *)
+    | _, LetIn (_,b,_,t) ->
+	share_names tenv n l avoid env c (subst1 b t)
+    (* If it is an open proof: we cheat and eta-expand *)
+    | _, Prod (na',t',c') ->
+        let t' = detype tenv avoid env t' in
+        let avoid = name_cons na' avoid and env = add_name na' env in
+        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+        share_names tenv (n-1) ((na',None,t')::l) avoid env appc c'
+    (* If built with the f/n notation: we renounce to share names *)
+    | _ ->
+        if n>0 then warning "Detyping.detype: cannot factorize fix enough";
+        let c = detype tenv avoid env c in
+        let t = detype tenv avoid env t in
+        (l,c,t)
 
 and detype_eqn tenv avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f2d8d97dd..a2ea06e4ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -244,31 +244,54 @@ let rec pretype tycon env isevars lvar = function
 	     { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
 	 | None -> error_unsolvable_implicit loc env (evars_of isevars) k)
 
-  | RRec (loc,fixkind,names,lar,vdef) ->
+  | RRec (loc,fixkind,names,bl,lar,vdef) ->
+      let rec type_bl env ctxt = function
+          [] -> ctxt
+        | (na,None,ty)::bl ->
+            let ty' = pretype_type empty_valcon env isevars lvar ty in
+            let dcl = (na,None,ty'.utj_val) in
+            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        | (na,Some bd,ty)::bl ->
+            let ty' = pretype_type empty_valcon env isevars lvar ty in
+            let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+            let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+      let ctxtv = Array.map (type_bl env empty_rel_context) bl in
       let larj =
-        Array.map (pretype_type empty_valcon env isevars lvar) lar in
+        array_map2
+          (fun e ar ->
+            pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+          ctxtv lar in
       let lara = Array.map (fun a -> a.utj_val) larj in
+      let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
       let nbfix = Array.length lar in
       let names = Array.map (fun id -> Name id) names in
-      let newenv = push_rec_types (names,lara,[||]) env in
+      (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+      let newenv = push_rec_types (names,ftys,[||]) env in
       let vdefj =
-	Array.mapi 
-	  (fun i def -> (* we lift nbfix times the type in tycon, because of
-			 * the nbfix variables pushed to newenv *)
-             pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
-               newenv isevars lvar def)
-          vdef in
-      evar_type_fixpoint loc env isevars names lara vdefj;
+	array_map2_i 
+	  (fun i ctxt def ->
+            (* we lift nbfix times the type in tycon, because of
+	     * the nbfix variables pushed to newenv *)
+            let (ctxt,ty) =
+              decompose_prod_n_assum (rel_context_length ctxt)
+                (lift nbfix ftys.(i)) in
+            let nenv = push_rel_context ctxt newenv in
+            let j = pretype (mk_tycon ty) nenv isevars lvar def in
+            { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+              uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+          ctxtv vdef in
+      evar_type_fixpoint loc env isevars names ftys vdefj;
       let fixj =
 	match fixkind with
 	  | RFix (vn,i as vni) ->
-	      let fix = (vni,(names,lara,Array.map j_val vdefj)) in
+	      let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) lara.(i)
+	      make_judge (mkFix fix) ftys.(i)
 	  | RCoFix i -> 
-	      let cofix = (i,(names,lara,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkCoFix cofix) lara.(i) in
+	      make_judge (mkCoFix cofix) ftys.(i) in
       inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
   | RSort (loc,s) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 6442ca9693..6e7f8f70fc 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -70,19 +70,20 @@ type rawconstr =
   | RCases of loc * (rawconstr option * rawconstr option ref) *
       (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-      (* Rem: "ref" used for the v7->v8 translation only *)
   | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
       rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * 
+  | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+and rawdecl = name * rawconstr option * rawconstr
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,{contents=(na,None)}) -> [na]
@@ -97,6 +98,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
+let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
@@ -114,9 +116,12 @@ let map_rawconstr f = function
       RLetTuple (loc,nal,(na,option_app f po),f b,f c)
   | RIf (loc,c,(na,po),b1,b2) ->
       RIf (loc,f c,(na,option_app f po),f b1,f b2)
-  | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
+  | RRec (loc,fk,idl,bl,tyl,bv) ->
+      RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
+            Array.map f tyl,Array.map f bv)
   | RCast (loc,c,t) -> RCast (loc,f c,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+  
 
 (*
 let name_app f e = function
@@ -176,9 +181,18 @@ let occur_rawconstr id =
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
-    | RRec (loc,fk,idl,tyl,bv) ->
-	(array_exists occur tyl) or
-	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
+    | RRec (loc,fk,idl,bl,tyl,bv) ->
+        not (array_for_all4 (fun fid bl ty bd ->
+          let rec occur_fix = function
+              [] -> not (occur ty) && (fid=id or not(occur bd))
+            | (na,bbd,bty)::bl ->
+                not (occur bty) &&
+                (match bbd with
+                    Some bd -> not (occur bd)
+                  | _ -> true) &&
+                (na=Name id or not(occur_fix bl)) in
+          occur_fix bl)
+          idl bl tyl bv)
     | RCast (loc,c,t) -> (occur c) or (occur t)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
 
@@ -275,11 +289,17 @@ let rec subst_raw subst raw =
 	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
           RIf (loc,c',(na,po'),b1',b2')
 
-  | RRec (loc,fix,ida,ra1,ra2) -> 
+  | RRec (loc,fix,ida,bl,ra1,ra2) -> 
       let ra1' = array_smartmap (subst_raw subst) ra1
       and ra2' = array_smartmap (subst_raw subst) ra2 in
-	if ra1' == ra1 && ra2' == ra2 then raw else
-	  RRec (loc,fix,ida,ra1',ra2')
+      let bl' = array_smartmap
+        (list_smartmap (fun (na,obd,ty as dcl) ->
+          let ty' = subst_raw subst ty in
+          let obd' = option_smartmap (subst_raw subst) obd in
+          if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
+        bl in
+	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
+	  RRec (loc,fix,ida,bl',ra1',ra2')
 
   | RSort _ -> raw
 
@@ -310,7 +330,7 @@ let loc_of_rawconstr = function
   | ROrderedCase (loc,_,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
-  | RRec (loc,_,_,_,_) -> loc
+  | RRec (loc,_,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
   | RCast (loc,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 869861ccd7..e5b2a23fe8 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -73,13 +73,15 @@ type rawconstr =
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * 
+  | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+and rawdecl = name * rawconstr option * rawconstr
+
 val cases_predicate_names : 
   (rawconstr * (name * (loc * inductive * name list) option) ref) list ->
       name list