From 603bfb392805fb8d1559d304bcf1b9c7b938bb6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 17:16:18 +0200 Subject: Getting rid of AUContext abstraction breakers in Recordops. --- API/API.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index 9f7a6ded81..a661b34c5b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,6 +84,11 @@ sig val empty : t end + module AUContext : + sig + type t = Univ.AUContext.t + end + type universe_context = UContext.t [@@ocaml.deprecated "alias of API.Univ.UContext.t"] @@ -2884,7 +2889,7 @@ sig | Default_cs type obj_typ = Recordops.obj_typ = { o_DEF : Term.constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : Term.constr list; (** ordered *) o_TPARAMS : Term.constr list; (** ordered *) -- cgit v1.2.3 From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 21:51:23 +0200 Subject: Safer API for Global.body_of_constant and variants. We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. --- API/API.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index a661b34c5b..48fd3a682f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2716,8 +2716,8 @@ sig val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t - val body_of_constant_body : Declarations.constant_body -> Term.constr option - val body_of_constant : Names.Constant.t -> Term.constr option + val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option + val body_of_constant : Names.Constant.t -> (Term.constr * Univ.AUContext.t) option val add_constraints : Univ.Constraint.t -> unit end -- cgit v1.2.3 From 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 22:49:32 +0200 Subject: Make the typeclass implementation fully compatible with universe polymorphism. This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. --- API/API.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index 48fd3a682f..0f3394fe9f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3048,6 +3048,7 @@ end module Typeclasses : sig type typeclass = Typeclasses.typeclass = { + cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; cl_props : Context.Rel.t; -- cgit v1.2.3 From 71563ebb86a83bc7cdfc17f58493f59428d764b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:49:26 +0200 Subject: Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. --- API/API.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index 0f3394fe9f..f8fb96aa96 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2684,10 +2684,8 @@ sig val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set - val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr val new_univ_level : Names.DirPath.t -> Univ.Level.t - val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds @@ -2713,6 +2711,8 @@ sig val env_of_context : Environ.named_context_val -> Environ.env val is_polymorphic : Globnames.global_reference -> bool + val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t -- cgit v1.2.3 From 469a9b3242891b089b4a211e96b5b568277f7fc0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 15:55:51 +0200 Subject: Remove the function Global.type_of_global_unsafe. --- API/API.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'API/API.mli') diff --git a/API/API.mli b/API/API.mli index f8fb96aa96..e8418552c4 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2713,7 +2713,6 @@ sig val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t - val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option -- cgit v1.2.3