diff options
| author | Matthieu Sozeau | 2015-09-23 16:11:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | 26628315688e07c43b9881872a737454e93fe4c9 (patch) | |
| tree | 36dfc2e0a04a5901c840990bc0bd989e1d7feff7 | |
| parent | e841deb4750d43ab19f91907476d75fc73860c5a (diff) | |
Univs: minimization, adapt to graph invariants.
We are forced to declare universes that are global and appear in the
local constraints as we start from an empty universe graph.
| -rw-r--r-- | library/universes.ml | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index 0544585dce..0133f5deb6 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -843,7 +843,25 @@ let normalize_context_set ctx us algs = let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.merge_constraints csts Univ.empty_universes in + let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g) + ctx Univ.empty_universes + in + let g = + Univ.Constraint.fold (fun (l, d, r) g -> + let g = + if not (Level.is_small l || LSet.mem l ctx) then + try Univ.add_universe l true g + with Univ.AlreadyDeclared -> g + else g + in + let g = + if not (Level.is_small r || LSet.mem r ctx) then + try Univ.add_universe r true g + with Univ.AlreadyDeclared -> g + else g + in g) csts g + in + let g = Univ.Constraint.fold Univ.enforce_constraint csts g in Univ.constraints_of_universes g in let noneqs = @@ -852,6 +870,8 @@ let normalize_context_set ctx us algs = else (* We ignore the trivial Prop/Set <= i constraints. *) if d == Le && Univ.Level.is_small l then noneqs + else if Level.is_small l && d == Lt && not (LSet.mem r ctx) then + noneqs else Constraint.add cstr noneqs) csts Constraint.empty in |