src/Pure/General/graph.ML
author berghofe
Fri, 22 Sep 2006 14:30:37 +0200
changeset 20679 c09af1bd255a
parent 19950 fd74bf4e603e
child 20736 934358468a1b
permissions -rw-r--r--
Added function all_paths (formerly find_paths).
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$
15759
wenzelm
parents: 15570
diff changeset
     3
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6134
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
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    12
  exception DUP of key
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    13
  exception DUPS of key list
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    14
  exception SAME
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    15
  exception UNDEF of key
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    16
  val empty: 'a T
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    17
  val keys: 'a T -> key list
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    18
  val dest: 'a T -> (key * key list) list
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    19
  val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    20
  val minimals: 'a T -> key list
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    21
  val maximals: 'a T -> key list
6142
wenzelm
parents: 6134
diff changeset
    22
  val map_nodes: ('a -> 'b) -> 'a T -> 'b T
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    23
  val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b
15759
wenzelm
parents: 15570
diff changeset
    24
  val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
6142
wenzelm
parents: 6134
diff changeset
    25
  val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
    26
  val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
6142
wenzelm
parents: 6134
diff changeset
    27
  val imm_preds: 'a T -> key -> key list
wenzelm
parents: 6134
diff changeset
    28
  val imm_succs: 'a T -> key -> key list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    29
  val all_preds: 'a T -> key list -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    30
  val all_succs: 'a T -> key list -> key list
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
    31
  val strong_conn: 'a T -> key list list
19950
fd74bf4e603e replaced subgraph by project
haftmann
parents: 19615
diff changeset
    32
  val project: (key -> bool) -> 'a T -> 'a T
15759
wenzelm
parents: 15570
diff changeset
    33
  val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
17179
28802c8a9816 canonical interface for 'default'
haftmann
parents: 17140
diff changeset
    34
  val default_node: key * 'a -> 'a T -> 'a T
15759
wenzelm
parents: 15570
diff changeset
    35
  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    36
  val is_edge: 'a T -> key * key -> bool
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    37
  val add_edge: key * key -> 'a T -> 'a T
6152
wenzelm
parents: 6142
diff changeset
    38
  val del_edge: key * key -> 'a T -> 'a T
15759
wenzelm
parents: 15570
diff changeset
    39
  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    40
  val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    41
    'a T * 'a T -> 'a T                                               (*exception DUPS*)
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
    42
  val irreducible_paths: 'a T -> key * key -> key list list
20679
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
    43
  val all_paths: 'a T -> key * key -> key list list
6142
wenzelm
parents: 6134
diff changeset
    44
  exception CYCLES of key list list
15759
wenzelm
parents: 15570
diff changeset
    45
  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
wenzelm
parents: 15570
diff changeset
    46
  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
wenzelm
parents: 15570
diff changeset
    47
  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
wenzelm
parents: 15570
diff changeset
    48
  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
wenzelm
parents: 15570
diff changeset
    49
  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    50
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    51
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    52
functor GraphFun(Key: KEY): GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    53
struct
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    54
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    55
(* keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    56
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    57
type key = Key.key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    58
18970
d055a29ddd23 Library.is_equal;
wenzelm
parents: 18921
diff changeset
    59
val eq_key = is_equal o Key.ord;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    60
18921
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
    61
val member_key = member eq_key;
15759
wenzelm
parents: 15570
diff changeset
    62
val remove_key = remove eq_key;
6152
wenzelm
parents: 6142
diff changeset
    63
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    64
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    65
(* tables and sets of keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    66
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    67
structure Table = TableFun(Key);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    68
type keys = unit Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    69
6142
wenzelm
parents: 6134
diff changeset
    70
val empty_keys = Table.empty: keys;
wenzelm
parents: 6134
diff changeset
    71
18921
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
    72
fun member_keys tab = Table.defined (tab: keys);
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
    73
fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
6134
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
6142
wenzelm
parents: 6134
diff changeset
    76
(* graphs *)
6134
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
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    79
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    80
exception DUP = Table.DUP;
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    81
exception DUPS = Table.DUPS;
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    82
exception UNDEF = Table.UNDEF;
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    83
exception SAME = Table.SAME;
6134
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
val empty = Graph Table.empty;
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    86
fun keys (Graph tab) = Table.keys tab;
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    87
fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    88
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    89
fun fold_graph f (Graph tab) = Table.fold f tab;
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    90
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    91
fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
    92
fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    93
6142
wenzelm
parents: 6134
diff changeset
    94
fun get_entry (Graph tab) x =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    95
  (case Table.lookup tab x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
    96
    SOME entry => entry
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
    97
  | NONE => raise UNDEF x);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    98
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
    99
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
19290
wenzelm
parents: 19029
diff changeset
   100
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   101
fun map_entry_yield x f (G as Graph tab) =
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   102
  let val (a, node') = f (get_entry G x)
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   103
  in (a, Graph (Table.update (x, node') tab)) end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   104
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   105
6142
wenzelm
parents: 6134
diff changeset
   106
(* nodes *)
wenzelm
parents: 6134
diff changeset
   107
wenzelm
parents: 6134
diff changeset
   108
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   109
19290
wenzelm
parents: 19029
diff changeset
   110
fun fold_map_nodes f (Graph tab) =
wenzelm
parents: 19029
diff changeset
   111
  apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab;
17580
78a286d696c1 added fold_map_graph
haftmann
parents: 17412
diff changeset
   112
6142
wenzelm
parents: 6134
diff changeset
   113
fun get_node G = #1 o get_entry G;
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   114
6142
wenzelm
parents: 6134
diff changeset
   115
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
19290
wenzelm
parents: 19029
diff changeset
   116
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   117
fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   118
  let val (a, i') = f i in (a, (i', ps)) end);
6142
wenzelm
parents: 6134
diff changeset
   119
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   120
6142
wenzelm
parents: 6134
diff changeset
   121
(* reachability *)
wenzelm
parents: 6134
diff changeset
   122
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   123
(*nodes reachable from xs -- topologically sorted for acyclic graphs*)
6142
wenzelm
parents: 6134
diff changeset
   124
fun reachable next xs =
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   125
  let
18006
535de280c812 reachable - abandoned foldl_map in favor of fold_map
haftmann
parents: 17912
diff changeset
   126
    fun reach x (rs, R) =
18921
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
   127
      if member_keys R x then (rs, R)
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
   128
      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
18006
535de280c812 reachable - abandoned foldl_map in favor of fold_map
haftmann
parents: 17912
diff changeset
   129
  in fold_map (fn x => reach x o pair []) xs empty_keys end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   130
6142
wenzelm
parents: 6134
diff changeset
   131
(*immediate*)
wenzelm
parents: 6134
diff changeset
   132
fun imm_preds G = #1 o #2 o get_entry G;
wenzelm
parents: 6134
diff changeset
   133
fun imm_succs G = #2 o #2 o get_entry G;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   134
6142
wenzelm
parents: 6134
diff changeset
   135
(*transitive*)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19409
diff changeset
   136
fun all_preds G = flat o fst o reachable (imm_preds G);
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19409
diff changeset
   137
fun all_succs G = flat o fst o reachable (imm_succs G);
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   138
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   139
(*strongly connected components; see: David King and John Launchbury,
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   140
  "Structuring Depth First Search Algorithms in Haskell"*)
18006
535de280c812 reachable - abandoned foldl_map in favor of fold_map
haftmann
parents: 17912
diff changeset
   141
fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19409
diff changeset
   142
  (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   143
17912
410ec3b7e771 added subgraph
haftmann
parents: 17767
diff changeset
   144
(*subgraph induced by node subset*)
19950
fd74bf4e603e replaced subgraph by project
haftmann
parents: 19615
diff changeset
   145
fun project proj G =
17912
410ec3b7e771 added subgraph
haftmann
parents: 17767
diff changeset
   146
  let
19409
wenzelm
parents: 19290
diff changeset
   147
    fun subg (k, (i, (preds, succs))) =
19950
fd74bf4e603e replaced subgraph by project
haftmann
parents: 19615
diff changeset
   148
      K (proj k) ? Table.update (k, (i, (filter proj preds, filter proj succs)));
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   149
  in Graph (fold_graph subg G Table.empty) end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   150
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   151
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   152
(* nodes *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   153
6152
wenzelm
parents: 6142
diff changeset
   154
fun new_node (x, info) (Graph tab) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
   155
  Graph (Table.update_new (x, (info, ([], []))) tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   156
17179
28802c8a9816 canonical interface for 'default'
haftmann
parents: 17140
diff changeset
   157
fun default_node (x, info) (Graph tab) =
28802c8a9816 canonical interface for 'default'
haftmann
parents: 17140
diff changeset
   158
  Graph (Table.default (x, (info, ([], []))) tab);
17140
5be3a21ec949 added 'default' function
haftmann
parents: 16894
diff changeset
   159
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   160
fun del_nodes xs (Graph tab) =
15759
wenzelm
parents: 15570
diff changeset
   161
  Graph (tab
wenzelm
parents: 15570
diff changeset
   162
    |> fold Table.delete xs
wenzelm
parents: 15570
diff changeset
   163
    |> Table.map (fn (i, (preds, succs)) =>
wenzelm
parents: 15570
diff changeset
   164
      (i, (fold remove_key xs preds, fold remove_key xs succs))));
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   165
6152
wenzelm
parents: 6142
diff changeset
   166
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   167
(* edges *)
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   168
18921
f47c46d7d654 canonical member/insert/merge;
wenzelm
parents: 18133
diff changeset
   169
fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   170
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   171
fun add_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   172
  if is_edge G (x, y) then G
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   173
  else
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   174
    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   175
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   176
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   177
fun del_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   178
  if is_edge G (x, y) then
15759
wenzelm
parents: 15570
diff changeset
   179
    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
wenzelm
parents: 15570
diff changeset
   180
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   181
  else G;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   182
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   183
fun diff_edges G1 G2 =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19409
diff changeset
   184
  flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
   185
    if is_edge G2 (x, y) then NONE else SOME (x, y))));
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   186
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   187
fun edges G = diff_edges G empty;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   188
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   189
18126
b74145e46e0d added join function
haftmann
parents: 18006
diff changeset
   190
(* join and merge *)
b74145e46e0d added join function
haftmann
parents: 18006
diff changeset
   191
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   192
fun no_edges (i, _) = (i, ([], []));
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   193
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   194
fun join f (Graph tab1, G2 as Graph tab2) =
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
   195
  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   196
  in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
6152
wenzelm
parents: 6142
diff changeset
   197
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   198
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   199
  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   200
  in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
6152
wenzelm
parents: 6142
diff changeset
   201
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   202
fun merge eq GG = gen_merge add_edge eq GG;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   203
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   204
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   205
(* irreducible paths -- Hasse diagram *)
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   206
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   207
fun irreducible_preds G X path z =
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   208
  let
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   209
    fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   210
    fun irreds [] xs' = xs'
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   211
      | irreds (x :: xs) xs' =
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   212
          if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   213
            exists (red x) xs orelse exists (red x) xs'
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   214
          then irreds xs xs'
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   215
          else irreds xs (x :: xs');
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   216
  in irreds (imm_preds G z) [] end;
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   217
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   218
fun irreducible_paths G (x, y) =
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   219
  let
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   220
    val (_, X) = reachable (imm_succs G) [x];
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   221
    fun paths path z =
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   222
      if eq_key (x, z) then cons (z :: path)
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   223
      else fold (paths (z :: path)) (irreducible_preds G X path z);
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   224
  in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   225
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   226
20679
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   227
(* find ALL paths from x to y *)
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   228
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   229
fun all_paths G (x, y) =
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   230
  let
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   231
    val (_, X) = reachable (imm_succs G) [x];
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   232
    fun paths ps p =
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   233
      if not (null ps) andalso eq_key (p, x) then [p :: ps]
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   234
      else if member_keys X p andalso not (member_key ps p)
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   235
      then List.concat (map (paths (p :: ps)) (imm_preds G p))
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   236
      else [];
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   237
  in paths [] y end;
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   238
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   239
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   240
(* maintain acyclic graphs *)
6142
wenzelm
parents: 6134
diff changeset
   241
wenzelm
parents: 6134
diff changeset
   242
exception CYCLES of key list list;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   243
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   244
fun add_edge_acyclic (x, y) G =
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   245
  if is_edge G (x, y) then G
9347
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   246
  else
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   247
    (case irreducible_paths G (y, x) of
9347
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   248
      [] => add_edge (x, y) G
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   249
    | cycles => raise CYCLES (map (cons x) cycles));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   250
15759
wenzelm
parents: 15570
diff changeset
   251
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   252
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   253
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   254
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   255
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   256
(* maintain transitive acyclic graphs *)
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   257
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   258
fun add_edge_trans_acyclic (x, y) G =
19290
wenzelm
parents: 19029
diff changeset
   259
  add_edge_acyclic (x, y) G
wenzelm
parents: 19029
diff changeset
   260
  |> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   261
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   262
fun merge_trans_acyclic eq (G1, G2) =
19290
wenzelm
parents: 19029
diff changeset
   263
  merge_acyclic eq (G1, G2)
wenzelm
parents: 19029
diff changeset
   264
  |> fold add_edge_trans_acyclic (diff_edges G1 G2)
wenzelm
parents: 19029
diff changeset
   265
  |> fold add_edge_trans_acyclic (diff_edges G2 G1);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   266
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   267
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   268
(*final declarations of this structure!*)
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   269
val fold = fold_graph;
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   270
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   271
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   272
16810
2406588f99cb Graph: fast_string_ord;
wenzelm
parents: 16445
diff changeset
   273
structure Graph = GraphFun(type key = string val ord = fast_string_ord);
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   274
structure IntGraph = GraphFun(type key = int val ord = int_ord);