# HG changeset patch
# User huffman
# Date 1330014457 -3600
# Node ID 08cb66dc7d2cb81f08b4a84ac6f7e81eb23eba71
# Parent  a8c342aa53d6e72beaf53ccb85651f309bde5516# Parent  cd0e6841ab9cf8f153af453f965ad7da696688a4
merged

diff -r a8c342aa53d6 -r 08cb66dc7d2c src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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"
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Pure/General/graph.ML
--- 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 *)
 
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Pure/General/graph.scala
--- /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)
+}
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Pure/build-jars
--- 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
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Pure/sorts.ML
--- 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;
 
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Tools/Code/code_target.ML
--- 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
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Tools/Code/code_thingol.ML
--- 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;
 
diff -r a8c342aa53d6 -r 08cb66dc7d2c src/Tools/subtyping.ML
--- 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, []);