From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/typeops.ml | 158 ++++++++++++++++++++++++++---------------------------- 1 file changed, 75 insertions(+), 83 deletions(-) (limited to 'kernel/typeops.ml') 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,_)) = -- cgit v1.2.3