diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-10 17:28:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-20 17:53:14 +0200 |
| commit | ecaea9a428c052ea431ec7c392e81aaf918d5d96 (patch) | |
| tree | 6ef8e9a62ded2734d307e7f917d4c310f893aa6a /library/universes.mli | |
| parent | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (diff) | |
Fix minimization to be insensitive to redundant arcs.
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/library/universes.mli b/library/universes.mli index a5740ec49..c8cf7047e 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -243,28 +243,31 @@ val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> univ val compute_lbound : (constraint_type * Univ.universe) list -> universe option +type lowermap = constraint_type Univ.LMap.t + val instantiate_with_lbound : Univ.LMap.key -> Univ.universe -> + lowermap -> bool -> bool -> Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints -> (Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe) + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints) * + (bool * bool * Univ.universe * lowermap) val minimize_univ_variables : Univ.LSet.t -> Univ.universe option Univ.LMap.t -> Univ.LSet.t -> - constraints_map -> constraints_map -> + constraints_map -> constraints_map -> Univ.constraints -> Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints + (bool * bool * Univ.universe * lowermap) Univ.LMap.t * Univ.constraints (** {6 Support for old-style sort-polymorphism } *) |