author | wenzelm |
Sun, 10 Jan 2010 23:43:25 +0100 | |
changeset 34304 | b32c68328d24 |
parent 34301 | 78c10aea025d |
child 36011 | 3ff725ac13a4 |
permissions | -rw-r--r-- |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/linear_set.scala |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
3 |
Author: Fabian Immler, TU Munich |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
4 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
5 |
Sets with canonical linear order, or immutable linked-lists. |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
6 |
*/ |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
7 |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
9 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
10 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
11 |
object Linear_Set |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
12 |
{ |
32465 | 13 |
private case class Rep[A]( |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
14 |
val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) |
32465 | 15 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
16 |
private def empty_rep[A] = Rep[A](None, None, Map(), Map()) |
32465 | 17 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
18 |
private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A]) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
19 |
: Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) } |
32465 | 20 |
|
21 |
def empty[A]: Linear_Set[A] = new Linear_Set |
|
22 |
def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
23 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
24 |
class Duplicate(s: String) extends Exception(s) |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
25 |
class Undefined(s: String) extends Exception(s) |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
26 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
27 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
28 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
29 |
class Linear_Set[A] extends scala.collection.immutable.Set[A] |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
30 |
{ |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
31 |
/* representation */ |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
32 |
|
32465 | 33 |
protected val rep = Linear_Set.empty_rep[A] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
34 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
35 |
|
32465 | 36 |
/* auxiliary operations */ |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
37 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
38 |
def next(elem: A): Option[A] = rep.nexts.get(elem) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
39 |
def prev(elem: A): Option[A] = rep.prevs.get(elem) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
40 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
41 |
def insert_after(hook: Option[A], elem: A): Linear_Set[A] = |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
42 |
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
43 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
44 |
hook match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
45 |
case None => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
46 |
rep.first match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
47 |
case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map()) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
48 |
case Some(elem1) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
49 |
Linear_Set.make(Some(elem), rep.last, |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
50 |
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
51 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
52 |
case Some(elem1) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
53 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
54 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
55 |
rep.nexts.get(elem1) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
56 |
case None => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
57 |
Linear_Set.make(rep.first, Some(elem), |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
58 |
rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
59 |
case Some(elem2) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
60 |
Linear_Set.make(rep.first, rep.last, |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
61 |
rep.nexts + (elem1 -> elem) + (elem -> elem2), |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
62 |
rep.prevs + (elem2 -> elem) + (elem -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
63 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
64 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
65 |
|
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
66 |
def delete_after(hook: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
67 |
hook match { |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
68 |
case None => |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
69 |
rep.first match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
70 |
case None => throw new Linear_Set.Undefined("") |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
71 |
case Some(elem1) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
72 |
rep.nexts.get(elem1) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
73 |
case None => empty |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
74 |
case Some(elem2) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
75 |
Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
76 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
77 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
78 |
case Some(elem1) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
79 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
80 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
81 |
rep.nexts.get(elem1) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
82 |
case None => throw new Linear_Set.Undefined("") |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
83 |
case Some(elem2) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
84 |
rep.nexts.get(elem2) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
85 |
case None => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
86 |
Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
87 |
case Some(elem3) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
88 |
Linear_Set.make(rep.first, rep.last, |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
89 |
rep.nexts - elem2 + (elem1 -> elem3), |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
90 |
rep.prevs - elem2 + (elem3 -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
91 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
92 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
93 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
94 |
|
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
95 |
def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] = |
32591 | 96 |
(elems :\ this)((elem, set) => set.insert_after(hook, elem)) |
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
97 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
98 |
def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
99 |
{ |
32591 | 100 |
if (isEmpty) this |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
101 |
else { |
32465 | 102 |
val next = |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
103 |
if (from == rep.last) None |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
104 |
else if (from == None) rep.first |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
105 |
else from.map(rep.nexts(_)) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
106 |
if (next == to) this |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
107 |
else delete_after(from).delete_between(from, to) |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
108 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
109 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
110 |
|
32465 | 111 |
|
112 |
/* Set methods */ |
|
113 |
||
114 |
override def stringPrefix = "Linear_Set" |
|
115 |
||
116 |
def empty[B]: Linear_Set[B] = Linear_Set.empty |
|
117 |
||
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
118 |
override def isEmpty: Boolean = !rep.first.isDefined |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
119 |
def size: Int = if (isEmpty) 0 else rep.nexts.size + 1 |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
120 |
|
34304 | 121 |
def contains(elem: A): Boolean = |
122 |
!isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem)) |
|
123 |
||
124 |
private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] { |
|
125 |
private var next_elem = start |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
126 |
def hasNext = next_elem.isDefined |
34301 | 127 |
def next = |
128 |
next_elem match { |
|
129 |
case Some(elem) => |
|
130 |
next_elem = rep.nexts.get(elem) |
|
131 |
elem |
|
132 |
case None => throw new NoSuchElementException("next on empty iterator") |
|
133 |
} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
134 |
} |
32465 | 135 |
|
34304 | 136 |
def elements: Iterator[A] = elements_from(rep.first) |
137 |
||
138 |
def elements(elem: A): Iterator[A] = |
|
139 |
if (contains(elem)) elements_from(Some(elem)) |
|
140 |
else throw new Linear_Set.Undefined(elem.toString) |
|
32465 | 141 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
142 |
def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem) |
32465 | 143 |
|
144 |
override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] = |
|
145 |
this + elem1 + elem2 ++ elems |
|
146 |
override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem) |
|
147 |
override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem) |
|
148 |
||
149 |
def - (elem: A): Linear_Set[A] = |
|
150 |
if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString) |
|
151 |
else delete_after(prev(elem)) |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
152 |
} |