--- 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) =
--- 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);
--- 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) }
--- 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 () =>
--- 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;
--- 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