Fix restrict_universe_context

dev/ci/user-overlays/07495-gares-elpi-test-bug.sh

@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then
+
+    # this branch contains a commit not present on coq-master that triggers
+    # the universe restriction bug #7472
+    Elpi_CI_BRANCH=overlay-7495
+    Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git
+
+fi

engine/univops.ml

@@ -35,79 +35,14 @@ let universes_of_constr env c =
     | _ -> 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)

engine/univops.mli

@@ -14,5 +14,8 @@ open Univ
 (** The universes of monomorphic constants appear. *)
 val universes_of_constr : Environ.env -> constr -> LSet.t
 
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t

kernel/uGraph.ml

@@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g =
     let () = cleanup_universes g in
     raise e
 
-let add_universe vlev strict g =
+let add_universe_gen vlev g =
   try
     let _arcv = UMap.find vlev g.entries in
       raise AlreadyDeclared
@@ -520,8 +520,14 @@ let add_universe vlev strict g =
     }
     in
     let entries = UMap.add vlev (Canonical v) g.entries in
-    let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in
-    insert_edge strict (get_set_arc g) v g
+    { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v
+
+let add_universe vlev strict g =
+  let g, v = add_universe_gen vlev g in
+  insert_edge strict (get_set_arc g) v g
+
+let add_universe_unconstrained vlev g =
+  fst (add_universe_gen vlev g)
 
 exception Found_explanation of explanation
 
@@ -696,6 +702,9 @@ let enforce_univ_lt u v g =
     error_inconsistency Lt u v (get_explanation false v u g)
 
 let empty_universes =
+  { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+
+let initial_universes =
   let set_arc = Canonical {
     univ = Level.set;
     ltle = LMap.empty;
@@ -718,9 +727,6 @@ let empty_universes =
   let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in
   enforce_univ_lt Level.prop Level.set empty
 
-(* Prop = Set is forbidden here. *)
-let initial_universes = empty_universes
-
 let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries
 
 let enforce_constraint cst g =
@@ -780,6 +786,42 @@ let constraints_of_universes g =
   let csts = UMap.fold constraints_of g.entries Constraint.empty in
   csts, UF.partition uf
 
+(* domain g.entries = kept + removed *)
+let constraints_for ~kept g =
+  (* rmap: partial map from canonical universes to kept universes *)
+  let rmap, csts = LSet.fold (fun u (rmap,csts) ->
+      let arcu = repr g u in
+      if LSet.mem arcu.univ kept then
+        LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts
+      else
+        match LMap.find arcu.univ rmap with
+        | v -> rmap, enforce_eq_level u v csts
+        | exception Not_found -> LMap.add arcu.univ u rmap, csts)
+      kept (LMap.empty,Constraint.empty)
+  in
+  let rec add_from u csts todo = match todo with
+    | [] -> csts
+    | (v,strict)::todo ->
+      let v = repr g v in
+      (match LMap.find v.univ rmap with
+       | v ->
+         let d = if strict then Lt else Le in
+         let csts = Constraint.add (u,d,v) csts in
+         add_from u csts todo
+       | exception Not_found ->
+         (* v is not equal to any kept universe *)
+         let todo = LMap.fold (fun v' strict' todo ->
+             (v',strict || strict') :: todo)
+             v.ltle todo
+         in
+         add_from u csts todo)
+  in
+  LSet.fold (fun u csts ->
+      let arc = repr g u in
+      LMap.fold (fun v strict csts -> add_from u csts [v,strict])
+        arc.ltle csts)
+    kept csts
+
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
     will be strict most of the time), but is not necessarily minimal.

kernel/uGraph.mli

@@ -49,13 +49,15 @@ exception AlreadyDeclared
 
 val add_universe : Level.t -> bool -> t -> t
 
+(** Add a universe without (Prop,Set) <= u *)
+val add_universe_unconstrained : Level.t -> t -> t
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
 
 (** The empty graph of universes *)
 val empty_universes : t
-[@@ocaml.deprecated "Use UGraph.initial_universes"]
 
 val sort_universes : t -> t
 
@@ -64,6 +66,12 @@ val sort_universes : t -> t
    of the universes into equivalence classes. *)
 val constraints_of_universes : t -> Constraint.t * LSet.t list
 
+(** [constraints_for ~kept g] returns the constraints about the
+   universes [kept] in [g] up to transitivity.
+
+    eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *)
+val constraints_for : kept:LSet.t -> t -> Constraint.t
+
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)