--- a/src/Pure/General/linear_set.scala Tue Sep 15 15:44:57 2009 +0200
+++ b/src/Pure/General/linear_set.scala Tue Sep 15 23:57:07 2009 +0200
@@ -1,22 +1,22 @@
/* Title: Pure/General/linear_set.scala
Author: Makarius
- Author: Fabian Immler TU Munich
+ Author: Fabian Immler, TU Munich
Sets with canonical linear order, or immutable linked-lists.
*/
+
package isabelle
object Linear_Set
{
private case class Rep[A](
- val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
-
- private def empty_rep[A] = Rep[A](None, None, Map())
+ val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
- private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
- new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
+ 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) }
def empty[A]: Linear_Set[A] = new Linear_Set
def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
@@ -35,48 +35,71 @@
/* auxiliary operations */
- def next(elem: A) = rep.body.get(elem)
- def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1) // slow
+ def next(elem: A): Option[A] = rep.nexts.get(elem)
+ def prev(elem: A): Option[A] = rep.prevs.get(elem)
- private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
+ def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
- else hook match {
- case Some(hook) =>
- if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
- else if (rep.body.isDefinedAt(hook))
- Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
- else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
+ else
+ hook match {
+ case None =>
+ rep.first match {
+ case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+ case Some(elem1) =>
+ Linear_Set.make(Some(elem), rep.last,
+ rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem),
+ rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+ case Some(elem2) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts + (elem1 -> elem) + (elem -> elem2),
+ rep.prevs + (elem2 -> elem) + (elem -> elem1))
+ }
+ }
+
+ def delete_after(hook: Option[A]): Linear_Set[A] =
+ hook match {
case None =>
- if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
- else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
+ rep.first 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)
+ }
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None => throw new Linear_Set.Undefined("")
+ case Some(elem2) =>
+ rep.nexts.get(elem2) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ case Some(elem3) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts - elem2 + (elem1 -> elem3),
+ rep.prevs - elem2 + (elem3 -> elem1))
+ }
+ }
}
- def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
- elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
-
- def delete_after(elem: Option[A]): Linear_Set[A] =
- elem match {
- case Some(elem) =>
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
- else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
- else if (rep.body(elem) == rep.last_elem.get)
- Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
- else Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
- case None =>
- if (isEmpty) throw new Linear_Set.Undefined(null)
- else if (size == 1) empty
- else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
- }
-
- def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
- if(!rep.first_elem.isDefined) this
+ def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
+ {
+ if (!rep.first.isDefined) this
else {
val next =
- if (from == rep.last_elem) None
- else if (from == None) rep.first_elem
- else from.map(rep.body(_))
+ if (from == rep.last) None
+ else if (from == None) rep.first
+ else from.map(rep.nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
}
@@ -89,23 +112,23 @@
def empty[B]: Linear_Set[B] = Linear_Set.empty
- override def isEmpty: Boolean = !rep.last_elem.isDefined
- def size: Int = if (isEmpty) 0 else rep.body.size + 1
+ override def isEmpty: Boolean = !rep.first.isDefined
+ def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
def elements = new Iterator[A] {
- private var next_elem = rep.first_elem
+ private var next_elem = rep.first
def hasNext = next_elem.isDefined
def next = {
val elem = next_elem.get
- next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
+ next_elem = if (rep.nexts.isDefinedAt(elem)) Some(rep.nexts(elem)) else None
elem
}
}
def contains(elem: A): Boolean =
- !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+ !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
- def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+ 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