Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 75 insertions, 83 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 66b2e24d..779a427a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typeops.ml,v 1.89.2.1 2004/07/16 19:30:28 herbelin Exp $ *)
+(* $Id: typeops.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
 
 open Util
 open Names
@@ -19,11 +19,24 @@ open Entries
 open Reduction
 open Inductive
 open Type_errors
-
+  
+let conv = default_conv CONV
+let conv_leq = default_conv CUMUL
+
+let conv_leq_vecti env v1 v2 =
+  array_fold_left2_i 
+    (fun i c t1 t2 ->
+      let c' =
+        try default_conv CUMUL env t1 t2 
+        with NotConvertible -> raise (NotConvertibleVect i) in
+      Constraint.union c c')
+    Constraint.empty
+    v1
+    v2
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
-  match kind_of_term(whd_betadeltaiota env (body_of_type j.uj_type)) with
+  match kind_of_term(whd_betadeltaiota env j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
@@ -34,11 +47,9 @@ let assumption_of_judgment env j =
   with TypeError _ ->
     error_assumption env j
 
-(*
-let aojkey = Profile.declare_profile "assumption_of_judgment";;
-let assumption_of_judgment env j
-  = Profile.profile2 aojkey assumption_of_judgment env j;;
-*)
+let sort_judgment env j = (type_judgment env j).utj_type
+
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
 (************************************************)
 (* Incremental typing rules: builds a typing judgement given the *)
@@ -49,11 +60,11 @@ let assumption_of_judgment env j
 (* Prop and Set *)
 
 let judge_of_prop =
-  { uj_val = body_of_type mkProp;
+  { uj_val = mkProp;
     uj_type = mkSort type_0 }
 
 let judge_of_set =
-  { uj_val = body_of_type mkSet;
+  { uj_val = mkSet;
     uj_type = mkSort type_0 }
 
 let judge_of_prop_contents = function
@@ -64,7 +75,7 @@ let judge_of_prop_contents = function
 
 let judge_of_type u =
   let uu = super u in
-  { uj_val = body_of_type (mkType u);
+  { uj_val = mkType u;
     uj_type = mkType uu }
 
 (*s Type of a de Bruijn index. *)
@@ -77,30 +88,23 @@ let judge_of_relative env n =
   with Not_found -> 
     error_unbound_rel env n
 
-(*
-let relativekey = Profile.declare_profile "judge_of_relative";;
-let judge_of_relative env n =
-  Profile.profile2 relativekey judge_of_relative env n;;
-*)
-
 (* Type of variables *)
 let judge_of_variable env id =
   try
-    let (_,_,ty) = lookup_named id env in
+    let ty = named_type id env in
     make_judge (mkVar id) ty
   with Not_found -> 
     error_unbound_var env id
 
 (* Management of context of variables. *)
 
-(* Checks if a context of variable can be instanciated by the
+(* Checks if a context of variable can be instantiated by the
    variables of the current env *)
 (* TODO: check order? *)
 let rec check_hyps_inclusion env sign =
-  let env_sign = named_context env in
   Sign.fold_named_context
     (fun (id,_,ty1) () ->
-      let (_,_,ty2) = Sign.lookup_named id env_sign in
+      let ty2 = named_type id env in
       if not (eq_constr ty2 ty1) then
         error "types do not match")
     sign
@@ -108,7 +112,6 @@ let rec check_hyps_inclusion env sign =
 
 
 let check_args env c hyps =
-  let hyps' = named_context env in
   try check_hyps_inclusion env hyps
   with UserError _ | Not_found ->
     error_reference_variables env c
@@ -132,12 +135,6 @@ let judge_of_constant env cst =
     check_args env constr ce.const_hyps in 
   make_judge constr (constant_type env cst)
 
-(*
-let tockey = Profile.declare_profile "type_of_constant";;
-let type_of_constant env c 
-  = Profile.profile3 tockey type_of_constant env c;;
-*)
-
 (* Type of a lambda-abstraction. *)
 
 (* [judge_of_abstraction env name var j] implements the rule
@@ -203,9 +200,11 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          domsort
+          Type (sup u1 base_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop _,  Type _)  -> rangsort
+    | (Prop Pos,  Type u2)  -> Type (sup base_univ u2)
+    (* Product rule (Prop,Type_i,Type_i) *)
+    | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
     | (Type u1, Type u2) -> Type (sup u1 u2)
 
@@ -231,11 +230,14 @@ let judge_of_product env name t1 t2 =
          env |- c:typ2
 *)
 
-let judge_of_cast env cj tj =
+let judge_of_cast env cj k tj =
   let expected_type = tj.utj_val in
   try 
-    let cst = conv_leq env cj.uj_type expected_type in
-    { uj_val = mkCast (j_val cj, expected_type);
+    let cst = 
+      match k with
+      | VMcast -> vm_conv CUMUL env cj.uj_type expected_type
+      | DEFAULTcast -> conv_leq env cj.uj_type expected_type in
+    { uj_val = mkCast (cj.uj_val, k, expected_type);
       uj_type = expected_type },
     cst
   with NotConvertible ->
@@ -249,13 +251,8 @@ let judge_of_inductive env i =
     let (kn,_) = i in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_inductive env i)
-
-(*
-let toikey = Profile.declare_profile "judge_of_inductive";;
-let judge_of_inductive env i
-  = Profile.profile2 toikey judge_of_inductive env i;;
-*)
+  let specif = lookup_mind_specif env i in
+  make_judge constr (type_of_inductive specif)
 
 (* Constructors. *)
 
@@ -265,21 +262,16 @@ let judge_of_constructor env c =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_constructor env c)
-
-(*
-let tockey = Profile.declare_profile "judge_of_constructor";;
-let judge_of_constructor env cstr
-  = Profile.profile2 tockey judge_of_constructor env cstr;;
-*)
+  let specif = lookup_mind_specif env (inductive_of_constructor c) in
+  make_judge constr (type_of_constructor c specif)
 
 (* Case. *)
 
-let check_branch_types env cj (lft,explft) = 
-  try conv_leq_vecti env lft explft
+let check_branch_types env cj (lfj,explft) = 
+  try conv_leq_vecti env (Array.map j_type lfj) explft
   with
       NotConvertibleVect i ->
-        error_ill_formed_branch env cj.uj_val i lft.(i) explft.(i)
+        error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i)
     | Invalid_argument _ ->
         error_number_branches env cj (Array.length explft)
 
@@ -290,20 +282,12 @@ let judge_of_case env ci pj cj lfj =
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in
-  let (_,kind) = dest_arity env pj.uj_type in
-  let lft = Array.map j_type lfj in
-  let univ' = check_branch_types env cj (lft,bty) in
+  let univ' = check_branch_types env cj (lfj,bty) in
   ({ uj_val  = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
                        Array.map j_val lfj);
      uj_type = rslty },
   Constraint.union univ univ')
 
-(*
-let tocasekey = Profile.declare_profile "judge_of_case";;
-let judge_of_case env ci pj cj lfj
-  = Profile.profile6 tocasekey judge_of_case env ci pj cj lfj;;
-*)
-
 (* Fixpoints. *)
 
 (* Checks the type of a general (co)fixpoint, i.e. without checking *)
@@ -313,9 +297,7 @@ let type_fixpoint env lna lar vdefj =
   let lt = Array.length vdefj in
   assert (Array.length lar = lt);
   try
-    conv_leq_vecti env
-      (Array.map (fun j -> body_of_type j.uj_type) vdefj)
-      (Array.map (fun ty -> lift lt ty) lar)
+    conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar)
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna vdefj lar
 
@@ -354,8 +336,12 @@ let rec execute env cstr cu =
     | App (f,args) ->
 	let (j,cu1) = execute env f cu in
         let (jl,cu2) = execute_array env args cu1 in
-	univ_combinator cu2
-	  (judge_of_apply env j jl)
+	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)
 	    
     | Lambda (name,c1,c2) -> 
         let (varj,cu1) = execute_type env c1 cu in
@@ -372,16 +358,17 @@ let rec execute env cstr cu =
     | LetIn (name,c1,c2,c3) ->
         let (j1,cu1) = execute env c1 cu in
         let (j2,cu2) = execute_type env c2 cu1 in
-        let (_,cu3) = univ_combinator cu2 (judge_of_cast env j1 j2) in
+        let (_,cu3) = 
+	  univ_combinator cu2 (judge_of_cast env j1 DEFAULTcast j2) in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let (j',cu4) = execute env1 c3 cu3 in
         (judge_of_letin env name j1 j2 j', cu4)
 	  
-    | Cast (c,t) ->
+    | Cast (c,k, t) ->
         let (cj,cu1) = execute env c cu in
         let (tj,cu2) = execute_type env t cu1 in
 	univ_combinator cu2
-          (judge_of_cast env cj tj)
+          (judge_of_cast env cj k tj)
 
     (* Inductive types *)
     | Ind ind ->
@@ -430,27 +417,32 @@ and execute_recdef env (names,lar,vdef) i cu =
   univ_combinator cu2
     ((lara.(i),(names,lara,vdefv)),cst)
 
-and execute_array env v cu =
-  let (jl,cu1) = execute_list env (Array.to_list v) cu in
-  (Array.of_list jl, cu1)
-
-and execute_list env l cu =
-  match l with
-  | [] -> 
-      ([], cu)
-  | c::r -> 
-      let (j,cu1) = execute env c cu in 
-      let (jr,cu2) = execute_list env r cu1 in
-      (j::jr, cu2)
+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,_)) =
     execute env constr (Constraint.empty, universes env) in
-  let j = if j.uj_val = constr then { j with uj_val = constr } else
-    (error "Kernel built a body different from its input\n";
-     flush stdout; j) in
-  (j, cst)
+  assert (j.uj_val = constr);
+  ({ j with uj_val = constr }, cst)
 
 let infer_type env constr =
   let (j,(cst,_)) =