From ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 19:07:16 +0100 Subject: Classops API using EConstr. --- pretyping/classops.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/classops.mli') diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d509739cf4..4b8a2c1c07 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -59,15 +59,15 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list +val find_class_type : evar_map -> EConstr.types -> cl_typ * Univ.universe_instance * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> types -> types * cl_index +val class_of : env -> evar_map -> EConstr.types -> types * cl_index (** raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : env -> evar_map -> types -> constr list +val class_args_of : env -> evar_map -> EConstr.types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) val declare_coercion : @@ -84,11 +84,11 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer (** @raise Not_found in the following functions when no path exists *) val lookup_path_between_class : cl_index * cl_index -> inheritance_path -val lookup_path_between : env -> evar_map -> types * types -> +val lookup_path_between : env -> evar_map -> EConstr.types * EConstr.types -> types * types * inheritance_path -val lookup_path_to_fun_from : env -> evar_map -> types -> +val lookup_path_to_fun_from : env -> evar_map -> EConstr.types -> types * inheritance_path -val lookup_path_to_sort_from : env -> evar_map -> types -> +val lookup_path_to_sort_from : env -> evar_map -> EConstr.types -> types * inheritance_path val lookup_pattern_path_between : env -> inductive * inductive -> (constructor * int) list -- cgit v1.2.3 From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 20:33:06 +0100 Subject: Coercion API using EConstr. --- pretyping/classops.mli | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'pretyping/classops.mli') diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 4b8a2c1c07..9fb70534fd 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -8,6 +8,7 @@ open Names open Term +open EConstr open Evd open Environ open Mod_subst @@ -59,15 +60,15 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> EConstr.types -> cl_typ * Univ.universe_instance * constr list +val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> EConstr.types -> types * cl_index +val class_of : env -> evar_map -> types -> types * cl_index (** raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : env -> evar_map -> EConstr.types -> constr list +val class_args_of : env -> evar_map -> types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) val declare_coercion : @@ -84,11 +85,11 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer (** @raise Not_found in the following functions when no path exists *) val lookup_path_between_class : cl_index * cl_index -> inheritance_path -val lookup_path_between : env -> evar_map -> EConstr.types * EConstr.types -> +val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path -val lookup_path_to_fun_from : env -> evar_map -> EConstr.types -> +val lookup_path_to_fun_from : env -> evar_map -> types -> types * inheritance_path -val lookup_path_to_sort_from : env -> evar_map -> EConstr.types -> +val lookup_path_to_sort_from : env -> evar_map -> types -> types * inheritance_path val lookup_pattern_path_between : env -> inductive * inductive -> (constructor * int) list @@ -104,7 +105,7 @@ val install_path_printer : val string_of_class : cl_typ -> string val pr_class : cl_typ -> std_ppcmds val pr_cl_index : cl_index -> std_ppcmds -val get_coercion_value : coe_index -> constr +val get_coercion_value : coe_index -> Constr.t val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list val coercions : unit -> coe_index list -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- pretyping/classops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/classops.mli') diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 9fb70534fd..a1d030f125 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -8,9 +8,9 @@ open Names open Term +open Environ open EConstr open Evd -open Environ open Mod_subst (** {6 This is the type of class kinds } *) -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- pretyping/classops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/classops.mli') diff --git a/pretyping/classops.mli b/pretyping/classops.mli index a1d030f125..0d741a5a5d 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -60,7 +60,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list +val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index -- cgit v1.2.3