renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
authorwenzelm
Fri Dec 29 17:24:46 2006 +0100 (2006-12-29)
changeset 219354e20a5397b57
parent 21934 ba683b0b2456
child 21936 c7a7d3ab81d0
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
src/Pure/General/graph.ML
     1.1 --- a/src/Pure/General/graph.ML	Fri Dec 29 17:24:45 2006 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Fri Dec 29 17:24:46 2006 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
     1.5    val minimals: 'a T -> key list
     1.6    val maximals: 'a T -> key list
     1.7 +  val subgraph: (key -> bool) -> 'a T -> 'a T
     1.8    val map_nodes: ('a -> 'b) -> 'a T -> 'b T
     1.9    val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b
    1.10    val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    1.11 @@ -29,7 +30,6 @@
    1.12    val all_preds: 'a T -> key list -> key list
    1.13    val all_succs: 'a T -> key list -> key list
    1.14    val strong_conn: 'a T -> key list list
    1.15 -  val project: (key -> bool) -> 'a T -> 'a T
    1.16    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    1.17    val default_node: key * 'a -> 'a T -> 'a T
    1.18    val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    1.19 @@ -91,6 +91,12 @@
    1.20  fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
    1.21  fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
    1.22  
    1.23 +fun subgraph P G =
    1.24 +  let
    1.25 +    fun subg (k, (i, (preds, succs))) =
    1.26 +      if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
    1.27 +  in Graph (fold_graph subg G Table.empty) end;
    1.28 +
    1.29  fun get_entry (Graph tab) x =
    1.30    (case Table.lookup tab x of
    1.31      SOME entry => entry
    1.32 @@ -141,13 +147,6 @@
    1.33  fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
    1.34    (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
    1.35  
    1.36 -(*subgraph induced by node subset*)
    1.37 -fun project proj G =
    1.38 -  let
    1.39 -    fun subg (k, (i, (preds, succs))) =
    1.40 -      proj k ? Table.update (k, (i, (filter proj preds, filter proj succs)));
    1.41 -  in Graph (fold_graph subg G Table.empty) end;
    1.42 -
    1.43  
    1.44  (* nodes *)
    1.45