diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml
index 07056a2b7f00edc1f7a00a5b171f084d91a4b140..8d71938a308dfe10ffcb3e7653ebb06129af25d7 100644
--- a/src/libraries/utils/wto.ml
+++ b/src/libraries/utils/wto.ml
@@ -153,8 +153,12 @@ module Make(N:sig
this loop with the lowest level. This vertex is also the deepest in the
stack and the neareast vertex from the root that is below [vertex] in
the spanning tree built by the DFS);
- - [partition] is returned completed. *)
- let rec visit ~pref state vertex partition =
+ - [partition] is returned completed.
+
+ A tail-recursive implementation of this function is now used to avoid
+ stack overflow errors on very large functions. This function is kept
+ for documentation purposes, as it is simpler and more readable. *)
+ let rec _visit ~pref state vertex partition =
match DFN.find state.dfn vertex with
(* The vertex is already in the partition *)
| Invisible -> NoLoop, partition (* skip it *)
@@ -171,7 +175,7 @@ module Make(N:sig
(* Visit all its successors *)
let succs = state.succs vertex in
let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
- let (loop',partition) = visit ~pref state succ partition in
+ let (loop',partition) = _visit ~pref state succ partition in
let loop = min_loop loop loop' in
(loop,partition)
) (NoLoop,partition) succs
@@ -211,7 +215,7 @@ module Make(N:sig
(* Restart the component analysis *)
let component = List.fold_left
(fun component succ ->
- let (loop,component) = visit ~pref state succ component in
+ let (loop,component) = _visit ~pref state succ component in
(* Since we reset the component we should have no loop *)
assert (loop = NoLoop);
component
@@ -224,12 +228,123 @@ module Make(N:sig
be added during the second visit of the SCC. *)
(loop,partition)
+
+ (* Types for the tail-recursive function of [visit]. *)
+
+ (* Whether to apply [min_loop] at the end of the visit of a vertex. *)
+ type kind = Default | MinLoop
+
+ (* [visit] contains two recursive calls; its tail-recursive version is split
+ into several steps accordingly. For the visit of a vertex, this type
+ indicates the step that must be done. *)
+ type step =
+ | Start of kind
+ (* Starts the visit of a vertex. If [kind] = [MinLoop], then apply
+ [min_loop] between the previous and the resulting loop. *)
+ | Continue
+ (* Resumes the visit of a vertex after the first recursive call. *)
+ | End of N.t partition
+ (* Ends the visit of a vertex after the second recursive call. *)
+ | Min_loop of loop
+ (* Apply [Min_loop] between [loop] (from the previous result) and the
+ current loop. *)
+
+ (* The list of steps that must be done, with their related vertex. It starts
+ with [init, Start Default] and grows for each original recursive call. *)
+ type continuation = (N.t * step) list
+
+ (** Tail-recursive version of the [visit] function above. *)
+ let tail_recursive_visit ~pref state vertex partition =
+ (* Visit according to the next step to be done. *)
+ let rec visit (cont: continuation) (loop, partition) =
+ match cont with
+ | [] -> loop, partition
+ | (vertex, step) :: cont ->
+ match step with
+ | Start kind ->
+ let cont =
+ if kind = MinLoop then (vertex, Min_loop loop) :: cont else cont
+ in
+ visit_first cont vertex partition
+ | Continue ->
+ visit_second cont vertex loop partition
+ | End partition' ->
+ assert (loop = NoLoop);
+ let r = NoLoop, Component (vertex, partition) :: partition' in
+ visit cont r
+ | Min_loop loop' ->
+ let r = min_loop loop' loop, partition in
+ visit cont r
+
+ (* Visits all successors of [vertex], then continue with [next] and the
+ [continuation]. The status of [vertex] is first set to [status]. *)
+ and visit_succs continuation next (vertex, status) kind acc =
+ let succs = state.succs vertex in
+ DFN.replace state.dfn vertex status;
+ let list = List.map (fun v -> v, Start kind) succs in
+ visit (list @ (vertex, next) :: continuation) (NoLoop, acc)
+
+ and visit_first continuation vertex partition =
+ match DFN.find state.dfn vertex with
+ (* The vertex is already in the partition *)
+ | Invisible ->
+ visit continuation (NoLoop, partition) (* skip it *)
+ (* The vertex have been visited but is not yet in the partition *)
+ | Parent i ->
+ visit continuation (Loop (vertex,i), partition) (* we are in a loop *)
+ (* The vertex have not been visited yet *)
+ | exception Not_found ->
+ (* Put the current vertex into the stack *)
+ Stack.push vertex state.stack;
+ (* Number it and mark it as visited *)
+ let n = state.num + 1 in
+ state.num <- n;
+ (* Visit all its successors. *)
+ visit_succs continuation Continue (vertex, Parent n) MinLoop partition
+
+ and visit_second continuation vertex loop partition =
+ match loop with
+ (* We are not in a loop. Add the vertex to the partition *)
+ | NoLoop ->
+ let _ = Stack.pop state.stack in
+ DFN.replace state.dfn vertex Invisible;
+ visit continuation (NoLoop,Node(vertex)::partition)
+ (* We are in a loop and the current vertex is the head of this loop *)
+ | Loop(head,_) when N.equal head vertex ->
+ (* Unmark all vertices in the loop, and, if pref is given, try to
+ return a better head *)
+ let rec reset_SCC best_head =
+ (** pop until vertex *)
+ let element = Stack.pop state.stack in
+ DFN.remove state.dfn element;
+ if not (N.equal element vertex) then begin
+ (** the strict is important because we are conservative *)
+ let best_head =
+ if pref best_head element < 0 then element else best_head
+ in
+ reset_SCC best_head
+ end
+ else
+ best_head
+ in
+ let best_head = reset_SCC vertex in
+ let vertex = if N.equal best_head vertex then vertex else best_head in
+ (* Makes [vertex] invisible and visits all its successors. *)
+ visit_succs continuation (End partition) (vertex, Invisible) Default []
+ | _ ->
+ (* [vertex] is part of a strongly connected component but is not the
+ head. Do not update partition; the vertex will
+ be added during the second visit of the SCC. *)
+ visit continuation (loop, partition)
+ in
+ visit [vertex, Start Default] (NoLoop, partition)
+
type pref = N.t -> N.t -> int
let partition ~pref ~init ~succs =
let state = {dfn = DFN.create 17; num = 0; succs;
stack = Stack.create () } in
- let loop,component = visit ~pref state init [] in
+ let loop,component = tail_recursive_visit ~pref state init [] in
assert (loop = NoLoop);
component