aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/universes.ml')
-rw-r--r--engine/universes.ml54
1 files changed, 19 insertions, 35 deletions
diff --git a/engine/universes.ml b/engine/universes.ml
index e5f9212a7..27d5e3e23 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -923,52 +923,36 @@ let normalize_context_set g ctx us algs weak =
let uf = UF.create () in
(** Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
- Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
- if d == Le then
- if Univ.Level.is_small l then
- if is_set_minimization () && LSet.mem r ctx then
- (Constraint.add cstr smallles, noneqs)
- else (smallles, noneqs)
- else if Level.is_small r then
- if Level.is_prop r then
- raise (Univ.UniverseInconsistency
- (Le,Universe.make l,Universe.make r,None))
- else (smallles, Constraint.add (l,Eq,r) noneqs)
- else (smallles, Constraint.add cstr noneqs)
- else (smallles, Constraint.add cstr noneqs))
- csts (Constraint.empty, Constraint.empty)
+ Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+ in
+ let smallles = if is_set_minimization ()
+ then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+ else Constraint.empty
in
let csts =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
- let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+ let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
ctx UGraph.initial_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 UGraph.add_universe l false g
- with UGraph.AlreadyDeclared -> g
- else g
- in
- let g =
- if not (Level.is_small r || LSet.mem r ctx) then
- try UGraph.add_universe r false g
- with UGraph.AlreadyDeclared -> g
- else g
- in g) csts g
+ let add_soft u g =
+ if not (Level.is_small u || LSet.mem u ctx)
+ then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+ else g
+ in
+ let g = Constraint.fold
+ (fun (l, d, r) g -> add_soft r (add_soft l g))
+ csts g
in
- let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+ let g = UGraph.merge_constraints csts g in
UGraph.constraints_of_universes g
in
let noneqs =
Constraint.fold (fun (l,d,r as cstr) noneqs ->
if d == Eq then (UF.union l r uf; noneqs)
else (* We ignore the trivial Prop/Set <= i constraints. *)
- if d == Le && Univ.Level.is_small l then noneqs
- else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
+ if d == Le && Level.is_small l then noneqs
+ else if Level.is_prop l && d == Lt && Level.is_set r
then noneqs
else Constraint.add cstr noneqs)
csts Constraint.empty
@@ -980,12 +964,12 @@ let normalize_context_set g ctx us algs weak =
let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
(* Add equalities for globals which can't be merged anymore. *)
let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) global
+ Constraint.add (canon, Eq, g) cst) global
cstrs
in
(* Also add equalities for rigid variables *)
let cstrs = LSet.fold (fun g cst ->
- Constraint.add (canon, Univ.Eq, g) cst) rigid
+ Constraint.add (canon, Eq, g) cst) rigid
cstrs
in
let canonu = Some (Universe.make canon) in