Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing

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

5 files changed, 143 insertions, 112 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 96eef5700..8be72eb94 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,10 +21,16 @@ let is_defined cb =
 
 let is_opaque cb = cb.const_opaque
 
+(*s Global and local constant declaration. *)
+
 type constant_entry = {
   const_entry_body : constr;
   const_entry_type : constr option }
 
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
 (* Inductive entries *)
 
 type recarg = 
@@ -45,7 +51,8 @@ type one_inductive_body = {
   mind_nrealargs : int;
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
-  mind_finite : bool }
+  mind_finite : bool;
+  mind_nparams : int }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
@@ -53,8 +60,7 @@ type mutual_inductive_body = {
   mind_hyps : named_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
+  mind_singl : constr option }
 
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
@@ -68,10 +74,17 @@ let mind_user_arity mip = match mip.mind_user_arity with
 
 (*s Declaration. *)
 
-type mutual_inductive_entry = {
+type one_inductive_entry = {
   mind_entry_nparams : int;
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
   mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+  mind_entry_inds : one_inductive_entry list }
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 0cc927c8c..e24ac3bdd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -25,12 +25,16 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-(*s Constant declaration. *)
+(*s Global and local constant declaration. *)
 
 type constant_entry = {
   const_entry_body : constr;
   const_entry_type : constr option }
 
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
 (*s Inductive types (internal representation). *)
 
 type recarg = 
@@ -56,7 +60,8 @@ type one_inductive_body = {
   mind_nrealargs : int;
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
-  mind_finite : bool }
+  mind_finite : bool;
+  mind_nparams : int }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
@@ -64,8 +69,7 @@ type mutual_inductive_body = {
   mind_hyps : named_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
+  mind_singl : constr option }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
 val mind_user_lc : one_inductive_body -> types array
@@ -76,8 +80,14 @@ val mind_arities_context : mutual_inductive_body -> rel_declaration list
 
 (*s Declaration of inductive types. *)
 
-type mutual_inductive_entry = {
+type one_inductive_entry = {
   mind_entry_nparams : int;
-  mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
 
+type mutual_inductive_entry = {
+  mind_entry_finite : bool;
+  mind_entry_inds : one_inductive_entry list }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ece400ad1..f10e59c9c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -59,7 +59,9 @@ let check_constructors_names id =
 let mind_check_names mie =
   let rec check indset cstset = function
     | [] -> ()
-    | (id,_,cl,_)::inds -> 
+    | ind::inds -> 
+	let id = ind.mind_entry_typename in
+	let cl = ind.mind_entry_consnames in
 	if Idset.mem id indset then
 	  raise (InductiveError (SameNamesTypes id))
 	else
@@ -74,35 +76,20 @@ let mind_check_names mie =
 
 let mind_extract_params n c =
   let (l,c') = decompose_prod_n_assum n c in (l,c')
-  
-let extract nparams c =
-  try fst (mind_extract_params nparams c)
-  with UserError _ -> raise (InductiveError BadEntry)
-
-let check_params params params' =
-  if not (params = params') then raise (InductiveError BadEntry)
-
-let mind_extract_and_check_params mie =
-  let nparams = mie.mind_entry_nparams in
-  match mie.mind_entry_inds with
-    | [] -> anomaly "empty inductive types declaration"
-    | (_,ar,_,_)::l -> 
-	let params = extract nparams ar in
-	List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
-	params
-
-let mind_check_lc params mie =
-  let nparams = List.length params in
-  let check_lc (_,_,_,lc) =
-    List.iter (fun c -> check_params params (extract nparams c)) lc in
-  List.iter check_lc mie.mind_entry_inds
 
 let mind_check_arities env mie =
   let check_arity id c =
     if not (is_arity env Evd.empty c) then 
       raise (InductiveError (NotAnArity id))
   in
-  List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+  List.iter
+    (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
+    mie.mind_entry_inds
+
+let mind_check_wellformed env mie =
+  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+  mind_check_names mie;
+  mind_check_arities env mie
 
 (***********************************************************************)
 
@@ -313,9 +300,9 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
-let cci_inductive env env_ar kind nparams finite inds cst =
+let cci_inductive env env_ar kind finite inds cst =
   let ntypes = List.length inds in
-  let one_packet i (id,ar,cnames,issmall,isunit,lc) =
+  let one_packet i (nparams,id,ar,cnames,issmall,isunit,lc) =
     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
@@ -340,11 +327,12 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;
-      mind_finite = finite }
+      mind_finite = finite;
+      mind_nparams = nparams }
   in
   let ids = 
     List.fold_left 
-      (fun acc (_,ar,_,_,_,lc) -> 
+      (fun acc (_,_,ar,_,_,_,lc) -> 
 	 Idset.union (global_vars_set (body_of_type ar))
 	   (Array.fold_left
 	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
@@ -358,5 +346,4 @@ let cci_inductive env env_ar kind nparams finite inds cst =
     mind_hyps = keep_hyps ids (named_context env);
     mind_packets = packets;
     mind_constraints = cst;
-    mind_singl = None;
-    mind_nparams = nparams }
+    mind_singl = None }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 71041c279..b8ea65f16 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -28,39 +28,27 @@ type inductive_error =
   | BadInduction of bool * identifier * sorts
   | NotMutualInScheme
 
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
-  decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
-   i.e. that all the types and constructors names are distinct. 
-   It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
-   types declaration. It raises an exception [InductiveError _] if there is
-   not enough abstractions in any of the terms of the field 
-   [mind_entry_inds]. *)
-
-val mind_extract_and_check_params : 
-  mutual_inductive_entry -> Sign.rel_context
+(* [mind_extract_params] extracts the parameters of an inductive
+   type declaration. *)
 
 val mind_extract_params : int -> constr -> Sign.rel_context * constr
 
-val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
+exception InductiveError of inductive_error
+
+(*s The following function does checks on inductive declarations. *)
 
-(* [mind_check_arities] checks that the types declared for all the
-   inductive types are some arities. *)
+(* [mind_check_wellformed env mie] checks that the types declared for
+   all the inductive types are arities. It checks also that
+   constructor and inductive names altogether are distinct. It raises
+   an exception [InductiveError _] if [mie] is not well-formed *)
 
-val mind_check_arities : env -> mutual_inductive_entry -> unit
+val mind_check_wellformed : env -> mutual_inductive_entry -> unit
 
 (* [cci_inductive] checks positivity and builds an inductive body *)
 
 val cci_inductive : 
-  env -> env -> path_kind -> int -> bool -> 
-   (identifier * types * identifier list * bool * bool * types array)
+  env -> env -> path_kind -> bool -> 
+   (int * identifier * types * identifier list * bool * bool * types array)
       list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c0e700a13..64968c509 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -269,6 +269,23 @@ let push_rel_assum = push_rel_or_named_assum push_rel_assum
 let push_rels_with_univ vars env =
   List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
 
+let safe_infer_local_decl env id = function
+  | LocalDef c -> 
+      let (j,cst) = safe_infer env c in
+      (Name id, Some j.uj_val, j.uj_type), cst
+  | LocalAssum c ->
+      let (j,cst) = safe_infer env c in
+      (Name id, None, assumption_of_judgment env Evd.empty j), cst
+
+let safe_infer_local_decls env decls =
+  let rec inferec env = function
+  | (id, d) :: l -> 
+      let env, l, cst1 = inferec env l in
+      let d, cst2 = safe_infer_local_decl env id d in
+      push_rel d env, d :: l, Constraint.union cst1 cst2
+  | [] -> env, [], Constraint.empty in
+  inferec env decls
+
 (* Insertion of constants and parameters in environment. *)
 
 let add_parameter sp t env =
@@ -370,12 +387,9 @@ let is_unit arinfos constrsinfos =
    | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
    | _ -> false
 
-let small_unit constrsinfos (env_ar,nparams,ar) =
+let small_unit constrsinfos (env_ar_par,short_arity) =
   let issmall = List.for_all is_small constrsinfos in
-  let arinfos =
-    let (params,a) = mind_extract_params nparams ar in
-    let env_par = push_rels params env_ar in
-    infos_and_sort env_par a in
+  let arinfos = infos_and_sort env_ar_par short_arity in
   let isunit = is_unit arinfos constrsinfos in
   issmall, isunit
 
@@ -386,63 +400,82 @@ let enforce_type_constructor arsort smax cst =
     | Type uc, Type ua -> Constraint.add (ua,Geq,uc) cst
     | _,_ -> cst
 
-let type_one_constructor env_ar nparams arsort c =
-  let infos = 
-    let (params,dc) = mind_extract_params nparams c in
-    let env_par = push_rels params env_ar in
-    infos_and_sort env_par dc 
-  in
-  (* Constructors are typed-checked here *)
-  let (j,cst) = safe_infer_type env_ar c in
+let type_one_constructor env_ar_par params arsort c =
+  let infos = infos_and_sort env_ar_par c in
+
+  (* Each constructor is typed-checked here *)
+  let (j,cst) = safe_infer_type env_ar_par c in
+  let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
 
   (* If the arity is at some level Type arsort, then the sort of the
      constructor must be below arsort; here we consider constructors with the
      global parameters (which add a priori more constraints on their sort) *)
   let cst2 = enforce_type_constructor arsort j.utj_type cst in
 
-  (infos, j.utj_val, cst2)
+  (infos, full_cstr_type, cst2)
 
-let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
-  let arsort = sort_of_arity env_ar ar in
+let infer_constructor_packet env_ar params short_arity arsort vc =
+  let env_ar_par = push_rels params env_ar in
   let (constrsinfos,jlc,cst) = 
     List.fold_right
-      (fun c (infosl,jl,cst) -> 
-	 let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
-	 (infos::infosl,jc::jl, Constraint.union cst cst'))
+      (fun c (infosl,l,cst) ->
+	 let (infos,ct,cst') =
+	   type_one_constructor env_ar_par params arsort c in
+	 (infos::infosl,ct::l, Constraint.union cst cst'))
       vc
-      ([],[],Constraint.empty)
-  in
+      ([],[],Constraint.empty) in
   let vc' = Array.of_list jlc in
-  let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
-  let (_,tyar) = lookup_rel_type (ninds+1-i) env_ar in
-  ((id,tyar,cnames,issmall,isunit,vc'), cst)
+  let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
+  (issmall,isunit,vc', cst)
 
 let add_mind sp mie env =
-  mind_check_names mie;
-  mind_check_arities env mie;
-  let params = mind_extract_and_check_params mie in
-  let nparams = mie.mind_entry_nparams in
-  mind_check_lc params mie;
-  let ninds = List.length mie.mind_entry_inds in
-  let types_sign = 
-    List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
-  in
-  (* Arities with params are typed-checked here *)
-  let env_arities = push_rels_with_univ types_sign env in
-  let env_params = push_rels params env_arities in
-  let _,inds,cst =
-    List.fold_right
-      (fun ind (i,inds,cst) -> 
-	 let (ind',cst') = 
-	   type_one_inductive i env_arities env_params nparams ninds ind 
+  mind_check_wellformed env mie;
+
+  (* We first type params and arity of each inductive definition *)
+  (* This allows to build the environment of arities and to share *)
+  (* the set of constraints *)
+  let cst, env_arities, rev_params_arity_list =
+    List.fold_left
+      (fun (cst,env_arities,l) ind ->
+         (* Params are typed-checked here *)
+	 let params = ind.mind_entry_params in
+	 let env_params, params, cst1 = safe_infer_local_decls env params in
+         (* Arities (without params) are typed-checked here *)
+	 let arity, cst2 = safe_infer_type env_params ind.mind_entry_arity in
+	 (* We do not need to generate the universe of full_arity; if
+	    later, after the validation of the inductive definition,
+	    full_arity is used as argument or subject to cast, an
+	    upper universe will be generated *)
+	 let id = ind.mind_entry_typename in
+	 let full_arity = it_mkProd_or_LetIn arity.utj_val params in
+	 Constraint.union cst (Constraint.union cst1 cst2),
+	 push_rel_assum (Name id, full_arity) env_arities,
+         (params, id, full_arity, arity.utj_val)::l)
+      (Constraint.empty,env,[])
+      mie.mind_entry_inds in
+
+  let params_arity_list = List.rev rev_params_arity_list in
+
+  (* Now, we type the constructors (without params) *)
+  let inds,cst =
+    List.fold_right2
+      (fun ind (params,id,full_arity,short_arity) (inds,cst) ->
+	 let arsort = sort_of_arity env full_arity in
+	 let lc = ind.mind_entry_lc in
+	 let (issmall,isunit,lc',cst') =
+	   infer_constructor_packet env_arities params short_arity arsort lc
 	 in
-	 (i-1,ind'::inds, Constraint.union cst cst'))
+	 let nparams = ind.mind_entry_nparams in
+	 let consnames = ind.mind_entry_consnames in
+	 let ind' = (nparams,id,full_arity,consnames,issmall,isunit,lc') in
+	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
-      (ninds,[],Constraint.empty) 
-  in
+      params_arity_list
+      ([],Constraint.empty) in
+
+  (* Finally, we build the inductive packet and push it to env *)
   let kind = kind_of_path sp in
-  let mib = 
-    cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
+  let mib = cci_inductive env env_arities kind mie.mind_entry_finite inds cst
   in
   add_mind sp mib (add_constraints cst env)