From 90b61424761c5ba1ddbecf20c29d78b485584ae7 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Mon, 12 Dec 2016 14:18:48 +0100 Subject: Extend Fast_typeops to be a replacement for Typeops This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors. --- kernel/typeops.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel/typeops.mli') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 81fd1427d0..cfc82c1589 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -102,10 +102,10 @@ val judge_of_case : env -> case_info -> unsafe_judgment (** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit +(* val type_fixpoint : env -> Name.t array -> types array *) +(* -> unsafe_judgment array -> unit *) -val type_of_constant : env -> pconstant -> types constrained +(* val type_of_constant : env -> pconstant -> types constrained *) val type_of_constant_type : env -> constant_type -> types @@ -116,8 +116,8 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained +(* val type_of_constant_knowing_parameters : *) +(* env -> pconstant -> types Lazy.t array -> types constrained *) val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types -- cgit v1.2.3 From 421d846d80c19226ba0922ff3c3b0006c98c21b6 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Mon, 12 Dec 2016 14:49:01 +0100 Subject: Replace Typeops by Fast_typeops This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial changes in the other files, the real changes are in the parent commit. --- kernel/typeops.mli | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'kernel/typeops.mli') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index cfc82c1589..73c63db681 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -101,15 +101,11 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -(* val type_fixpoint : env -> Name.t array -> types array *) -(* -> unsafe_judgment array -> unit *) - (* val type_of_constant : env -> pconstant -> types constrained *) val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types @@ -127,4 +123,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit -- cgit v1.2.3 From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sat, 28 Jan 2017 14:11:50 +0100 Subject: Remove useless comments --- kernel/typeops.mli | 8 -------- 1 file changed, 8 deletions(-) (limited to 'kernel/typeops.mli') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 73c63db681..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,8 +98,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(* val type_of_constant : env -> pconstant -> types constrained *) - val type_of_constant_type : env -> constant_type -> types val type_of_projection_constant : env -> Names.projection puniverses -> types @@ -112,9 +107,6 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -(* val type_of_constant_knowing_parameters : *) -(* env -> pconstant -> types Lazy.t array -> types constrained *) - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types -- cgit v1.2.3