From 5d3126557d4567560ed8691ff8bc8ab919a54b4d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 01:14:09 +0100
Subject: univ minimization: Partially let-lift [enforce_uppers]

---
 engine/universes.ml | 30 ++++++++++++++----------------
 1 file changed, 14 insertions(+), 16 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 3b7a40dab..c6682156c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -811,6 +811,15 @@ let not_lower lower (d,l) =
          (** No constraint existing on l *) true) l
 
 exception UpperBoundedAlg
+let enforce_uppers upper lbound cstrs =
+  List.fold_left (fun cstrs (d, r) ->
+      if d == Univ.Le then
+        enforce_leq lbound (Universe.make r) cstrs
+      else
+        try let lev = Option.get (Universe.level lbound) in
+          Constraint.add (lev, d, r) cstrs
+        with Option.IsNone -> raise UpperBoundedAlg)
+    cstrs upper
 
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
@@ -876,24 +885,13 @@ let minimize_univ_variables ctx us algs left right cstrs =
                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
             end
     in
-    let enforce_uppers acc =
+    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
       match LMap.find u right with
       | exception Not_found -> acc
-      | cstrs ->
-	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
-	  if List.is_empty dangling then acc
-	  else
-            let ((ctx, us, algs, insts, cstrs), ({lbound=inst;lower} as b)) = acc in
-            let cstrs = List.fold_left (fun cstrs (d, r) ->
-	      if d == Univ.Le then
-		enforce_leq inst (Universe.make r) cstrs
-	      else
-		try let lev = Option.get (Universe.level inst) in
-		      Constraint.add (lev, d, r) cstrs
-                with Option.IsNone -> raise UpperBoundedAlg)
-	      cstrs dangling
-	    in
-              (ctx, us, algs, insts, cstrs), b
+      | upper ->
+        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
+        let cstrs = enforce_uppers upper b.lbound cstrs in
+        (ctx, us, algs, insts, cstrs), b
     in
     if not (LSet.mem u ctx)
     then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-- 
cgit v1.2.3