From 23d30ddc2a7cdfa3f71e99f57d36818b16ad40b7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Jul 2014 23:45:01 +0200
Subject: Cleanup code related to the constraint solving, which sits now
 outside the kernel in library/universes.ml.

---
 kernel/indtypes.ml        |   1 -
 kernel/univ.ml            | 100 ++--------------------------------------------
 kernel/univ.mli           |  27 +++++--------
 library/universes.ml      |  70 ++++++++++++++++++++++++++++++++
 library/universes.mli     |   5 +++
 pretyping/inductiveops.ml |   6 +--
 toplevel/command.ml       |   2 +-
 7 files changed, 92 insertions(+), 119 deletions(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cc56428fa4..ee4a404a7c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -320,7 +320,6 @@ let typecheck_inductive env ctx mie =
 	in
 	  match s with
 	  | Type u when expltype (* Explicitly polymorphic *) ->
-	      (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *)
 	    (* The polymorphic level is a function of the level of the *)
 	    (* conclusions of the parameters *)
             (* We enforce [u >= lev] in case [lev] has a strict upper *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6a11251b06..256ce5e92c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1657,110 +1657,18 @@ let sort_universes orig =
   in
   Array.fold_left_i fold sorted types
 
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
-
 (* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
+   occur in a universe *)
 
-let remove_large_constraint u v min = 
+let univ_level_mem u v = Huniv.mem (Expr.make u) v
+
+let univ_level_rem u v min = 
   match Universe.level v with
   | Some u' -> if Level.equal u u' then min else v
   | None -> Huniv.remove (Universe.Expr.make u) v
 
-(* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
-let is_direct_constraint u v =
-  match Universe.level v with
-  | Some u' -> Level.equal u u'
-  | None -> 
-    let expr = Universe.Expr.make u in
-      Universe.exists (Universe.Expr.equal expr) v
-
-(*
-   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 -> is_direct_constraint u v
-  | None -> false
-
-let solve_constraints_system levels level_bounds level_min =
-  let levels =
-    Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> 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) <- remove_large_constraint u v.(i) level_min.(i)
-      | None -> ()
-    done
-  done;
-  v
-
-let subst_large_constraint u u' v =
-  match level u with
-  | Some u ->
-      (* if is_direct_constraint u v then  *)
-	Universe.sup u' (remove_large_constraint u v type0m_univ)
-      (* else v *)
-  | _ ->
-      anomaly (Pp.str "expect a universe level")
-
-let subst_large_constraints =
-  List.fold_right (fun (u,u') -> subst_large_constraint u u')
-
-let no_upper_constraints u cst =
-  match level u with
-  | Some u ->
-    let test (u1, _, _) =
-      not (Int.equal (Level.compare u1 u) 0) in
-    Constraint.for_all test cst
-  | _ -> anomaly (Pp.str "no_upper_constraints")
-
 (* Is u mentionned in v (or equals to v) ? *)
 
-let univ_depends u v =
-  match atom u with
-    | Some u -> Huniv.mem u v
-    | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg")
 
 (**********************************************************************)
 (** Universe polymorphism                                             *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8166d75e62..9b68dbc8ce 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -129,6 +129,15 @@ val super : universe -> universe
 
 val universe_level : universe -> universe_level option
 
+(** [univ_level_mem l u] Is l is mentionned in u ? *)
+
+val univ_level_mem : universe_level -> universe -> bool
+
+(** [univ_level_rem u v min] removes [u] from [v], resulting in [min]
+    if [v] was exactly [u]. *)
+
+val univ_level_rem : universe_level -> universe -> universe -> universe
+
 (** {6 Graphs of universes. } *)
 
 type universes
@@ -211,24 +220,6 @@ val constraints_of_universes : universes -> constraints
 val check_constraint  : universes -> univ_constraint -> bool
 val check_constraints : constraints -> universes -> bool
 
-(** {6 Support for old-style sort-polymorphism } *)
-
-val solve_constraints_system : universe option array -> universe array -> universe array ->
-  universe array
-
-val remove_large_constraint : universe_level -> universe -> universe -> universe
-
-val subst_large_constraint : universe -> universe -> universe -> universe
-
-val subst_large_constraints :
-  (universe * universe) list -> universe -> universe
-
-val no_upper_constraints : universe -> constraints -> bool
-
-(** Is u mentionned in v (or equals to v) ? *)
-
-val univ_depends : universe -> universe -> bool
-
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
diff --git a/library/universes.ml b/library/universes.ml
index e84f1f975c..1c704bc229 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
diff --git a/library/universes.mli b/library/universes.mli
index 5b09519286..2fc476732c 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -243,3 +243,8 @@ val minimize_univ_variables :
            Univ.LSet.t * Univ.universe option Univ.LMap.t *
 	     Univ.LSet.t *
            (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
+
+(** {6 Support for old-style sort-polymorphism } *)
+
+val solve_constraints_system : universe option array -> universe array -> universe array ->
+  universe array
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07a3378363..313bf6110c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -480,13 +480,13 @@ let rec instantiate_universes env evdref scl is = function
       d :: instantiate_universes env evdref scl is (sign, exp)
   | d::sign, None::exp ->
       d :: instantiate_universes env evdref scl is (sign, exp)
-  | (na,None,ty)::sign, Some u::exp ->
+  | (na,None,ty)::sign, Some l::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
-      let u = Univ.Universe.make u in
+      let u = Univ.Universe.make l in
       let s =
 	(* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
-        if univ_depends u is then
+        if univ_level_mem l is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstrained sort: replace by fresh universe *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4fc574daf5..ff2e89351e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -413,7 +413,7 @@ let inductive_levels env evdref poly arities inds =
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
-  let levels' = Univ.solve_constraints_system (Array.of_list levels)
+  let levels' = Universes.solve_constraints_system (Array.of_list levels)
     (Array.of_list cstrs_levels) (Array.of_list min_levels)
   in
   let evd =
-- 
cgit v1.2.3