Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 32 insertions, 33 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 779a427a..8299a3c9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typeops.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: typeops.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Util
 open Names
@@ -245,14 +245,28 @@ let judge_of_cast env cj k tj =
 
 (* Inductive types. *)
 
-let judge_of_inductive env i =
-  let constr = mkInd i in
-  let _ =
-    let (kn,_) = i in
-    let mib = lookup_mind kn env in
-    check_args env constr mib.mind_hyps in 
-  let specif = lookup_mind_specif env i in
-  make_judge constr (type_of_inductive specif)
+(* The type is parametric over the uniform parameters whose conclusion
+   is in Type; to enforce the internal constraints between the
+   parameters and the instances of Type occurring in the type of the
+   constructors, we use the level variables _statically_ assigned to
+   the conclusions of the parameters as mediators: e.g. if a parameter
+   has conclusion Type(alpha), static constraints of the form alpha<=v
+   exist between alpha and the Type's occurring in the constructor
+   types; when the parameters is finally instantiated by a term of
+   conclusion Type(u), then the constraints u<=alpha is computed in
+   the App case of execute; from this constraints, the expected
+   dynamic constraints of the form u<=v are enforced *)
+
+let judge_of_inductive_knowing_parameters env ind jl =
+  let c = mkInd ind in
+  let (mib,mip) = lookup_mind_specif env ind in
+  check_args env c mib.mind_hyps;
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in
+  make_judge c t
+
+let judge_of_inductive env ind =
+  judge_of_inductive_knowing_parameters env ind [||]
 
 (* Constructors. *)
 
@@ -334,14 +348,15 @@ let rec execute env cstr cu =
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-	let (j,cu1) = execute env f cu in
-        let (jl,cu2) = execute_array env args cu1 in
-	let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in
-	if isInd f then
-	  (* Sort-polymorphism of inductive types *)
-	  adjust_inductive_level env (destInd f) args (j',cu)
-	else
-	  (j',cu)
+        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
+	in
+	univ_combinator cu2 (judge_of_apply env j jl)
 	    
     | Lambda (name,c1,c2) -> 
         let (varj,cu1) = execute_type env c1 cu in
@@ -421,22 +436,6 @@ and execute_array env = array_fold_map' (execute env)
 
 and execute_list env = list_fold_map' (execute env) 
 
-and adjust_inductive_level env ind args (j,cu) =
-  let specif = lookup_mind_specif env ind in
-  if is_small_inductive specif then
-    (* No polymorphism *)
-    (j,cu)
-  else
-    (* Retyping constructor with the actual arguments *)
-    let env',llc,ls0 = constructor_instances env specif ind args in
-    let (llj,cu1) = array_fold_map' (execute_array env') llc cu in
-    let ls =
-      Array.map (fun lj ->
-	max_inductive_sort (Array.map (sort_judgment env) lj)) llj
-    in
-    let s = find_inductive_level env specif ind ls0 ls in
-    (on_judgment_type (set_inductive_level env s) j, cu1)
-
 (* Derived functions *)
 let infer env constr =
   let (j,(cst,_)) =