aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:00:40 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:00:40 +0200
commit56be411d5c582d6f644129dabda7ba036a4419a7 (patch)
treedef26fef6fc8b864253040206a099b14c5823703 /engine
parentf6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff)
parent3490e3c0b7bbd574228725f8132082c519d0f1a2 (diff)
Merge PR #7495: Fix restrict_universe_context
Diffstat (limited to 'engine')
-rw-r--r--engine/univops.ml85
-rw-r--r--engine/univops.mli5
2 files changed, 14 insertions, 76 deletions
diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa250..3fd518490 100644
--- a/engine/univops.ml
+++ b/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)
diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414c..0b37ab975 100644
--- a/engine/univops.mli
+++ b/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