diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 363 |
1 files changed, 170 insertions, 193 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 3400d8ce6..09fd4cc7f 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -20,19 +20,21 @@ open Reduction open Inductive open Type_errors -let conv_leq l2r = default_conv CUMUL ~l2r +let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y 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 - union_constraints c c') - empty_constraint + (fun i _ t1 t2 -> + try conv_leq false env t1 t2 + with NotConvertible -> raise (NotConvertibleVect i)) + () v1 v2 +let check_constraints cst env = + if Environ.check_constraints cst env then () + else error_unsatisfied_constraints env cst + (* 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 j.uj_type) with @@ -69,9 +71,9 @@ let judge_of_prop_contents = function (* Type of Type(i). *) let judge_of_type u = - let uu = super u in - { uj_val = mkType u; - uj_type = mkType uu } + let uu = Universe.super u in + { uj_val = mkType u; + uj_type = mkType uu } (*s Type of a de Bruijn index. *) @@ -111,53 +113,32 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -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 l = - let fold l (_, b, p) = match b with - | None -> extract_level env p :: l - | _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> - 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 - (* 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 = constant_type env cst +let type_of_constant_in env cst = constant_type_in env cst +let type_of_constant_knowing_parameters env t _ = t +let type_of_constant_type env cst = cst -let type_of_constant env cst = - type_of_constant_type env (constant_type env cst) +let judge_of_constant env (kn,u as cst) = + let c = mkConstU cst in + let cb = lookup_constant kn env in + let _ = check_hyps_inclusion env c cb.const_hyps in + let ty, cu = type_of_constant env cst in + let _ = Environ.check_constraints cu env in + (make_judge c ty) -let judge_of_constant_knowing_parameters env cst jl = - let c = mkConst cst in +let type_of_projection env (cst,u) = let cb = lookup_constant cst env in - let _ = check_hyps_inclusion env c cb.const_hyps in - let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in - make_judge c t + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in + let subst = make_inductive_subst mib u in + Vars.subst_univs_constr subst pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] (* Type of a lambda-abstraction. *) @@ -184,26 +165,27 @@ let judge_of_letin env name defj typj j = (* Type of an application. *) let judge_of_apply env funj argjv = - let len = Array.length argjv in - let rec apply_rec n typ cst = - if len <= n then - { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ }, - cst - else - let hj = Array.unsafe_get argjv n in - match kind_of_term (whd_betadeltaiota env typ) with - | Prod (_,c1,c2) -> - let c = - try conv_leq false env hj.uj_type c1 - with NotConvertible -> - error_cant_apply_bad_type env (n + 1, c1, hj.uj_type) funj argjv - in - let cst' = union_constraints cst c in - apply_rec (n+1) (subst1 hj.uj_val c2) cst' - | _ -> - error_cant_apply_not_functional env funj argjv + let rec apply_rec n typ = function + | [] -> + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } + | hj::restjl -> + (match kind_of_term (whd_betadeltaiota env typ) with + | Prod (_,c1,c2) -> + (try + let () = conv_leq false env hj.uj_type c1 in + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + with NotConvertible -> + error_cant_apply_bad_type env + (n,c1, hj.uj_type) + funj argjv) + + | _ -> + error_cant_apply_not_functional env funj argjv) in - apply_rec 0 funj.uj_type empty_constraint + apply_rec 1 + funj.uj_type + (Array.to_list argjv) (* Type of product *) @@ -221,14 +203,14 @@ let sort_of_product env domsort rangsort = rangsort | _ -> (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (sup u1 type0_univ) + Type (Universe.sup Universe.type0 u1) end (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (sup type0_univ u2) + | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 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) + | (Type u1, Type u2) -> Type (Universe.sup u1 u2) (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule @@ -262,18 +244,17 @@ let judge_of_cast env cj k tj = vm_conv CUMUL env cj.uj_type expected_type | DEFAULTcast -> mkCast (cj.uj_val, k, expected_type), - conv_leq false env cj.uj_type expected_type + default_conv ~l2r:false CUMUL env cj.uj_type expected_type | REVERTcast -> cj.uj_val, - conv_leq true env cj.uj_type expected_type + default_conv ~l2r:true CUMUL env cj.uj_type expected_type | NATIVEcast -> let sigma = Nativelambda.empty_evars in mkCast (cj.uj_val, k, expected_type), native_conv CUMUL sigma env cj.uj_type expected_type in - { uj_val = c; - uj_type = expected_type }, - cst + { uj_val = c; + uj_type = expected_type } with NotConvertible -> error_actual_type env cj expected_type @@ -291,50 +272,70 @@ let judge_of_cast env cj k tj = 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 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 = in *) +(* make_judge c t *) + +let judge_of_inductive env (ind,u as indu) = + let c = mkIndU indu in let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env c mib.mind_hyps; - let paramstyp = Array.map (fun j -> lazy 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 [||] + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + (make_judge c t) (* Constructors. *) -let judge_of_constructor env c = - let constr = mkConstruct c in +let judge_of_constructor env (c,u as cu) = + let constr = mkConstructU cu in let _ = let ((kn,_),_) = c in let mib = lookup_mind kn env in check_hyps_inclusion env constr mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in - make_judge constr (type_of_constructor c specif) + let t,cst = constrained_type_of_constructor cu specif in + let () = check_constraints cst env in + (make_judge constr t) (* Case. *) -let check_branch_types env ind cj (lfj,explft) = +let check_branch_types env (ind,u) 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 (ind,i+1) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) | Invalid_argument _ -> error_number_branches env cj (Array.length explft) let judge_of_case env ci pj cj lfj = - let indspec = + let (pind, _ as indspec) = try find_rectype env cj.uj_type with Not_found -> error_case_not_inductive env cj in - let _ = check_case_info env (fst indspec) ci in - let (bty,rslty,univ) = + let _ = check_case_info env pind ci in + let (bty,rslty) = type_case_branches env indspec pj cj.uj_val in - let univ' = check_branch_types env (fst indspec) cj (lfj,bty) in + let () = check_branch_types env pind cj (lfj,bty) in ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty }, - union_constraints univ univ') + uj_type = rslty }) + +let judge_of_projection env p cj = + let pb = lookup_projection p env in + let (ind,u), args = + try find_rectype env cj.uj_type + with Not_found -> error_case_not_inductive env cj + in + assert(eq_mind pb.proj_ind (fst ind)); + let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in + let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in + let ty = substl (cj.uj_val :: List.rev args) ty in + (* TODO: Universe polymorphism for projections *) + {uj_val = mkProj (p,cj.uj_val); + uj_type = ty} (* Fixpoints. *) @@ -352,104 +353,88 @@ let type_fixpoint env lna lar vdefj = (************************************************************************) (************************************************************************) -(* This combinator adds the universe constraints both in the local - graph and in the universes of the environment. This is to ensure - that the infered local graph is satisfiable. *) -let univ_combinator (cst,univ) (j,c') = - (j,(union_constraints cst c', merge_constraints c' univ)) - (* The typing machine. *) (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) -let rec execute env cstr cu = +let rec execute env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - (judge_of_prop_contents c, cu) - + judge_of_prop_contents c + | Sort (Type u) -> - (judge_of_type u, cu) + judge_of_type u | Rel n -> - (judge_of_relative env n, cu) + judge_of_relative env n | Var id -> - (judge_of_variable env id, cu) + judge_of_variable env id | Const c -> - (judge_of_constant env c, cu) + judge_of_constant env c + + | Proj (p, c) -> + let cj = execute env c in + judge_of_projection env p cj (* Lambda calculus operators *) | App (f,args) -> - let (jl,cu1) = execute_array env args cu in - let (j,cu2) = - 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) + let jl = execute_array env args in + let j = execute env f in + judge_of_apply env j jl | Lambda (name,c1,c2) -> - let (varj,cu1) = execute_type env c1 cu in - let env1 = push_rel (name,None,varj.utj_val) env in - let (j',cu2) = execute env1 c2 cu1 in - (judge_of_abstraction env name varj j', cu2) + let varj = execute_type env c1 in + let env1 = push_rel (name,None,varj.utj_val) env in + let j' = execute env1 c2 in + judge_of_abstraction env name varj j' | Prod (name,c1,c2) -> - let (varj,cu1) = execute_type env c1 cu in - let env1 = push_rel (name,None,varj.utj_val) env in - let (varj',cu2) = execute_type env1 c2 cu1 in - (judge_of_product env name varj varj', cu2) + let varj = execute_type env c1 in + let env1 = push_rel (name,None,varj.utj_val) env in + let varj' = execute_type env1 c2 in + judge_of_product env name varj varj' | 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 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) + let j1 = execute env c1 in + let j2 = execute_type env c2 in + let _ = judge_of_cast env j1 DEFAULTcast j2 in + let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in + let j' = execute env1 c3 in + judge_of_letin env name j1 j2 j' | 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 k tj) + let cj = execute env c in + let tj = execute_type env t in + judge_of_cast env cj k tj (* Inductive types *) | Ind ind -> - (judge_of_inductive env ind, cu) + judge_of_inductive env ind | Construct c -> - (judge_of_constructor env c, cu) + judge_of_constructor env c | Case (ci,p,c,lf) -> - let (cj,cu1) = execute env c cu in - let (pj,cu2) = execute env p cu1 in - let (lfj,cu3) = execute_array env lf cu2 in - univ_combinator cu3 - (judge_of_case env ci pj cj lfj) + let cj = execute env c in + let pj = execute env p in + let lfj = execute_array env lf in + judge_of_case env ci pj cj lfj | Fix ((vn,i as vni),recdef) -> - let ((fix_ty,recdef'),cu1) = execute_recdef env recdef i cu in - let fix = (vni,recdef') in + let (fix_ty,recdef') = execute_recdef env recdef i in + let fix = (vni,recdef') in check_fix env fix; - (make_judge (mkFix fix) fix_ty, cu1) - + make_judge (mkFix fix) fix_ty + | CoFix (i,recdef) -> - let ((fix_ty,recdef'),cu1) = execute_recdef env recdef i cu in - let cofix = (i,recdef') in + let (fix_ty,recdef') = execute_recdef env recdef i in + let cofix = (i,recdef') in check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty, cu1) - + (make_judge (mkCoFix cofix) fix_ty) + (* Partial proofs: unsupported by the kernel *) | Meta _ -> anomaly (Pp.str "the kernel does not support metavariables") @@ -457,61 +442,53 @@ let rec execute env cstr cu = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_type env constr cu = - let (j,cu1) = execute env constr cu in - (type_judgment env j, cu1) +and execute_type env constr = + let j = execute env constr in + type_judgment env j -and execute_recdef env (names,lar,vdef) i cu = - let (larj,cu1) = execute_array env lar cu in +and execute_recdef env (names,lar,vdef) i = + let larj = execute_array env lar in let lara = Array.map (assumption_of_judgment env) larj in let env1 = push_rec_types (names,lara,vdef) env in - let (vdefj,cu2) = execute_array env1 vdef cu1 in + let vdefj = execute_array env1 vdef in let vdefv = Array.map j_val vdefj in - let cst = type_fixpoint env1 names lara vdefj in - univ_combinator cu2 - ((lara.(i),(names,lara,vdefv)),cst) + let () = type_fixpoint env1 names lara vdefj in + (lara.(i),(names,lara,vdefv)) -and execute_array env = Array.fold_map' (execute env) +and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let (j,(cst,_)) = - execute env constr (empty_constraint, universes env) in - assert (eq_constr j.uj_val constr); - (j, cst) + let j = execute env constr in + assert (eq_constr j.uj_val constr); + j + +(* let infer_key = Profile.declare_profile "infer" *) +(* let infer = Profile.profile2 infer_key infer *) let infer_type env constr = - let (j,(cst,_)) = - execute_type env constr (empty_constraint, universes env) in - (j, cst) + let j = execute_type env constr in + j let infer_v env cv = - let (jv,(cst,_)) = - execute_array env cv (empty_constraint, universes env) in - (jv, cst) + let jv = execute_array env cv in + jv (* Typing of several terms. *) let infer_local_decl env id = function | LocalDef c -> - let (j,cst) = infer env c in - (Name id, Some j.uj_val, j.uj_type), cst + let j = infer env c in + (Name id, Some j.uj_val, j.uj_type) | LocalAssum c -> - let (j,cst) = infer env c in - (Name id, None, assumption_of_judgment env j), cst + let j = infer env c in + (Name id, None, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> - let env, l, cst1 = inferec env l in - let d, cst2 = infer_local_decl env id d in - push_rel d env, add_rel_decl d l, union_constraints cst1 cst2 - | [] -> env, empty_rel_context, empty_constraint in + let (env, l) = inferec env l in + let d = infer_local_decl env id d in + (push_rel d env, add_rel_decl d l) + | [] -> (env, empty_rel_context) in inferec env decls - -(* Exported typing functions *) - -let typing env c = - let (j,cst) = infer env c in - let _ = add_constraints cst env in - j |