From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 engine/univops.ml | 100 +++++++-----------------------------------------------
 1 file changed, 12 insertions(+), 88 deletions(-)

(limited to 'engine/univops.ml')

diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa25..7f9672f8 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -11,103 +11,27 @@
 open Univ
 open Constr
 
-let universes_of_constr env c =
-  let open Declarations in
-  let rec aux s c = 
+let universes_of_constr c =
+  let rec aux s c =
     match kind c with
     | Const (c, u) ->
-      begin match (Environ.lookup_constant c env).const_universes with
-        | Polymorphic_const _ ->
           LSet.fold LSet.add (Instance.levels u) s
-        | Monomorphic_const (univs, _) ->
-          LSet.union s univs
-      end
     | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-      begin match (Environ.lookup_mind mind env).mind_universes with
-        | Cumulative_ind _ | Polymorphic_ind _ ->
           LSet.fold LSet.add (Instance.levels u) s
-        | Monomorphic_ind (univs,_) ->
-          LSet.union s univs
-      end
     | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
 
-type graphnode = {
-  mutable up : constraint_type LMap.t;
-  mutable visited : bool
-}
-
-let merge_types d d0 =
-  match d, d0 with
-  | _, Lt | Lt, _ -> Lt
-  | Le, _ | _, Le -> Le
-  | Eq, Eq -> Eq
-
-let merge_up d b up =
-  let find = try Some (LMap.find b up) with Not_found -> None in
-  match find with
-  | Some d0 ->
-    let d = merge_types d d0 in
-    if d == d0 then up else LMap.add b d up
-  | None -> LMap.add b d up
-
-let add_up a d b graph =
-  let node, graph =
-    try LMap.find a graph, graph
-    with Not_found ->
-      let node = { up = LMap.empty; visited = false } in
-      node, LMap.add a node graph
-  in
-  node.up <- merge_up d b node.up;
-  graph
-
-(* for each node transitive close until you find a non removable, discard the rest *)
-let transitive_close removable graph =
-  let rec do_node a node =
-    if not node.visited
-    then
-      let keepup =
-        LMap.fold (fun b d keepup ->
-            if not (LSet.mem b removable)
-            then merge_up d b keepup
-            else
-              begin
-                match LMap.find b graph with
-                | bnode ->
-                  do_node b bnode;
-                  LMap.fold (fun k d' keepup ->
-                    merge_up (merge_types d d') k keepup)
-                    bnode.up keepup
-                | exception Not_found -> keepup
-              end
-          )
-          node.up LMap.empty
-      in
-      node.up <- keepup;
-      node.visited <- true
-  in
-  LMap.iter do_node graph
-
-let restrict_universe_context (univs,csts) keep =
-  let removable = LSet.diff univs keep in
-  let (csts, rem) =
-    Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
-        if LSet.mem a removable || LSet.mem b removable
-        then (csts, add_up a d b rem)
-        else (Constraint.add cst csts, rem))
-      csts (Constraint.empty, LMap.empty)
-  in
-  transitive_close removable rem;
-  let csts =
-    LMap.fold (fun a node csts ->
-        if LSet.mem a removable
-        then csts
-        else
-          LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
-            node.up csts)
-      rem csts
-  in
+let restrict_universe_context (univs, csts) keep =
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
   (LSet.inter univs keep, csts)
-- 
cgit v1.2.3