author | wenzelm |
Thu, 23 Feb 2012 19:35:05 +0100 | |
changeset 46623 | bce24d3f29e7 |
parent 46615 | c29bf6741ace |
child 46659 | b257053a4cbe |
permissions | -rw-r--r-- |
46611 | 1 |
/* Title: Pure/General/graph.scala |
2 |
Module: PIDE |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Directed graphs. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
import scala.annotation.tailrec |
|
12 |
||
13 |
||
14 |
object Graph |
|
15 |
{ |
|
16 |
class Duplicate[Key](x: Key) extends Exception |
|
17 |
class Undefined[Key](x: Key) extends Exception |
|
18 |
class Cycles[Key](cycles: List[List[Key]]) extends Exception |
|
19 |
||
46623 | 20 |
private val empty_val: Graph[Any, Nothing] = new Graph[Any, Nothing](Map.empty) |
21 |
def empty[Key, A]: Graph[Key, A] = empty_val.asInstanceOf[Graph[Key, A]] |
|
46611 | 22 |
} |
23 |
||
24 |
||
25 |
class Graph[Key, A] private(rep: Map[Key, (A, (Set[Key], Set[Key]))]) |
|
26 |
extends Iterable[(Key, (A, (Set[Key], Set[Key])))] |
|
27 |
{ |
|
28 |
type Keys = Set[Key] |
|
29 |
type Entry = (A, (Keys, Keys)) |
|
30 |
||
31 |
def iterator: Iterator[(Key, Entry)] = rep.iterator |
|
32 |
||
33 |
def is_empty: Boolean = rep.isEmpty |
|
34 |
||
35 |
def keys: Set[Key] = rep.keySet.toSet |
|
36 |
||
37 |
def dest: List[(Key, List[Key])] = |
|
38 |
(for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList |
|
39 |
||
40 |
||
41 |
/* entries */ |
|
42 |
||
43 |
private def get_entry(x: Key): Entry = |
|
44 |
rep.get(x) match { |
|
45 |
case Some(entry) => entry |
|
46 |
case None => throw new Graph.Undefined(x) |
|
47 |
} |
|
48 |
||
49 |
private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] = |
|
50 |
new Graph[Key, A](rep + (x -> f(get_entry(x)))) |
|
51 |
||
52 |
||
53 |
/* nodes */ |
|
54 |
||
55 |
def get_node(x: Key): A = get_entry(x)._1 |
|
56 |
||
57 |
def map_node(x: Key, f: A => A): Graph[Key, A] = |
|
58 |
map_entry(x, { case (i, ps) => (f(i), ps) }) |
|
59 |
||
46615 | 60 |
def map_nodes[B](f: A => B): Graph[Key, B] = |
61 |
new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) }) |
|
62 |
||
46611 | 63 |
|
64 |
/* reachability */ |
|
65 |
||
66 |
/*nodes reachable from xs -- topologically sorted for acyclic graphs*/ |
|
67 |
def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = |
|
68 |
{ |
|
69 |
def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) = |
|
70 |
{ |
|
71 |
val (rs, r_set) = reached |
|
72 |
if (r_set(x)) reached |
|
73 |
else { |
|
74 |
val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach) |
|
75 |
(x :: rs1, r_set1) |
|
76 |
} |
|
77 |
} |
|
78 |
def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = |
|
79 |
{ |
|
80 |
val (rss, r_set) = reached |
|
81 |
val (rs, r_set1) = reach((Nil, r_set), x) |
|
82 |
(rs :: rss, r_set1) |
|
83 |
} |
|
84 |
((List.empty[List[Key]], Set.empty[Key]) /: xs)(reachs) |
|
85 |
} |
|
86 |
||
87 |
/*immediate*/ |
|
88 |
def imm_preds(x: Key): Keys = get_entry(x)._2._1 |
|
89 |
def imm_succs(x: Key): Keys = get_entry(x)._2._2 |
|
90 |
||
91 |
/*transitive*/ |
|
92 |
def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten |
|
93 |
def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten |
|
94 |
||
46613 | 95 |
/*strongly connected components; see: David King and John Launchbury, |
96 |
"Structuring Depth First Search Algorithms in Haskell"*/ |
|
97 |
def strong_conn: List[List[Key]] = |
|
98 |
reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse |
|
99 |
||
46611 | 100 |
|
101 |
/* minimal and maximal elements */ |
|
102 |
||
103 |
def minimals: List[Key] = |
|
104 |
(List.empty[Key] /: rep) { |
|
105 |
case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms } |
|
106 |
||
107 |
def maximals: List[Key] = |
|
108 |
(List.empty[Key] /: rep) { |
|
109 |
case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms } |
|
110 |
||
111 |
def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty |
|
112 |
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty |
|
113 |
||
114 |
||
115 |
/* nodes */ |
|
116 |
||
117 |
def new_node(x: Key, info: A): Graph[Key, A] = |
|
118 |
{ |
|
119 |
if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x) |
|
120 |
else new Graph[Key, A](rep + (x -> (info, (Set.empty, Set.empty)))) |
|
121 |
} |
|
122 |
||
46613 | 123 |
def default_node(x: Key, info: A): Graph[Key, A] = |
124 |
{ |
|
125 |
if (rep.isDefinedAt(x)) this |
|
126 |
else new_node(x, info) |
|
127 |
} |
|
128 |
||
46611 | 129 |
def del_nodes(xs: List[Key]): Graph[Key, A] = |
130 |
{ |
|
131 |
xs.foreach(get_entry) |
|
132 |
new Graph[Key, A]( |
|
133 |
(rep -- xs) mapValues { case (i, (preds, succs)) => (i, (preds -- xs, succs -- xs)) }) |
|
134 |
} |
|
135 |
||
136 |
private def del_adjacent(fst: Boolean, x: Key)(map: Map[Key, Entry], y: Key): Map[Key, Entry] = |
|
137 |
map.get(y) match { |
|
138 |
case None => map |
|
139 |
case Some((i, (preds, succs))) => |
|
140 |
map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x))) |
|
141 |
} |
|
142 |
||
143 |
def del_node(x: Key): Graph[Key, A] = |
|
144 |
{ |
|
145 |
val (preds, succs) = get_entry(x)._2 |
|
146 |
new Graph[Key, A]( |
|
147 |
(((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x))) |
|
148 |
} |
|
149 |
||
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset
|
150 |
def restrict(pred: Key => Boolean): Graph[Key, A] = |
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset
|
151 |
(this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } |
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset
|
152 |
|
46611 | 153 |
|
154 |
/* edges */ |
|
155 |
||
156 |
def is_edge(x: Key, y: Key): Boolean = |
|
157 |
try { imm_succs(x)(y) } |
|
158 |
catch { case _: Graph.Undefined[_] => false } |
|
159 |
||
160 |
def add_edge(x: Key, y: Key): Graph[Key, A] = |
|
161 |
if (is_edge(x, y)) this |
|
162 |
else |
|
163 |
map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }). |
|
164 |
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) }) |
|
165 |
||
166 |
def del_edge(x: Key, y: Key): Graph[Key, A] = |
|
167 |
if (is_edge(x, y)) |
|
168 |
map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }). |
|
169 |
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) }) |
|
170 |
else this |
|
171 |
||
172 |
||
173 |
/* irreducible paths -- Hasse diagram */ |
|
174 |
||
175 |
def irreducible_preds(x_set: Set[Key], path: List[Key], z: Key): List[Key] = |
|
176 |
{ |
|
177 |
def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z |
|
178 |
@tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] = |
|
179 |
xs0 match { |
|
180 |
case Nil => xs1 |
|
181 |
case x :: xs => |
|
182 |
if (!(x_set(x)) || x == z || path.contains(x) || |
|
183 |
xs.exists(red(x)) || xs1.exists(red(x))) |
|
184 |
irreds(xs, xs1) |
|
185 |
else irreds(xs, x :: xs1) |
|
186 |
} |
|
187 |
irreds(imm_preds(z).toList, Nil) |
|
188 |
} |
|
189 |
||
190 |
def irreducible_paths(x: Key, y: Key): List[List[Key]] = |
|
191 |
{ |
|
192 |
val (_, x_set) = reachable(imm_succs, List(x)) |
|
193 |
def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] = |
|
194 |
if (x == z) (z :: path) :: ps |
|
195 |
else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path)) |
|
196 |
if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y) |
|
197 |
} |
|
198 |
||
199 |
||
200 |
/* maintain acyclic graphs */ |
|
201 |
||
202 |
def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] = |
|
203 |
if (is_edge(x, y)) this |
|
204 |
else { |
|
205 |
irreducible_paths(y, x) match { |
|
206 |
case Nil => add_edge(x, y) |
|
207 |
case cycles => throw new Graph.Cycles(cycles.map(x :: _)) |
|
208 |
} |
|
209 |
} |
|
210 |
||
211 |
def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] = |
|
212 |
(this /: xs)(_.add_edge_acyclic(_, y)) |
|
213 |
||
214 |
def topological_order: List[Key] = all_succs(minimals) |
|
215 |
} |