# HG changeset patch
# User wenzelm
# Date 1330008580 -3600
# Node ID 165886a4fe648cff0e097878bdc650a6a902a36e
# Parent  74331911375d5e84b53ef7f2fdbb1faebed82bb8
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;

diff -r 74331911375d -r 165886a4fe64 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Pure/General/graph.ML	Thu Feb 23 15:49:40 2012 +0100
@@ -25,7 +25,6 @@
   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 get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -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*)
@@ -115,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
@@ -209,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 74331911375d -r 165886a4fe64 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 15:49:40 2012 +0100
@@ -146,6 +146,9 @@
       (((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 */
 
diff -r 74331911375d -r 165886a4fe64 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Pure/sorts.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:49:40 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 74331911375d -r 165886a4fe64 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Tools/subtyping.ML	Thu Feb 23 15:49:40 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, []);