author | wenzelm |
Thu, 20 Feb 2014 14:36:17 +0100 | |
changeset 55618 | 995162143ef4 |
parent 48761 | 6a355b4b6a59 |
child 56658 | 86f9c6912965 |
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 |
46686 | 2 |
Module: PIDE |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
4 |
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
|
5 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
6 |
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
|
7 |
*/ |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
8 |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
9 |
package isabelle |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
10 |
|
55618 | 11 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
12 |
import scala.collection.SetLike |
36781 | 13 |
import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom, |
14 |
GenericSetTemplate, GenericCompanion} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
15 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
16 |
|
36781 | 17 |
object Linear_Set extends ImmutableSetFactory[Linear_Set] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
18 |
{ |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
19 |
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
20 |
override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]] |
32465 | 21 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
22 |
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
23 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
24 |
class Duplicate[A](x: A) extends Exception |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
25 |
class Undefined[A](x: A) extends Exception |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
26 |
class Next_Undefined[A](x: Option[A]) extends Exception |
32464
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 |
|
46712 | 30 |
final class Linear_Set[A] private( |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
31 |
start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
32 |
extends scala.collection.immutable.Set[A] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
33 |
with GenericSetTemplate[A, Linear_Set] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
34 |
with SetLike[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
|
35 |
{ |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
36 |
override def companion: GenericCompanion[Linear_Set] = Linear_Set |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
37 |
|
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
38 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
39 |
/* relative addressing */ |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
40 |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
41 |
def next(elem: A): Option[A] = |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
42 |
if (contains(elem)) nexts.get(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
43 |
else throw new Linear_Set.Undefined(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
44 |
|
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
45 |
def prev(elem: A): Option[A] = |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
46 |
if (contains(elem)) prevs.get(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
47 |
else throw new Linear_Set.Undefined(elem) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
48 |
|
38368 | 49 |
def get_after(hook: Option[A]): Option[A] = |
50 |
hook match { |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
51 |
case None => start |
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
52 |
case Some(elem) => next(elem) |
38368 | 53 |
} |
54 |
||
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
55 |
def insert_after(hook: Option[A], elem: A): Linear_Set[A] = |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
56 |
if (contains(elem)) throw new Linear_Set.Duplicate(elem) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
57 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
58 |
hook match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
59 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
60 |
start match { |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
61 |
case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map()) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
62 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
63 |
new Linear_Set[A](Some(elem), end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
64 |
nexts + (elem -> elem1), prevs + (elem1 -> elem)) |
32576
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 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
67 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
68 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
69 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
70 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
71 |
new Linear_Set[A](start, Some(elem), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
72 |
nexts + (elem1 -> elem), prevs + (elem -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
73 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
74 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
75 |
nexts + (elem1 -> elem) + (elem -> elem2), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
76 |
prevs + (elem2 -> elem) + (elem -> elem1)) |
32576
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 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
79 |
|
48753 | 80 |
def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] = // FIXME reverse fold |
48748
89b4e7d83d6f
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
wenzelm
parents:
48747
diff
changeset
|
81 |
((hook, this) /: elems) { |
89b4e7d83d6f
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
wenzelm
parents:
48747
diff
changeset
|
82 |
case ((last, set), elem) => (Some(elem), set.insert_after(last, elem)) |
89b4e7d83d6f
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
wenzelm
parents:
48747
diff
changeset
|
83 |
}._2 |
89b4e7d83d6f
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
wenzelm
parents:
48747
diff
changeset
|
84 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
85 |
def delete_after(hook: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
86 |
hook match { |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
87 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
88 |
start match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
89 |
case None => throw new Linear_Set.Next_Undefined[A](None) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
90 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
91 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
92 |
case None => empty |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
93 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
94 |
new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
95 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
96 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
97 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
98 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
99 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
100 |
nexts.get(elem1) match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
101 |
case None => throw new Linear_Set.Next_Undefined(Some(elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
102 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
103 |
nexts.get(elem2) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
104 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
105 |
new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
106 |
case Some(elem3) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
107 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
108 |
nexts - elem2 + (elem1 -> elem3), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
109 |
prevs - elem2 + (elem3 -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
110 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
111 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
112 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
113 |
|
32465 | 114 |
|
115 |
/* Set methods */ |
|
116 |
||
117 |
override def stringPrefix = "Linear_Set" |
|
118 |
||
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
119 |
override def isEmpty: Boolean = !start.isDefined |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
120 |
override def size: Int = if (isEmpty) 0 else nexts.size + 1 |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
121 |
|
34304 | 122 |
def contains(elem: A): Boolean = |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
123 |
!isEmpty && (end.get == elem || nexts.isDefinedAt(elem)) |
34304 | 124 |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
125 |
private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] { |
46620 | 126 |
private var next_elem = from |
38583 | 127 |
def hasNext(): Boolean = next_elem.isDefined |
128 |
def next(): A = |
|
34301 | 129 |
next_elem match { |
130 |
case Some(elem) => |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
131 |
next_elem = nexts.get(elem) |
34301 | 132 |
elem |
38583 | 133 |
case None => Iterator.empty.next() |
34301 | 134 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
135 |
} |
32465 | 136 |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
137 |
override def iterator: Iterator[A] = make_iterator(start) |
34304 | 138 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
139 |
def iterator(elem: A): Iterator[A] = |
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
140 |
if (contains(elem)) make_iterator(Some(elem)) |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
141 |
else throw new Linear_Set.Undefined(elem) |
32465 | 142 |
|
48747 | 143 |
def iterator(from: A, to: A): Iterator[A] = |
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
144 |
if (contains(to)) |
48747 | 145 |
nexts.get(to) match { |
146 |
case None => iterator(from) |
|
147 |
case Some(stop) => iterator(from).takeWhile(_ != stop) |
|
148 |
} |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
149 |
else throw new Linear_Set.Undefined(to) |
48747 | 150 |
|
48753 | 151 |
def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts) |
152 |
||
153 |
override def last: A = reverse.head |
|
154 |
||
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
155 |
def + (elem: A): Linear_Set[A] = insert_after(end, elem) |
32465 | 156 |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
157 |
def - (elem: A): Linear_Set[A] = delete_after(prev(elem)) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
158 |
} |