src/Pure/General/graph.scala
changeset 59212 ecf64bc69778
parent 56372 fadb0fef09d7
child 59245 be4180f3c236
equal deleted inserted replaced
59211:7b74e8408711 59212:ecf64bc69778
    19   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
    19   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
    20 
    20 
    21   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    21   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    22     new Graph[Key, A](SortedMap.empty(ord))
    22     new Graph[Key, A](SortedMap.empty(ord))
    23 
    23 
    24   def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
    24   def make[Key, A](entries: List[((Key, A), List[Key])], converse: Boolean = false)(
    25     : Graph[Key, A] =
    25     implicit ord: Ordering[Key]): Graph[Key, A] =
    26   {
    26   {
    27     val graph1 =
    27     val graph1 =
    28       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    28       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    29     val graph2 =
    29     val graph2 =
    30       (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
    30       (graph1 /: entries) { case (graph, ((x, _), ys)) =>
       
    31         if (converse) (graph /: ys)(_.add_edge(_, x)) else (graph /: ys)(_.add_edge(x, _))
       
    32       }
    31     graph2
    33     graph2
    32   }
    34   }
    33 
    35 
    34   def string[A]: Graph[String, A] = empty(Ordering.String)
    36   def string[A]: Graph[String, A] = empty(Ordering.String)
    35   def int[A]: Graph[Int, A] = empty(Ordering.Int)
    37   def int[A]: Graph[Int, A] = empty(Ordering.Int)
    42     ((graph: Graph[Key, A]) => {
    44     ((graph: Graph[Key, A]) => {
    43       import XML.Encode._
    45       import XML.Encode._
    44       list(pair(pair(key, info), list(key)))(graph.dest)
    46       list(pair(pair(key, info), list(key)))(graph.dest)
    45     })
    47     })
    46 
    48 
    47   def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
    49   def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A], converse: Boolean = false)(
    48       : XML.Decode.T[Graph[Key, A]] =
    50     implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
    49     ((body: XML.Body) => {
    51     ((body: XML.Body) => {
    50       import XML.Decode._
    52       import XML.Decode._
    51       make(list(pair(pair(key, info), list(key)))(body))(ord)
    53       make(list(pair(pair(key, info), list(key)))(body), converse)(ord)
    52     })
    54     })
    53 }
    55 }
    54 
    56 
    55 
    57 
    56 final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
    58 final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])