clarified topological ordering: preserve order of adjacency via reverse fold;
authorwenzelm
Thu Jul 19 15:45:59 2012 +0200 (2012-07-19)
changeset 4835009bf3b73e446
parent 48349 a78e5d399599
child 48351 a0b95a762abb
clarified topological ordering: preserve order of adjacency via reverse fold;
src/Pure/General/graph.ML
src/Pure/General/graph.scala
src/Pure/System/build.scala
     1.1 --- a/src/Pure/General/graph.ML	Thu Jul 19 14:24:40 2012 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Thu Jul 19 15:45:59 2012 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    let
     1.5      fun reach x (rs, R) =
     1.6        if Keys.member R x then (rs, R)
     1.7 -      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
     1.8 +      else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
     1.9      fun reachs x (rss, R) =
    1.10        reach x ([], R) |>> (fn rs => rs :: rss);
    1.11    in fold reachs xs ([], Keys.empty) end;
     2.1 --- a/src/Pure/General/graph.scala	Thu Jul 19 14:24:40 2012 +0200
     2.2 +++ b/src/Pure/General/graph.scala	Thu Jul 19 15:45:59 2012 +0200
     2.3 @@ -73,19 +73,19 @@
     2.4    /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
     2.5    def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
     2.6    {
     2.7 -    def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
     2.8 +    def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
     2.9      {
    2.10        val (rs, r_set) = reached
    2.11        if (r_set(x)) reached
    2.12        else {
    2.13 -        val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
    2.14 +        val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
    2.15          (x :: rs1, r_set1)
    2.16        }
    2.17      }
    2.18      def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
    2.19      {
    2.20        val (rss, r_set) = reached
    2.21 -      val (rs, r_set1) = reach((Nil, r_set), x)
    2.22 +      val (rs, r_set1) = reach(x, (Nil, r_set))
    2.23        (rs :: rss, r_set1)
    2.24      }
    2.25      ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
     3.1 --- a/src/Pure/System/build.scala	Thu Jul 19 14:24:40 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 15:45:59 2012 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4        object Ordering extends scala.math.Ordering[Key]
     3.5        {
     3.6          def compare(key1: Key, key2: Key): Int =
     3.7 -          key2.order compare key1.order match {
     3.8 +          key1.order compare key2.order match {
     3.9              case 0 => key1.name compare key2.name
    3.10              case ord => ord
    3.11            }