From f53f84d32dff2820043df92e743234e3fdaa3520 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Jun 2019 10:54:14 +0200
Subject: Minimize Prop <= i to i := Set

Fix part of #8196, fix #12414
Replaces #9343
---
 engine/uState.ml    | 2 +-
 engine/univMinim.ml | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 2cb88c7fff..9557111cfd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -675,7 +675,7 @@ let subst_univs_context_with_def def usubst (ctx, cst) =
   (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
 
 let is_trivial_leq (l,d,r) =
-  Level.is_prop l && (d == Le || (d == Lt && Level.is_set r))
+  Level.is_prop l && (d == Le || d == Lt) && Level.is_set r
 
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c5854e27f3..4ed6e97526 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -292,17 +292,23 @@ let is_bound l lbound = match lbound with
 | UGraph.Bound.Prop -> Level.is_prop l
 | UGraph.Bound.Set -> Level.is_set l
 
+(* if [is_minimal u] then constraints [u <= v] may be dropped and get
+   used only for set_minimization. *)
+let is_minimal ~lbound u =
+  Level.is_sprop u || Level.is_prop u || is_bound u lbound
+
 (* TODO check is_small/sprop *)
 let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && is_minimal ~lbound l) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
     else Constraint.empty
   in
+  let smallles = Constraint.map (fun (_,_,r) -> Level.set, Le, r) smallles in
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-- 
cgit v1.2.3