diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 132 |
1 files changed, 33 insertions, 99 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b814deb6eb..7f36f3813f 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,16 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors open Util open Names open Univ -open Term +open Sorts +open Constr open Vars open Declarations open Environ @@ -38,7 +41,7 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let check_type env c t = - match kind_of_term(whd_all env t) with + match kind(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -57,7 +60,7 @@ let check_assumption env t ty = (* Prop and Set *) -let type1 = mkSort type1_sort +let type1 = mkSort Sorts.type1 (* Type of Type(i). *) @@ -65,6 +68,10 @@ let type_of_type u = let uu = Universe.super u in mkType uu +let type_of_sort = function + | Prop | Set -> type1 + | Type u -> type_of_type u + (*s Type of a de Bruijn index. *) let type_of_relative env n = @@ -111,36 +118,17 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (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_knowing_parameters env (kn,u as cst) args = +let type_of_constant env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - let ty = type_of_constant_type_knowing_parameters env ty args in let () = check_constraints cu env in ty -let type_of_constant_knowing_parameters_in env (kn,u as cst) args = +let type_of_constant_in env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty args - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let type_of_constant_in env cst = - type_of_constant_knowing_parameters_in env cst [||] - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -167,7 +155,7 @@ let type_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then typ else - (match kind_of_term (whd_all env typ) with + (match kind (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try @@ -190,11 +178,11 @@ let type_of_apply env func funt argsv argstv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | ((Prop | Set), Set) -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | (Type u1, Set) -> if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -202,9 +190,9 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (Universe.sup u1 u2) @@ -233,7 +221,7 @@ let check_cast env c ct k expected_type = try match k with | VMcast -> - vm_conv CUMUL env ct expected_type + Vconv.vm_conv CUMUL env ct expected_type | DEFAULTcast -> default_conv ~l2r:false CUMUL env ct expected_type | REVERTcast -> @@ -308,14 +296,14 @@ let type_of_case env ci p pt c ct lf lft = rslty let type_of_projection env p c ct = - let pb = lookup_projection p env in + let pty = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty + assert(eq_ind (Projection.inductive p) ind); + let ty = Vars.subst_instance_constr u pty in + substl (c :: CList.rev args) ty (* Fixpoints. *) @@ -340,13 +328,9 @@ let check_fixpoint env lna lar vdef vdeft = arbitraires et non plus des variables *) let rec execute env cstr = let open Context.Rel.Declaration in - match kind_of_term cstr with + match kind cstr with (* Atomic terms *) - | Sort (Prop c) -> - type1 - - | Sort (Type u) -> - type_of_type u + | Sort s -> type_of_sort s | Rel n -> type_of_relative env n @@ -365,13 +349,10 @@ let rec execute env cstr = | App (f,args) -> let argst = execute_array env args in let ft = - match kind_of_term f with + match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - let args = Array.map (fun t -> lazy t) argst in - type_of_constant_knowing_parameters env cst args | _ -> (* No template polymorphism *) execute env f @@ -456,8 +437,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = @@ -500,17 +481,11 @@ let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 let judge_of_type u = make_judge (mkType u) (type_of_type u) -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) -let judge_of_constant_knowing_parameters env cst args = - make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) let judge_of_projection env p cj = make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) @@ -549,44 +524,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") - -(* Instantiation of terms on real arguments. *) - -(* 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) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | RelDecl.LocalAssum (_,p) -> extract_level env p :: l - | RelDecl.LocalDef _ -> 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) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t |