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/fast_typeops.mli | 106 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 104 insertions(+), 2 deletions(-) (limited to 'kernel/fast_typeops.mli') diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 41cff607e7..73c63db681 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names +open Univ open Term open Environ +open Entries 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. @@ -22,3 +25,102 @@ open Declarations val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment + +val infer_local_decls : + env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + +(** {6 Basic operations of the typing machine. } *) + +(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] + returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) + +val assumption_of_judgment : env -> unsafe_judgment -> types +val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment + +(** {6 Type of sorts. } *) +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment +val judge_of_prop_contents : contents -> unsafe_judgment +val judge_of_type : universe -> unsafe_judgment + +(** {6 Type of a bound variable. } *) +val judge_of_relative : env -> int -> unsafe_judgment + +(** {6 Type of variables } *) +val judge_of_variable : env -> variable -> unsafe_judgment + +(** {6 type of a constant } *) + +val judge_of_constant : env -> pconstant -> unsafe_judgment + +val judge_of_constant_knowing_parameters : + env -> pconstant -> types Lazy.t array -> unsafe_judgment + +(** {6 type of an applied projection } *) + +val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment + +(** {6 Type of application. } *) +val judge_of_apply : + env -> unsafe_judgment -> unsafe_judgment array + -> unsafe_judgment + +(** {6 Type of an abstraction. } *) +val judge_of_abstraction : + env -> Name.t -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +val sort_of_product : env -> sorts -> sorts -> sorts + +(** {6 Type of a product. } *) +val judge_of_product : + env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment + -> unsafe_judgment + +(** s Type of a let in. *) +val judge_of_letin : + env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +(** {6 Type of a cast. } *) +val judge_of_cast : + env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> + unsafe_judgment + +(** {6 Inductive types. } *) + +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. } *) +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 + +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 + +(** Make a type polymorphic if an arity *) +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 -> ('a -> constr) -> 'a -> Context.Named.t -> unit -- 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/fast_typeops.mli | 126 ------------------------------------------------ 1 file changed, 126 deletions(-) delete mode 100644 kernel/fast_typeops.mli (limited to 'kernel/fast_typeops.mli') diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 73c63db681..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment - -val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) - -(** {6 Basic operations of the typing machine. } *) - -(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] - returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) - -val assumption_of_judgment : env -> unsafe_judgment -> types -val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment - -(** {6 Type of sorts. } *) -val judge_of_prop : unsafe_judgment -val judge_of_set : unsafe_judgment -val judge_of_prop_contents : contents -> unsafe_judgment -val judge_of_type : universe -> unsafe_judgment - -(** {6 Type of a bound variable. } *) -val judge_of_relative : env -> int -> unsafe_judgment - -(** {6 Type of variables } *) -val judge_of_variable : env -> variable -> unsafe_judgment - -(** {6 type of a constant } *) - -val judge_of_constant : env -> pconstant -> unsafe_judgment - -val judge_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> unsafe_judgment - -(** {6 type of an applied projection } *) - -val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment - -(** {6 Type of application. } *) -val judge_of_apply : - env -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment - -(** {6 Type of an abstraction. } *) -val judge_of_abstraction : - env -> Name.t -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment - -val sort_of_product : env -> sorts -> sorts -> sorts - -(** {6 Type of a product. } *) -val judge_of_product : - env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment - -> unsafe_judgment - -(** s Type of a let in. *) -val judge_of_letin : - env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment - -(** {6 Type of a cast. } *) -val judge_of_cast : - env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> - unsafe_judgment - -(** {6 Inductive types. } *) - -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. } *) -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 - -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 - -(** Make a type polymorphic if an arity *) -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 -> ('a -> constr) -> 'a -> Context.Named.t -> unit -- cgit v1.2.3