6134

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


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Directed graphs.


6 
*)


7 


8 
signature GRAPH =


9 
sig


10 
type key


11 
type 'a T


12 
exception UNDEFINED of key


13 
val empty: 'a T

6142

14 
val get_nodes: 'a T > (key * 'a) list


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


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


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


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


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

6134

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


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


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

6142

23 
exception DUPLICATE of key

6134

24 
val add_node: key * 'a > 'a T > 'a T


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

6142

26 
exception CYCLES of key list list

6134

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


28 
val derive_node: key * 'a > key list > 'a T > 'a T


29 
end;


30 


31 
functor GraphFun(Key: KEY): GRAPH =


32 
struct


33 


34 


35 
(* keys *)


36 


37 
type key = Key.key;


38 


39 
val eq_key = equal EQUAL o Key.ord;


40 


41 
infix mem_key;


42 
val op mem_key = gen_mem eq_key;


43 


44 
infix ins_key;


45 
val op ins_key = gen_ins eq_key;


46 


47 


48 
(* tables and sets of keys *)


49 


50 
structure Table = TableFun(Key);


51 
type keys = unit Table.table;


52 

6142

53 
val empty_keys = Table.empty: keys;


54 

6134

55 
infix mem_keys;


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


57 


58 
infix ins_keys;


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


60 


61 
fun dest_keys tab = rev (Table.foldl (fn (xs, (x, ())) => x :: xs) ([], tab: keys));


62 


63 

6142

64 
(* graphs *)

6134

65 


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


67 


68 
exception UNDEFINED of key;


69 


70 
val empty = Graph Table.empty;


71 

6142

72 
fun get_entry (Graph tab) x =

6134

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

6142

74 
Some entry => entry

6134

75 
 None => raise UNDEFINED x);


76 

6142

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

6134

78 


79 

6142

80 
(* nodes *)


81 


82 
fun get_nodes (Graph tab) =


83 
rev (Table.foldl (fn (nodes, (x, (i, _))) => (x, i) :: nodes) ([], tab));


84 


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

6134

86 

6142

87 
fun get_node G = #1 o get_entry G;


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


89 


90 


91 
(* reachability *)


92 


93 
fun reachable next xs =

6134

94 
let


95 
fun reach (R, x) =


96 
if x mem_keys R then R


97 
else reachs (x ins_keys R, next x)


98 
and reachs R_xs = foldl reach R_xs;


99 
in reachs (empty_keys, xs) end;


100 

6142

101 
(*immediate*)


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


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

6134

104 

6142

105 
(*transitive*)


106 
fun all_preds G = dest_keys o reachable (imm_preds G);


107 
fun all_succs G = dest_keys o reachable (imm_succs G);

6134

108 


109 

6142

110 
(* paths *)

6134

111 


112 
fun find_paths G (x, y) =


113 
let

6142

114 
val X = reachable (imm_succs G) [x];

6134

115 
fun paths ps p =


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


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

6142

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


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

6134

120 


121 


122 
(* build graphs *)


123 

6142

124 
exception DUPLICATE of key;


125 

6134

126 
fun add_node (x, info) (Graph tab) =


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


128 
handle Table.DUP key => raise DUPLICATE key);


129 


130 
fun add_edge (x, y) G =

6142

131 
G > map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs)))


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


133 


134 
exception CYCLES of key list list;

6134

135 


136 
fun add_edge_acyclic (x, y) G =


137 
(case find_paths G (y, x) of


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


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


140 


141 
fun derive_node (x, y) zs G =


142 
foldl (fn (H, z) => add_edge_acyclic (z, x) H) (add_node (x, y) G, zs);


143 


144 


145 
end;


146 


147 


148 
(*graphs indexed by strings*)


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