# HG changeset patch # User wenzelm # Date 1330018710 -3600 # Node ID 7a8dd77c9f931a48df2360b7bf4b42740ab770bb # Parent 9aea30f3b954ad7bdac5e1456ff8b09d32dedce8 streamlined abstract datatype, eliminating odd representation class; diff -r 9aea30f3b954 -r 7a8dd77c9f93 src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Thu Feb 23 18:14:58 2012 +0100 +++ b/src/Pure/General/linear_set.scala Thu Feb 23 18:38:30 2012 +0100 @@ -14,16 +14,10 @@ object Linear_Set extends ImmutableSetFactory[Linear_Set] { - protected case class Rep[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](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) } + private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) + override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]] implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] - override def empty[A] = new Linear_Set[A] class Duplicate[A](x: A) extends Exception class Undefined[A](x: A) extends Exception @@ -31,7 +25,8 @@ } -class Linear_Set[A] +class Linear_Set[A] private( + start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) extends scala.collection.immutable.Set[A] with GenericSetTemplate[A, Linear_Set] with SetLike[A, Linear_Set[A]] @@ -39,20 +34,15 @@ override def companion: GenericCompanion[Linear_Set] = Linear_Set - /* representation */ - - protected val rep = Linear_Set.empty_rep[A] - - /* relative addressing */ // FIXME check definedness?? - def next(elem: A): Option[A] = rep.nexts.get(elem) - def prev(elem: A): Option[A] = rep.prevs.get(elem) + def next(elem: A): Option[A] = nexts.get(elem) + def prev(elem: A): Option[A] = prevs.get(elem) def get_after(hook: Option[A]): Option[A] = hook match { - case None => rep.start + case None => start case Some(elem) => if (!contains(elem)) throw new Linear_Set.Undefined(elem) next(elem) @@ -63,51 +53,51 @@ else hook match { case None => - rep.start match { - case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map()) + start match { + case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map()) case Some(elem1) => - Linear_Set.make(Some(elem), rep.end, - rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem)) + new Linear_Set[A](Some(elem), end, + nexts + (elem -> elem1), prevs + (elem1 -> elem)) } case Some(elem1) => if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else - rep.nexts.get(elem1) match { + nexts.get(elem1) match { case None => - Linear_Set.make(rep.start, Some(elem), - rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1)) + new Linear_Set[A](start, Some(elem), + nexts + (elem1 -> elem), prevs + (elem -> elem1)) case Some(elem2) => - Linear_Set.make(rep.start, rep.end, - rep.nexts + (elem1 -> elem) + (elem -> elem2), - rep.prevs + (elem2 -> elem) + (elem -> elem1)) + new Linear_Set[A](start, end, + nexts + (elem1 -> elem) + (elem -> elem2), + prevs + (elem2 -> elem) + (elem -> elem1)) } } def delete_after(hook: Option[A]): Linear_Set[A] = hook match { case None => - rep.start match { + start match { case None => throw new Linear_Set.Next_Undefined[A](None) case Some(elem1) => - rep.nexts.get(elem1) match { + nexts.get(elem1) match { case None => empty case Some(elem2) => - Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2) + new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2) } } case Some(elem1) => if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else - rep.nexts.get(elem1) match { + nexts.get(elem1) match { case None => throw new Linear_Set.Next_Undefined(Some(elem1)) case Some(elem2) => - rep.nexts.get(elem2) match { + nexts.get(elem2) match { case None => - Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2) + new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2) case Some(elem3) => - Linear_Set.make(rep.start, rep.end, - rep.nexts - elem2 + (elem1 -> elem3), - rep.prevs - elem2 + (elem3 -> elem1)) + new Linear_Set[A](start, end, + nexts - elem2 + (elem1 -> elem3), + prevs - elem2 + (elem3 -> elem1)) } } } @@ -122,9 +112,9 @@ if (isEmpty) this else { val next = - if (from == rep.end) None - else if (from == None) rep.start - else from.map(rep.nexts(_)) + if (from == end) None + else if (from == None) start + else from.map(nexts(_)) if (next == to) this else delete_after(from).delete_between(from, to) } @@ -135,11 +125,11 @@ override def stringPrefix = "Linear_Set" - override def isEmpty: Boolean = !rep.start.isDefined - override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1 + override def isEmpty: Boolean = !start.isDefined + override def size: Int = if (isEmpty) 0 else nexts.size + 1 def contains(elem: A): Boolean = - !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem)) + !isEmpty && (end.get == elem || nexts.isDefinedAt(elem)) private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] { private var next_elem = from @@ -153,17 +143,17 @@ } } - override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts) + override def iterator: Iterator[A] = make_iterator(start, nexts) def iterator(elem: A): Iterator[A] = - if (contains(elem)) make_iterator(Some(elem), rep.nexts) + if (contains(elem)) make_iterator(Some(elem), nexts) else throw new Linear_Set.Undefined(elem) def reverse_iterator(elem: A): Iterator[A] = - if (contains(elem)) make_iterator(Some(elem), rep.prevs) + if (contains(elem)) make_iterator(Some(elem), prevs) else throw new Linear_Set.Undefined(elem) - def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem) + def + (elem: A): Linear_Set[A] = insert_after(end, elem) def - (elem: A): Linear_Set[A] = if (!contains(elem)) throw new Linear_Set.Undefined(elem)