diff options
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index d198fbfbe..c44f2c1d7 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst val ugraph : t -> UGraph.t (** The current graph extended with the local constraints *) +val initial_graph : t -> UGraph.t +(** The initial graph with just the declarations of new universes. *) + val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) @@ -105,7 +108,7 @@ 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 constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t @@ -115,9 +118,26 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** {5 TODO: Document me} *) +(** [universe_context names extensible ctx] + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to [names] come + first in the order defined by that list. + + If [extensible] is false, check that the universes of [names] are + the only local universes. -val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context + Also return the association list of universe names and universes + (including those not in [names]). *) +val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> + (Id.t * Univ.Level.t) list * Univ.universe_context + +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context + +(** {5 TODO: Document me} *) val update_sigma_env : t -> Environ.env -> t |