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