Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: root.tex Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/General/graph.ML
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen

Directed graphs.
*)

signature GRAPH =
sig
  type key
  structure Keys:
  sig
    type T
    val is_empty: T -> bool
    val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
    val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
    val dest: T -> key list
  end
  type 'a T
  exception DUP of key
  exception SAME
  exception UNDEF of key
  val empty: 'a T
  val is_empty: 'a T -> bool
  val keys: 'a T -> key 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 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
  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 map_strong_conn: ((key * 'a) list -> 'b list) -> 'a T -> 'b T
  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 is_isolated: 'a T -> key -> bool
  val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*)
  val default_node: key * 'a -> 'a T -> 'a T
  val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
  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 dest: 'a T -> ((key * 'a) * key list) list
  val make: ((key * 'a) * key list) list -> 'a T                      (*exception DUP | UNDEF*)
  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*)
  val irreducible_paths: 'a T -> key * key -> key list list
  exception CYCLES of key list list
  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
  val topological_order: 'a T -> key list
  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
  exception DEP of key * key
  val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*)
  val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
  val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
end;

functor Graph(Key: KEY): GRAPH =
struct

(* keys *)

type key = Key.key;
val eq_key = is_equal o Key.ord;

structure Table = Table(Key);

structure Keys =
struct

abstype T = Keys of unit Table.table
with

val empty = Keys Table.empty;
fun is_empty (Keys tab) = Table.is_empty tab;

fun member (Keys tab) = Table.defined tab;
fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
fun remove x (Keys tab) = Keys (Table.delete_safe x tab);

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 dest keys = fold_rev cons keys [];

fun filter P keys = fold (fn x => P x ? insert x) keys empty;

end;
end;

(* graphs *)

datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;

exception DUP = Table.DUP;
exception UNDEF = Table.UNDEF;
exception SAME = Table.SAME;

val empty = Graph Table.empty;
fun is_empty (Graph tab) = Table.is_empty tab;
fun keys (Graph tab) = Table.keys tab;

fun get_first f (Graph tab) = Table.get_first f tab;
fun fold_graph f (Graph tab) = Table.fold f tab;

fun get_entry (Graph tab) x =
  (case Table.lookup_key tab x of
    SOME entry => entry
  | NONE => raise UNDEF x);

fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);

(* nodes *)

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));

fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);

(* reachability *)

(*nodes reachable from xs -- topologically sorted for acyclic graphs*)
fun reachable next xs =
  let
    fun reach x (rs, R) =
      if Keys.member R x then (rs, R)
      else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
    fun reachs x (rss, R) =
      reach x ([], R) |>> (fn rs => rs :: rss);
  in fold reachs xs ([], Keys.empty) end;

(*immediate*)
fun imm_preds G = #1 o #2 o #2 o get_entry G;
fun imm_succs G = #2 o #2 o #2 o get_entry G;

fun immediate_preds G = Keys.dest o imm_preds G;
fun immediate_succs G = Keys.dest o imm_succs G;

(*transitive*)
fun all_preds G = flat o #1 o reachable (imm_preds G);
fun all_succs G = flat o #1 o reachable (imm_succs G);

(*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)))));

fun map_strong_conn f G =
  let
    val xss = strong_conn G;
    fun map' xs =
      fold2 (curry Table.update) xs (f (AList.make (get_node G) xs));
    val tab' = Table.empty
      |> fold map' xss;
  in map_nodes (fn x => fn _ => the (Table.lookup tab' x)) G end;

(* 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);

fun is_isolated G x = is_minimal G x andalso is_maximal G x;

(* node operations *)

fun new_node (x, info) (Graph tab) =
  Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);

fun default_node (x, info) (Graph tab) =
  Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);

fun del_node x (G as Graph tab) =
  let
    fun del_adjacent which y =
      Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
    val (preds, succs) = #2 (#2 (get_entry G x));
  in
    Graph (tab
      |> Table.delete x
      |> Keys.fold (del_adjacent apsnd) preds
      |> Keys.fold (del_adjacent apfst) succs)
  end;

fun restrict pred G =
  fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;

(* edge operations *)

fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;

fun add_edge (x, y) G =
  if is_edge G (x, y) then G
  else
    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));

fun del_edge (x, y) G =
  if is_edge G (x, y) then
    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
  else G;

fun diff_edges G1 G2 =
  fold_graph (fn (x, (_, (_, succs))) =>
    Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];

fun edges G = diff_edges G empty;

(* dest and make *)

fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];

fun make entries =
  empty
  |> fold (new_node o fst) entries
  |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;

(* join and merge *)

fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));

fun join f (G1 as Graph tab1, G2 as Graph tab2) =
  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
    if pointer_eq (G1, G2) then G1
    else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
  end;

fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
    if pointer_eq (G1, G2) then G1
    else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
  end;

fun merge eq GG = gen_merge add_edge eq GG;

(* irreducible paths -- Hasse diagram *)

fun irreducible_preds G X path z =
  let
    fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
    fun irreds [] xs' = xs'
      | irreds (x :: xs) xs' =
          if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
            exists (red x) xs orelse exists (red x) xs'
          then irreds xs xs'
          else irreds xs (x :: xs');
  in irreds (immediate_preds G z) [] end;

fun irreducible_paths G (x, y) =
  let
    val (_, X) = reachable (imm_succs G) [x];
    fun paths path z =
      if eq_key (x, z) then cons (z :: path)
      else fold (paths (z :: path)) (irreducible_preds G X path z);
  in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;

(* maintain acyclic graphs *)

exception CYCLES of key list list;

fun add_edge_acyclic (x, y) G =
  if is_edge G (x, y) then G
  else
    (case irreducible_paths G (y, x) of
      [] => add_edge (x, y) G
    | cycles => raise CYCLES (map (cons x) cycles));

fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;

fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;

fun topological_order G = minimals G |> all_succs G;

(* maintain transitive acyclic graphs *)

fun add_edge_trans_acyclic (x, y) G =
  add_edge_acyclic (x, y) G
  |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);

fun merge_trans_acyclic eq (G1, G2) =
  if pointer_eq (G1, G2) then G1
  else
    merge_acyclic eq (G1, G2)
    |> fold add_edge_trans_acyclic (diff_edges G1 G2)
    |> fold add_edge_trans_acyclic (diff_edges G2 G1);

(* schedule acyclic graph *)

exception DEP of key * key;

fun schedule f G =
  let
    val xs = topological_order G;
    val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
      let
        val a = get_node G x;
        val deps = immediate_preds G x |> map (fn y =>
          (case Table.lookup tab y of
            SOME b => (y, b)
          | NONE => raise DEP (x, y)));
      in Table.update (x, f deps (x, a)) tab end);
  in map (the o Table.lookup results) xs end;

(* XML data representation *)

fun encode key info G =
  dest G |>
    let open XML.Encode
    in list (pair (pair key info) (list key)) end;

fun decode key info body =
  body |>
    let open XML.Decode
    in list (pair (pair key info) (list key)) end |> make;

(*final declarations of this structure!*)
val map = map_nodes;
val fold = fold_graph;

end;

structure Graph = Graph(type key = string val ord = fast_string_ord);
structure String_Graph = Graph(type key = string val ord = string_ord);
structure Int_Graph = Graph(type key = int val ord = int_ord);

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.