src/Pure/General/graph.ML
author wenzelm
Mon, 18 Jan 1999 21:08:27 +0100
changeset 6134 ec6092b0599d
child 6142 c0c93b9434ef
permissions -rw-r--r--
added General/graph.ML: generic direct graphs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/graph.ML
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     4
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     5
Directed graphs.
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     6
*)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     7
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     8
signature GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     9
sig
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    10
  type key
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    11
  type 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    12
  exception UNDEFINED of key
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    13
  exception DUPLICATE of key
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    14
  exception CYCLES of key list list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    15
  val empty: 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    16
  val map : ('a -> 'b) -> 'a T -> 'b T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    17
  val foldl : ('a * (key * ('b * (key list * key list))) -> 'a) -> 'a * 'b T -> 'a
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    18
  val info: 'a T -> key -> 'a
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    19
  val map_info: ('a -> 'a) -> key -> 'a T -> 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    20
  val preds: 'a T -> key -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    21
  val succs: 'a T -> key -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    22
  val all_preds: 'a T -> key list -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    23
  val all_succs: 'a T -> key list -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    24
  val find_paths: 'a T -> key * key -> key list list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    25
  val add_node: key * 'a -> 'a T -> 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    26
  val add_edge: key * key -> 'a T -> 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    27
  val add_edge_acyclic: key * key -> 'a T -> 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    28
  val derive_node: key * 'a -> key list -> 'a T -> 'a T
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    29
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    30
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    31
functor GraphFun(Key: KEY): GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    32
struct
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    33
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    34
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    35
(* keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    36
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    37
type key = Key.key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    38
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    39
val eq_key = equal EQUAL o Key.ord;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    40
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    41
infix mem_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    42
val op mem_key = gen_mem eq_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    43
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    44
infix ins_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    45
val op ins_key = gen_ins eq_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    46
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    47
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    48
(* tables and sets of keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    49
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    50
structure Table = TableFun(Key);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    51
type keys = unit Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    52
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    53
infix mem_keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    54
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    55
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    56
infix ins_keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    57
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    58
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    59
val empty_keys = Table.empty: keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    60
fun make_keys xs = foldl (fn (tab, x) => x ins_keys tab) (empty_keys, xs);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    61
fun dest_keys tab = rev (Table.foldl (fn (xs, (x, ())) => x :: xs) ([], tab: keys));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    62
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    63
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    64
(* datatype of graphs *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    65
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    66
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    67
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    68
exception UNDEFINED of key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    69
exception DUPLICATE of key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    70
exception CYCLES of key list list;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    71
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    72
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    73
(* basic operations *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    74
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    75
fun map_graph f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    76
fun foldl_graph f (x, Graph tab) = Table.foldl f (x, tab);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    77
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    78
val empty = Graph Table.empty;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    79
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    80
fun get_node (Graph tab) x =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    81
  (case Table.lookup (tab, x) of
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    82
    Some node => node
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    83
  | None => raise UNDEFINED x);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    84
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    85
fun info G = #1 o get_node G;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    86
fun preds G = #1 o #2 o get_node G;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    87
fun succs G = #2 o #2 o get_node G;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    88
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    89
fun map_node f x (G as Graph tab) =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    90
  let val node = get_node G x
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    91
  in Graph (Table.update ((x, f node), tab)) end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    92
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    93
fun map_info f = map_node (fn (info, ps) => (f info, ps));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    94
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    95
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    96
(* reachable nodes *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    97
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    98
fun reachable_keys next xs =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    99
  let
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   100
    fun reach (R, x) =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   101
      if x mem_keys R then R
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   102
      else reachs (x ins_keys R, next x)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   103
    and reachs R_xs = foldl reach R_xs;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   104
  in reachs (empty_keys, xs) end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   105
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   106
val reachable = dest_keys oo reachable_keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   107
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   108
fun all_preds G = reachable (preds G);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   109
fun all_succs G = reachable (succs G);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   110
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   111
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   112
(* find_paths *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   113
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   114
fun find_paths G (x, y) =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   115
  let
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   116
    val X = reachable_keys (succs G) [x];
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   117
    fun paths ps p =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   118
      if eq_key (p, x) then [p :: ps]
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   119
      else flat (map (paths (p :: ps))
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   120
        (filter (fn pp => pp mem_keys X andalso not (pp mem_key ps)) (preds G p)));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   121
  in if y mem_keys X then (paths [] y) else [] end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   122
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   123
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   124
(* build graphs *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   125
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   126
fun add_node (x, info) (Graph tab) =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   127
  Graph (Table.update_new ((x, (info, ([], []))), tab)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   128
    handle Table.DUP key => raise DUPLICATE key);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   129
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   130
fun add_edge (x, y) G =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   131
  (get_node G x; get_node G y;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   132
    G |> map_node (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) x
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   133
      |> map_node (fn (i, (preds, succs)) => (i, (x ins_key preds, succs))) y);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   135
fun add_edge_acyclic (x, y) G =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   136
  (case find_paths G (y, x) of
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   137
    [] => add_edge (x, y) G
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   138
  | cycles => raise CYCLES (map (cons x) cycles));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   139
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   140
fun derive_node (x, y) zs G =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   141
  foldl (fn (H, z) => add_edge_acyclic (z, x) H) (add_node (x, y) G, zs);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   142
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   143
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   144
(*final declarations of this structure!*)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   145
val map = map_graph;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   146
val foldl = foldl_graph;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   147
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   148
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   149
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   150
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   151
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   152
(*graphs indexed by strings*)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   153
structure Graph = GraphFun(type key = string val ord = string_ord);