# HG changeset patch # User wenzelm # Date 1253051827 -7200 # Node ID 20b261654e33413afef0055c01cda8e0ca4c05bb # Parent bf6c78d9f94c2e09203532090ba7d7b80617626d double linking for improved performance of "prev"; misc tuning; diff -r bf6c78d9f94c -r 20b261654e33 src/Pure/General/linear_set.scala --- 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