6134

1 
(* Title: Pure/General/graph.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen

8806

4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

6134

5 


6 
Directed graphs.


7 
*)


8 


9 
signature GRAPH =


10 
sig


11 
type key


12 
type 'a T

9321

13 
exception UNDEF of key


14 
exception DUP of key


15 
exception DUPS of key list

6134

16 
val empty: 'a T

6659

17 
val keys: 'a T > key list

6142

18 
val map_nodes: ('a > 'b) > 'a T > 'b T


19 
val get_node: 'a T > key > 'a


20 
val map_node: key > ('a > 'a) > 'a T > 'a T


21 
val imm_preds: 'a T > key > key list


22 
val imm_succs: 'a T > key > key list

6134

23 
val all_preds: 'a T > key list > key list


24 
val all_succs: 'a T > key list > key list


25 
val find_paths: 'a T > key * key > key list list

6152

26 
val new_node: key * 'a > 'a T > 'a T

6659

27 
val del_nodes: key list > 'a T > 'a T

9321

28 
val edges: 'a T > (key * key) list

6134

29 
val add_edge: key * key > 'a T > 'a T

6152

30 
val del_edge: key * key > 'a T > 'a T

6142

31 
exception CYCLES of key list list

6134

32 
val add_edge_acyclic: key * key > 'a T > 'a T

9321

33 
val add_deps_acyclic: key * key list > 'a T > 'a T


34 
val merge_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T

6134

35 
end;


36 


37 
functor GraphFun(Key: KEY): GRAPH =


38 
struct


39 


40 


41 
(* keys *)


42 


43 
type key = Key.key;


44 


45 
val eq_key = equal EQUAL o Key.ord;


46 


47 
infix mem_key;


48 
val op mem_key = gen_mem eq_key;


49 


50 
infix ins_key;


51 
val op ins_key = gen_ins eq_key;


52 

6152

53 
infix del_key;


54 
fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;


55 

6659

56 
infix del_keys;


57 
val op del_keys = foldl (op del_key);


58 

6134

59 


60 
(* tables and sets of keys *)


61 


62 
structure Table = TableFun(Key);


63 
type keys = unit Table.table;


64 

6142

65 
val empty_keys = Table.empty: keys;


66 

6134

67 
infix mem_keys;


68 
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));


69 


70 
infix ins_keys;


71 
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);


72 


73 

6142

74 
(* graphs *)

6134

75 


76 
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;


77 

9321

78 
exception UNDEF of key;


79 
exception DUP = Table.DUP;


80 
exception DUPS = Table.DUPS;

6134

81 


82 
val empty = Graph Table.empty;

6659

83 
fun keys (Graph tab) = Table.keys tab;

6134

84 

6142

85 
fun get_entry (Graph tab) x =

6134

86 
(case Table.lookup (tab, x) of

6142

87 
Some entry => entry

9321

88 
 None => raise UNDEF x);

6134

89 

6142

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

6134

91 


92 

6142

93 
(* nodes *)


94 


95 
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);

6134

96 

6142

97 
fun get_node G = #1 o get_entry G;


98 
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));


99 


100 


101 
(* reachability *)


102 

6659

103 
(*nodes reachable from xs  topologically sorted for acyclic graphs*)

6142

104 
fun reachable next xs =

6134

105 
let

6659

106 
fun reach ((rs, R), x) =


107 
if x mem_keys R then (rs, R)


108 
else apfst (cons x) (reachs ((rs, x ins_keys R), next x))

6134

109 
and reachs R_xs = foldl reach R_xs;

6659

110 
in reachs (([], empty_keys), xs) end;

6134

111 

6142

112 
(*immediate*)


113 
fun imm_preds G = #1 o #2 o get_entry G;


114 
fun imm_succs G = #2 o #2 o get_entry G;

6134

115 

6142

116 
(*transitive*)

6659

117 
fun all_preds G = #1 o reachable (imm_preds G);


118 
fun all_succs G = #1 o reachable (imm_succs G);

6134

119 


120 

6142

121 
(* paths *)

6134

122 


123 
fun find_paths G (x, y) =


124 
let

6659

125 
val (_, X) = reachable (imm_succs G) [x];

6134

126 
fun paths ps p =


127 
if eq_key (p, x) then [p :: ps]


128 
else flat (map (paths (p :: ps))

6142

129 
(filter (fn pp => pp mem_keys X andalso not (pp mem_key ps)) (imm_preds G p)));


130 
in get_entry G y; if y mem_keys X then (paths [] y) else [] end;

6134

131 


132 

9321

133 
(* nodes *)

6134

134 

6142

135 
exception DUPLICATE of key;


136 

6152

137 
fun new_node (x, info) (Graph tab) =

9321

138 
Graph (Table.update_new ((x, (info, ([], []))), tab));

6134

139 

6659

140 
fun del_nodes xs (Graph tab) =


141 
let


142 
fun del (x, (i, (preds, succs))) =


143 
if x mem_key xs then None


144 
else Some (x, (i, (preds del_keys xs, succs del_keys xs)));


145 
in Graph (Table.make (mapfilter del (Table.dest tab))) end;


146 

6152

147 

9321

148 
(* edges *)


149 


150 
fun edges (Graph tab) =


151 
flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab));


152 

6152

153 
fun add_edge (x, y) =


154 
map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o


155 
map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));


156 


157 
fun del_edge (x, y) =


158 
map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o


159 
map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));


160 

6142

161 


162 
exception CYCLES of key list list;

6134

163 


164 
fun add_edge_acyclic (x, y) G =


165 
(case find_paths G (y, x) of


166 
[] => add_edge (x, y) G


167 
 cycles => raise CYCLES (map (cons x) cycles));


168 

9321

169 
fun add_deps_acyclic (y, xs) G =


170 
foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);


171 


172 


173 
(* merge_acyclic *)


174 


175 
fun merge_acyclic eq (Graph tab1, G2 as Graph tab2) =


176 
foldl (fn (G, xy) => add_edge_acyclic xy G)


177 
(Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);


178 

6134

179 


180 
end;


181 


182 


183 
(*graphs indexed by strings*)


184 
structure Graph = GraphFun(type key = string val ord = string_ord);
