1 open list
  2 open pool
  3 
  4 (* In this approach, we do not need each node to carry a Boolean mark.
  5    Instead, we use the hidden [adopter] field for this purpose. If a node is
  6    currently adopted by the old pool, then it has not been visited yet. If it
  7    is adopted by the new pool, then it has been visited. This technique
  8    presents several advantages with respect to a more naïve approach based on
  9    Boolean marks: 1- it re-uses the space taken up by the [adopter] field; 2-
 10    it does not a priori require the marks to be re-initialized after (or
 11    before) each traversal; 3- it allows a strong update, i.e. the nodes that
 12    have been visited do not have the same type as the nodes that have not yet
 13    been visited. *)
 14 
 15 val preorder
 16   [unvisited, visited, p : perm]
 17   exclusive visited =>
 18   (
 19     (* A pool of all nodes. *)
 20     nodes: pool unvisited,
 21     (* A list of the root nodes. *)
 22     roots: list dynamic,
 23     (* A function that visits a node, changing its state from
 24        [unvisited] to [visited], and returns its successors. *)
 25     visit: (consumes node: unvisited | p) -> (list dynamic | node @ visited)
 26     (* The permission [p] required by [visit]. *)
 27     | p
 28   )
 29     (* We return a new pool of the visited nodes. *)
 30     : pool visited
 31   =
 32 
 33   (* Create a new pool that adopts the visited nodes. *)
 34   let reached = Pool in
 35 
 36   let rec dfs (node: dynamic |
 37     nodes @ pool unvisited *
 38     reached @ pool visited *
 39     p
 40   ) : () =
 41     (* Perform a dynamic ownership test. *)
 42     if nodes owns node then begin
 43       (* This node has not been visited yet. *)
 44       take node from nodes;
 45       (* Visit it, and obtain a list of its successors. *)
 46       let successors = visit node in
 47       (* Mark this node visited by placing it in the new pool. *)
 48       give node to reached;
 49       (* Examine the successors. *)
 50       iter (successors, dfs)
 51     end
 52   in
 53 
 54   (* Examine each of the roots. *)
 55   iter (roots, dfs);
 56 
 57   (* Return the new pool. *)
 58   reached
 59 
 60 (* For a postorder traversal, our requirements must be slightly different.
 61    The action of marking a node as discovered and the action of visiting
 62    the node are performed at distinct instants in time. As a result, we
 63    need three node states instead of two. *)
 64 
 65 val prepostorder
 66   [unvisited, visiting, visited, p : perm]
 67   exclusive visited =>
 68   (
 69     (* A pool of all nodes. *)
 70     nodes: pool unvisited,
 71     (* A list of the root nodes. *)
 72     roots: list dynamic,
 73     (* A flag that indicates whether we should abort when a cycle is
 74        detected. *)
 75     detect: bool,
 76     (* A function that changes the state of a node from [unvisited]
 77        to [visiting] and returns its successors. *)
 78     pre: (consumes node: unvisited | p) -> (list dynamic | node @ visiting),
 79     (* A function that changes the state of a node from [visiting]
 80        to [visited]. *)
 81     post: (consumes node: visiting | p) -> (| node @ visited)
 82     (* The permission [p] required by [pre] and [post]. *)
 83     | p
 84   )
 85 : (
 86   (* A new pool of the visited nodes. *)
 87   pool visited,
 88   (* An option that indicates: 1. whether a cycle was detected and 2. if so,
 89      the list of nodes that were in the state [visiting] when the cycle was
 90      detected. These nodes form a path in the graph that ends in a cycle. *)
 91   option (list visiting)
 92 )
 93   =
 94 
 95   (* One might think that we need two new pools, which adopt the
 96      nodes in the [visiting] and [visited] states. Actually, we
 97      only need one pool, which adopts [visited] nodes. The nodes
 98      in the [visiting] state can simply be framed out. In short,
 99      the [null] adopter pointer serves as the mark for these nodes. *)
100   let completed = Pool in
101 
102   (* This reference is used when we have detected a cycle and are
103      building a list on the way back. *)
104   let path = newref nil in
105 
106   (* The Boolean value returned by [dfs] is [true] if everything
107      went well and [false] is a cycle was detected. *)
108   let rec dfs (node: dynamic |
109     nodes @ pool unvisited *
110     completed @ pool visited *
111     path @ ref (list visiting) *
112     p
113   ) : bool =
114     (* Perform a dynamic ownership test. *)
115     if nodes owns node then begin
116       (* This node has not been reached yet. *)
117       take node from nodes;
118       (* Change its state to [visiting] and obtain its successors. *)
119       let successors = pre node in
120       (* At this point, the node is not a member of any of the two pools. We
121          own it. Examine its successors, stopping the loop early if a cycle
122          is detected. *)
123       let ok = for_all (dfs, successors) in
124       (* After the recursive call, we still own this node, so we
125          know that its state has not changed: it is still [visiting]. *)
126       if ok then begin
127         (* Change its state to [visited]. *)
128         post node;
129         (* We can now place this node in the final pool. *)
130         give node to completed
131       end
132       else
133         (* If a cycle was detected during the recursive call, push
134            this node onto the path. *)
135         path := cons (node, !path);
136       (* In either case, propagate the result. *)
137       ok
138     end
139     else if completed owns node then
140       (* There is nothing to do. *)
141       true
142     else
143       (* There is a cycle. *)
144       not detect
145   in
146 
147   (* Examine each of the roots. *)
148   let ok = for_all (dfs, roots) in
149 
150   (* Return a pair of the new pool and (if a cycle was detected)
151      the path that was constructed. *)
152   let outcome : option (list visiting) =
153     if ok then none else some !path
154   in
155   completed, outcome
156 
157 (* TEMPORARY getting rid of the type annotation on [outcome]
158    would be nice. *)
159