# HG changeset patch
# User wenzelm
# Date 1348576361 -7200
# Node ID 11430dd89e358adc8c6bf6099a0ce3382bb4af33
# Parent  c3a6e110679b15bb41abdb84eae1ae9c71c3d650
added graph encode/decode operations;
tuned signature;

diff -r c3a6e110679b -r 11430dd89e35 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Pure/General/graph.ML	Tue Sep 25 14:32:41 2012 +0200
@@ -22,7 +22,6 @@
   val empty: 'a T
   val is_empty: 'a T -> bool
   val keys: 'a T -> key list
-  val dest: 'a T -> (key * key list) list
   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
@@ -48,6 +47,8 @@
   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val restrict: (key -> bool) -> 'a T -> 'a T
+  val dest: 'a T -> ((key * 'a) * key list) list
+  val make: ((key * 'a) * key list) list -> 'a T                      (*exception DUP | UNDEF*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUP*)
@@ -61,6 +62,8 @@
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
   exception DEP of key * key
   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
+  val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
+  val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
 end;
 
 functor Graph(Key: KEY): GRAPH =
@@ -108,7 +111,6 @@
 val empty = Graph Table.empty;
 fun is_empty (Graph tab) = Table.is_empty tab;
 fun keys (Graph tab) = Table.keys tab;
-fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
 
 fun get_first f (Graph tab) = Table.get_first f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
@@ -215,12 +217,22 @@
   else G;
 
 fun diff_edges G1 G2 =
-  flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
-    if is_edge G2 (x, y) then NONE else SOME (x, y))));
+  fold_graph (fn (x, (_, (_, succs))) =>
+    Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
 
 fun edges G = diff_edges G empty;
 
 
+(* dest and make *)
+
+fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
+
+fun make entries =
+  empty
+  |> fold (new_node o fst) entries
+  |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;
+
+
 (* join and merge *)
 
 fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
@@ -312,6 +324,19 @@
   in map (the o Table.lookup results) xs end;
 
 
+(* XML data representation *)
+
+fun encode key info G =
+  dest G |>
+    let open XML.Encode
+    in list (pair (pair key info) (list key)) end;
+
+fun decode key info body =
+  body |>
+    let open XML.Decode
+    in list (pair (pair key info) (list key)) end |> make;
+
+
 (*final declarations of this structure!*)
 val map = map_nodes;
 val fold = fold_graph;
diff -r c3a6e110679b -r 11430dd89e35 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Pure/General/graph.scala	Tue Sep 25 14:32:41 2012 +0200
@@ -21,9 +21,35 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
+  def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
+    : Graph[Key, A] =
+  {
+    val graph1 =
+      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
+    val graph2 =
+      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
+    graph2
+  }
+
   def string[A]: Graph[String, A] = empty(Ordering.String)
   def int[A]: Graph[Int, A] = empty(Ordering.Int)
   def long[A]: Graph[Long, A] = empty(Ordering.Long)
+
+
+  /* XML data representation */
+
+  def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
+    ((graph: Graph[Key, A]) => {
+      import XML.Encode._
+      list(pair(pair(key, info), list(key)))(graph.dest)
+    })
+
+  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
+      : XML.Decode.T[Graph[Key, A]] =
+    ((body: XML.Body) => {
+      import XML.Decode._
+      make(list(pair(pair(key, info), list(key)))(body))(ord)
+    })
 }
 
 
@@ -44,11 +70,12 @@
   def entries: Iterator[(Key, Entry)] = rep.iterator
   def keys: Iterator[Key] = entries.map(_._1)
 
-  def dest: List[(Key, List[Key])] =
-    (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
+  def dest: List[((Key, A), List[Key])] =
+    (for ((x, (i, (_, succs))) <- entries) yield ((x, i), succs.toList)).toList
 
   override def toString: String =
-    dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
+    dest.map({ case ((x, _), ys) =>
+        x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
       .mkString("Graph(", ", ", ")")
 
   private def get_entry(x: Key): Entry =
diff -r c3a6e110679b -r 11430dd89e35 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Pure/ROOT.ML	Tue Sep 25 14:32:41 2012 +0200
@@ -50,7 +50,6 @@
 use "General/same.ML";
 use "General/ord_list.ML";
 use "General/balanced_tree.ML";
-use "General/graph.ML";
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
@@ -66,6 +65,8 @@
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 
+use "General/graph.ML";
+
 
 (* concurrency within the ML runtime *)
 
diff -r c3a6e110679b -r 11430dd89e35 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Pure/display.ML	Tue Sep 25 14:32:41 2012 +0200
@@ -194,7 +194,8 @@
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
-    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
+    val clsses =
+      Name_Space.dest_table ctxt (class_space, Symtab.make (map (apfst fst) (Graph.dest classes)));
     val tdecls = Name_Space.dest_table ctxt types;
     val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
 
diff -r c3a6e110679b -r 11430dd89e35 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Tools/subtyping.ML	Tue Sep 25 14:32:41 2012 +0200
@@ -908,7 +908,7 @@
             Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^
             Syntax.string_of_typ ctxt (T1 --> T2));
         val new_edges =
-          flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y =>
+          flat (Graph.dest G'' |> map (fn ((x, _), ys) => ys |> map_filter (fn y =>
             if Graph.is_edge G' (x, y) then NONE else SOME (x, y))));
         val G_and_new = Graph.add_edge (a, b) G';