--- 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;
--- 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 =
--- 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 *)
--- 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);
--- 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';