Changement de la structure des points fixes

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

7 files changed, 64 insertions, 64 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 4611008161..b864d10314 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -368,17 +368,18 @@ and cbv_norm_value info = function (* reduction under binders *)
   | LAM (x,a,b,env) ->
       mkLambda (x, cbv_norm_term info env a,
 		cbv_norm_term info (subs_lift env) b)
-  | FIXP ((lij,(lty,lna,bds)),env,args) ->
+  | FIXP ((lij,(names,lty,bds)),env,args) ->
       applistc
         (mkFix (lij,
-		(Array.map (cbv_norm_term info env) lty, lna, 
+		(names,
+                 Array.map (cbv_norm_term info env) lty,
 		 Array.map (cbv_norm_term info 
 			      (subs_liftn (Array.length lty) env)) bds)))
         (List.map (cbv_norm_value info) args)
-  | COFIXP ((j,(lty,lna,bds)),env,args) ->
+  | COFIXP ((j,(names,lty,bds)),env,args) ->
       applistc
         (mkCoFix (j,
-		  (Array.map (cbv_norm_term info env) lty, lna, 
+		  (names,Array.map (cbv_norm_term info env) lty,
 		   Array.map (cbv_norm_term info 
 				(subs_liftn (Array.length lty) env)) bds)))
         (List.map (cbv_norm_value info) args)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 877dca8c94..170de079b7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -333,8 +333,8 @@ let rec detype avoid env t =
 	in 
 	RCases (dummy_loc,tag,pred,[tomatch],eqnl)
 	
-    | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
-    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt
+    | IsFix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef
+    | IsCoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
 
 and detype_reference avoid env ref args =
   let args = 
@@ -350,13 +350,13 @@ and detype_reference avoid env ref args =
   if args = [] then f
   else RApp (dummy_loc, f, List.map (detype avoid env) args)
 
-and detype_fix fk avoid env cl lfn vt =
-  let lfi = List.map (fun id -> next_name_away id avoid) lfn in
-  let def_avoid = lfi@avoid in
+and detype_fix avoid env fixkind (names,tys,bodies) =
+  let lfi = Array.map (fun id -> next_name_away id avoid) names in
+  let def_avoid = Array.to_list lfi@avoid in
   let def_env =
-    List.fold_left (fun env id -> add_name (Name id) env) env lfi in
-  RRec(dummy_loc,fk,Array.of_list lfi,Array.map (detype avoid env) cl,
-       Array.map (detype def_avoid def_env) vt)
+    Array.fold_left (fun env id -> add_name (Name id) env) env lfi in
+  RRec(dummy_loc,fixkind,lfi,Array.map (detype avoid env) tys,
+       Array.map (detype def_avoid def_env) bodies)
 
 
 and detype_eqn avoid env constr_id construct_nargs branch =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 382fba7f07..3d8653da03 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -252,7 +252,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-	| IsFix (li1,(tys1,_,bds1 as recdef1)), IsFix (li2,(tys2,_,bds2)) ->
+	| IsFix (li1,(_,tys1,bds1 as recdef1)), IsFix (li2,(_,tys2,bds2)) ->
 	    li1=li2
 	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
 	    & (array_for_all2
@@ -260,7 +260,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		 bds1 bds2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	     
-	| IsCoFix (i1,(tys1,_,bds1 as recdef1)), IsCoFix (i2,(tys2,_,bds2)) ->
+	| IsCoFix (i1,(_,tys1,bds1 as recdef1)), IsCoFix (i2,(_,tys2,bds2)) ->
 	    i1=i2 
 	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
 	    & (array_for_all2
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 14ee93f26d..1667867508 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
     error_number_branches_loc loc CCI env c
       (mkAppliedInd indt) (mis_nconstr mispec);
   if mis_is_recursive_subset [tyi] mispec then
-    let dep = find_case_dep_nparams env sigma (c,p) indf pt in 
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in 
     let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
     let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
     (* build now the fixpoint *)
@@ -90,10 +90,10 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 	       else
 		 let args = extended_rel_list 1 lnames in
 		 whd_beta (applist (lift (nar+1) p, args)))))
-          lnames 
-      in
-      let fix = mkFix (([|nar|],0),
-		       ([|typPfix|],[Name(id_of_string "F")],[|deffix|])) in
+          lnames in
+      let fix =
+        mkFix (([|nar|],0),
+	       ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in
       applist (fix,realargs@[c])
   else
     let ci = make_default_case_info mispec in
@@ -261,29 +261,29 @@ let rec pretype tycon env isevars lvar lmeta = function
 		      (loc,"pretype",
 		       [< 'sTR "Cannot infer a term for this placeholder" >])))
 
-  | RRec (loc,fixkind,lfi,lar,vdef) ->
-      let larj = Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in
+  | RRec (loc,fixkind,names,lar,vdef) ->
+      let larj =
+        Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in
       let lara = Array.map (fun a -> a.utj_val) larj in
-      let nbfix = Array.length lfi in
-      let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in
-      let newenv =
-	array_fold_left2 (fun env id ar -> (push_rel_assum (id,ar) env))
-	  env (Array.of_list lfi) (vect_lift_type 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
       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
-	       lmeta def) vdef in
-      evar_type_fixpoint env isevars lfi lara vdefj;
+             pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
+               newenv isevars lvar lmeta def)
+          vdef in
+      evar_type_fixpoint env isevars names lara vdefj;
       let fixj =
 	match fixkind with
 	  | RFix (vn,i as vni) ->
-	      let fix = (vni,(lara,lfi,Array.map j_val vdefj)) in
+	      let fix = (vni,(names,lara,Array.map j_val vdefj)) in
 	      check_fix env (evars_of isevars) fix;
 	      make_judge (mkFix fix) lara.(i)
 	  | RCoFix i -> 
-	      let cofix = (i,(lara,lfi,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,lara,Array.map j_val vdefj)) in
 	      check_cofix env (evars_of isevars) cofix;
 	      make_judge (mkCoFix cofix) lara.(i) in
       inh_conv_coerce_to_tycon loc env isevars fixj tycon
@@ -299,7 +299,9 @@ let rec pretype tycon env isevars lvar lmeta = function
 	| c::rest ->
 	    let argloc = loc_of_rawconstr c in
 	    let resj = inh_app_fun env isevars resj in
-      	    match kind_of_term (whd_betadeltaiota env (evars_of isevars) resj.uj_type) with
+            let resty =
+              whd_betadeltaiota env (evars_of isevars) resj.uj_type in
+      	    match kind_of_term resty with
 	      | IsProd (na,c1,c2) ->
 		  let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in
 		  let newresj =
@@ -398,7 +400,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 
       let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in
 
-      let dep = find_case_dep_nparams env (evars_of isevars)
+      let (dep,_) = find_case_dep_nparams env (evars_of isevars)
         (cj.uj_val,pj.uj_val) indf evalPt in
 
       let (p,pt) =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 43e0a91f92..a2b98a6d82 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -45,8 +45,8 @@ let sort_of_atomic_type env sigma ft args =
   in concl_of_arity env ft
 
 let typeur sigma metamap =
-let rec type_of env cstr=
-  match kind_of_term cstr with
+  let rec type_of env cstr=
+    match kind_of_term cstr with
     | IsMeta n ->
           (try strip_outer_cast (List.assoc n metamap)
            with Not_found -> anomaly "type_of: this is not a well-typed term")
@@ -73,16 +73,16 @@ let rec type_of env cstr=
           mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2)
     | IsLetIn (name,b,c1,c2) ->
          subst1 b (type_of (push_rel_def (name,b,c1) env) c2)
-    | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
-    | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
+    | IsFix ((_,i),(_,tys,_)) -> tys.(i)
+    | IsCoFix (i,(_,tys,_)) -> tys.(i)
     | IsApp(f,args)->
-      strip_outer_cast (subst_type env sigma (type_of env f) 
-			  (Array.to_list args))
+        strip_outer_cast
+          (subst_type env sigma (type_of env f) (Array.to_list args))
     | IsCast (c,t) -> t
     | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
 
-and sort_of env t = 
-  match kind_of_term t with
+  and sort_of env t = 
+    match kind_of_term t with
     | IsCast (c,s) when isSort s -> destSort s
     | IsSort (Prop c) -> type_0
     | IsSort (Type u) -> Type Univ.dummy_univ
@@ -95,7 +95,7 @@ and sort_of env t =
         anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
 
-in type_of, sort_of
+  in type_of, sort_of
 
 let get_type_of env sigma c = fst (typeur sigma []) env c
 let get_sort_of env sigma t = snd (typeur sigma []) env t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f651766020..72ebb6626e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -76,7 +76,7 @@ let _ =
    == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p))
    with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *)
 
-let check_fix_reversibility labs args ((lv,i),(tys,_,bds)) =
+let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   let n = List.length labs in
   let nargs = List.length args in
   if nargs > n then raise Elimconst;
@@ -156,13 +156,12 @@ let compute_consteval_mutual_fix sigma env ref =
     match kind_of_term c' with
       | IsLambda (na,t,g) when l=[] ->
 	  srec (push_rel_assum (na,t) env) (minarg+1) (t::labs) ref g
-      | IsFix ((lv,i),(_,names,_) as fix) ->
+      | IsFix ((lv,i),(names,_,_) as fix) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
 	  (match compute_consteval_direct sigma env ref with
 	     | NotAnElimination -> (*Above const was eliminable but this not!*)
 		 NotAnElimination
 	     | EliminationFix (minarg',infos) ->
-		 let names = Array.of_list names in
 		 let refs =
 		   Array.map
 		     (invert_name labs l names.(i) env sigma ref) names in
@@ -291,8 +290,7 @@ let reduce_mind_case_use_function (sp,args) env mia =
 	let ncargs = (fst mia.mci).(i-1) in
 	let real_cargs = list_lastn ncargs mia.mcargs in
 	applist (mia.mlf.(i-1), real_cargs)
-    | IsCoFix (_,(_,names,_) as cofix) ->
-	let names = Array.of_list names in
+    | IsCoFix (_,(names,_,_) as cofix) ->
 	let build_fix_name i =
 	  match names.(i) with 
 	    | Name id ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c39197af73..f782163363 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -59,23 +59,22 @@ let rec execute mf env sigma cstr =
         let cj = execute mf env sigma c in
         let pj = execute mf env sigma p in
         let lfj = execute_array mf env sigma lf in
-        type_of_case env sigma ci pj cj lfj
+        let (j,_) = judge_of_case env sigma ci pj cj lfj in
+        j
   
-    | IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
+    | IsFix ((vn,i as vni),recdef) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let larjv,vdefv = execute_fix mf env sigma lar lfi vdef in
- 	let larv = Array.map body_of_type larjv in
-	let fix = vni,(larv,lfi,vdefv) in
+        let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in
+	let fix = (vni,recdef') in
         check_fix env sigma fix;
-	make_judge (mkFix fix) larjv.(i)
+	make_judge (mkFix fix) tys.(i)
 	  
-    | IsCoFix (i,(lar,lfi,vdef)) ->
-        let (larjv,vdefv) = execute_fix mf env sigma lar lfi vdef in
-	let larv = Array.map body_of_type larjv in
-        let cofix = i,(larv,lfi,vdefv) in
+    | IsCoFix (i,recdef) ->
+        let (_,tys,_ as recdef') = execute_fix mf env sigma recdef in
+        let cofix = (i,recdef') in
         check_cofix env sigma cofix;
-	make_judge (mkCoFix cofix) larjv.(i)
+	make_judge (mkCoFix cofix) tys.(i)
 	  
     | IsSort (Prop c) -> 
 	judge_of_prop_contents c
@@ -122,17 +121,17 @@ let rec execute mf env sigma cstr =
         let j, _ = cast_rel env sigma cj tj in
 	j
 	  
-and execute_fix mf env sigma lar lfi vdef =
+and execute_fix mf env sigma (names,lar,vdef) =
   let larj = execute_array mf env sigma lar in
   let lara = Array.map (assumption_of_judgment env sigma) larj in
-  let nlara = 
-    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
+  let ctxt = 
+    array_map2_i (fun i na ty -> (na, type_app (lift i) ty)) names lara in
   let env1 = 
-    List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in
+    Array.fold_left (fun env nvar -> push_rel_assum nvar env) env ctxt in
   let vdefj = execute_array mf env1 sigma vdef in
   let vdefv = Array.map j_val vdefj in
-  let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
-  (lara,vdefv)
+  let cst3 = type_fixpoint env1 sigma names lara vdefj in
+  (names,lara,vdefv)
 
 and execute_array mf env sigma v =
   let jl = execute_list mf env sigma (Array.to_list v) in