summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/General/graph.scala

changeset 48350 | 09bf3b73e446 |

parent 48348 | cbb25adad26f |

child 48507 | 1182677e4728 |

equal
deleted
inserted
replaced

48349:a78e5d399599 | 48350:09bf3b73e446 |
---|---|

71 /* reachability */ |
71 /* reachability */ |

72 |
72 |

73 /*nodes reachable from xs -- topologically sorted for acyclic graphs*/ |
73 /*nodes reachable from xs -- topologically sorted for acyclic graphs*/ |

74 def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = |
74 def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = |

75 { |
75 { |

76 def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) = |
76 def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) = |

77 { |
77 { |

78 val (rs, r_set) = reached |
78 val (rs, r_set) = reached |

79 if (r_set(x)) reached |
79 if (r_set(x)) reached |

80 else { |
80 else { |

81 val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach) |
81 val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach) |

82 (x :: rs1, r_set1) |
82 (x :: rs1, r_set1) |

83 } |
83 } |

84 } |
84 } |

85 def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = |
85 def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = |

86 { |
86 { |

87 val (rss, r_set) = reached |
87 val (rss, r_set) = reached |

88 val (rs, r_set1) = reach((Nil, r_set), x) |
88 val (rs, r_set1) = reach(x, (Nil, r_set)) |

89 (rs :: rss, r_set1) |
89 (rs :: rss, r_set1) |

90 } |
90 } |

91 ((List.empty[List[Key]], empty_keys) /: xs)(reachs) |
91 ((List.empty[List[Key]], empty_keys) /: xs)(reachs) |

92 } |
92 } |

93 |
93 |