From 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 18:28:36 +0100 Subject: 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. --- engine/universes.mli | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'engine/universes.mli') 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 -> -- cgit v1.2.3