1structure ImplicitGraph :> ImplicitGraph =
2struct
3
4type 'a graph = 'a -> 'a list
5
6fun smem s e = HOLset.member(s,e)
7fun sadd e s = HOLset.add(s,e)
8
9fun dfs g cmp fold start A0 =
10    let
11      fun recurse seen to_visit A =
12          case to_visit of
13              [] => A
14            | (v,d)::vs =>
15              if smem seen v then recurse seen vs A
16              else recurse (sadd v seen)
17                           (map (fn v => (v,d+1)) (g v) @ vs)
18                           (fold d v A)
19    in
20      recurse (HOLset.empty cmp) [(start,0)] A0
21    end
22
23fun bfs g cmp fold start A0 =
24    let
25      fun recurse seen to_visit A =
26          case to_visit of
27              [] => A
28            | (v,d)::vs =>
29              if smem seen v then recurse seen vs A
30              else recurse (sadd v seen)
31                           (vs @ map (fn v => (v,d+1)) (g v))
32                           (fold d v A)
33    in
34      recurse (HOLset.empty cmp) [(start,0)] A0
35    end
36
37fun limdfs g cmp fold max_depth start A0 =
38    let
39      fun recurse seen to_visit A =
40          case to_visit of
41              [] => A
42            | (v,d) :: vs =>
43              if d > max_depth orelse smem seen v then recurse seen vs A
44              else recurse (sadd v seen)
45                           (map (fn v => (v,d+1)) (g v) @ vs)
46                           (fold d v A)
47    in
48      recurse (HOLset.empty cmp) [(start,0)] A0
49    end
50
51fun limbfs g cmp fold max_depth start A0 =
52    let
53      fun recurse seen to_visit A =
54          case to_visit of
55              [] => A
56            | (v,d) :: vs =>
57              if d > max_depth orelse smem seen v then recurse seen vs A
58              else recurse (sadd v seen)
59                           (vs @ map (fn v => (v,d+1)) (g v))
60                           (fold d v A)
61    in
62      recurse (HOLset.empty cmp) [(start,0)] A0
63    end
64
65end (* struct *)
66