From f52826877059858fb3fcd4314c629ed63d90a042 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 19:50:41 +0200 Subject: Hardening the API of evarmaps. The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap. --- engine/evd.mli | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 94d9d5f662..e240ebc310 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -143,6 +143,10 @@ val has_undefined : evar_map -> bool (** [has_undefined sigma] is [true] if and only if there are uninstantiated evars in [sigma]. *) +val new_evar : evar_map -> + ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar +(** Creates a fresh evar mapping to the given information. *) + val add : evar_map -> evar -> evar_info -> evar_map (** [add sigma ev info] adds [ev] with evar info [info] in sigma. Precondition: ev must not preexist in [sigma]. *) @@ -230,14 +234,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val evar_declare : - named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map -(** Convenience function. Just a wrapper around {!add}. *) - -val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map +val restrict : evar -> Filter.t -> ?candidates:constr list -> + evar_map -> evar_map * evar (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) @@ -614,3 +612,7 @@ val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) val create_goal_evar_defs : evar_map -> evar_map + +(** {5 Summary names} *) + +val evar_counter_summary_name : string -- cgit v1.2.3 From ca14b0bb67c9db000736333a056fc147c6f5199c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 14:16:54 +0200 Subject: Removing uselessly duplicated function in Evd. --- engine/evd.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index e240ebc310..0902191818 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -611,8 +611,6 @@ val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) -val create_goal_evar_defs : evar_map -> evar_map - (** {5 Summary names} *) val evar_counter_summary_name : string -- cgit v1.2.3 From 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 16:36:10 +0200 Subject: Removing subst_defined_metas_evars from Evd. --- engine/evd.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 0902191818..cfe4adc09d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -457,7 +457,6 @@ val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status val retract_coercible_metas : evar_map -> metabinding list * evar_map -val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option (** {5 FIXME: Nothing to do here} *) -- cgit v1.2.3 From a3d7630d74b720b771e880dcf0fcad05de553a6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 16:39:36 +0200 Subject: Removing meta_with_name from Evd. --- engine/evd.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index cfe4adc09d..bc81bd8189 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -440,7 +440,6 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_ val meta_type : evar_map -> metavariable -> types val meta_ftype : evar_map -> metavariable -> types freelisted val meta_name : evar_map -> metavariable -> Name.t -val meta_with_name : evar_map -> Id.t -> metavariable val meta_declare : metavariable -> types -> ?name:Name.t -> evar_map -> evar_map val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- engine/evd.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index db60f5ff43..22d0174973 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -489,7 +489,7 @@ val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map val universe_of_name : evar_map -> string -> Univ.universe_level val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map -val universes : evar_map -> Univ.universes +val universes : evar_map -> UGraph.t val add_constraints_context : evar_universe_context -> Univ.constraints -> evar_universe_context @@ -532,7 +532,7 @@ val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst -val universes : evar_map -> Univ.universes +val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map -- cgit v1.2.3 From 68863acca9abf4490c651df889721ef7f6a4d375 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Oct 2015 15:32:03 +0200 Subject: Dedicated file for universe unification context manipulation. This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar. --- engine/evd.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index d659b8826e..796f503746 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -119,7 +119,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) -type evar_universe_context +type evar_universe_context = UState.t (** The universe context associated to an evar map *) type evar_map @@ -464,7 +464,7 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (** Rigid or flexible universe variables *) -type rigid = +type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) -- cgit v1.2.3 From d558bf5289e87899a850dda410a3a3c4de1ce979 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Oct 2015 18:55:42 +0200 Subject: Clarifying and documenting the UState API. --- engine/evd.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 796f503746..dc498ed42e 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -474,7 +474,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * evar_universe_context -val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set +val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set val evar_universe_context_constraints : evar_universe_context -> Univ.constraints val evar_context_universe_context : evar_universe_context -> Univ.universe_context val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context @@ -482,6 +482,8 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst +val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map -- cgit v1.2.3 From 42db8dc57c5d96812520e594d31a22dc242ae848 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:17:32 +0100 Subject: Remove duplicate declarations. --- engine/evd.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 57399f2b5e..220c693ad6 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -494,8 +494,6 @@ val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map val universe_of_name : evar_map -> string -> Univ.universe_level val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map -val universes : evar_map -> UGraph.t - val add_constraints_context : evar_universe_context -> Univ.constraints -> evar_universe_context @@ -517,7 +515,6 @@ val is_sort_variable : evar_map -> sorts -> Univ.universe_level option not a local sort variable declared in [evm] *) val is_flexible_level : evar_map -> Univ.Level.t -> bool -val whd_sort_variable : evar_map -> constr -> constr (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) val normalize_universe : evar_map -> Univ.universe -> Univ.universe val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- engine/evd.mli | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 57399f2b5e..34169b0214 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -10,7 +10,6 @@ open Util open Loc open Names open Term -open Context open Environ (** {5 Existential variables and unification states} @@ -105,8 +104,8 @@ type evar_info = { val make_evar : named_context_val -> types -> evar_info val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context +val evar_context : evar_info -> Context.Named.t +val evar_filtered_context : evar_info -> Context.Named.t val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body @@ -223,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr @@ -423,7 +422,7 @@ val evar_list : constr -> existential list val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : named_context -> Evar.Set.t +val evars_of_named_context : Context.Named.t -> Evar.Set.t val evars_of_filtered_evar_info : evar_info -> Evar.Set.t -- cgit v1.2.3 From 8d0ff142913fc6351ff7f0a6b8eacc6c21d36000 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Feb 2016 15:12:53 +0100 Subject: Allowing to attach location to universes in UState. --- engine/evd.mli | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index a9ca9a7408..3ae6e586c1 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -504,9 +504,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -541,10 +541,10 @@ val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a +val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context @@ -559,12 +559,12 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts +val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** -- cgit v1.2.3