--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 23 17:27:37 2012 +0100
@@ -476,7 +476,7 @@
fun generate (use_modes, ensure_groundness) ctxt const =
let
fun strong_conn_of gr keys =
- Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
+ Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
val gr = Core_Data.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
@@ -487,7 +487,7 @@
SOME mode =>
let
val moded_gr = mk_moded_clauses_graph ctxt scc gr
- val moded_gr' = Mode_Graph.subgraph
+ val moded_gr' = Mode_Graph.restrict
(member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr
val scc = Mode_Graph.strong_conn moded_gr'
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 23 17:27:37 2012 +0100
@@ -132,7 +132,7 @@
val _ = print_step options "Fetching definitions from theory..."
val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
(fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
- |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
+ |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Feb 23 17:27:37 2012 +0100
@@ -1439,7 +1439,7 @@
val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
val thy' = extend_intro_graph names thy |> Theory.checkpoint;
fun strong_conn_of gr keys =
- Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
+ Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
val scc = strong_conn_of (PredData.get thy') names
val thy'' = fold preprocess_intros (flat scc) thy'
val thy''' = fold_rev
--- a/src/Pure/General/graph.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Pure/General/graph.ML Thu Feb 23 17:27:37 2012 +0100
@@ -25,23 +25,22 @@
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 subgraph: (key -> bool) -> 'a T -> 'a T
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*)
- val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
+ val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val imm_preds: 'a T -> key -> Keys.T
val imm_succs: 'a T -> key -> Keys.T
val immediate_preds: 'a T -> key -> key list
val immediate_succs: 'a T -> key -> key list
val all_preds: 'a T -> key list -> key list
val all_succs: 'a T -> key list -> key list
+ val strong_conn: 'a T -> key list list
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val is_minimal: 'a T -> key -> bool
val is_maximal: 'a T -> key -> bool
- val strong_conn: 'a T -> key list list
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*)
@@ -49,6 +48,7 @@
val is_edge: 'a T -> key * key -> bool
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 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*)
@@ -91,7 +91,6 @@
fun fold f (Keys tab) = Table.fold (f o #1) tab;
fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
-fun make xs = Basics.fold insert xs empty;
fun dest keys = fold_rev cons keys [];
fun filter P keys = fold (fn x => P x ? insert x) keys empty;
@@ -116,13 +115,6 @@
fun get_first f (Graph tab) = Table.get_first f tab;
fun fold_graph f (Graph tab) = Table.fold f tab;
-fun subgraph P G =
- let
- fun subg (k, (i, (preds, succs))) =
- if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
- else I;
- in Graph (fold_graph subg G Table.empty) end;
-
fun get_entry (Graph tab) x =
(case Table.lookup_key tab x of
SOME entry => entry
@@ -137,8 +129,6 @@
(* nodes *)
-fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
-
fun get_node G = #1 o #2 o get_entry G;
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
@@ -146,6 +136,8 @@
fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
let val (a, i') = f i in (a, (i', ps)) end);
+fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
+
(* reachability *)
@@ -170,17 +162,19 @@
fun all_preds G = flat o #1 o reachable (imm_preds G);
fun all_succs G = flat o #1 o reachable (imm_succs G);
-(*minimal and maximal elements*)
+(*strongly connected components; see: David King and John Launchbury,
+ "Structuring Depth First Search Algorithms in Haskell"*)
+fun strong_conn G =
+ rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
+
+
+(* minimal and maximal elements *)
+
fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
fun is_minimal G x = Keys.is_empty (imm_preds G x);
fun is_maximal G x = Keys.is_empty (imm_succs G x);
-(*strongly connected components; see: David King and John Launchbury,
- "Structuring Depth First Search Algorithms in Haskell"*)
-fun strong_conn G =
- rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
-
(* nodes *)
@@ -208,6 +202,9 @@
|> Keys.fold (del_adjacent apfst) succs)
end;
+fun restrict pred G =
+ fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
+
(* edges *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graph.scala Thu Feb 23 17:27:37 2012 +0100
@@ -0,0 +1,214 @@
+/* Title: Pure/General/graph.scala
+ Module: PIDE
+ Author: Makarius
+
+Directed graphs.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+
+object Graph
+{
+ class Duplicate[Key](x: Key) extends Exception
+ class Undefined[Key](x: Key) extends Exception
+ class Cycles[Key](cycles: List[List[Key]]) extends Exception
+
+ def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)
+}
+
+
+class Graph[Key, A] private(rep: Map[Key, (A, (Set[Key], Set[Key]))])
+ extends Iterable[(Key, (A, (Set[Key], Set[Key])))]
+{
+ type Keys = Set[Key]
+ type Entry = (A, (Keys, Keys))
+
+ def iterator: Iterator[(Key, Entry)] = rep.iterator
+
+ def is_empty: Boolean = rep.isEmpty
+
+ def keys: Set[Key] = rep.keySet.toSet
+
+ def dest: List[(Key, List[Key])] =
+ (for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList
+
+
+ /* entries */
+
+ private def get_entry(x: Key): Entry =
+ rep.get(x) match {
+ case Some(entry) => entry
+ case None => throw new Graph.Undefined(x)
+ }
+
+ private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
+ new Graph[Key, A](rep + (x -> f(get_entry(x))))
+
+
+ /* nodes */
+
+ def get_node(x: Key): A = get_entry(x)._1
+
+ def map_node(x: Key, f: A => A): Graph[Key, A] =
+ map_entry(x, { case (i, ps) => (f(i), ps) })
+
+ def map_nodes[B](f: A => B): Graph[Key, B] =
+ new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) })
+
+
+ /* reachability */
+
+ /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
+ def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
+ {
+ def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
+ {
+ val (rs, r_set) = reached
+ if (r_set(x)) reached
+ else {
+ val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
+ (x :: rs1, r_set1)
+ }
+ }
+ def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
+ {
+ val (rss, r_set) = reached
+ val (rs, r_set1) = reach((Nil, r_set), x)
+ (rs :: rss, r_set1)
+ }
+ ((List.empty[List[Key]], Set.empty[Key]) /: xs)(reachs)
+ }
+
+ /*immediate*/
+ def imm_preds(x: Key): Keys = get_entry(x)._2._1
+ def imm_succs(x: Key): Keys = get_entry(x)._2._2
+
+ /*transitive*/
+ def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
+ def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
+
+ /*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.toList))._1.filterNot(_.isEmpty).reverse
+
+
+ /* minimal and maximal elements */
+
+ def minimals: List[Key] =
+ (List.empty[Key] /: rep) {
+ case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
+
+ def maximals: List[Key] =
+ (List.empty[Key] /: rep) {
+ case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
+
+ def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
+ def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
+
+
+ /* nodes */
+
+ def new_node(x: Key, info: A): Graph[Key, A] =
+ {
+ if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)
+ else new Graph[Key, A](rep + (x -> (info, (Set.empty, Set.empty))))
+ }
+
+ def default_node(x: Key, info: A): Graph[Key, A] =
+ {
+ if (rep.isDefinedAt(x)) this
+ else new_node(x, info)
+ }
+
+ def del_nodes(xs: List[Key]): Graph[Key, A] =
+ {
+ xs.foreach(get_entry)
+ new Graph[Key, A](
+ (rep -- xs) mapValues { case (i, (preds, succs)) => (i, (preds -- xs, succs -- xs)) })
+ }
+
+ private def del_adjacent(fst: Boolean, x: Key)(map: Map[Key, Entry], y: Key): Map[Key, Entry] =
+ map.get(y) match {
+ case None => map
+ case Some((i, (preds, succs))) =>
+ map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
+ }
+
+ def del_node(x: Key): Graph[Key, A] =
+ {
+ val (preds, succs) = get_entry(x)._2
+ new Graph[Key, A](
+ (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
+ }
+
+ def restrict(pred: Key => Boolean): Graph[Key, A] =
+ (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+
+
+ /* edges */
+
+ def is_edge(x: Key, y: Key): Boolean =
+ try { imm_succs(x)(y) }
+ catch { case _: Graph.Undefined[_] => false }
+
+ def add_edge(x: Key, y: Key): Graph[Key, A] =
+ if (is_edge(x, y)) this
+ else
+ map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
+ map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
+
+ def del_edge(x: Key, y: Key): Graph[Key, A] =
+ if (is_edge(x, y))
+ map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
+ map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
+ else this
+
+
+ /* irreducible paths -- Hasse diagram */
+
+ def irreducible_preds(x_set: Set[Key], path: List[Key], z: Key): List[Key] =
+ {
+ def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
+ @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
+ xs0 match {
+ case Nil => xs1
+ case x :: xs =>
+ if (!(x_set(x)) || x == z || path.contains(x) ||
+ xs.exists(red(x)) || xs1.exists(red(x)))
+ irreds(xs, xs1)
+ else irreds(xs, x :: xs1)
+ }
+ irreds(imm_preds(z).toList, Nil)
+ }
+
+ def irreducible_paths(x: Key, y: Key): List[List[Key]] =
+ {
+ val (_, x_set) = reachable(imm_succs, List(x))
+ def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
+ if (x == z) (z :: path) :: ps
+ else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
+ if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
+ }
+
+
+ /* maintain acyclic graphs */
+
+ def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
+ if (is_edge(x, y)) this
+ else {
+ irreducible_paths(y, x) match {
+ case Nil => add_edge(x, y)
+ case cycles => throw new Graph.Cycles(cycles.map(x :: _))
+ }
+ }
+
+ def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] =
+ (this /: xs)(_.add_edge_acyclic(_, y))
+
+ def topological_order: List[Key] = all_succs(minimals)
+}
--- a/src/Pure/build-jars Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Pure/build-jars Thu Feb 23 17:27:37 2012 +0100
@@ -14,6 +14,7 @@
Concurrent/simple_thread.scala
Concurrent/volatile.scala
General/exn.scala
+ General/graph.scala
General/linear_set.scala
General/path.scala
General/position.scala
--- a/src/Pure/sorts.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Pure/sorts.ML Thu Feb 23 17:27:37 2012 +0100
@@ -308,7 +308,7 @@
SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
| NONE => NONE)
else NONE;
- val classes' = classes |> Graph.subgraph P;
+ val classes' = classes |> Graph.restrict P;
val arities' = arities |> Symtab.map (map_filter o restrict_arity);
in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
--- a/src/Tools/Code/code_target.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Tools/Code/code_target.ML Thu Feb 23 17:27:37 2012 +0100
@@ -311,7 +311,7 @@
let
val ctxt = Proof_Context.init_global thy;
val names2 = subtract (op =) names_hidden names1;
- val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
+ val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
val names4 = Graph.all_succs program3 names2;
val empty_funs = filter_out (member (op =) abortable)
(Code_Thingol.empty_funs program3);
@@ -319,7 +319,7 @@
if null empty_funs then ()
else error ("No code equations for " ^
commas (map (Proof_Context.extern_const ctxt) empty_funs));
- val program4 = Graph.subgraph (member (op =) names4) program3;
+ val program4 = Graph.restrict (member (op =) names4) program3;
in (names4, program4) end;
fun prepare_serializer thy abortable serializer literals reserved all_includes
--- a/src/Tools/Code/code_thingol.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML Thu Feb 23 17:27:37 2012 +0100
@@ -908,7 +908,7 @@
let
fun project_consts consts (naming, program) =
if permissive then (consts, (naming, program))
- else (consts, (naming, Graph.subgraph
+ else (consts, (naming, Graph.restrict
(member (op =) (Graph.all_succs program consts)) program));
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
@@ -940,7 +940,7 @@
val deps = Graph.immediate_succs program1 Term.dummy_patternN;
val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
val deps_all = Graph.all_succs program2 deps;
- val program3 = Graph.subgraph (member (op =) deps_all) program2;
+ val program3 = Graph.restrict (member (op =) deps_all) program2;
in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
in
ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
@@ -1015,7 +1015,7 @@
let
val (_, eqngr) = Code_Preproc.obtain true thy consts [];
val all_consts = Graph.all_succs eqngr consts;
- in Graph.subgraph (member (op =) all_consts) eqngr end;
+ in Graph.restrict (member (op =) all_consts) eqngr end;
fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
--- a/src/Tools/subtyping.ML Thu Feb 23 16:09:16 2012 +0100
+++ b/src/Tools/subtyping.ML Thu Feb 23 17:27:37 2012 +0100
@@ -88,8 +88,7 @@
(** utils **)
-fun restrict_graph G =
- Graph.subgraph (fn key => if Graph.get_node G key = 0 then true else false) G;
+fun restrict_graph G = Graph.restrict (fn x => Graph.get_node G x = 0) G;
fun nameT (Type (s, [])) = s;
fun t_of s = Type (s, []);