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 
exception DUPLICATE of key


14 
exception CYCLES of key list list


15 
val empty: 'a T


16 
val map : ('a > 'b) > 'a T > 'b T


17 
val foldl : ('a * (key * ('b * (key list * key list))) > 'a) > 'a * 'b T > 'a


18 
val info: 'a T > key > 'a


19 
val map_info: ('a > 'a) > key > 'a T > 'a T


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


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


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


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


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


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


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


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 


53 
infix mem_keys;


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


55 


56 
infix ins_keys;


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


58 


59 
val empty_keys = Table.empty: keys;


60 
fun make_keys xs = foldl (fn (tab, x) => x ins_keys tab) (empty_keys, xs);


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


62 


63 


64 
(* datatype of graphs *)


65 


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


67 


68 
exception UNDEFINED of key;


69 
exception DUPLICATE of key;


70 
exception CYCLES of key list list;


71 


72 


73 
(* basic operations *)


74 


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


76 
fun foldl_graph f (x, Graph tab) = Table.foldl f (x, tab);


77 


78 
val empty = Graph Table.empty;


79 


80 
fun get_node (Graph tab) x =


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


82 
Some node => node


83 
 None => raise UNDEFINED x);


84 


85 
fun info G = #1 o get_node G;


86 
fun preds G = #1 o #2 o get_node G;


87 
fun succs G = #2 o #2 o get_node G;


88 


89 
fun map_node f x (G as Graph tab) =


90 
let val node = get_node G x


91 
in Graph (Table.update ((x, f node), tab)) end;


92 


93 
fun map_info f = map_node (fn (info, ps) => (f info, ps));


94 


95 


96 
(* reachable nodes *)


97 


98 
fun reachable_keys next xs =


99 
let


100 
fun reach (R, x) =


101 
if x mem_keys R then R


102 
else reachs (x ins_keys R, next x)


103 
and reachs R_xs = foldl reach R_xs;


104 
in reachs (empty_keys, xs) end;


105 


106 
val reachable = dest_keys oo reachable_keys;


107 


108 
fun all_preds G = reachable (preds G);


109 
fun all_succs G = reachable (succs G);


110 


111 


112 
(* find_paths *)


113 


114 
fun find_paths G (x, y) =


115 
let


116 
val X = reachable_keys (succs G) [x];


117 
fun paths ps p =


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


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


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


121 
in if y mem_keys X then (paths [] y) else [] end;


122 


123 


124 
(* build graphs *)


125 


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 =


131 
(get_node G x; get_node G y;


132 
G > map_node (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) x


133 
> map_node (fn (i, (preds, succs)) => (i, (x ins_key preds, succs))) y);


134 


135 
fun add_edge_acyclic (x, y) G =


136 
(case find_paths G (y, x) of


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


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


139 


140 
fun derive_node (x, y) zs G =


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


142 


143 


144 
(*final declarations of this structure!*)


145 
val map = map_graph;


146 
val foldl = foldl_graph;


147 


148 


149 
end;


150 


151 


152 
(*graphs indexed by strings*)


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