author  wenzelm 
Thu, 19 Jul 2012 14:15:08 +0200  
changeset 48348  cbb25adad26f 
parent 46712  8650d9a95736 
child 48350  09bf3b73e446 
permissions  rwrr 
46611  1 
/* Title: Pure/General/graph.scala 
2 
Module: PIDE 

3 
Author: Makarius 

4 

5 
Directed graphs. 

6 
*/ 

7 

8 
package isabelle 

9 

10 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

11 
import scala.collection.immutable.{SortedMap, SortedSet} 
46611  12 
import scala.annotation.tailrec 
13 

14 

15 
object Graph 

16 
{ 

48348  17 
class Duplicate[Key](val key: Key) extends Exception 
18 
class Undefined[Key](val key: Key) extends Exception 

19 
class Cycles[Key](val cycles: List[List[Key]]) extends Exception 

46611  20 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

21 
def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] = 
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

22 
new Graph[Key, A](SortedMap.empty(ord)) 
46667  23 

24 
def string[A]: Graph[String, A] = empty(Ordering.String) 

25 
def int[A]: Graph[Int, A] = empty(Ordering.Int) 

26 
def long[A]: Graph[Long, A] = empty(Ordering.Long) 

46611  27 
} 
28 

29 

46712  30 
final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) 
46611  31 
{ 
46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

32 
type Keys = SortedSet[Key] 
46611  33 
type Entry = (A, (Keys, Keys)) 
34 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

35 
def ordering: Ordering[Key] = rep.ordering 
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

36 
def empty_keys: Keys = SortedSet.empty[Key](ordering) 
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

37 

46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

38 

b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

39 
/* graphs */ 
46611  40 

41 
def is_empty: Boolean = rep.isEmpty 

42 

46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

43 
def entries: Iterator[(Key, Entry)] = rep.iterator 
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

44 
def keys: Iterator[Key] = entries.map(_._1) 
46611  45 

46 
def dest: List[(Key, List[Key])] = 

46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

47 
(for ((x, (_, (_, succs))) < entries) yield (x, succs.toList)).toList 
46611  48 

46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

49 
override def toString: String = 
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

50 
dest.map(p => p._1.toString + " > " + p._2.map(_.toString).mkString("{", ", ", "}")) 
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

51 
.mkString("Graph(", ", ", ")") 
46611  52 

53 
private def get_entry(x: Key): Entry = 

54 
rep.get(x) match { 

55 
case Some(entry) => entry 

56 
case None => throw new Graph.Undefined(x) 

57 
} 

58 

59 
private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] = 

60 
new Graph[Key, A](rep + (x > f(get_entry(x)))) 

61 

62 

63 
/* nodes */ 

64 

65 
def get_node(x: Key): A = get_entry(x)._1 

66 

67 
def map_node(x: Key, f: A => A): Graph[Key, A] = 

68 
map_entry(x, { case (i, ps) => (f(i), ps) }) 

69 

70 

71 
/* reachability */ 

72 

73 
/*nodes reachable from xs  topologically sorted for acyclic graphs*/ 

74 
def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = 

75 
{ 

76 
def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) = 

77 
{ 

78 
val (rs, r_set) = reached 

79 
if (r_set(x)) reached 

80 
else { 

81 
val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach) 

82 
(x :: rs1, r_set1) 

83 
} 

84 
} 

85 
def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = 

86 
{ 

87 
val (rss, r_set) = reached 

88 
val (rs, r_set1) = reach((Nil, r_set), x) 

89 
(rs :: rss, r_set1) 

90 
} 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

91 
((List.empty[List[Key]], empty_keys) /: xs)(reachs) 
46611  92 
} 
93 

94 
/*immediate*/ 

95 
def imm_preds(x: Key): Keys = get_entry(x)._2._1 

96 
def imm_succs(x: Key): Keys = get_entry(x)._2._2 

97 

98 
/*transitive*/ 

99 
def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten 

100 
def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten 

101 

46613  102 
/*strongly connected components; see: David King and John Launchbury, 
103 
"Structuring Depth First Search Algorithms in Haskell"*/ 

104 
def strong_conn: List[List[Key]] = 

46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

105 
reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse 
46613  106 

46611  107 

108 
/* minimal and maximal elements */ 

109 

110 
def minimals: List[Key] = 

111 
(List.empty[Key] /: rep) { 

112 
case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms } 

113 

114 
def maximals: List[Key] = 

115 
(List.empty[Key] /: rep) { 

116 
case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms } 

117 

118 
def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty 

119 
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty 

120 

121 

46668  122 
/* node operations */ 
46611  123 

124 
def new_node(x: Key, info: A): Graph[Key, A] = 

125 
{ 

126 
if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x) 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

127 
else new Graph[Key, A](rep + (x > (info, (empty_keys, empty_keys)))) 
46611  128 
} 
129 

46613  130 
def default_node(x: Key, info: A): Graph[Key, A] = 
131 
{ 

132 
if (rep.isDefinedAt(x)) this 

133 
else new_node(x, info) 

134 
} 

135 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

136 
private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key) 
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

137 
: SortedMap[Key, Entry] = 
46611  138 
map.get(y) match { 
139 
case None => map 

140 
case Some((i, (preds, succs))) => 

141 
map + (y > (i, if (fst) (preds  x, succs) else (preds, succs  x))) 

142 
} 

143 

144 
def del_node(x: Key): Graph[Key, A] = 

145 
{ 

146 
val (preds, succs) = get_entry(x)._2 

147 
new Graph[Key, A]( 

148 
(((rep  x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x))) 

149 
} 

150 

46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

151 
def restrict(pred: Key => Boolean): Graph[Key, A] = 
46666
b01b6977a5e8
clarified signature  avoid oddities of Iterable like Iterator.map;
wenzelm
parents:
46661
diff
changeset

152 
(this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } 
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

153 

46611  154 

46668  155 
/* edge operations */ 
46611  156 

157 
def is_edge(x: Key, y: Key): Boolean = 

158 
try { imm_succs(x)(y) } 

159 
catch { case _: Graph.Undefined[_] => false } 

160 

161 
def add_edge(x: Key, y: Key): Graph[Key, A] = 

162 
if (is_edge(x, y)) this 

163 
else 

164 
map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }). 

165 
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) }) 

166 

167 
def del_edge(x: Key, y: Key): Graph[Key, A] = 

168 
if (is_edge(x, y)) 

169 
map_entry(y, { case (i, (preds, succs)) => (i, (preds  x, succs)) }). 

170 
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs  y)) }) 

171 
else this 

172 

173 

174 
/* irreducible paths  Hasse diagram */ 

175 

46661
d2ac78ba805e
prefer sorted Map/Set for canonical order of results  pass ordering via fresh copy of empty;
wenzelm
parents:
46659
diff
changeset

176 
private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] = 
46611  177 
{ 
178 
def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z 

179 
@tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] = 

180 
xs0 match { 

181 
case Nil => xs1 

182 
case x :: xs => 

183 
if (!(x_set(x))  x == z  path.contains(x)  

184 
xs.exists(red(x))  xs1.exists(red(x))) 

185 
irreds(xs, xs1) 

186 
else irreds(xs, x :: xs1) 

187 
} 

188 
irreds(imm_preds(z).toList, Nil) 

189 
} 

190 

191 
def irreducible_paths(x: Key, y: Key): List[List[Key]] = 

192 
{ 

193 
val (_, x_set) = reachable(imm_succs, List(x)) 

194 
def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] = 

195 
if (x == z) (z :: path) :: ps 

196 
else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path)) 

197 
if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y) 

198 
} 

199 

200 

201 
/* maintain acyclic graphs */ 

202 

203 
def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] = 

204 
if (is_edge(x, y)) this 

205 
else { 

206 
irreducible_paths(y, x) match { 

207 
case Nil => add_edge(x, y) 

208 
case cycles => throw new Graph.Cycles(cycles.map(x :: _)) 

209 
} 

210 
} 

211 

48348  212 
def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] = 
46611  213 
(this /: xs)(_.add_edge_acyclic(_, y)) 
214 

215 
def topological_order: List[Key] = all_succs(minimals) 

216 
} 