src/Pure/General/graph.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12451 0224f472be71
child 14161 73ad4884441f
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6134
     1
(*  Title:      Pure/General/graph.ML
wenzelm@6134
     2
    ID:         $Id$
wenzelm@6134
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6134
     5
wenzelm@6134
     6
Directed graphs.
wenzelm@6134
     7
*)
wenzelm@6134
     8
wenzelm@6134
     9
signature GRAPH =
wenzelm@6134
    10
sig
wenzelm@6134
    11
  type key
wenzelm@6134
    12
  type 'a T
wenzelm@9321
    13
  exception UNDEF of key
wenzelm@9321
    14
  exception DUP of key
wenzelm@9321
    15
  exception DUPS of key list
wenzelm@6134
    16
  val empty: 'a T
wenzelm@6659
    17
  val keys: 'a T -> key list
wenzelm@6142
    18
  val map_nodes: ('a -> 'b) -> 'a T -> 'b T
wenzelm@6142
    19
  val get_node: 'a T -> key -> 'a
wenzelm@6142
    20
  val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
wenzelm@6142
    21
  val imm_preds: 'a T -> key -> key list
wenzelm@6142
    22
  val imm_succs: 'a T -> key -> key list
wenzelm@6134
    23
  val all_preds: 'a T -> key list -> key list
wenzelm@6134
    24
  val all_succs: 'a T -> key list -> key list
wenzelm@6134
    25
  val find_paths: 'a T -> key * key -> key list list
wenzelm@6152
    26
  val new_node: key * 'a -> 'a T -> 'a T
wenzelm@6659
    27
  val del_nodes: key list -> 'a T -> 'a T
wenzelm@9321
    28
  val edges: 'a T -> (key * key) list
wenzelm@6134
    29
  val add_edge: key * key -> 'a T -> 'a T
wenzelm@6152
    30
  val del_edge: key * key -> 'a T -> 'a T
wenzelm@6142
    31
  exception CYCLES of key list list
wenzelm@6134
    32
  val add_edge_acyclic: key * key -> 'a T -> 'a T
wenzelm@9321
    33
  val add_deps_acyclic: key * key list -> 'a T -> 'a T
wenzelm@9321
    34
  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
wenzelm@6134
    35
end;
wenzelm@6134
    36
wenzelm@6134
    37
functor GraphFun(Key: KEY): GRAPH =
wenzelm@6134
    38
struct
wenzelm@6134
    39
wenzelm@6134
    40
wenzelm@6134
    41
(* keys *)
wenzelm@6134
    42
wenzelm@6134
    43
type key = Key.key;
wenzelm@6134
    44
wenzelm@6134
    45
val eq_key = equal EQUAL o Key.ord;
wenzelm@6134
    46
wenzelm@6134
    47
infix mem_key;
wenzelm@6134
    48
val op mem_key = gen_mem eq_key;
wenzelm@6134
    49
wenzelm@6134
    50
infix ins_key;
wenzelm@6134
    51
val op ins_key = gen_ins eq_key;
wenzelm@6134
    52
wenzelm@6152
    53
infix del_key;
wenzelm@6152
    54
fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
wenzelm@6152
    55
wenzelm@6659
    56
infix del_keys;
wenzelm@6659
    57
val op del_keys = foldl (op del_key);
wenzelm@6659
    58
wenzelm@6134
    59
wenzelm@6134
    60
(* tables and sets of keys *)
wenzelm@6134
    61
wenzelm@6134
    62
structure Table = TableFun(Key);
wenzelm@6134
    63
type keys = unit Table.table;
wenzelm@6134
    64
wenzelm@6142
    65
val empty_keys = Table.empty: keys;
wenzelm@6142
    66
wenzelm@6134
    67
infix mem_keys;
wenzelm@6134
    68
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
wenzelm@6134
    69
wenzelm@6134
    70
infix ins_keys;
wenzelm@6134
    71
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
wenzelm@6134
    72
wenzelm@6134
    73
wenzelm@6142
    74
(* graphs *)
wenzelm@6134
    75
wenzelm@6134
    76
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
wenzelm@6134
    77
wenzelm@9321
    78
exception UNDEF of key;
wenzelm@9321
    79
exception DUP = Table.DUP;
wenzelm@9321
    80
exception DUPS = Table.DUPS;
wenzelm@6134
    81
wenzelm@6134
    82
val empty = Graph Table.empty;
wenzelm@6659
    83
fun keys (Graph tab) = Table.keys tab;
wenzelm@6134
    84
wenzelm@6142
    85
fun get_entry (Graph tab) x =
wenzelm@6134
    86
  (case Table.lookup (tab, x) of
wenzelm@6142
    87
    Some entry => entry
wenzelm@9321
    88
  | None => raise UNDEF x);
wenzelm@6134
    89
wenzelm@6142
    90
fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab));
wenzelm@6134
    91
wenzelm@6134
    92
wenzelm@6142
    93
(* nodes *)
wenzelm@6142
    94
wenzelm@6142
    95
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
wenzelm@6134
    96
wenzelm@6142
    97
fun get_node G = #1 o get_entry G;
wenzelm@6142
    98
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
wenzelm@6142
    99
wenzelm@6142
   100
wenzelm@6142
   101
(* reachability *)
wenzelm@6142
   102
wenzelm@6659
   103
(*nodes reachable from xs -- topologically sorted for acyclic graphs*)
wenzelm@6142
   104
fun reachable next xs =
wenzelm@6134
   105
  let
wenzelm@6659
   106
    fun reach ((rs, R), x) =
wenzelm@6659
   107
      if x mem_keys R then (rs, R)
wenzelm@6659
   108
      else apfst (cons x) (reachs ((rs, x ins_keys R), next x))
wenzelm@6134
   109
    and reachs R_xs = foldl reach R_xs;
wenzelm@6659
   110
  in reachs (([], empty_keys), xs) end;
wenzelm@6134
   111
wenzelm@6142
   112
(*immediate*)
wenzelm@6142
   113
fun imm_preds G = #1 o #2 o get_entry G;
wenzelm@6142
   114
fun imm_succs G = #2 o #2 o get_entry G;
wenzelm@6134
   115
wenzelm@6142
   116
(*transitive*)
wenzelm@6659
   117
fun all_preds G = #1 o reachable (imm_preds G);
wenzelm@6659
   118
fun all_succs G = #1 o reachable (imm_succs G);
wenzelm@6134
   119
wenzelm@6134
   120
wenzelm@6142
   121
(* paths *)
wenzelm@6134
   122
wenzelm@6134
   123
fun find_paths G (x, y) =
wenzelm@6134
   124
  let
wenzelm@6659
   125
    val (_, X) = reachable (imm_succs G) [x];
wenzelm@6134
   126
    fun paths ps p =
berghofe@12451
   127
      if not (null ps) andalso eq_key (p, x) then [p :: ps]
berghofe@12451
   128
      else if p mem_keys X andalso not (p mem_key ps)
berghofe@12451
   129
      then flat (map (paths (p :: ps)) (imm_preds G p))
berghofe@12451
   130
      else [];
berghofe@12451
   131
  in paths [] y end;
wenzelm@6134
   132
wenzelm@6134
   133
wenzelm@9321
   134
(* nodes *)
wenzelm@6134
   135
wenzelm@6142
   136
exception DUPLICATE of key;
wenzelm@6142
   137
wenzelm@6152
   138
fun new_node (x, info) (Graph tab) =
wenzelm@9321
   139
  Graph (Table.update_new ((x, (info, ([], []))), tab));
wenzelm@6134
   140
wenzelm@6659
   141
fun del_nodes xs (Graph tab) =
wenzelm@6659
   142
  let
wenzelm@6659
   143
    fun del (x, (i, (preds, succs))) =
wenzelm@6659
   144
      if x mem_key xs then None
wenzelm@6659
   145
      else Some (x, (i, (preds del_keys xs, succs del_keys xs)));
wenzelm@6659
   146
  in Graph (Table.make (mapfilter del (Table.dest tab))) end;
wenzelm@6659
   147
wenzelm@6152
   148
wenzelm@9321
   149
(* edges *)
wenzelm@9321
   150
wenzelm@9321
   151
fun edges (Graph tab) =
wenzelm@9321
   152
  flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab));
wenzelm@9321
   153
wenzelm@6152
   154
fun add_edge (x, y) =
wenzelm@6152
   155
  map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o
wenzelm@6152
   156
   map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
wenzelm@6152
   157
wenzelm@6152
   158
fun del_edge (x, y) =
wenzelm@6152
   159
  map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o
wenzelm@6152
   160
   map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));
wenzelm@6152
   161
wenzelm@6142
   162
wenzelm@6142
   163
exception CYCLES of key list list;
wenzelm@6134
   164
wenzelm@6134
   165
fun add_edge_acyclic (x, y) G =
wenzelm@9347
   166
  if y mem_key imm_succs G x then G
wenzelm@9347
   167
  else
wenzelm@9347
   168
    (case find_paths G (y, x) of
wenzelm@9347
   169
      [] => add_edge (x, y) G
wenzelm@9347
   170
    | cycles => raise CYCLES (map (cons x) cycles));
wenzelm@6134
   171
wenzelm@9321
   172
fun add_deps_acyclic (y, xs) G =
wenzelm@9321
   173
  foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
wenzelm@9321
   174
wenzelm@9321
   175
wenzelm@9321
   176
(* merge_acyclic *)
wenzelm@9321
   177
wenzelm@9321
   178
fun merge_acyclic eq (Graph tab1, G2 as Graph tab2) =
wenzelm@9321
   179
  foldl (fn (G, xy) => add_edge_acyclic xy G)
wenzelm@9321
   180
    (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
wenzelm@9321
   181
wenzelm@6134
   182
wenzelm@6134
   183
end;
wenzelm@6134
   184
wenzelm@6134
   185
wenzelm@6134
   186
(*graphs indexed by strings*)
wenzelm@6134
   187
structure Graph = GraphFun(type key = string val ord = string_ord);