From 05c87ba330a9b4d02b150c196e390b9dd30be341 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Oct 2013 11:56:30 +0100 Subject: Fix interface for template polymorphism, cleaning up code in all typing algorithms. --- kernel/environ.ml | 24 ++++++++++++++++++++++++ kernel/environ.mli | 17 +++++++++++++++-- kernel/fast_typeops.ml | 20 ++++++++++---------- kernel/typeops.ml | 12 ++++++------ kernel/typeops.mli | 2 +- library/global.ml | 2 +- pretyping/pretyping.ml | 7 ++----- pretyping/retyping.ml | 6 +++--- pretyping/termops.ml | 7 ++++--- pretyping/termops.mli | 2 +- pretyping/typing.ml | 4 ++-- proofs/logic.ml | 18 ++++++++---------- 12 files changed, 77 insertions(+), 44 deletions(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 1f29fd67a..ef0f0ca4d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -315,6 +315,18 @@ let evaluable_constant kn env = | OpaqueDef _ -> false | Undef _ -> false +let template_polymorphic_constant (cst,u) env = + if not (Univ.Instance.is_empty u) then false + else + match (lookup_constant cst env).const_type with + | TemplateArity _ -> true + | RegularArity _ -> false + +let polymorphic_constant (cst,u) env = + if Univ.Instance.is_empty u then false + else + (lookup_constant cst env).const_polymorphic + let lookup_projection cst env = match (lookup_constant cst env).const_proj with | Some pb -> pb @@ -328,6 +340,18 @@ let is_projection cst env = (* Mutual Inductives *) let lookup_mind = lookup_mind +let template_polymorphic_ind ((mind,i),u) env = + if not (Univ.Instance.is_empty u) then false + else + match (lookup_mind mind env).mind_packets.(i).mind_arity with + | TemplateArity _ -> true + | RegularArity _ -> false + +let polymorphic_ind ((mind,i),u) env = + if Univ.Instance.is_empty u then false + else + (lookup_mind mind env).mind_polymorphic + let add_mind_key kn mind_key env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = diff --git a/kernel/environ.mli b/kernel/environ.mli index 330d9c277..d885ddd56 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -127,8 +127,11 @@ val add_constant_key : constant -> constant_body -> Pre_env.link_info ref -> val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool -val lookup_projection : Names.projection -> env -> projection_body -val is_projection : constant -> env -> bool +(** New-style polymorphism *) +val polymorphic_constant : pconstant -> env -> bool + +(** Old-style polymorphism *) +val template_polymorphic_constant : pconstant -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if @@ -157,6 +160,10 @@ val constant_value_in : env -> constant puniverses -> constr val constant_type_in : env -> constant puniverses -> constant_type val constant_opt_value_in : env -> constant puniverses -> constr option +(** {6 Primitive projections} *) + +val lookup_projection : Names.projection -> env -> projection_body +val is_projection : constant -> env -> bool (** {5 Inductive types } *) val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env @@ -166,6 +173,12 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env raises [Not_found] if the required path is not found *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +(** New-style polymorphism *) +val polymorphic_ind : pinductive -> env -> bool + +(** Old-style polymorphism *) +val template_polymorphic_ind : pinductive -> env -> bool + (** {5 Modules } *) val add_modtype : module_type_body -> env -> env diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index a68888c8c..e03720997 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -384,17 +384,17 @@ let rec execute env cstr = let argst = execute_array env args in let ft = match kind_of_term f with - | Ind ind -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args - | Const cst -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun t -> lazy t) argst in + | Ind ind when Environ.template_polymorphic_ind ind env -> + (* Template sort-polymorphism of inductive types *) + let args = Array.map (fun t -> lazy t) argst in + judge_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_constant cst env -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | _ -> + (* Full or no sort-polymorphism *) + execute env f in judge_of_apply env f ft args argst diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9428ace38..1a7d96b55 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -158,12 +158,11 @@ let type_of_constant_in env cst = let ar = constant_type_in env cst in type_of_constant_type_knowing_parameters env ar [||] -let judge_of_constant_knowing_parameters env (kn,u as cst) jl = +let judge_of_constant_knowing_parameters env (kn,u as cst) args = let c = mkConstU cst in let cb = lookup_constant kn 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 ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = type_of_constant_knowing_parameters env cst args in let _ = Environ.check_constraints cu env in make_judge c ty @@ -428,13 +427,14 @@ let rec execute env cstr = let jl = execute_array env args in let j = match kind_of_term f with - | Ind ind -> + | Ind ind when Environ.template_polymorphic_ind ind env -> (* Sort-polymorphism of inductive types *) let args = Array.map (fun j -> lazy j.uj_type) jl in judge_of_inductive_knowing_parameters env ind args - | Const cst -> + | Const cst when Environ.template_polymorphic_constant cst env -> (* Sort-polymorphism of constant *) - judge_of_constant_knowing_parameters env cst jl + let args = Array.map (fun j -> lazy j.uj_type) jl in + judge_of_constant_knowing_parameters env cst args | _ -> (* No sort-polymorphism *) execute env f diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 9747dbe83..e6fdf3d6c 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -55,7 +55,7 @@ val judge_of_variable : env -> variable -> unsafe_judgment val judge_of_constant : env -> pconstant -> unsafe_judgment val judge_of_constant_knowing_parameters : - env -> pconstant -> unsafe_judgment array -> unsafe_judgment + env -> pconstant -> types Lazy.t array -> unsafe_judgment (** {6 type of an applied projection } *) diff --git a/library/global.ml b/library/global.ml index fbba81b51..812178bbb 100644 --- a/library/global.ml +++ b/library/global.ml @@ -192,7 +192,7 @@ let type_of_global_in_context env r = Inductive.type_of_constructor (cstr,inst) specif, univs let is_polymorphic r = - let env = env() in + let env = env() in match r with | VarRef id -> false | ConstRef c -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0ef8d3f3c..3f14de282 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -549,15 +549,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - begin match kind_of_term f with - | Ind _ | Const _ - when isInd f || has_polymorphic_type (fst (destConst f)) - -> + if is_template_polymorphic env f then let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in make_judge c (* use this for keeping evars: resj.uj_val *) t - | _ -> resj end + else resj | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 9aecd2d1f..4ba6b01dc 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -124,7 +124,7 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (name,Some b,c1) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when isGlobalRef f -> + | App(f,args) when is_template_polymorphic env f -> let t = type_of_global_reference_knowing_parameters env f args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> @@ -154,7 +154,7 @@ let retype ?(polyprop=true) sigma = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when isGlobalRef f -> + | App(f,args) when is_template_polymorphic env f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args @@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma = let s2 = sort_family_of (push_rel (name,None,t) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when isGlobalRef f -> + | App(f,args) when is_template_polymorphic env f -> let t = type_of_global_reference_knowing_parameters env f args in family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> diff --git a/pretyping/termops.ml b/pretyping/termops.ml index ee7538b22..27c1d252d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -868,9 +868,10 @@ let isGlobalRef c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let has_polymorphic_type c = - match (Global.lookup_constant c).Declarations.const_type with - | Declarations.TemplateArity _ -> true +let is_template_polymorphic env f = + match kind_of_term f with + | Ind ind -> Environ.template_polymorphic_ind ind env + | Const c -> Environ.template_polymorphic_constant c env | _ -> false let base_sort_cmp pb s0 s1 = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index eec4a9b9d..6ef3d11da 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -271,7 +271,7 @@ val is_section_variable : Id.t -> bool val isGlobalRef : constr -> bool -val has_polymorphic_type : constant -> bool +val is_template_polymorphic : env -> constr -> bool (** Combinators on judgments *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cc473bd86..339ca19fb 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -207,12 +207,12 @@ let rec execute env evdref cstr = let jl = execute_array env evdref args in let j = match kind_of_term f with - | Ind ind -> + | Ind ind when Environ.template_polymorphic_ind ind env -> (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind (Evarutil.jv_nf_evar !evdref jl)) - | Const cst -> + | Const cst when Environ.template_polymorphic_constant cst env -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst diff --git a/proofs/logic.ml b/proofs/logic.ml index fb88b8754..47645d295 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -379,16 +379,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - match kind_of_term f with - | Ind _ | Const _ - when (isInd f || has_polymorphic_type (fst (destConst f))) -> - let sigma, ty = - (* Sort-polymorphism of definition and inductive types *) - type_of_global_reference_knowing_conclusion env sigma f conclty - in - goalacc, ty, sigma, f - | _ -> - mk_hdgoals sigma goal goalacc f + if is_template_polymorphic env f then + let sigma, ty = + (* Template sort-polymorphism of definition and inductive types *) + type_of_global_reference_knowing_conclusion env sigma f conclty + in + goalacc, ty, sigma, f + else + mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in -- cgit v1.2.3