From 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 13:27:16 +0100 Subject: Typeclasses API using EConstr. --- pretyping/typeclasses.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2530f5dfae..ec36c57e04 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c (** These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance. *) -val dest_class_app : env -> constr -> typeclass puniverses * constr list +val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list (** Get the instantiated typeclass structure for a given universe instance. *) val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference @@ -99,11 +99,11 @@ val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool -val is_class_type : evar_map -> types -> bool +val is_class_type : evar_map -> EConstr.types -> bool val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map -val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t -val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t +val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> open_constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit -- cgit v1.2.3 From 67507df457be05ee5b651a423031a8cd584934ef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 00:35:43 +0100 Subject: Class_tactics API using EConstr. --- pretyping/typeclasses.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ec36c57e04..e95aba695d 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -103,7 +103,7 @@ val is_class_type : evar_map -> EConstr.types -> bool val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map -val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> val remove_instance_hint : global_reference -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t -val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> open_constr) Hook.t +val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- pretyping/typeclasses.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e95aba695d..0c30296d35 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -67,7 +67,7 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference -- 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/typeclasses.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 7990b12cdb..8d1c0b94ca 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c (** These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance. *) -val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list +val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option +val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option val instance_impl : instance -> global_reference -- cgit v1.2.3