diff options
Diffstat (limited to 'engine/universes.mli')
-rw-r--r-- | engine/universes.mli | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 4af944347..4823c5746 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -14,6 +14,9 @@ open Constr open Environ open Univ +(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) +module UPairSet : CSet.S with type elt = (Level.t * Level.t) + val set_minimization : bool ref val is_set_minimization : unit -> bool @@ -69,12 +72,15 @@ val new_sort_in_family : Sorts.family -> Sorts.t When doing conversion of universes, not only do we have =/<= constraints but also Lub constraints which correspond to unification of two levels which might not be necessary if unfolding is performed. + + UWeak constraints come from irrelevant universes in cumulative polymorphism. *) type universe_constraint = | ULe of Universe.t * Universe.t | UEq of Universe.t * Universe.t | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t module Constraints : sig include Set.S with type elt = universe_constraint @@ -96,7 +102,9 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -val to_constraints : UGraph.t -> Constraints.t -> Constraint.t +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -167,9 +175,10 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -val normalize_context_set : ContextSet.t -> +val normalize_context_set : UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> - LSet.t (* univ variables that can be substituted by algebraics *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set val normalize_univ_variables : universe_opt_subst -> |