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 /library | |
| 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.
Diffstat (limited to 'library')
| -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 |