From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:23:15 +0200 Subject: Use type Universes.universe_binders. --- API/API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 1f1b05eadb..d912dc7714 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2882,7 +2882,7 @@ sig val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - (Names.Id.t * Univ.Level.t) list * Univ.UContext.t + Universes.universe_binders * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map -- cgit v1.2.3 From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- API/API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index d912dc7714..63c6752211 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2869,7 +2869,7 @@ sig val clear_metas : evar_map -> evar_map (** Allocates a new evar that represents a {i sort}. *) - val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t + val new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t val remove : evar_map -> Evar.t -> evar_map val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env -> -- cgit v1.2.3 From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- API/API.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 63c6752211..889050d90a 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2882,7 +2882,8 @@ sig val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t + val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map -- cgit v1.2.3 From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- API/API.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 889050d90a..5c78606715 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2881,12 +2881,12 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool -- cgit v1.2.3 From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- API/API.mli | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 5c78606715..ad5d5490b8 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1417,7 +1417,7 @@ sig | TemplateArity of 'b type constant_universes = - | Monomorphic_const of Univ.UContext.t + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.AUContext.t type projection_body = { @@ -1484,7 +1484,7 @@ sig | MEwith of module_alg_expr * with_declaration type abstract_inductive_universes = - | Monomorphic_ind of Univ.UContext.t + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t @@ -1551,7 +1551,7 @@ sig | LocalAssumEntry of constr type inductive_universes = - | Monomorphic_ind_entry of Univ.UContext.t + | Monomorphic_ind_entry of Univ.ContextSet.t | Polymorphic_ind_entry of Univ.UContext.t | Cumulative_ind_entry of Univ.CumulativityInfo.t @@ -1580,8 +1580,9 @@ sig type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.UContext.t + | Monomorphic_const_entry of Univ.ContextSet.t | Polymorphic_const_entry of Univ.UContext.t + type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1592,7 +1593,7 @@ sig const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } - type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline + type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline type projection_entry = { proj_entry_ind : MutInd.t; -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- API/API.mli | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index ad5d5490b8..4405bf8da5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2764,6 +2764,9 @@ sig val context_set : t -> Univ.ContextSet.t val of_context_set : Univ.ContextSet.t -> t + val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes + type rigid = | UnivRigid | UnivFlexible of bool @@ -2887,6 +2890,8 @@ sig val from_ctx : UState.t -> evar_map val to_universe_context : evar_map -> Univ.UContext.t + val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes val meta_list : evar_map -> (Constr.metavariable * clbinding) list @@ -4669,11 +4674,11 @@ sig val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> - ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t -> - Constr.t Univ.in_universe_context_set -> Names.Constant.t + ?local:bool -> Names.Id.t -> ?types:Constr.t -> + Constr.t Entries.in_constant_universes_entry -> Names.Constant.t val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:Constr.types -> - ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry val definition_message : Names.Id.t -> unit val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name -- cgit v1.2.3