author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73362 | dde25151c3c1 |
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 |
|
55618 | 10 |
|
73136 | 11 |
import scala.collection.mutable |
12 |
import scala.collection.immutable.SetOps |
|
13 |
import scala.collection.{IterableFactory, IterableFactoryDefaults} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
14 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
15 |
|
75393 | 16 |
object Linear_Set extends IterableFactory[Linear_Set] { |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
17 |
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) |
71601 | 18 |
override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]] |
32465 | 19 |
|
73362 | 20 |
def from[A](entries: IterableOnce[A]): Linear_Set[A] = |
21 |
entries.iterator.foldLeft(empty[A])(_.incl(_)) |
|
73136 | 22 |
|
23 |
override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A] |
|
75393 | 24 |
private class Builder[A] extends mutable.Builder[A, Linear_Set[A]] { |
73136 | 25 |
private var res = empty[A] |
73340 | 26 |
override def clear(): Unit = { res = empty[A] } |
73136 | 27 |
override def addOne(elem: A): this.type = { res = res.incl(elem); this } |
28 |
override def result(): Linear_Set[A] = res |
|
29 |
} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
30 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
35 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
36 |
|
46712 | 37 |
final class Linear_Set[A] private( |
75393 | 38 |
start: Option[A], |
39 |
end: Option[A], |
|
40 |
val nexts: Map[A, A], prevs: Map[A, A]) |
|
73136 | 41 |
extends Iterable[A] |
42 |
with SetOps[A, Linear_Set, Linear_Set[A]] |
|
75393 | 43 |
with IterableFactoryDefaults[A, Linear_Set] { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
44 |
/* relative addressing */ |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
45 |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
46 |
def next(elem: A): Option[A] = |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
47 |
if (contains(elem)) nexts.get(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
48 |
else throw new Linear_Set.Undefined(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
49 |
|
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
50 |
def prev(elem: A): Option[A] = |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
51 |
if (contains(elem)) prevs.get(elem) |
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
52 |
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
|
53 |
|
38368 | 54 |
def get_after(hook: Option[A]): Option[A] = |
55 |
hook match { |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
56 |
case None => start |
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
57 |
case Some(elem) => next(elem) |
38368 | 58 |
} |
59 |
||
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
60 |
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
|
61 |
if (contains(elem)) throw new Linear_Set.Duplicate(elem) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
62 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
63 |
hook match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
64 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
65 |
start match { |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
66 |
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
|
67 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
68 |
new Linear_Set[A](Some(elem), end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
69 |
nexts + (elem -> elem1), prevs + (elem1 -> elem)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
70 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
71 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
72 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
73 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
74 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
75 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
76 |
new Linear_Set[A](start, Some(elem), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
77 |
nexts + (elem1 -> elem), prevs + (elem -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
78 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
79 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
80 |
nexts + (elem1 -> elem) + (elem -> elem2), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
81 |
prevs + (elem2 -> elem) + (elem -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
82 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
83 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
84 |
|
73136 | 85 |
def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold |
73359 | 86 |
elems.foldLeft((hook, this)) { |
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
|
87 |
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
|
88 |
}._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
|
89 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
90 |
def delete_after(hook: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
91 |
hook match { |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
92 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
93 |
start match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
94 |
case None => throw new Linear_Set.Next_Undefined[A](None) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
95 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
96 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
97 |
case None => empty |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
98 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
99 |
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
|
100 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
101 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
102 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
103 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
104 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
105 |
nexts.get(elem1) match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
106 |
case None => throw new Linear_Set.Next_Undefined(Some(elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
107 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
108 |
nexts.get(elem2) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
109 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
110 |
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
|
111 |
case Some(elem3) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
112 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
113 |
nexts - elem2 + (elem1 -> elem3), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
114 |
prevs - elem2 + (elem3 -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
115 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
116 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
117 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
118 |
|
32465 | 119 |
|
120 |
/* Set methods */ |
|
121 |
||
71383 | 122 |
override def isEmpty: Boolean = start.isEmpty |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
123 |
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
|
124 |
|
34304 | 125 |
def contains(elem: A): Boolean = |
59319 | 126 |
nonEmpty && (end.get == elem || nexts.isDefinedAt(elem)) |
34304 | 127 |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
128 |
private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] { |
46620 | 129 |
private var next_elem = from |
73337 | 130 |
def hasNext: Boolean = next_elem.isDefined |
38583 | 131 |
def next(): A = |
34301 | 132 |
next_elem match { |
133 |
case Some(elem) => |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
134 |
next_elem = nexts.get(elem) |
34301 | 135 |
elem |
38583 | 136 |
case None => Iterator.empty.next() |
34301 | 137 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
138 |
} |
32465 | 139 |
|
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
140 |
override def iterator: Iterator[A] = make_iterator(start) |
34304 | 141 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
142 |
def iterator(elem: A): Iterator[A] = |
48746
9e1b2aafbc7f
more direct Linear_Set.reverse, swapping orientation of the graph;
wenzelm
parents:
46712
diff
changeset
|
143 |
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
|
144 |
else throw new Linear_Set.Undefined(elem) |
32465 | 145 |
|
48747 | 146 |
def iterator(from: A, to: A): Iterator[A] = |
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
147 |
if (contains(to)) |
48747 | 148 |
nexts.get(to) match { |
149 |
case None => iterator(from) |
|
150 |
case Some(stop) => iterator(from).takeWhile(_ != stop) |
|
151 |
} |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
152 |
else throw new Linear_Set.Undefined(to) |
48747 | 153 |
|
48753 | 154 |
def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts) |
155 |
||
156 |
override def last: A = reverse.head |
|
157 |
||
73136 | 158 |
def incl(elem: A): Linear_Set[A] = insert_after(end, elem) |
159 |
def excl(elem: A): Linear_Set[A] = delete_after(prev(elem)) |
|
32465 | 160 |
|
73136 | 161 |
override def iterableFactory: IterableFactory[Linear_Set] = Linear_Set |
162 |
||
163 |
override def toString: String = mkString("Linear_Set(", ", ", ")") |
|
48761
6a355b4b6a59
clarified Linear_Set.next/prev: check definedness;
wenzelm
parents:
48753
diff
changeset
|
164 |
} |