clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
authorwenzelm
Thu Feb 23 15:49:40 2012 +0100 (2012-02-23)
changeset 46614165886a4fe64
parent 46613 74331911375d
child 46615 c29bf6741ace
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/General/graph.ML
src/Pure/General/graph.scala
src/Pure/sorts.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 23 15:15:59 2012 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 23 15:49:40 2012 +0100
     1.3 @@ -476,7 +476,7 @@
     1.4  fun generate (use_modes, ensure_groundness) ctxt const =
     1.5    let 
     1.6      fun strong_conn_of gr keys =
     1.7 -      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
     1.8 +      Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
     1.9      val gr = Core_Data.intros_graph_of ctxt
    1.10      val gr' = add_edges depending_preds_of const gr
    1.11      val scc = strong_conn_of gr' [const]
    1.12 @@ -487,7 +487,7 @@
    1.13        SOME mode =>
    1.14          let
    1.15            val moded_gr = mk_moded_clauses_graph ctxt scc gr
    1.16 -          val moded_gr' = Mode_Graph.subgraph
    1.17 +          val moded_gr' = Mode_Graph.restrict
    1.18              (member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr
    1.19            val scc = Mode_Graph.strong_conn moded_gr' 
    1.20          in
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 23 15:15:59 2012 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 23 15:49:40 2012 +0100
     2.3 @@ -132,7 +132,7 @@
     2.4      val _ = print_step options "Fetching definitions from theory..."
     2.5      val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
     2.6            (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
     2.7 -          |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
     2.8 +          |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
     2.9      val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
    2.10    in
    2.11      cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 23 15:15:59 2012 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 23 15:49:40 2012 +0100
     3.3 @@ -1439,7 +1439,7 @@
     3.4      val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
     3.5      val thy' = extend_intro_graph names thy |> Theory.checkpoint;
     3.6      fun strong_conn_of gr keys =
     3.7 -      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
     3.8 +      Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
     3.9      val scc = strong_conn_of (PredData.get thy') names
    3.10      val thy'' = fold preprocess_intros (flat scc) thy'
    3.11      val thy''' = fold_rev
     4.1 --- a/src/Pure/General/graph.ML	Thu Feb 23 15:15:59 2012 +0100
     4.2 +++ b/src/Pure/General/graph.ML	Thu Feb 23 15:49:40 2012 +0100
     4.3 @@ -25,7 +25,6 @@
     4.4    val dest: 'a T -> (key * key list) list
     4.5    val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
     4.6    val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
     4.7 -  val subgraph: (key -> bool) -> 'a T -> 'a T
     4.8    val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
     4.9    val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    4.10    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    4.11 @@ -49,6 +48,7 @@
    4.12    val is_edge: 'a T -> key * key -> bool
    4.13    val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    4.14    val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    4.15 +  val restrict: (key -> bool) -> 'a T -> 'a T
    4.16    val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    4.17    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    4.18      'a T * 'a T -> 'a T                                               (*exception DUP*)
    4.19 @@ -115,13 +115,6 @@
    4.20  fun get_first f (Graph tab) = Table.get_first f tab;
    4.21  fun fold_graph f (Graph tab) = Table.fold f tab;
    4.22  
    4.23 -fun subgraph P G =
    4.24 -  let
    4.25 -    fun subg (k, (i, (preds, succs))) =
    4.26 -      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
    4.27 -      else I;
    4.28 -  in Graph (fold_graph subg G Table.empty) end;
    4.29 -
    4.30  fun get_entry (Graph tab) x =
    4.31    (case Table.lookup_key tab x of
    4.32      SOME entry => entry
    4.33 @@ -209,6 +202,9 @@
    4.34        |> Keys.fold (del_adjacent apfst) succs)
    4.35    end;
    4.36  
    4.37 +fun restrict pred G =
    4.38 +  fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
    4.39 +
    4.40  
    4.41  (* edges *)
    4.42  
     5.1 --- a/src/Pure/General/graph.scala	Thu Feb 23 15:15:59 2012 +0100
     5.2 +++ b/src/Pure/General/graph.scala	Thu Feb 23 15:49:40 2012 +0100
     5.3 @@ -146,6 +146,9 @@
     5.4        (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
     5.5    }
     5.6  
     5.7 +  def restrict(pred: Key => Boolean): Graph[Key, A] =
     5.8 +    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
     5.9 +
    5.10  
    5.11    /* edges */
    5.12  
     6.1 --- a/src/Pure/sorts.ML	Thu Feb 23 15:15:59 2012 +0100
     6.2 +++ b/src/Pure/sorts.ML	Thu Feb 23 15:49:40 2012 +0100
     6.3 @@ -308,7 +308,7 @@
     6.4              SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
     6.5          | NONE => NONE)
     6.6        else NONE;
     6.7 -    val classes' = classes |> Graph.subgraph P;
     6.8 +    val classes' = classes |> Graph.restrict P;
     6.9      val arities' = arities |> Symtab.map (map_filter o restrict_arity);
    6.10    in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
    6.11  
     7.1 --- a/src/Tools/Code/code_target.ML	Thu Feb 23 15:15:59 2012 +0100
     7.2 +++ b/src/Tools/Code/code_target.ML	Thu Feb 23 15:49:40 2012 +0100
     7.3 @@ -311,7 +311,7 @@
     7.4    let
     7.5      val ctxt = Proof_Context.init_global thy;
     7.6      val names2 = subtract (op =) names_hidden names1;
     7.7 -    val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
     7.8 +    val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
     7.9      val names4 = Graph.all_succs program3 names2;
    7.10      val empty_funs = filter_out (member (op =) abortable)
    7.11        (Code_Thingol.empty_funs program3);
    7.12 @@ -319,7 +319,7 @@
    7.13        if null empty_funs then ()
    7.14        else error ("No code equations for " ^
    7.15          commas (map (Proof_Context.extern_const ctxt) empty_funs));
    7.16 -    val program4 = Graph.subgraph (member (op =) names4) program3;
    7.17 +    val program4 = Graph.restrict (member (op =) names4) program3;
    7.18    in (names4, program4) end;
    7.19  
    7.20  fun prepare_serializer thy abortable serializer literals reserved all_includes
     8.1 --- a/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:15:59 2012 +0100
     8.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Feb 23 15:49:40 2012 +0100
     8.3 @@ -908,7 +908,7 @@
     8.4    let
     8.5      fun project_consts consts (naming, program) =
     8.6        if permissive then (consts, (naming, program))
     8.7 -      else (consts, (naming, Graph.subgraph
     8.8 +      else (consts, (naming, Graph.restrict
     8.9          (member (op =) (Graph.all_succs program consts)) program));
    8.10      fun generate_consts thy algebra eqngr =
    8.11        fold_map (ensure_const thy algebra eqngr permissive);
    8.12 @@ -940,7 +940,7 @@
    8.13          val deps = Graph.immediate_succs program1 Term.dummy_patternN;
    8.14          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
    8.15          val deps_all = Graph.all_succs program2 deps;
    8.16 -        val program3 = Graph.subgraph (member (op =) deps_all) program2;
    8.17 +        val program3 = Graph.restrict (member (op =) deps_all) program2;
    8.18        in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
    8.19    in
    8.20      ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
    8.21 @@ -1015,7 +1015,7 @@
    8.22    let
    8.23      val (_, eqngr) = Code_Preproc.obtain true thy consts [];
    8.24      val all_consts = Graph.all_succs eqngr consts;
    8.25 -  in Graph.subgraph (member (op =) all_consts) eqngr end;
    8.26 +  in Graph.restrict (member (op =) all_consts) eqngr end;
    8.27  
    8.28  fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
    8.29  
     9.1 --- a/src/Tools/subtyping.ML	Thu Feb 23 15:15:59 2012 +0100
     9.2 +++ b/src/Tools/subtyping.ML	Thu Feb 23 15:49:40 2012 +0100
     9.3 @@ -88,8 +88,7 @@
     9.4  
     9.5  (** utils **)
     9.6  
     9.7 -fun restrict_graph G =
     9.8 -  Graph.subgraph (fn key => if Graph.get_node G key = 0 then true else false) G;
     9.9 +fun restrict_graph G = Graph.restrict (fn x => Graph.get_node G x = 0) G;
    9.10  
    9.11  fun nameT (Type (s, [])) = s;
    9.12  fun t_of s = Type (s, []);