# HG changeset patch
# User wenzelm
# Date 1330180416 -3600
# Node ID f4ce220d2799bffe92564c7d38e01a072a175372
# Parent  bc03b533b061b6e72a9cd3aed7cc17953cf3f625# Parent  9034b44844bd6edc2aefcccf754dc9660b6c0503
merged

diff -r bc03b533b061 -r f4ce220d2799 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 15:33:36 2012 +0100
@@ -143,8 +143,6 @@
                  [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
   | is_problem_line_tautology _ _ _ = false
 
-structure String_Graph = Graph(type key = string val ord = string_ord);
-
 fun order_facts ord = sort (ord o pairself ident_of_problem_line)
 fun order_problem_facts _ [] = []
   | order_problem_facts ord ((heading, lines) :: problem) =
diff -r bc03b533b061 -r f4ce220d2799 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 25 15:33:36 2012 +0100
@@ -43,7 +43,6 @@
   val is_maximal: 'a T -> key -> bool
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
-  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
@@ -175,7 +174,7 @@
 fun is_maximal G x = Keys.is_empty (imm_succs G x);
 
 
-(* nodes *)
+(* node operations *)
 
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
@@ -183,12 +182,6 @@
 fun default_node (x, info) (Graph tab) =
   Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
 
-fun del_nodes xs (Graph tab) =
-  Graph (tab
-    |> fold Table.delete xs
-    |> Table.map (fn _ => fn (i, (preds, succs)) =>
-      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
-
 fun del_node x (G as Graph tab) =
   let
     fun del_adjacent which y =
@@ -205,7 +198,7 @@
   fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
 
 
-(* edges *)
+(* edge operations *)
 
 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
 
@@ -326,4 +319,5 @@
 end;
 
 structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure String_Graph = Graph(type key = string val ord = string_ord);
 structure Int_Graph = Graph(type key = int val ord = int_ord);
diff -r bc03b533b061 -r f4ce220d2799 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/Pure/General/graph.scala	Sat Feb 25 15:33:36 2012 +0100
@@ -20,11 +20,14 @@
 
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
+
+  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)
 }
 
 
 class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
-  extends Iterable[(Key, (A, (SortedSet[Key], SortedSet[Key])))]
 {
   type Keys = SortedSet[Key]
   type Entry = (A, (Keys, Keys))
@@ -32,17 +35,20 @@
   def ordering: Ordering[Key] = rep.ordering
   def empty_keys: Keys = SortedSet.empty[Key](ordering)
 
-  override def iterator: Iterator[(Key, Entry)] = rep.iterator
+
+  /* graphs */
 
   def is_empty: Boolean = rep.isEmpty
 
-  def keys: List[Key] = rep.keySet.toList
+  def entries: Iterator[(Key, Entry)] = rep.iterator
+  def keys: Iterator[Key] = entries.map(_._1)
 
   def dest: List[(Key, List[Key])] =
-    (for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList
+    (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
 
-
-  /* entries */
+  override def toString: String =
+    dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
+      .mkString("Graph(", ", ", ")")
 
   private def get_entry(x: Key): Entry =
     rep.get(x) match {
@@ -96,7 +102,7 @@
   /*strongly connected components; see: David King and John Launchbury,
     "Structuring Depth First Search Algorithms in Haskell"*/
   def strong_conn: List[List[Key]] =
-    reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
+    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
 
 
   /* minimal and maximal elements */
@@ -113,7 +119,7 @@
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
 
 
-  /* nodes */
+  /* node operations */
 
   def new_node(x: Key, info: A): Graph[Key, A] =
   {
@@ -143,10 +149,10 @@
   }
 
   def restrict(pred: Key => Boolean): Graph[Key, A] =
-    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+    (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
 
 
-  /* edges */
+  /* edge operations */
 
   def is_edge(x: Key, y: Key): Boolean =
     try { imm_succs(x)(y) }
diff -r bc03b533b061 -r f4ce220d2799 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Feb 25 15:33:36 2012 +0100
@@ -146,7 +146,7 @@
       val succs = thy_graph Graph.all_succs [name];
       val _ = Output.urgent_message (loader_msg "removing" succs);
       val _ = List.app (perform Remove) succs;
-      val _ = change_thys (Graph.del_nodes succs);
+      val _ = change_thys (fold Graph.del_node succs);
     in () end);
 
 fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
diff -r bc03b533b061 -r f4ce220d2799 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Feb 25 15:33:36 2012 +0100
@@ -938,7 +938,7 @@
         val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
           Graph.get_node program1 Term.dummy_patternN;
         val deps = Graph.immediate_succs program1 Term.dummy_patternN;
-        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
+        val program2 = Graph.del_node Term.dummy_patternN program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.restrict (member (op =) deps_all) program2;
       in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
diff -r bc03b533b061 -r f4ce220d2799 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sat Feb 25 09:07:53 2012 +0100
+++ b/src/Tools/subtyping.ML	Sat Feb 25 15:33:36 2012 +0100
@@ -522,7 +522,7 @@
         val T = Type_Infer.deref tye (hd nodes);
         val P = new_imm_preds G nodes;
         val S = new_imm_succs G nodes;
-        val G' = Typ_Graph.del_nodes (tl nodes) G;
+        val G' = fold Typ_Graph.del_node (tl nodes) G;
         fun check_and_gen super T' =
           let val U = Type_Infer.deref tye T';
           in