author  wenzelm 
Sat, 25 Feb 2012 13:00:32 +0100  
changeset 46666  b01b6977a5e8 
parent 46661  d2ac78ba805e 
child 46667  318b669fe660 
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 
{ 

17 
class Duplicate[Key](x: Key) extends Exception 

18 
class Undefined[Key](x: Key) extends Exception 

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

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)) 
46611  23 
} 
24 

25 

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

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

28 
type Keys = SortedSet[Key] 
46611  29 
type Entry = (A, (Keys, Keys)) 
30 

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

31 
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

32 
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

33 

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

34 

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

35 
/* graphs */ 
46611  36 

37 
def is_empty: Boolean = rep.isEmpty 

38 

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

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

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

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

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

43 
(for ((x, (_, (_, succs))) < entries) yield (x, succs.toList)).toList 
46611  44 

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

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

46 
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

47 
.mkString("Graph(", ", ", ")") 
46611  48 

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

50 
rep.get(x) match { 

51 
case Some(entry) => entry 

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

53 
} 

54 

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

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

57 

58 

59 
/* nodes */ 

60 

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

62 

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

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

65 

66 

67 
/* reachability */ 

68 

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

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

71 
{ 

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

73 
{ 

74 
val (rs, r_set) = reached 

75 
if (r_set(x)) reached 

76 
else { 

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

78 
(x :: rs1, r_set1) 

79 
} 

80 
} 

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

82 
{ 

83 
val (rss, r_set) = reached 

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

85 
(rs :: rss, r_set1) 

86 
} 

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

87 
((List.empty[List[Key]], empty_keys) /: xs)(reachs) 
46611  88 
} 
89 

90 
/*immediate*/ 

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

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

93 

94 
/*transitive*/ 

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

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

97 

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

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

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

101 
reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse 
46613  102 

46611  103 

104 
/* minimal and maximal elements */ 

105 

106 
def minimals: List[Key] = 

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

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

109 

110 
def maximals: List[Key] = 

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

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

113 

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

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

116 

117 

118 
/* nodes */ 

119 

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

121 
{ 

122 
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

123 
else new Graph[Key, A](rep + (x > (info, (empty_keys, empty_keys)))) 
46611  124 
} 
125 

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

128 
if (rep.isDefinedAt(x)) this 

129 
else new_node(x, info) 

130 
} 

131 

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

132 
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

133 
: SortedMap[Key, Entry] = 
46611  134 
map.get(y) match { 
135 
case None => map 

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

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

138 
} 

139 

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

141 
{ 

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

143 
new Graph[Key, A]( 

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

145 
} 

146 

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

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

148 
(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

149 

46611  150 

151 
/* edges */ 

152 

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

154 
try { imm_succs(x)(y) } 

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

156 

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

158 
if (is_edge(x, y)) this 

159 
else 

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

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

162 

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

164 
if (is_edge(x, y)) 

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

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

167 
else this 

168 

169 

170 
/* irreducible paths  Hasse diagram */ 

171 

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

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

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

176 
xs0 match { 

177 
case Nil => xs1 

178 
case x :: xs => 

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

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

181 
irreds(xs, xs1) 

182 
else irreds(xs, x :: xs1) 

183 
} 

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

185 
} 

186 

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

188 
{ 

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

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

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

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

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

194 
} 

195 

196 

197 
/* maintain acyclic graphs */ 

198 

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

200 
if (is_edge(x, y)) this 

201 
else { 

202 
irreducible_paths(y, x) match { 

203 
case Nil => add_edge(x, y) 

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

205 
} 

206 
} 

207 

208 
def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] = 

209 
(this /: xs)(_.add_edge_acyclic(_, y)) 

210 

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

212 
} 