diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2013-10-31 11:56:30 +0100 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
commit | 05c87ba330a9b4d02b150c196e390b9dd30be341 (patch) | |
tree | fc19f68a21198754134aee6fe68a5cb5516b41b7 /kernel | |
parent | 1c1accf7186438228be9c426db9071aa95a7e992 (diff) |
Fix interface for template polymorphism, cleaning up code in all typing algorithms.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/environ.ml | 24 | ||||
-rw-r--r-- | kernel/environ.mli | 17 | ||||
-rw-r--r-- | kernel/fast_typeops.ml | 20 | ||||
-rw-r--r-- | kernel/typeops.ml | 12 | ||||
-rw-r--r-- | kernel/typeops.mli | 2 |
5 files changed, 56 insertions, 19 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 } *) |