src/Pure/General/graph.ML
author wenzelm
Sun, 09 Oct 2011 16:47:58 +0200
changeset 45107 76fef3e57004
parent 44338 700008399ee5
child 46611 669601fa1a62
permissions -rw-r--r--
tuned;
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
15759
wenzelm
parents: 15570
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     3
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     4
Directed graphs.
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     5
*)
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
signature GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     8
sig
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     9
  type key
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    10
  structure Keys:
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    11
  sig
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    12
    type T
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    13
    val is_empty: T -> bool
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    14
    val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    15
    val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    16
    val dest: T -> key list
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    17
  end
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    18
  type 'a T
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    19
  exception DUP of key
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    20
  exception SAME
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    21
  exception UNDEF of key
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    22
  val empty: 'a T
28204
2d93b158ad99 added is_empty;
wenzelm
parents: 28183
diff changeset
    23
  val is_empty: 'a T -> bool
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    24
  val keys: 'a T -> key list
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    25
  val dest: 'a T -> (key * key list) list
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    26
  val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    27
  val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
21935
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
    28
  val subgraph: (key -> bool) -> 'a T -> 'a T
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    29
  val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
39021
139aada5caf8 Graph.map, in analogy to Table.map
haftmann
parents: 39020
diff changeset
    30
  val map: (key -> 'a -> 'b) -> 'a T -> 'b T
15759
wenzelm
parents: 15570
diff changeset
    31
  val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
6142
wenzelm
parents: 6134
diff changeset
    32
  val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
    33
  val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    34
  val imm_preds: 'a T -> key -> Keys.T
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    35
  val imm_succs: 'a T -> key -> Keys.T
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    36
  val immediate_preds: 'a T -> key -> key list
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    37
  val immediate_succs: 'a T -> key -> key list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    38
  val all_preds: 'a T -> key list -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    39
  val all_succs: 'a T -> key list -> key list
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    40
  val minimals: 'a T -> key list
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    41
  val maximals: 'a T -> key list
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    42
  val is_minimal: 'a T -> key -> bool
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    43
  val is_maximal: 'a T -> key -> bool
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
    44
  val strong_conn: 'a T -> key list list
15759
wenzelm
parents: 15570
diff changeset
    45
  val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
17179
28802c8a9816 canonical interface for 'default'
haftmann
parents: 17140
diff changeset
    46
  val default_node: key * 'a -> 'a T -> 'a T
15759
wenzelm
parents: 15570
diff changeset
    47
  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
28333
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
    48
  val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    49
  val is_edge: 'a T -> key * key -> bool
44202
44c4ae5c5ce2 touch descendants of edited nodes;
wenzelm
parents: 44162
diff changeset
    50
  val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
44c4ae5c5ce2 touch descendants of edited nodes;
wenzelm
parents: 44162
diff changeset
    51
  val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
23655
d2d1138e0ddc replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents: 21935
diff changeset
    52
  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
    53
  val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
23655
d2d1138e0ddc replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents: 21935
diff changeset
    54
    'a T * 'a T -> 'a T                                               (*exception DUP*)
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
    55
  val irreducible_paths: 'a T -> key * key -> key list list
20679
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
    56
  val all_paths: 'a T -> key * key -> key list list
6142
wenzelm
parents: 6134
diff changeset
    57
  exception CYCLES of key list list
44202
44c4ae5c5ce2 touch descendants of edited nodes;
wenzelm
parents: 44162
diff changeset
    58
  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
44c4ae5c5ce2 touch descendants of edited nodes;
wenzelm
parents: 44162
diff changeset
    59
  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
15759
wenzelm
parents: 15570
diff changeset
    60
  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
23964
d2df2797519b added topological_order;
wenzelm
parents: 23655
diff changeset
    61
  val topological_order: 'a T -> key list
44202
44c4ae5c5ce2 touch descendants of edited nodes;
wenzelm
parents: 44162
diff changeset
    62
  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
15759
wenzelm
parents: 15570
diff changeset
    63
  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
44162
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
    64
  exception DEP of key * key
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
    65
  val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    66
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    67
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31616
diff changeset
    68
functor Graph(Key: KEY): GRAPH =
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    69
struct
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    70
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    71
(* keys *)
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
type key = Key.key;
18970
d055a29ddd23 Library.is_equal;
wenzelm
parents: 18921
diff changeset
    74
val eq_key = is_equal o Key.ord;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    75
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    76
structure Table = Table(Key);
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    77
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    78
structure Keys =
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    79
struct
6152
wenzelm
parents: 6142
diff changeset
    80
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    81
abstype T = Keys of unit Table.table
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    82
with
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    83
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    84
val empty = Keys Table.empty;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    85
fun is_empty (Keys tab) = Table.is_empty tab;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    86
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    87
fun member (Keys tab) = Table.defined tab;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    88
fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    89
fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    90
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    91
fun fold f (Keys tab) = Table.fold (f o #1) tab;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    92
fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    93
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    94
fun make xs = Basics.fold insert xs empty;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    95
fun dest keys = fold_rev cons keys [];
6142
wenzelm
parents: 6134
diff changeset
    96
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    97
fun filter P keys = fold (fn x => P x ? insert x) keys empty;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    98
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
    99
end;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   100
end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   101
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   102
6142
wenzelm
parents: 6134
diff changeset
   103
(* graphs *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   104
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   105
datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   106
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   107
exception DUP = Table.DUP;
19029
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
   108
exception UNDEF = Table.UNDEF;
8635700e2c9c share exception UNDEF with Table;
wenzelm
parents: 18970
diff changeset
   109
exception SAME = Table.SAME;
6134
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
val empty = Graph Table.empty;
28204
2d93b158ad99 added is_empty;
wenzelm
parents: 28183
diff changeset
   112
fun is_empty (Graph tab) = Table.is_empty tab;
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   113
fun keys (Graph tab) = Table.keys tab;
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   114
fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   115
35012
c3e3ac3ca091 removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents: 32710
diff changeset
   116
fun get_first f (Graph tab) = Table.get_first f tab;
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   117
fun fold_graph f (Graph tab) = Table.fold f tab;
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   118
21935
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
   119
fun subgraph P G =
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
   120
  let
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
   121
    fun subg (k, (i, (preds, succs))) =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   122
      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   123
      else I;
21935
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
   124
  in Graph (fold_graph subg G Table.empty) end;
4e20a5397b57 renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents: 21565
diff changeset
   125
6142
wenzelm
parents: 6134
diff changeset
   126
fun get_entry (Graph tab) x =
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   127
  (case Table.lookup_key tab x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
   128
    SOME entry => entry
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
   129
  | NONE => raise UNDEF x);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   130
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   131
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
19290
wenzelm
parents: 19029
diff changeset
   132
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   133
fun map_entry_yield x f (G as Graph tab) =
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   134
  let val (a, node') = f (#2 (get_entry G x))
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   135
  in (a, Graph (Table.update (x, node') tab)) end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   136
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   137
6142
wenzelm
parents: 6134
diff changeset
   138
(* nodes *)
wenzelm
parents: 6134
diff changeset
   139
39021
139aada5caf8 Graph.map, in analogy to Table.map
haftmann
parents: 39020
diff changeset
   140
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   141
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   142
fun get_node G = #1 o #2 o get_entry G;
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   143
6142
wenzelm
parents: 6134
diff changeset
   144
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
19290
wenzelm
parents: 19029
diff changeset
   145
17767
504acb86c9f5 added fold_nodes, map_node_yield
haftmann
parents: 17580
diff changeset
   146
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
   147
  let val (a, i') = f i in (a, (i', ps)) end);
6142
wenzelm
parents: 6134
diff changeset
   148
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   149
6142
wenzelm
parents: 6134
diff changeset
   150
(* reachability *)
wenzelm
parents: 6134
diff changeset
   151
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   152
(*nodes reachable from xs -- topologically sorted for acyclic graphs*)
6142
wenzelm
parents: 6134
diff changeset
   153
fun reachable next xs =
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   154
  let
18006
535de280c812 reachable - abandoned foldl_map in favor of fold_map
haftmann
parents: 17912
diff changeset
   155
    fun reach x (rs, R) =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   156
      if Keys.member R x then (rs, R)
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   157
      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
32710
wenzelm
parents: 32709
diff changeset
   158
    fun reachs x (rss, R) =
wenzelm
parents: 32709
diff changeset
   159
      reach x ([], R) |>> (fn rs => rs :: rss);
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   160
  in fold reachs xs ([], Keys.empty) end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   161
6142
wenzelm
parents: 6134
diff changeset
   162
(*immediate*)
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   163
fun imm_preds G = #1 o #2 o #2 o get_entry G;
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   164
fun imm_succs G = #2 o #2 o #2 o get_entry G;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   165
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   166
fun immediate_preds G = Keys.dest o imm_preds G;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   167
fun immediate_succs G = Keys.dest o imm_succs G;
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   168
6142
wenzelm
parents: 6134
diff changeset
   169
(*transitive*)
32710
wenzelm
parents: 32709
diff changeset
   170
fun all_preds G = flat o #1 o reachable (imm_preds G);
wenzelm
parents: 32709
diff changeset
   171
fun all_succs G = flat o #1 o reachable (imm_succs G);
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   172
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   173
(*minimal and maximal elements*)
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   174
fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   175
fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   176
fun is_minimal G x = Keys.is_empty (imm_preds G x);
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   177
fun is_maximal G x = Keys.is_empty (imm_succs G x);
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   178
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   179
(*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
   180
  "Structuring Depth First Search Algorithms in Haskell"*)
32710
wenzelm
parents: 32709
diff changeset
   181
fun strong_conn G =
wenzelm
parents: 32709
diff changeset
   182
  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   183
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   184
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   185
(* nodes *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   186
6152
wenzelm
parents: 6142
diff changeset
   187
fun new_node (x, info) (Graph tab) =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   188
  Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   189
17179
28802c8a9816 canonical interface for 'default'
haftmann
parents: 17140
diff changeset
   190
fun default_node (x, info) (Graph tab) =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   191
  Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
17140
5be3a21ec949 added 'default' function
haftmann
parents: 16894
diff changeset
   192
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   193
fun del_nodes xs (Graph tab) =
15759
wenzelm
parents: 15570
diff changeset
   194
  Graph (tab
wenzelm
parents: 15570
diff changeset
   195
    |> fold Table.delete xs
39020
ac0f24f850c9 replaced Table.map' by Table.map
haftmann
parents: 37853
diff changeset
   196
    |> Table.map (fn _ => fn (i, (preds, succs)) =>
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   197
      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   198
28333
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   199
fun del_node x (G as Graph tab) =
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   200
  let
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   201
    fun del_adjacent which y =
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   202
      Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
43792
d5803c3d537a Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents: 39021
diff changeset
   203
    val (preds, succs) = #2 (#2 (get_entry G x));
28333
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   204
  in
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   205
    Graph (tab
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   206
      |> Table.delete x
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   207
      |> Keys.fold (del_adjacent apsnd) preds
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   208
      |> Keys.fold (del_adjacent apfst) succs)
28333
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   209
  end;
507b64f4cd2a added del_node, which is more efficient for sparse graphs;
wenzelm
parents: 28204
diff changeset
   210
6152
wenzelm
parents: 6142
diff changeset
   211
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   212
(* edges *)
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   213
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   214
fun is_edge G (x, y) = Keys.member (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
   215
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   216
fun add_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   217
  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
   218
  else
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   219
    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   220
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   221
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   222
fun del_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   223
  if is_edge G (x, y) then
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   224
    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   225
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   226
  else G;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   227
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   228
fun diff_edges G1 G2 =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19409
diff changeset
   229
  flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15160
diff changeset
   230
    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
   231
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   232
fun edges G = diff_edges G empty;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   233
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   234
18126
b74145e46e0d added join function
haftmann
parents: 18006
diff changeset
   235
(* join and merge *)
b74145e46e0d added join function
haftmann
parents: 18006
diff changeset
   236
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   237
fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   238
35974
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   239
fun join f (G1 as Graph tab1, G2 as Graph tab2) =
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   240
  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   241
    if pointer_eq (G1, G2) then G1
39020
ac0f24f850c9 replaced Table.map' by Table.map
haftmann
parents: 37853
diff changeset
   242
    else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
35974
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   243
  end;
6152
wenzelm
parents: 6142
diff changeset
   244
35974
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   245
fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   246
  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   247
    if pointer_eq (G1, G2) then G1
39020
ac0f24f850c9 replaced Table.map' by Table.map
haftmann
parents: 37853
diff changeset
   248
    else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
35974
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   249
  end;
6152
wenzelm
parents: 6142
diff changeset
   250
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   251
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
   252
18133
1d403623dabc avoid code redundancy;
wenzelm
parents: 18126
diff changeset
   253
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   254
(* irreducible paths -- Hasse diagram *)
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   255
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   256
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
   257
  let
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   258
    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
   259
    fun irreds [] xs' = xs'
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   260
      | irreds (x :: xs) xs' =
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   261
          if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   262
            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
   263
          then irreds xs xs'
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   264
          else irreds xs (x :: xs');
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   265
  in irreds (immediate_preds G z) [] end;
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   266
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   267
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
   268
  let
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   269
    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
   270
    fun paths path z =
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   271
      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
   272
      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
   273
  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
   274
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   275
20736
934358468a1b tuned all_paths;
wenzelm
parents: 20679
diff changeset
   276
(* all paths *)
20679
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   277
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   278
fun all_paths G (x, y) =
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   279
  let
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   280
    val (_, X) = reachable (imm_succs G) [x];
20736
934358468a1b tuned all_paths;
wenzelm
parents: 20679
diff changeset
   281
    fun paths path z =
934358468a1b tuned all_paths;
wenzelm
parents: 20679
diff changeset
   282
      if not (null path) andalso eq_key (x, z) then [z :: path]
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   283
      else if Keys.member X z andalso not (member eq_key path z)
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   284
      then maps (paths (z :: path)) (immediate_preds G z)
20679
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   285
      else [];
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   286
  in paths [] y end;
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   287
c09af1bd255a Added function all_paths (formerly find_paths).
berghofe
parents: 19950
diff changeset
   288
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   289
(* maintain acyclic graphs *)
6142
wenzelm
parents: 6134
diff changeset
   290
wenzelm
parents: 6134
diff changeset
   291
exception CYCLES of key list list;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   292
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   293
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
   294
  if is_edge G (x, y) then G
9347
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   295
  else
19580
c878a09fb849 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents: 19482
diff changeset
   296
    (case irreducible_paths G (y, x) of
9347
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   297
      [] => add_edge (x, y) G
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   298
    | cycles => raise CYCLES (map (cons x) cycles));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   299
15759
wenzelm
parents: 15570
diff changeset
   300
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   301
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   302
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   303
23964
d2df2797519b added topological_order;
wenzelm
parents: 23655
diff changeset
   304
fun topological_order G = minimals G |> all_succs G;
d2df2797519b added topological_order;
wenzelm
parents: 23655
diff changeset
   305
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   306
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   307
(* maintain transitive acyclic graphs *)
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   308
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   309
fun add_edge_trans_acyclic (x, y) G =
19290
wenzelm
parents: 19029
diff changeset
   310
  add_edge_acyclic (x, y) G
25538
58e8ba3b792b map_product and fold_product
haftmann
parents: 23964
diff changeset
   311
  |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   312
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   313
fun merge_trans_acyclic eq (G1, G2) =
35974
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   314
  if pointer_eq (G1, G2) then G1
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   315
  else
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   316
    merge_acyclic eq (G1, G2)
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   317
    |> fold add_edge_trans_acyclic (diff_edges G1 G2)
3a588b344749 low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35405
diff changeset
   318
    |> fold add_edge_trans_acyclic (diff_edges G2 G1);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   319
31540
4cfe0f756feb removed unused make;
wenzelm
parents: 31516
diff changeset
   320
44162
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   321
(* schedule acyclic graph *)
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   322
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   323
exception DEP of key * key;
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   324
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   325
fun schedule f G =
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   326
  let
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   327
    val xs = topological_order G;
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   328
    val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   329
      let
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   330
        val a = get_node G x;
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 44202
diff changeset
   331
        val deps = immediate_preds G x |> map (fn y =>
44162
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   332
          (case Table.lookup tab y of
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   333
            SOME b => (y, b)
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   334
          | NONE => raise DEP (x, y)));
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   335
      in Table.update (x, f deps (x, a)) tab end);
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   336
  in map (the o Table.lookup results) xs end;
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   337
5434899d955c general Graph.schedule;
wenzelm
parents: 43792
diff changeset
   338
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   339
(*final declarations of this structure!*)
39021
139aada5caf8 Graph.map, in analogy to Table.map
haftmann
parents: 39020
diff changeset
   340
val map = map_nodes;
19615
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   341
val fold = fold_graph;
e3ab6cd838a4 added fold;
wenzelm
parents: 19580
diff changeset
   342
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   343
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   344
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31616
diff changeset
   345
structure Graph = Graph(type key = string val ord = fast_string_ord);
35403
25a67a606782 modernized structure Int_Graph;
wenzelm
parents: 35012
diff changeset
   346
structure Int_Graph = Graph(type key = int val ord = int_ord);