From 004d7aeeca9f5ae4ceb9f109fa90a87e58457680 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Sep 2019 11:06:09 +0200
Subject: Postpone the computation of relative constraints in universe
 unification.

Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
---
 engine/uState.ml | 34 ++++++++++++++++++++--------------
 1 file changed, 20 insertions(+), 14 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index cb40e6eadd..5ebac4b817 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -178,6 +178,7 @@ exception UniversesDiffer
 
 let drop_weak_constraints = ref false
 
+
 let process_universe_constraints ctx cstrs =
   let open UnivSubst in
   let open UnivProblem in
@@ -236,22 +237,23 @@ let process_universe_constraints ctx cstrs =
       else 
           match cst with
           | ULe (l, r) ->
-            if UGraph.check_leq univs l r then
-              (* Keep Prop/Set <= var around if var might be instantiated by prop or set
-                 later. *)
-              match Universe.level l, Universe.level r with
-              | Some l, Some r ->
-                Constraint.add (l, Le, r) local
-              | _ -> local
-            else
-              begin match Universe.level r with
-              | None -> user_err Pp.(str "Algebraic universe on the right")
-              | Some r' ->
-                if Level.is_small r' then
+            begin match Univ.Universe.level r with
+            | None ->
+              if UGraph.check_leq univs l r then local
+              else user_err Pp.(str "Algebraic universe on the right")
+            | Some r' ->
+              if Level.is_small r' then
                   if not (Universe.is_levels l)
                   then
+                    if UGraph.check_leq univs l r then local
+                    else
                     raise (UniverseInconsistency (Le, l, r, None))
                   else
+                    if UGraph.check_leq univs l r then match Univ.Universe.level l with
+                    | Some l ->
+                      Univ.Constraint.add (l, Le, r') local
+                    | None -> local
+                    else
                     let levels = Universe.levels l in
                     let fold l' local =
                       let l = Universe.make l' in
@@ -260,8 +262,12 @@ let process_universe_constraints ctx cstrs =
                       else raise (UniverseInconsistency (Le, l, r, None))
                     in
                     LSet.fold fold levels local
-                else
-                  enforce_leq l r local
+              else
+                match Univ.Universe.level l with
+                | Some l ->
+                  Univ.Constraint.add (l, Le, r') local
+                | None ->
+                  if UGraph.check_leq univs l r then local else enforce_leq l r local
               end
           | ULub (l, r) ->
               equalize_variables true (Universe.make l) l (Universe.make r) r local
-- 
cgit v1.2.3