Cleanup code related to the constraint solving, which sits now outside the

kernel in library/universes.ml.

1 files changed, 70 insertions, 0 deletions

diff --git a/library/universes.ml b/library/universes.ml
index e84f1f975..1c704bc22 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -930,3 +930,73 @@ let refresh_constraints univs (ctx, cstrs) =
       else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
+
+
+(**********************************************************************)
+(* Tools for sort-polymorphic inductive types                         *)
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
+
+(*
+   Solve a system of universe constraint of the form
+
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
+
+where
+
+  - the ui (1 <= i <= n) are universe variables,
+  - the sjk select subsets of the ui for each equations,
+  - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let is_direct_sort_constraint s v = match s with
+  | Some u -> univ_level_mem u v
+  | None -> false
+
+let solve_constraints_system levels level_bounds level_min =
+  let open Univ in
+  let levels =
+    Array.map (Option.map
+		 (fun u -> match Universe.level u with 
+		 | Some u -> u 
+		 | _ -> Errors.anomaly (Pp.str"expects Atom")))
+      levels in
+  let v = Array.copy level_bounds in
+  let nind = Array.length v in
+  let clos = Array.map (fun _ -> Int.Set.empty) levels in
+  (* First compute the transitive closure of the levels dependencies *)
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+	clos.(i) <- Int.Set.add j clos.(i);
+    done;
+  done;
+  let rec closure () = 
+    let continue = ref false in
+      Array.iteri (fun i deps -> 
+	let deps' = 
+	  Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
+	in 
+	  if Int.Set.equal deps deps' then ()
+	  else (clos.(i) <- deps'; continue := true))
+	clos;
+      if !continue then closure ()
+      else ()
+  in 
+  closure ();
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
+	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
+	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
+    done;
+    for j=0 to nind-1 do
+      match levels.(j) with
+      | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i)
+      | None -> ()
+    done
+  done;
+  v