diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 18:28:36 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:30:12 +0100 |
| commit | 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 (patch) | |
| tree | ad7effee5b9ad3904ab84d81e1583d233ae5033a /engine/universes.mli | |
| parent | d640b676282285d52ac19038d693080e64eb5ea7 (diff) | |
Delayed weak constraints for cumulative inductive types.
When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.
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 -> |