Extension du polymorphisme de sorte au cas des définitions dans Type.

(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)


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

15 files changed, 161 insertions, 74 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index dffbb76c09..68d301eb46 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -122,7 +122,14 @@ let cook_constant env r =
     on_body (fun c ->
       abstract_constant_body (expmod_constr r.d_modlist c) hyps) 
       cb.const_body in
-  let typ =
-    abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
+  let typ = match cb.const_type with
+    | NonPolymorphicType t ->
+	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	NonPolymorphicType typ
+    | PolymorphicArity (ctx,s) ->
+	let t = mkArity (ctx,Type s.poly_level) in
+	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	let ctx,_ = dest_prod env typ in
+	PolymorphicArity (ctx,s) in
   let boxed = Cemitcodes.is_boxed cb.const_body_code in
   (body, typ, cb.const_constraints, cb.const_opaque, boxed)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 2e7a3639a2..0646b1c222 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -25,7 +25,7 @@ type recipe = {
 
 val cook_constant :
   env -> recipe -> 
-    constr_substituted option * constr * constraints * bool * bool
+    constr_substituted option * constant_type * constraints * bool * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 17a8d5ac9b..d0f2289dc4 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -25,6 +25,15 @@ type engagement = ImpredicativeSet
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
+type polymorphic_arity = {
+  poly_param_levels : universe option list;
+  poly_level : universe;
+}
+
+type constant_type =
+  | NonPolymorphicType of types
+  | PolymorphicArity of rel_context * polymorphic_arity
+
 type constr_substituted = constr substituted
 
 let from_val = from_val
@@ -36,7 +45,7 @@ let subst_constr_subst = subst_substituted
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
-    const_type : types;  
+    const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
@@ -90,11 +99,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
 *)
 
-type polymorphic_inductive_arity = {
-  mind_param_levels : universe option list;
-  mind_level : universe;
-}
-
 type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
@@ -102,7 +106,7 @@ type monomorphic_inductive_arity = {
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_inductive_arity
+| Polymorphic of polymorphic_arity
 
 type one_inductive_body = {
 
@@ -186,11 +190,15 @@ type mutual_inductive_body = {
     mind_equiv : kernel_name option
   }
 
+let subst_arity sub = function
+| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
+| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_body = option_map (subst_constr_subst sub) cb.const_body;
-    const_type = subst_mps sub cb.const_type;
+    const_type = subst_arity sub cb.const_type;
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2cbdc3eb39..22cfd62a0c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -26,6 +26,15 @@ type engagement = ImpredicativeSet
 (**********************************************************************)
 (*s Representation of constants (Definition/Axiom)                    *)
 
+type polymorphic_arity = {
+  poly_param_levels : universe option list;
+  poly_level : universe;
+}
+
+type constant_type =
+  | NonPolymorphicType of types
+  | PolymorphicArity of rel_context * polymorphic_arity
+
 type constr_substituted
 
 val from_val : constr -> constr_substituted
@@ -34,7 +43,7 @@ val force : constr_substituted -> constr
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
-    const_type : types;  
+    const_type : constant_type;
     const_body_code : to_patch_substituted;
    (*i const_type_code : to_patch;i*)
     const_constraints : constraints;
@@ -70,11 +79,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 \end{verbatim}
 *)
 
-type polymorphic_inductive_arity = {
-  mind_param_levels : universe option list;
-  mind_level : universe;
-}
-
 type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
@@ -82,7 +86,7 @@ type monomorphic_inductive_arity = {
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_inductive_arity
+| Polymorphic of polymorphic_arity
 
 type one_inductive_body = {
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b6d9bf6d38..5fa5f56740 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -129,7 +129,7 @@ type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value     : env -> constant -> constr
-val constant_type      : env -> constant -> types
+val constant_type      : env -> constant -> constant_type
 val constant_opt_value : env -> constant -> constr option
 
 (************************************************************************)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a41cc53beb..4187b8bd66 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -392,7 +392,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   let specif = lookup_mind_specif env mi in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive specif) lpar) env in
+              hnf_prod_applist env (type_of_inductive env specif) lpar) env in
   let ra_env' = 
     (Imbr mi,Rtree.mk_param 0) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -601,8 +601,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let arkind,kelim = match ar_kind with
     | Inr (param_levels,lev) ->
 	Polymorphic {
-	  mind_param_levels = param_levels;
-	  mind_level = lev; 
+	  poly_param_levels = param_levels;
+	  poly_level = lev; 
 	}, all_sorts
     | Inl ((issmall,isunit),ar,s) ->
 	let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bce14dc27f..7dd9aa7864 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -177,10 +177,10 @@ let rec make_subst env = function
   | [], _, _ ->
       assert false
 
-let instantiate_universes env ctx mip ar argsorts =
+let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
-  let ctx,subst = make_subst env (ctx,ar.mind_param_levels,args) in
-  let level = subst_large_constraints subst ar.mind_level in
+  let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
+  let level = subst_large_constraints subst ar.poly_level in
   ctx,
   if is_empty_univ level then mk_Prop
   else if is_base_univ level then mk_Set
@@ -192,9 +192,14 @@ let type_of_inductive_knowing_parameters env mip paramtyps =
       s.mind_user_arity
   | Polymorphic ar ->
       let ctx = List.rev mip.mind_arity_ctxt in
-      let ctx,s = instantiate_universes env ctx mip ar paramtyps in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
       mkArity (List.rev ctx,s)
 
+(* Type of a (non applied) inductive type *)
+
+let type_of_inductive env (_,mip) =
+  type_of_inductive_knowing_parameters env mip [||]
+
 (* The max of an array of universes *)
 
 let cumulate_constructor_univ u = function
@@ -205,20 +210,6 @@ let cumulate_constructor_univ u = function
 let max_inductive_sort =
   Array.fold_left cumulate_constructor_univ neutral_univ
 
-(* Type of a (non applied) inductive type *)
-
-let type_of_inductive (mib,mip) =
-  match mip.mind_arity with
-  | Monomorphic s -> s.mind_user_arity
-  | Polymorphic s ->
-      let s =
-        if mib.mind_nparams = 0 then 
-          if is_empty_univ s.mind_level then mk_Prop
-          else if is_base_univ s.mind_level then mk_Set
-          else Type s.mind_level
-        else Type s.mind_level in
-      mkArity (mip.mind_arity_ctxt,s)
-
 (************************************************************************)
 (* Type of a constructor *)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index deca20a6ba..9c75829d5b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -37,7 +37,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (*s Functions to build standard types related to inductive *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
 
-val type_of_inductive : mind_specif -> types
+val type_of_inductive : env -> mind_specif -> types
 
 val elim_sorts : mind_specif -> sorts_family list
 
@@ -84,6 +84,9 @@ val set_inductive_level : env -> sorts -> types -> types
 
 val max_inductive_sort : sorts array -> universe
 
+val instantiate_universes : env -> Sign.rel_context ->
+    polymorphic_arity -> types array -> Sign.rel_context * sorts
+
 (***************************************************************)
 (* Debug *)
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index efbee6af2b..785778235f 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -87,8 +87,8 @@ and merge_with env mtb with_decl =
 		match cb.const_body with
 		  | None -> 
 		      let (j,cst1) = Typeops.infer env' c in
-		      let cst2 = 
-			Reduction.conv_leq env' j.uj_type cb.const_type in
+		      let typ = Typeops.type_of_constant_type env' cb.const_type in
+		      let cst2 = Reduction.conv_leq env' j.uj_type typ in
 		      let cst = 
 			Constraint.union 
 			  (Constraint.union cb.const_constraints cst1)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 264bd62150..9cfce43037 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -119,6 +119,12 @@ type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
+let hcons_constant_type = function
+  | NonPolymorphicType t ->
+      NonPolymorphicType (hcons1_constr t)
+  | PolymorphicArity (ctx,s) ->
+      PolymorphicArity (map_rel_context hcons1_constr ctx,s)
+
 let hcons_constant_body cb =
   let body = match cb.const_body with
       None -> None
@@ -127,7 +133,7 @@ let hcons_constant_body cb =
   in
     { cb with
 	const_body = body;
-	const_type = hcons1_constr cb.const_type }
+	const_type = hcons_constant_type cb.const_type }
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c94219316b..12c7144114 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -96,7 +96,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2))
+      let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
@@ -164,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
    | Constant cb1 ->
       assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
       (*Start by checking types*)
-      let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_conv cst conv_leq env typ1 typ2 in
       let con = make_con (MPself msid1) empty_dirpath l in
       let cst =
        match cb2.const_body with
@@ -186,8 +188,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
-      let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv_leq env arity1 cb2.const_type
+      let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -197,7 +200,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv env ty1 cb2.const_type
+      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv env ty1 ty2
    | _ -> error ()
 	      
 let rec check_modules cst env msid1 l msb1 msb2 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f76c5ffe33..94cd397607 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,8 +22,35 @@ open Type_errors
 open Indtypes
 open Typeops
 
+let extract_level env p =
+  let _,c = dest_prod_assum env p in
+  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+
+let extract_context_levels env =
+  List.fold_left
+    (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
+
+let make_polymorphic_if_arity env t =
+  let params, ccl = dest_prod env t in
+  match kind_of_term ccl with
+  | Sort (Type u) -> 
+      let param_ccls = extract_context_levels env params in
+      let s = { poly_param_levels = param_ccls; poly_level = u} in
+      PolymorphicArity (params,s)
+  | _ -> NonPolymorphicType t
+
 let constrain_type env j cst1 = function
-  | None -> j.uj_type, cst1
+  | None ->
+      make_polymorphic_if_arity env j.uj_type, cst1
+  | Some t -> 
+      let (tj,cst2) = infer_type env t in
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
+      assert (t = tj.utj_val);
+      make_polymorphic_if_arity env t, Constraint.union (Constraint.union cst1 cst2) cst3
+
+let local_constrain_type env j cst1 = function
+  | None ->
+      j.uj_type, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
@@ -32,7 +59,7 @@ let constrain_type env j cst1 = function
 
 let translate_local_def env (b,topt) =
   let (j,cst) = infer env b in
-  let (typ,cst) = constrain_type env j cst topt in
+  let (typ,cst) = local_constrain_type env j cst topt in
     (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
@@ -83,16 +110,25 @@ let infer_declaration env dcl =
         c.const_entry_opaque, c.const_entry_boxed
   | ParameterEntry t ->
       let (j,cst) = infer env t in
-      None, Typeops.assumption_of_judgment env j, cst, false, false
+      None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
+        false, false
+
+let global_vars_set_constant_type env = function
+  | NonPolymorphicType t -> global_vars_set env t
+  | PolymorphicArity (ctx,_) ->
+      Sign.fold_rel_context 
+        (fold_rel_declaration
+	  (fun t c -> Idset.union (global_vars_set env t) c))
+      ctx ~init:Idset.empty
 
 let build_constant_declaration env kn (body,typ,cst,op,boxed) =
   let ids =
     match body with 
-    | None -> global_vars_set env typ
+    | None -> global_vars_set_constant_type env typ
     | Some b ->
         Idset.union 
 	  (global_vars_set env (Declarations.force b)) 
-	  (global_vars_set env typ)
+	  (global_vars_set_constant_type env typ)
   in
   let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
   let hyps = keep_hyps env ids in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6fac9e0507..83434e2ec8 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -26,12 +26,11 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry -> 
-   Declarations.constr_substituted option * Term.types * Univ.constraints *
-    bool * bool
+   constr_substituted option * constant_type * constraints * bool * bool
 
-val build_constant_declaration : env ->    'a ->
-    Declarations.constr_substituted option * Term.types * Univ.constraints *
-    bool * bool -> Declarations.constant_body
+val build_constant_declaration : env -> 'a ->
+    constr_substituted option * constant_type * constraints * bool * bool ->
+      constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0d2874cb76..3c335d115b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -126,12 +126,31 @@ let check_hyps id env hyps =
 (* Instantiation of terms on real arguments. *)
 
 (* Type of constants *)
+
+let type_of_constant_knowing_parameters env t paramtyps =
+  match t with
+  | NonPolymorphicType t -> t
+  | PolymorphicArity (sign,ar) ->
+      let ctx = List.rev sign in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+let type_of_constant_type env t =
+  type_of_constant_knowing_parameters env t [||]
+
+let type_of_constant env cst =
+  type_of_constant_type env (constant_type env cst)
+
+let judge_of_constant_knowing_parameters env cst jl =
+  let c = mkConst cst in
+  let cb = lookup_constant cst env in
+  let _ = check_args env c cb.const_hyps in 
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in
+  make_judge c t
+
 let judge_of_constant env cst =
-  let constr = mkConst cst in
-  let _ =
-    let ce = lookup_constant cst env in
-    check_args env constr ce.const_hyps in 
-  make_judge constr (constant_type env cst)
+  judge_of_constant_knowing_parameters env cst [||]
 
 (* Type of a lambda-abstraction. *)
 
@@ -348,11 +367,16 @@ let rec execute env cstr cu =
     | App (f,args) ->
         let (jl,cu1) = execute_array env args cu in
 	let (j,cu2) =
-	  if isInd f then
-	    (* Sort-polymorphism of inductive types *)
-	    judge_of_inductive_knowing_parameters env (destInd f) jl, cu1
-	  else
-	    execute env f cu1
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+		judge_of_inductive_knowing_parameters env ind jl, cu1
+	    | Const cst -> 
+		(* Sort-polymorphism of constant *)
+		judge_of_constant_knowing_parameters env cst jl, cu1
+	    | _ -> 
+		(* No sort-polymorphism *)
+		execute env f cu1
 	in
 	univ_combinator cu2 (judge_of_apply env j jl)
 	    
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index aeb4d294bc..43d7b33db7 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -14,6 +14,7 @@ open Univ
 open Term
 open Environ
 open Entries
+open Declarations
 (*i*)
 
 (*s Typing functions (not yet tagged as safe) *)
@@ -47,6 +48,9 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 (*s type of a constant *)
 val judge_of_constant : env -> constant -> unsafe_judgment
 
+val judge_of_constant_knowing_parameters :
+  env -> constant -> unsafe_judgment array -> unsafe_judgment
+
 (*s Type of application. *)
 val judge_of_apply : 
   env -> unsafe_judgment -> unsafe_judgment array
@@ -93,8 +97,9 @@ val type_fixpoint : env -> name array -> types array
 (* Kernel safe typing but applicable to partial proofs *)
 val typing : env -> constr -> unsafe_judgment
 
-(* A virer *)
-val execute : Environ.env ->
-    Term.types ->
-    Univ.Constraint.t * Univ.universes ->
-    Environ.unsafe_judgment * (Univ.Constraint.t * Univ.universes)
+val type_of_constant : env -> constant -> types
+
+val type_of_constant_type : env -> constant_type -> types
+
+val type_of_constant_knowing_parameters : 
+  env -> constant_type -> constr array -> types