1 open list
 2 open pool
 3 
 4 (* A depth-first preorder traversal of a graph. *)
 5 
 6 (* The code is polymorphic in the type of the graph nodes. Furthermore,
 7    the code allows the type of a node to change as the node is visited.
 8    The unvisited nodes have type [unvisited], while the visited nodes
 9    have type [visited]. Both of these types are assumed to be exclusive. *)
10 
11 (* We assume that all nodes are initially adopted by the object [nodes],
12    which has type [pool unvisited]. When a node is visited, it is taken
13    away from this pool; its type changes from [unvisited] to [visited];
14    and it is then adopted by a new pool, which has type [pool visited].
15    At the end of the traversal, the original pool contains the unreachable
16    nodes, while the new pool contains the reachable nodes. *)
17 
18 (* We require a list [roots] of the root nodes for the traversal. We also
19    require a function [visit], which changes the state of its node argument
20    from [unvisited] to [visited], and returns a list of this node's
21    successors. *)
22 
23 (* The function [visit] may require a permission [p]. We echo this
24    requirement. *)
25 
26 val preorder:
27   [unvisited, visited, p : perm]
28   exclusive visited =>
29   (
30     (* A pool of all nodes. *)
31     nodes: pool unvisited,
32     (* A list of the root nodes. *)
33     roots: list dynamic,
34     (* A function that visits a node, changing its state from
35        [unvisited] to [visited], and returns its successors. *)
36     visit: (consumes node: unvisited | p) -> (list dynamic | node @ visited)
37     (* The permission [p] required by [visit]. *)
38     | p
39   )
40     (* We return a new pool of the visited nodes. *)
41     -> pool visited
42 
43 (* A more general traversal function, which allows a pre- and a post-action,
44    and optionally detects a cycle in the graph. *)
45 
46 (* Because the pre- and post-action are distinguished, there are three node
47    states: [unvisited], [visiting], and [visited]. *)
48 
49 val prepostorder:
50   [unvisited, visiting, visited, p : perm]
51   exclusive visited =>
52   (
53     (* A pool of all nodes. *)
54     nodes: pool unvisited,
55     (* A list of the root nodes. *)
56     roots: list dynamic,
57     (* A flag that indicates whether we should abort when a cycle is
58        detected. *)
59     detect: bool,
60     (* A function that changes the state of a node from [unvisited]
61        to [visiting] and returns its successors. *)
62     pre: (consumes node: unvisited | p) -> (list dynamic | node @ visiting),
63     (* A function that changes the state of a node from [visiting]
64        to [visited]. *)
65     post: (consumes node: visiting | p) -> (| node @ visited)
66     (* The permission [p] required by [pre] and [post]. *)
67     | p
68   )
69 ->(
70   (* A new pool of the visited nodes. *)
71   pool visited,
72   (* An option that indicates: 1. whether a cycle was detected and 2. if so,
73      the list of nodes that were in the state [visiting] when the cycle was
74      detected. These nodes form a path in the graph that ends in a cycle. *)
75   option (list visiting)
76 )