--- a/src/Pure/General/linear_set.scala Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/linear_set.scala Mon Mar 29 22:43:56 2010 +0200
@@ -7,27 +7,36 @@
package isabelle
+import scala.collection.SetLike
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
-object Linear_Set
+
+object Linear_Set extends SetFactory[Linear_Set]
{
private case class Rep[A](
- val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
+ val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
private def empty_rep[A] = Rep[A](None, None, Map(), Map())
- private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
- : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
+ private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+ : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
- def empty[A]: Linear_Set[A] = new Linear_Set
- def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+ implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+ override def empty[A] = new Linear_Set[A]
class Duplicate(s: String) extends Exception(s)
class Undefined(s: String) extends Exception(s)
}
-class Linear_Set[A] extends scala.collection.immutable.Set[A]
+class Linear_Set[A]
+ extends scala.collection.immutable.Set[A]
+ with GenericSetTemplate[A, Linear_Set]
+ with SetLike[A, Linear_Set[A]]
{
+ override def companion: GenericCompanion[Linear_Set] = Linear_Set
+
+
/* representation */
protected val rep = Linear_Set.empty_rep[A]
@@ -43,10 +52,10 @@
else
hook match {
case None =>
- rep.first match {
+ rep.start match {
case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
case Some(elem1) =>
- Linear_Set.make(Some(elem), rep.last,
+ Linear_Set.make(Some(elem), rep.end,
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
}
case Some(elem1) =>
@@ -54,10 +63,10 @@
else
rep.nexts.get(elem1) match {
case None =>
- Linear_Set.make(rep.first, Some(elem),
+ Linear_Set.make(rep.start, Some(elem),
rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
case Some(elem2) =>
- Linear_Set.make(rep.first, rep.last,
+ Linear_Set.make(rep.start, rep.end,
rep.nexts + (elem1 -> elem) + (elem -> elem2),
rep.prevs + (elem2 -> elem) + (elem -> elem1))
}
@@ -66,13 +75,13 @@
def delete_after(hook: Option[A]): Linear_Set[A] =
hook match {
case None =>
- rep.first match {
+ rep.start match {
case None => throw new Linear_Set.Undefined("")
case Some(elem1) =>
rep.nexts.get(elem1) match {
case None => empty
case Some(elem2) =>
- Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+ Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
}
}
case Some(elem1) =>
@@ -83,9 +92,9 @@
case Some(elem2) =>
rep.nexts.get(elem2) match {
case None =>
- Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
case Some(elem3) =>
- Linear_Set.make(rep.first, rep.last,
+ Linear_Set.make(rep.start, rep.end,
rep.nexts - elem2 + (elem1 -> elem3),
rep.prevs - elem2 + (elem3 -> elem1))
}
@@ -100,8 +109,8 @@
if (isEmpty) this
else {
val next =
- if (from == rep.last) None
- else if (from == None) rep.first
+ if (from == rep.end) None
+ else if (from == None) rep.start
else from.map(rep.nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
@@ -113,15 +122,13 @@
override def stringPrefix = "Linear_Set"
- def empty[B]: Linear_Set[B] = Linear_Set.empty
-
- override def isEmpty: Boolean = !rep.first.isDefined
- def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+ override def isEmpty: Boolean = !rep.start.isDefined
+ override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
def contains(elem: A): Boolean =
- !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+ !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
- private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+ private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
private var next_elem = start
def hasNext = next_elem.isDefined
def next =
@@ -133,18 +140,13 @@
}
}
- def elements: Iterator[A] = elements_from(rep.first)
+ override def iterator: Iterator[A] = iterator_from(rep.start)
- def elements(elem: A): Iterator[A] =
- if (contains(elem)) elements_from(Some(elem))
+ def iterator(elem: A): Iterator[A] =
+ if (contains(elem)) iterator_from(Some(elem))
else throw new Linear_Set.Undefined(elem.toString)
- def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
-
- override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
- this + elem1 + elem2 ++ elems
- override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
- override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+ def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
def - (elem: A): Linear_Set[A] =
if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)