From 9ab85ef978c78edb3e4e5ec97ec93a970f021fc2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 2 Mar 2018 13:22:27 +0100
Subject: universe minimization: cleanup using standard combinators, open Univ

eg Constraint.partition + filter instead of a complicated fold.
---
 engine/universes.ml | 54 +++++++++++++++++++----------------------------------
 1 file changed, 19 insertions(+), 35 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3


From f53890d1629ea7aaff86ea92e5ac27ab027b2e8d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 2 Mar 2018 13:37:07 +0100
Subject: universe normalisation: put equivalence class partition in UGraph

ie don't go through having Eq constraints but directly to the unionfind.
---
 engine/universes.ml  | 21 ++++++---------------
 engine/universes.mli |  2 --
 kernel/uGraph.ml     | 10 +++++-----
 kernel/uGraph.mli    |  5 ++++-
 4 files changed, 15 insertions(+), 23 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 27d5e3e23..d1caf40ac 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -524,8 +524,6 @@ let new_global_univ () =
 
 (** Simplification *)
 
-module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
-
 let add_list_map u t map =
   try
     let l = LMap.find u map in
@@ -533,8 +531,6 @@ let add_list_map u t map =
   with Not_found ->
     LMap.add u [t] map
 
-module UF = LevelUnionFind
-
 (** Precondition: flexible <= ctx *)
 let choose_canonical ctx flexible algs s =
   let global = LSet.diff s ctx in
@@ -920,7 +916,6 @@ let minimize_univ_variables ctx us algs left right cstrs =
 
 let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
-  let uf = UF.create () in
   (** Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
     Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
@@ -929,7 +924,7 @@ let normalize_context_set g ctx us algs weak =
     then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
     else Constraint.empty
   in
-  let csts =
+  let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
     let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
@@ -947,18 +942,14 @@ let normalize_context_set g ctx us algs weak =
     let g = UGraph.merge_constraints csts g in
       UGraph.constraints_of_universes g
   in
+  (* We ignore the trivial Prop/Set <= i constraints. *)
   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 && 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
+    Constraint.filter
+      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+                           (Level.is_prop l && d == Lt && Level.is_set r)))
+      csts
   in
   let noneqs = Constraint.union noneqs smallles in
-  let partition = UF.partition uf in
   let flex x = LMap.mem x us in
   let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
     let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
diff --git a/engine/universes.mli b/engine/universes.mli
index 4823c5746..a0a7749f8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -162,8 +162,6 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t ->
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-module UF : Unionfind.PartitionSig with type elt = Level.t
-
 val level_subst_of : universe_subst_fn -> universe_level_subst_fn
 val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d1644614..c37df4c5e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -768,18 +768,18 @@ let normalize_universes g =
     g.entries g
 
 let constraints_of_universes g =
+  let module UF = Unionfind.Make (LSet) (LMap) in
+  let uf = UF.create () in
   let constraints_of u v acc =
     match v with
     | Canonical {univ=u; ltle} ->
       UMap.fold (fun v strict acc->
         let typ = if strict then Lt else Le in
         Constraint.add (u,typ,v) acc) ltle acc
-    | Equiv v -> Constraint.add (u,Eq,v) acc
+    | Equiv v -> UF.union u v uf; acc
   in
-  UMap.fold constraints_of g.entries Constraint.empty
-
-let constraints_of_universes g =
-  constraints_of_universes (normalize_universes g)
+  let csts = UMap.fold constraints_of g.entries Constraint.empty in
+  csts, UF.partition uf
 
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index d4fba63fb..cca2eb472 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,10 @@ val empty_universes : t
 
 val sort_universes : t -> t
 
-val constraints_of_universes : t -> Constraint.t
+(** [constraints_of_universes g] returns [csts] and [partition] where
+   [csts] are the non-Eq constraints and [partition] is the partition
+   of the universes into equivalence classes. *)
+val constraints_of_universes : t -> Constraint.t * LSet.t list
 
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
-- 
cgit v1.2.3


From e6b732d6fbb84d54eb3796e9fa1d10421532f3cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 3 Mar 2018 23:47:54 +0100
Subject: minimize_univ_variables: remove [and right] abbreviation.

---
 engine/universes.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index d1caf40ac..ce1180764 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -842,9 +842,6 @@ let minimize_univ_variables ctx us algs left right cstrs =
         let left = List.uniquize (List.filter not_lower left) in
         (acc, left, LMap.union newlow lower)
       with Not_found -> acc, [], LMap.empty
-    and right =
-      try Some (LMap.find u right)
-      with Not_found -> None
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
@@ -878,9 +875,9 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    instantiate_with_lbound u lbound lower false true acc
     in
     let acc' acc = 
-      match right with
-      | None -> acc
-      | Some cstrs -> 
+      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
-- 
cgit v1.2.3


From 4baca7221917685210899b766e71782ddae4249f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 3 Mar 2018 23:49:39 +0100
Subject: minimize_univ_variables: bool*bool*univ*lowermap replaced by record

---
 engine/universes.ml | 40 +++++++++++++++++++++-------------------
 1 file changed, 21 insertions(+), 19 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index ce1180764..fe7f406b4 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -738,10 +738,12 @@ let lower_add l c m =
 let lower_of_list l =
   List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
 
+type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
+
 exception Found of Level.t * lowermap
 let find_inst insts v =
-  try LMap.iter (fun k (enf,alg,v',lower) ->
-    if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
+  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
+    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
 	insts; raise Not_found
   with Found (f,l) -> (f,l)
 
@@ -761,18 +763,18 @@ let compute_lbound left =
 	   sup (Universe.super l) lbound
 	 else None))
       None left
-  
-let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
+
+let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
   if enforce then
     let inst = Universe.make u in
     let cstrs' = enforce_leq lbound inst cstrs in
       (ctx, us, LSet.remove u algs, 
-       LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
-      (enforce, alg, inst, lower)
+       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+      {enforce; alg; lbound=inst; lower}
   else (* Actually instantiate *)
     (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
-    (enforce, alg, lbound, lower)
+     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+    {enforce; alg; lbound; lower}
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
@@ -798,7 +800,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let lbounds' = 
 	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
 	  | None -> lbounds
-	  | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
+          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
                                    lbounds
 	in (Univ.LMap.remove r left, lbounds'))
       left (left, Univ.LMap.empty)
@@ -810,7 +812,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let acc, left, newlow, lower =
           List.fold_left
 	  (fun (acc, left', newlow, lower') (d, l) ->
-	   let acc', (enf,alg,l',lower) = aux acc l in
+           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
 	   let l' =
 	     if enf then Universe.make l
 	     else l'
@@ -849,7 +851,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	  (* u is algebraic: we instantiate it with its lower bound, if any,
               or enforce the constraints if it is bounded from the top. *)
           let lower = remove_lower lbound lower in
-	  instantiate_with_lbound u lbound lower true false acc
+          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
 	  | Some l -> (* The lowerbound is directly a level *) 
@@ -861,18 +863,18 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
 	       let acc' = remove_alg l acc in
-		 instantiate_with_lbound u lbound lower false false acc'
-	     else acc, (true, false, lbound, lower)
+                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc'
+             else acc, {enforce=true; alg=false; lbound; lower}
 	  | None ->
 	     try
 	       (* Another universe represents the same lower bound,
                   we can share them with no harm. *)
 	       let can, lower = find_inst insts lbound in
                let lower = LMap.remove can lower in
-	       instantiate_with_lbound u (Universe.make can) lower false false acc
+               instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
 	  with Not_found -> 
 	    (* We set u as the canonical universe representing lbound *)
-	    instantiate_with_lbound u lbound lower false true acc
+            instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
     in
     let acc' acc = 
       match LMap.find u right with
@@ -881,7 +883,7 @@ let minimize_univ_variables ctx us algs left right 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), (enf,_,inst,lower as b)) = acc in
+            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
@@ -893,15 +895,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
     in
-      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
+      if not (LSet.mem u ctx) then acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
       else
 	let lbound = compute_lbound left in
 	  match lbound with
 	  | None -> (* Nothing to do *)
-	    acc' (acc, (true, false, Universe.make u, lower))
+            acc' (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
 	  | Some lbound ->
 	     try acc' (instantiate_lbound lbound) 
-	     with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
+             with Failure _ -> acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
-- 
cgit v1.2.3


From bc0246f5a570f70c7befb150d7b544032acbaf7e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 3 Mar 2018 23:59:48 +0100
Subject: niv minimization: remove [remove_lower] abbreviation

It's not long, used only once and it's easier to understand what it
does when it's inlined.
---
 engine/universes.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index fe7f406b4..1b1ce7cec 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -788,10 +788,6 @@ let _pr_constraints_map (cmap:constraints_map) =
 let remove_alg l (ctx, us, algs, insts, cstrs) =
   (ctx, us, LSet.remove l algs, insts, cstrs)
 
-let remove_lower u lower =
-  let levels = Universe.levels u in
-  LSet.fold (fun l acc -> LMap.remove l acc) levels lower
-    
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
     Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
@@ -850,7 +846,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	if alg then
 	  (* u is algebraic: we instantiate it with its lower bound, if any,
               or enforce the constraints if it is bounded from the top. *)
-          let lower = remove_lower lbound lower in
+          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
           instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
-- 
cgit v1.2.3


From 998093e64d1eae5ed20900e826a081fac54a9eb9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:13:00 +0100
Subject: univ minimization: comment compare_constraint_type

---
 engine/universes.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 1b1ce7cec..ca6ce7184 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -705,6 +705,7 @@ let pr_universe_body = function
 
 let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
 
+(* Eq < Le < Lt *)
 let compare_constraint_type d d' =
   match d, d' with
   | Eq, Eq -> 0
-- 
cgit v1.2.3


From 9384726b851097957a139907907ced72f1ae461b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:13:18 +0100
Subject: univ minimization: simplify try-with block around [find u left]

This makes it clear where the Not_found can come from.
---
 engine/universes.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index ca6ce7184..6b2c76036 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -804,8 +804,9 @@ let minimize_univ_variables ctx us algs left right cstrs =
   in
   let rec instance (ctx', us, algs, insts, cstrs as acc) u =
     let acc, left, lower =
-      try
-        let l = LMap.find u left in
+      match LMap.find u left with
+      | exception Not_found -> acc, [], LMap.empty
+      | l ->
 	let acc, left, newlow, lower =
           List.fold_left
 	  (fun (acc, left', newlow, lower') (d, l) ->
@@ -840,7 +841,6 @@ let minimize_univ_variables ctx us algs left right cstrs =
         in
         let left = List.uniquize (List.filter not_lower left) in
         (acc, left, LMap.union newlow lower)
-      with Not_found -> acc, [], LMap.empty
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
-- 
cgit v1.2.3


From 5e4690453afb7898d2760f18201740517ae99d70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:26:30 +0100
Subject: univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/

---
 engine/universes.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 6b2c76036..fcde6b29c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -789,6 +789,8 @@ let _pr_constraints_map (cmap:constraints_map) =
 let remove_alg l (ctx, us, algs, insts, cstrs) =
   (ctx, us, LSet.remove l algs, insts, cstrs)
 
+exception UpperBoundedAlg
+
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
     Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
@@ -887,7 +889,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	      else
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
-		with Option.IsNone -> failwith "")
+                with Option.IsNone -> raise UpperBoundedAlg)
 	      cstrs dangling
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
@@ -900,7 +902,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
             acc' (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
 	  | Some lbound ->
 	     try acc' (instantiate_lbound lbound) 
-             with Failure _ -> acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+             with UpperBoundedAlg ->
+               acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
-- 
cgit v1.2.3


From 0099a8f8e1a77a224ff133fc211d5a8b983a7dcc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:39:05 +0100
Subject: univ minimization: simplify try-with block around find_insts

---
 engine/universes.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index fcde6b29c..727e50d6b 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -865,15 +865,16 @@ let minimize_univ_variables ctx us algs left right cstrs =
                  instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc'
              else acc, {enforce=true; alg=false; lbound; lower}
 	  | None ->
-	     try
-	       (* Another universe represents the same lower bound,
-                  we can share them with no harm. *)
-	       let can, lower = find_inst insts lbound in
-               let lower = LMap.remove can lower in
-               instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
-	  with Not_found -> 
-	    (* We set u as the canonical universe representing lbound *)
-            instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+            begin match find_inst insts lbound with
+              | can, lower ->
+                (* Another universe represents the same lower bound,
+                   we can share them with no harm. *)
+                let lower = LMap.remove can lower in
+                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
+              | exception Not_found ->
+                (* We set u as the canonical universe representing lbound *)
+                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+            end
     in
     let acc' acc = 
       match LMap.find u right with
-- 
cgit v1.2.3


From c097b83dc9a33a2410e61b8d2aa667229fbd411c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:52:24 +0100
Subject: univ minimization: let-lift [not_lower]

---
 engine/universes.ml | 44 ++++++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 727e50d6b..7aaeee244 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -789,6 +789,27 @@ let _pr_constraints_map (cmap:constraints_map) =
 let remove_alg l (ctx, us, algs, insts, cstrs) =
   (ctx, us, LSet.remove l algs, insts, cstrs)
 
+let not_lower lower (d,l) =
+  (* We're checking if (d,l) is already implied by the lower
+     constraints on some level u. If it represents l < u (d is Lt
+     or d is Le and i > 0, the i < 0 case is impossible due to
+     invariants of Univ), and the lower constraints only have l <=
+     u then it is not implied. *)
+  Univ.Universe.exists
+    (fun (l,i) ->
+       let d =
+         if i == 0 then d
+         else match d with
+           | Le -> Lt
+           | d -> d
+       in
+       try let d' = LMap.find l lower in
+         (* If d is stronger than the already implied lower
+          * constraints we must keep it. *)
+         compare_constraint_type d d' > 0
+       with Not_found ->
+         (** No constraint existing on l *) true) l
+
 exception UpperBoundedAlg
 
 let minimize_univ_variables ctx us algs left right cstrs =
@@ -820,28 +841,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
               lower_add l d newlow, lower_union lower lower')
 	  (acc, [], LMap.empty, LMap.empty) l
         in
-        let not_lower (d,l) =
-        (* We're checking if (d,l) is already implied by the lower
-	  constraints on some level u. If it represents l < u (d is Lt
-	  or d is Le and i > 0, the i < 0 case is impossible due to
-	  invariants of Univ), and the lower constraints only have l <=
-	  u then it is not implied. *)
-          Univ.Universe.exists
-          (fun (l,i) ->
-             let d =
-               if i == 0 then d
-               else match d with
-                    | Le -> Lt
-                    | d -> d
-             in
-             try let d' = LMap.find l lower in
-                 (* If d is stronger than the already implied lower
-                  * constraints we must keep it. *)
-                 compare_constraint_type d d' > 0
-             with Not_found ->
-               (** No constraint existing on l *) true) l
-        in
-        let left = List.uniquize (List.filter not_lower left) in
+        let left = List.uniquize (List.filter (not_lower lower) left) in
         (acc, left, LMap.union newlow lower)
     in
     let instantiate_lbound lbound =
-- 
cgit v1.2.3


From 8e00ec838eadffb5c868fdbfa693471cdd80ef8c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:56:30 +0100
Subject: univ minimization: use shadowing more

This avoids having multiple highly similar things in scope when we
only want one of them.
---
 engine/universes.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 7aaeee244..c05157c9c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -817,27 +817,27 @@ let minimize_univ_variables ctx us algs left right cstrs =
     Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
       if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
       else (* Fixed universe, just compute its glb for sharing *)
-	let lbounds' = 
+        let lbounds =
 	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
 	  | None -> lbounds
           | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
                                    lbounds
-	in (Univ.LMap.remove r left, lbounds'))
+        in (Univ.LMap.remove r left, lbounds))
       left (left, Univ.LMap.empty)
   in
-  let rec instance (ctx', us, algs, insts, cstrs as acc) u =
+  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
     let acc, left, lower =
       match LMap.find u left with
       | exception Not_found -> acc, [], LMap.empty
       | l ->
 	let acc, left, newlow, lower =
           List.fold_left
-	  (fun (acc, left', newlow, lower') (d, l) ->
+          (fun (acc, left, newlow, lower') (d, l) ->
            let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
 	   let l' =
 	     if enf then Universe.make l
 	     else l'
-	   in acc', (d, l') :: left',
+           in acc', (d, l') :: left,
               lower_add l d newlow, lower_union lower lower')
 	  (acc, [], LMap.empty, LMap.empty) l
         in
@@ -861,8 +861,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
-	       let acc' = remove_alg l acc in
-                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc'
+               let acc = remove_alg l acc in
+                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
              else acc, {enforce=true; alg=false; lbound; lower}
 	  | None ->
             begin match find_inst insts lbound with
@@ -883,8 +883,8 @@ let minimize_univ_variables ctx us algs left right 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) -> 
+            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
@@ -893,7 +893,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
                 with Option.IsNone -> raise UpperBoundedAlg)
 	      cstrs dangling
 	    in
-	      (ctx', us, algs, insts, cstrs'), b
+              (ctx, us, algs, insts, cstrs), b
     in
       if not (LSet.mem u ctx) then acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
       else
@@ -905,13 +905,13 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	     try acc' (instantiate_lbound lbound) 
              with UpperBoundedAlg ->
                acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-  and aux (ctx', us, algs, seen, cstrs as acc) u =
+  and aux (ctx, us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
   in
-    LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> 
+    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
       if v == None then fst (aux acc u)
-      else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
+      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
       us (ctx, us, algs, lbounds, cstrs)
 
 let normalize_context_set g ctx us algs weak =
-- 
cgit v1.2.3


From fc4dd229797ae341127ee615ec6201e953124727 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:59:00 +0100
Subject: univ minimization: rename acc' -> enforce_uppers

---
 engine/universes.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index c05157c9c..3b7a40dab 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -876,7 +876,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
             end
     in
-    let acc' acc = 
+    let enforce_uppers acc =
       match LMap.find u right with
       | exception Not_found -> acc
       | cstrs ->
@@ -895,16 +895,17 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    in
               (ctx, us, algs, insts, cstrs), b
     in
-      if not (LSet.mem u ctx) then acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-      else
-	let lbound = compute_lbound left in
-	  match lbound with
-	  | None -> (* Nothing to do *)
-            acc' (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
-	  | Some lbound ->
-	     try acc' (instantiate_lbound lbound) 
-             with UpperBoundedAlg ->
-               acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+    if not (LSet.mem u ctx)
+    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+    else
+      let lbound = compute_lbound left in
+      match lbound with
+      | None -> (* Nothing to do *)
+        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
+      | Some lbound ->
+        try enforce_uppers (instantiate_lbound lbound)
+        with UpperBoundedAlg ->
+          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
   and aux (ctx, us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
-- 
cgit v1.2.3


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


From 3cab61587008d26405760a71bfd362f13a386701 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 01:15:30 +0100
Subject: univ minimization [enforce_upper]: replace Option.get with match

---
 engine/universes.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index c6682156c..764164c52 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -816,9 +816,9 @@ let enforce_uppers upper lbound cstrs =
       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)
+        match Universe.level lbound with
+        | Some lev -> Constraint.add (lev, d, r) cstrs
+        | None -> raise UpperBoundedAlg)
     cstrs upper
 
 let minimize_univ_variables ctx us algs left right cstrs =
-- 
cgit v1.2.3


From 02372d2ce62bec843b34ca65f87f6619871fe931 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 01:20:22 +0100
Subject: univ minimization: comment [enforce_uppers]

---
 engine/universes.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 764164c52..e98708724 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -811,6 +811,11 @@ let not_lower lower (d,l) =
          (** No constraint existing on l *) true) l
 
 exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+   constraints to [lbound], adding them to [cstrs].
+
+    @raise UpperBoundedAlg if any [upper] constraints are strict and
+   [lbound] algebraic. *)
 let enforce_uppers upper lbound cstrs =
   List.fold_left (fun cstrs (d, r) ->
       if d == Univ.Le then
-- 
cgit v1.2.3