Skip to content

Commit

Permalink
Merge PR coq#16127: [acyclicGraph] is pure
Browse files Browse the repository at this point in the history 
Reviewed-by: ppedrot
Reviewed-by: mattam82
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
  • Loading branch information
@coqbot-app @ppedrot
coqbot-app[bot] and ppedrot committed Jun 19, 2022
2 parents 83ce48f + 548921f commit 7c2bf97
Showing 1 changed file with 76 additions and 100 deletions.
176 changes: 76 additions & 100 deletions lib/acyclicGraph.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ module Make (Point:Point) = struct
val mem : Point.t -> table -> bool
val find : Point.t -> table -> t
val repr : t -> table -> Point.t
val hash : t -> int
end =
struct
type t = int
Expand Down Expand Up @@ -95,13 +96,12 @@ module Make (Point:Point) = struct
tab_fwd = Int.Map.add n x t.tab_fwd;
tab_bwd = Point.Map.add x n t.tab_bwd;
}
let hash x = x
end

module PMap = Index.Map
module PSet = Index.Set

type status = NoMark | Visited | WeakVisited | ToMerge

(* Comparison on this type is pointer equality *)
type canonical_node =
{ canon: Index.t;
Expand All @@ -111,7 +111,6 @@ module Make (Point:Point) = struct
rank : int;
klvl: int;
ilvl: int;
mutable status: status
}

(* A Point.t is either an alias for another one, or a canonical one,
Expand All @@ -127,23 +126,23 @@ module Make (Point:Point) = struct
n_nodes : int; n_edges : int;
table : Index.table }

(** Used to cleanup mutable marks if a traversal function is
interrupted before it has the opportunity to do it itself. *)
let unsafe_cleanup_marks g =
let iter _ n = match n with
| Equiv _ -> ()
| Canonical n -> n.status <- NoMark
in
PMap.iter iter g.entries
module CN = struct
type t = canonical_node
let equal x y = x.canon == y.canon
let hash x = Index.hash x.canon
end

let rec cleanup_marks g =
try unsafe_cleanup_marks g
with e ->
(* The only way unsafe_cleanup_marks may raise an exception is when
a serious error (stack overflow, out of memory) occurs, or a signal is
sent. In this unlikely event, we relaunch the cleanup until we finally
succeed. *)
cleanup_marks g; raise e
module Status = struct
module Internal = Hashtbl.Make(CN)

(** we could experiment with creation size based on the size of [g] *)
let create (g:t) = Internal.create 17

let mem = Internal.mem
let find = Internal.find
let replace = Internal.replace
let fold = Internal.fold
end

(* Every Point.t has a unique canonical arc representative *)

Expand All @@ -155,7 +154,6 @@ module Make (Point:Point) = struct
PMap.modify u (fun _ a ->
match a with
| Canonical n ->
n.status <- NoMark;
Equiv v
| _ -> assert false) g.entries;
index = g.index;
Expand All @@ -172,8 +170,7 @@ module Make (Point:Point) = struct
PMap.modify n.canon
(fun _ a ->
match a with
| Canonical n' ->
n'.status <- NoMark;
| Canonical _ ->
Canonical n
| _ -> assert false)
g.entries }
Expand Down Expand Up @@ -231,7 +228,6 @@ module Make (Point:Point) = struct
(PMap.mem u.canon v.ltle ||
PMap.exists (fun l _ -> u == repr g l) v.ltle))
) u.gtge;
assert (u.status = NoMark);
assert (Index.equal l u.canon);
assert (u.ilvl > g.index);
assert (not (PMap.mem u.canon u.ltle));
Expand Down Expand Up @@ -281,16 +277,6 @@ module Make (Point:Point) = struct
let g = change_node g u in
u.gtge, u, g

(* [revert_graph] rollbacks the changes made to mutable fields in
nodes in the graph.
[to_revert] contains the touched nodes. *)
let revert_graph to_revert g =
List.iter (fun t ->
match PMap.find t g.entries with
| Equiv _ -> ()
| Canonical t ->
t.status <- NoMark) to_revert

exception AbortBackward of t
exception CycleDetected

Expand All @@ -304,25 +290,25 @@ module Make (Point:Point) = struct
corresponding step numbers of the algorithm described in Section
5.1 of this paper. *)

let rec backward_traverse to_revert b_traversed count g x =
let rec backward_traverse status b_traversed count g x =
let count = count - 1 in
if count < 0 then begin
revert_graph to_revert g;
raise_notrace (AbortBackward g)
end;
if x.status = NoMark then begin
x.status <- Visited;
let to_revert = x.canon::to_revert in
if Status.mem status x then b_traversed, count, g
else begin
Status.replace status x ();
let gtge, x, g = get_gtge g x in
let to_revert, b_traversed, count, g =
PSet.fold (fun y (to_revert, b_traversed, count, g) ->
let b_traversed, count, g =
PSet.fold (fun y (b_traversed, count, g) ->
let y = repr g y in
backward_traverse to_revert b_traversed count g y)
gtge (to_revert, b_traversed, count, g)
backward_traverse status b_traversed count g y)
gtge (b_traversed, count, g)
in
to_revert, x.canon::b_traversed, count, g
x.canon::b_traversed, count, g
end
else to_revert, b_traversed, count, g

let backward_traverse count g x = backward_traverse (Status.create g) [] count g x

let rec forward_traverse f_traversed g v_klvl x y =
let y = repr g y in
Expand All @@ -345,25 +331,29 @@ module Make (Point:Point) = struct
f_traversed, g
else f_traversed, g

let rec find_to_merge to_revert g x v =
let rec find_to_merge status g x v =
let x = repr g x in
match x.status with
| Visited -> false, to_revert | ToMerge -> true, to_revert
| NoMark ->
let to_revert = x::to_revert in
if Index.equal x.canon v then
begin x.status <- ToMerge; true, to_revert end
match Status.find status x with
| merge -> merge
| exception Not_found ->
if Index.equal x.canon v then begin
Status.replace status x true;
true
end
else
begin
let merge, to_revert = PSet.fold
(fun y (merge, to_revert) ->
let merge', to_revert = find_to_merge to_revert g y v in
merge' || merge, to_revert) x.gtge (false, to_revert)
let merge = PSet.fold
(fun y merge ->
let merge' = find_to_merge status g y v in
merge' || merge) x.gtge false
in
x.status <- if merge then ToMerge else Visited;
merge, to_revert
Status.replace status x merge;
merge
end
| _ -> assert false

let find_to_merge g x v =
let status = Status.create g in
status, find_to_merge status g x v

let get_new_edges g to_merge =
(* Computing edge sets. *)
Expand Down Expand Up @@ -409,8 +399,7 @@ module Make (Point:Point) = struct
let b_traversed, v_klvl, g =
let u = repr g u in
try
let to_revert, b_traversed, _, g = backward_traverse [] [] (u.klvl + 1) g u in
revert_graph to_revert g;
let b_traversed, _, g = backward_traverse (u.klvl + 1) g u in
let v_klvl = u.klvl in
b_traversed, v_klvl, g
with AbortBackward g ->
Expand All @@ -430,16 +419,13 @@ module Make (Point:Point) = struct
let to_merge, b_reindex, f_reindex =
if (repr g u).klvl = v_klvl then
begin
let merge, to_revert = find_to_merge [] g u v in
let r =
if merge then
List.filter (fun u -> u.status = ToMerge) to_revert,
List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed,
List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed
else [], b_traversed, f_traversed
in
List.iter (fun u -> u.status <- NoMark) to_revert;
r
let status, merge = find_to_merge g u v in
if merge then
let not_merged u = try not (Status.find status (repr g u)) with Not_found -> true in
Status.fold (fun u merged acc -> if merged then u::acc else acc) status [],
List.filter not_merged b_traversed,
List.filter not_merged f_traversed
else [], b_traversed, f_traversed
end
else [], b_traversed, f_traversed
in
Expand Down Expand Up @@ -512,10 +498,6 @@ module Make (Point:Point) = struct
change_node g v
with
| CycleDetected as e -> raise_notrace e
| e ->
(* Unlikely event: fatal error or signal *)
let () = cleanup_marks g in
raise e

let add ?(rank=0) v g =
if Index.mem v g.table then raise AlreadyDeclared
Expand All @@ -529,7 +511,6 @@ module Make (Point:Point) = struct
rank;
klvl = 0;
ilvl = g.index;
status = NoMark;
}
in
let entries = PMap.add v (Canonical node) g.entries in
Expand Down Expand Up @@ -581,50 +562,45 @@ module Make (Point:Point) = struct
- we do a BFS rather than a DFS because we expect to have a short
path (typically, the shortest path has length 1)
*)
exception Found of canonical_node list
exception Found
type visited = WeakVisited | Visited
let search_path strict u v g =
let rec loop to_revert todo next_todo =
let rec loop status todo next_todo =
match todo, next_todo with
| [], [] -> to_revert (* No path found *)
| [], _ -> loop to_revert next_todo []
| [], [] -> () (* No path found *)
| [], _ -> loop status next_todo []
| (u, strict)::todo, _ ->
if u.status = Visited || (u.status = WeakVisited && strict)
then loop to_revert todo next_todo
else
let to_revert =
if u.status = NoMark then u::to_revert else to_revert
in
u.status <- if strict then WeakVisited else Visited;
let is_visited = match Status.find status u with
| Visited -> true
| WeakVisited -> strict
| exception Not_found -> false
in
if is_visited
then loop status todo next_todo
else begin
Status.replace status u (if strict then WeakVisited else Visited);
if try PMap.find v.canon u.ltle || not strict
with Not_found -> false
then raise_notrace (Found to_revert)
then raise_notrace Found
else
begin
let next_todo =
PMap.fold (fun u strictu next_todo ->
let strict = not strictu && strict in
let u = repr g u in
if u == v && not strict then raise_notrace (Found to_revert)
if u == v && not strict then raise_notrace Found
else if topo_compare u v = 1 then next_todo
else (u, strict)::next_todo)
u.ltle next_todo
in
loop to_revert todo next_todo
loop status todo next_todo
end
end
in
if u == v then not strict
else
try
let res, to_revert =
try false, loop [] [u, strict] []
with Found to_revert -> true, to_revert
in
List.iter (fun u -> u.status <- NoMark) to_revert;
res
with e ->
(* Unlikely event: fatal error or signal *)
let () = cleanup_marks g in
raise e
try loop (Status.create g) [u, strict] []; false
with Found -> true

(** Uncomment to debug the cycle detection algorithm. *)
(*let insert_edge strict ucan vcan g =
Expand Down

0 comments on commit 7c2bf97

Please sign in to comment.