Correction incompatibilites dans la fn des types des inductifs

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

7 files changed, 47 insertions, 48 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9c6ffb172..c09254c2c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,8 +50,8 @@ type one_inductive_body = {
   mind_nf_lc : typed_type array;
   mind_nf_arity : typed_type;
   (* lc and arity as given by user if not in nf; useful e.g. for Ensemble.v *)
-  mind_user_lc : constr array option;
-  mind_user_arity : constr option;
+  mind_user_lc : typed_type array option;
+  mind_user_arity : typed_type option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -70,11 +70,11 @@ type mutual_inductive_body = {
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
 let mind_user_lc mip = match mip.mind_user_lc with
-  | None -> Array.map body_of_type mip.mind_nf_lc
+  | None -> mip.mind_nf_lc
   | Some lc -> lc
 
 let mind_user_arity mip = match mip.mind_user_arity with
-  | None -> body_of_type mip.mind_nf_arity
+  | None -> mip.mind_nf_arity
   | Some a -> a
 
 (*s Declaration. *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 4cfb3e2ab..0c8b15e3c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -55,8 +55,8 @@ type one_inductive_body = {
   mind_typename : identifier;
   mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
   mind_nf_arity : typed_type;
-  mind_user_lc : constr array option;
-  mind_user_arity : constr option;
+  mind_user_lc : typed_type array option;
+  mind_user_arity : typed_type option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -73,8 +73,8 @@ type mutual_inductive_body = {
   mind_nparams : int }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
-val mind_user_lc : one_inductive_body -> constr array
-val mind_user_arity : one_inductive_body -> constr
+val mind_user_lc : one_inductive_body -> typed_type array
+val mind_user_arity : one_inductive_body -> typed_type
 val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
 
 (*s Declaration of inductive types. *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c29d4385d..74b1a7602 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -206,7 +206,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     let (lpar,auxlargs) = list_chop auxnpar largs in 
     if not (List.for_all (noccur_between n ntypes) auxlargs) then
       raise (IllFormedInd (LocalNonPos n));
-    let auxlc = mis_lc mispeci 
+    let auxlc = mis_nf_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
     if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
     let lrecargs = List.map (check_weak_pos n) lpar in
@@ -313,28 +313,28 @@ let cci_inductive env env_ar kind nparams finite inds cst =
     let recargs = listrec_mconstr env_ar ntypes nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
     let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
+    
     let nf_ar,user_ar =
       if isArity (body_of_type ar) then ar,None
-      else 
+      else
 	(make_typed_lazy (prod_it (mkSort ar_sort) ar_sign)
 	   (fun _ -> level_of_type ar)),
-	Some (body_of_type ar) in
+	Some ar in
     let kelim = allowed_sorts issmall isunit ar_sort in
     let lc_bodies = Array.map body_of_type lc in
+
     let splayed_lc = Array.map (splay_prod_assum env Evd.empty) lc_bodies in
-    let nf_lc = Array.map
-		  (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
-    let nf_typed_lc,user_lc =
-      if nf_lc = lc_bodies then lc,None
-      else
-	(array_map2
-	   (fun nfc c -> make_typed_lazy nfc (fun _ -> level_of_type c))
-	   nf_lc lc),
-        Some lc_bodies in
+    let nf_lc =
+      array_map2
+	(fun (d,b) c ->
+	   make_typed_lazy 
+	     (it_mkProd_or_LetIn b d) (fun _ -> level_of_type c))
+	splayed_lc lc in
+    let nf_lc,user_lc = if nf_lc = lc then lc,None else nf_lc, Some lc in
     { mind_consnames = Array.of_list cnames;
       mind_typename = id;
       mind_user_lc = user_lc;
-      mind_nf_lc = nf_typed_lc;
+      mind_nf_lc = nf_lc;
       mind_user_arity  = user_ar;
       mind_nf_arity = nf_ar;
       mind_nrealargs = List.length ar_sign - nparams;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bbc7918dc..3436bf962 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -40,20 +40,26 @@ let mis_typepath mis =
 let mis_consnames mis = mis.mis_mip.mind_consnames
 let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
 
-let mis_typed_lc mis =
+let mis_typed_nf_lc mis =
   let sign = mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
   Array.map (fun t -> Instantiate.instantiate_type sign t args)
     mis.mis_mip.mind_nf_lc
 
-let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
+let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
+
+let mis_user_lc mis = 
+  let sign = mis.mis_mib.mind_hyps in
+  let args = Array.to_list mis.mis_args in
+  Array.map (fun t -> Instantiate.instantiate_type sign t args)
+    (mind_user_lc mis.mis_mip)
 
 (* gives the vector of constructors and of 
    types of constructors of an inductive definition 
    correctly instanciated *)
 
 let mis_type_mconstructs mispec =
-  let specif = mis_lc mispec
+  let specif = Array.map body_of_type (mis_user_lc mispec)
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) 
@@ -64,7 +70,7 @@ let mis_type_mconstructs mispec =
    Array.map (substl (list_tabulate make_Ik ntypes)) specif)
 
 let mis_type_nf_mconstruct i mispec =
-  let specif = mis_lc mispec
+  let specif = mis_nf_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
@@ -72,28 +78,27 @@ let mis_type_nf_mconstruct i mispec =
   substl (list_tabulate make_Ik ntypes) specif.(i-1)
 
 let mis_type_mconstruct i mispec = 
-  let specif = mis_typed_lc mispec
+  let specif = mis_user_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
   typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
-let mis_typed_arity mis =
+let mis_user_arity mis =
   let hyps = mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in
-  Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
+  Instantiate.instantiate_type hyps (mind_user_arity mis.mis_mip) largs
 
-(*
-let mis_arity mispec = incast_type (mis_typed_arity mispec)
-*)
-
-let mis_arity mis = body_of_type (mis_typed_arity mis)
+let mis_nf_arity mis =
+  let hyps = mis.mis_mib.mind_hyps 
+  and largs = Array.to_list mis.mis_args in
+  Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
 
 let mis_params_ctxt mispec =
   let paramsign,_ =
     decompose_prod_n_assum mispec.mis_mib.mind_nparams
-      (body_of_type (mis_typed_arity mispec))
+      (body_of_type (mis_nf_arity mispec))
   in paramsign
 
 let mis_sort mispec = mispec.mis_mip.mind_sort
@@ -250,7 +255,7 @@ let get_constructors (IndFamily (mispec,params) as indf) =
   Array.init (mis_nconstr mispec) (fun j -> get_constructor indf (j+1))
 
 let get_arity (IndFamily (mispec,params)) =
-  let arity = mis_arity mispec in
+  let arity = body_of_type (mis_nf_arity mispec) in
   destArity (prod_applist arity params)
 
 (* Functions to build standard types related to inductive *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3b45dad0b..727ccf409 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -42,15 +42,15 @@ val mis_typepath : inductive_instance -> section_path
 val mis_is_recursive_subset : int list -> inductive_instance -> bool
 val mis_is_recursive : inductive_instance -> bool
 val mis_consnames : inductive_instance -> identifier array
-val mis_typed_arity : inductive_instance -> typed_type
 val mis_inductive : inductive_instance -> inductive
-val mis_arity : inductive_instance -> constr
+val mis_nf_arity : inductive_instance -> typed_type
+val mis_user_arity : inductive_instance -> typed_type
 val mis_params_ctxt : inductive_instance -> rel_context
 val mis_sort : inductive_instance -> sorts
 val mis_type_mconstruct : int -> inductive_instance -> typed_type
 
 (* The ccl of constructor is pre-normalised in the following functions *)
-val mis_lc : inductive_instance -> constr array
+val mis_nf_lc : inductive_instance -> constr array
 val mis_type_mconstructs : inductive_instance -> constr array * constr array
 
 (*s [inductive_family] = [inductive_instance] applied to global parameters *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 74b207209..8421a0543 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -83,15 +83,7 @@ let type_of_constant = Instantiate.constant_type
 
 (* Inductive types. *)
 
-(* Q: A faire disparaitre ??
-let instantiate_arity mis =
-  let ids = ids_of_sign mis.mis_mib.mind_hyps in
-  let args = Array.to_list mis.mis_args in 
-  let arity = mis.mis_mip.mind_arity in
-  { body = instantiate_constr ids arity.body args;
-    typ = arity.typ }
-*)
-let instantiate_arity = mis_typed_arity
+let instantiate_arity = mis_user_arity
 
 let type_of_inductive env sigma i =
   (* TODO: check args *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f179bd370..76fc0b12a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -403,8 +403,10 @@ let pr_reln u r =
     | Terminal -> [< >]
   in 
   prec r
-    
+
 let pr_universes g =
   let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
   prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> pr_reln u r) graph
     
+
+