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/uState.mli | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 engine/uState.mli (limited to 'engine/uState.mli') diff --git a/engine/uState.mli b/engine/uState.mli new file mode 100644 index 0000000000..c3b28d0a6a --- /dev/null +++ b/engine/uState.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + +val make : Environ.env -> Id.t Loc.located list option -> t + +val is_empty : t -> bool + +val union : t -> t -> t + +val of_context_set : Univ.universe_context_set -> t + +(** {5 Projections} *) + +val context_set : Univ.universe_context -> t -> Univ.universe_context_set +val constraints : t -> Univ.constraints +val context : t -> Univ.universe_context +val subst : t -> Universes.universe_opt_subst +val ugraph : t -> UGraph.t +val variables : t -> Univ.LSet.t + +(** {5 Constraints handling} *) + +val add_constraints : t -> Univ.constraints -> t +val add_universe_constraints : t -> Universes.universe_constraints -> t + +(** {5 TODO: Document me} *) + +val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context + +val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds + +val restrict : t -> Univ.universe_set -> t + +type rigid = + | UnivRigid + | UnivFlexible of bool (** Is substitution by an algebraic ok? *) + +val univ_rigid : rigid +val univ_flexible : rigid +val univ_flexible_alg : rigid + +val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge_subst : t -> Universes.universe_opt_subst -> t +val emit_side_effects : Declareops.side_effects -> t -> t + +val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val add_global_univ : t -> Univ.Level.t -> t +val make_flexible_variable : t -> bool -> Univ.Level.t -> t + +val is_sort_variable : t -> Sorts.t -> Univ.Level.t option + +val normalize_variables : t -> Univ.universe_subst * t + +val abstract_undefined_variables : t -> t + +val fix_undefined_variables : t -> t + +val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst + +val normalize : t -> t + +val universe_of_name : t -> string -> Univ.Level.t + +val add_universe_name : t -> string -> Univ.Level.t -> t -- 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/uState.mli | 54 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 42 insertions(+), 12 deletions(-) (limited to 'engine/uState.mli') diff --git a/engine/uState.mli b/engine/uState.mli index c3b28d0a6a..56e0fe14e5 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -13,14 +13,14 @@ open Names exception UniversesDiffer type t +(** Type of universe unification states. They allow the incremental building of + universe constraints during an interactive proof. *) (** {5 Constructors} *) val empty : t -val from : Environ.env -> t - -val make : Environ.env -> Id.t Loc.located list option -> t +val make : UGraph.t -> t val is_empty : t -> bool @@ -30,23 +30,47 @@ val of_context_set : Univ.universe_context_set -> t (** {5 Projections} *) -val context_set : Univ.universe_context -> t -> Univ.universe_context_set -val constraints : t -> Univ.constraints -val context : t -> Univ.universe_context +val context_set : t -> Univ.universe_context_set +(** The local context of the state, i.e. a set of bound variables together + with their associated constraints. *) + val subst : t -> Universes.universe_opt_subst +(** The local universes that are unification variables *) + val ugraph : t -> UGraph.t -val variables : t -> Univ.LSet.t +(** The current graph extended with the local constraints *) + +val algebraics : t -> Univ.LSet.t +(** The subset of unification variables that can be instantiated with algebraic + universes as they appear in types and universe instances only. *) + +val constraints : t -> Univ.constraints +(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) + +val context : t -> Univ.universe_context +(** Shorthand for {!context_set} with {!Context_set.to_context}. *) (** {5 Constraints handling} *) val add_constraints : t -> Univ.constraints -> t +(** + @raise UniversesDiffer +*) + val add_universe_constraints : t -> Universes.universe_constraints -> t +(** + @raise UniversesDiffer +*) -(** {5 TODO: Document me} *) +(** {5 Names} *) -val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context +val add_universe_name : t -> string -> Univ.Level.t -> t +(** Associate a human-readable name to a local variable. *) -val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds +val universe_of_name : t -> string -> Univ.Level.t +(** Retrieve the universe associated to the name. *) + +(** {5 Unification} *) val restrict : t -> Univ.universe_set -> t @@ -70,6 +94,8 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t +val constrain_variables : Univ.LSet.t -> t -> Univ.constraints + val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t @@ -78,6 +104,10 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -val universe_of_name : t -> string -> Univ.Level.t +(** {5 TODO: Document me} *) -val add_universe_name : t -> string -> Univ.Level.t -> t +val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context + +(** {5 Pretty-printing} *) + +val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds -- cgit v1.2.3 From f7030a3358dda9bbc6de8058ab3357be277c031a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Nov 2015 14:19:37 +0100 Subject: Remove unneeded fixpoint in normalize_context_set. Note that it is no longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l). --- engine/uState.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/uState.mli') diff --git a/engine/uState.mli b/engine/uState.mli index 3a6f77e14e..a188a5269f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,7 +44,7 @@ val ugraph : t -> UGraph.t val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic - universes as they appear in types and universe instances only. *) + universes as they appear in inferred types only. *) val constraints : t -> Univ.constraints (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) -- cgit v1.2.3 From 3a29016f5b73815454ce8d9a74a017857e926706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 10:28:09 +0100 Subject: Fixing compilation of mli documentation. Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed. --- engine/uState.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/uState.mli') diff --git a/engine/uState.mli b/engine/uState.mli index a188a5269f..9dc96622ea 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -56,12 +56,12 @@ val context : t -> Univ.universe_context val add_constraints : t -> Univ.constraints -> t (** - @raise UniversesDiffer + @raise UniversesDiffer when universes differ *) val add_universe_constraints : t -> Universes.universe_constraints -> t (** - @raise UniversesDiffer + @raise UniversesDiffer when universes differ *) (** {5 Names} *) -- 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/uState.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/uState.mli') diff --git a/engine/uState.mli b/engine/uState.mli index 9dc96622ea..c5c454020c 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -84,11 +84,11 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t val merge_subst : t -> Universes.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t -val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t val make_flexible_variable : t -> bool -> Univ.Level.t -> t -- cgit v1.2.3