# HG changeset patch
# User wenzelm
# Date 1251804682 -7200
# Node ID 87f0e1b2d3f2bf08a8b208524827b89c07f9881a
# Parent  5b9731f83569d845364844cb543d3235f2994a1f
misc cleanup and internal reorganization;

diff -r 5b9731f83569 -r 87f0e1b2d3f2 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Tue Sep 01 11:52:19 2009 +0200
+++ b/src/Pure/General/linear_set.scala	Tue Sep 01 13:31:22 2009 +0200
@@ -1,5 +1,6 @@
 /*  Title:      Pure/General/linear_set.scala
     Author:     Makarius
+    Author:     Fabian Immler TU Munich
 
 Sets with canonical linear order, or immutable linked-lists.
 */
@@ -8,19 +9,20 @@
 
 object Linear_Set
 {
-  def empty[A]: Linear_Set[A] = new Linear_Set[A]
-  def apply[A](elems: A*): Linear_Set[A] =
-    (empty[A] /: elems) ((s, elem) => s + elem)
+  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())
+
+  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) }
+
+
+  def empty[A]: Linear_Set[A] = new Linear_Set
+  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
 
   class Duplicate(s: String) extends Exception(s)
   class Undefined(s: String) extends Exception(s)
-
-  private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): Linear_Set[A] =
-    new Linear_Set[A] {
-      override val first_elem = first
-      override val last_elem = last
-      override val body = b
-    }
 }
 
 
@@ -28,76 +30,89 @@
 {
   /* representation */
 
-  val first_elem: Option[A] = None
-  val last_elem: Option[A] = None
-  val body: Map[A, A] = Map.empty
+  protected val rep = Linear_Set.empty_rep[A]
 
 
-  /* basic methods */
+  /* auxiliary operations */
 
-  def next(elem: A) = body.get(elem)
-  def prev(elem: A) = body.find(_._2 == elem).map(_._1)
-  override def isEmpty: Boolean = !last_elem.isDefined
-  def size: Int = if (isEmpty) 0 else body.size + 1
-
-  def empty[B] = Linear_Set.empty[B]
-
-  def contains(elem: A): Boolean =
-    !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
+  def next(elem: A) = rep.body.get(elem)
+  def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1)   // slow
 
   private 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 (body.isDefinedAt(hook))
-          Linear_Set.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
-        else Linear_Set.make(first_elem, Some(elem), body + (hook -> elem))
+        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))
       case None =>
-        if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map.empty)
-        else Linear_Set.make(Some(elem), last_elem, body + (elem -> first_elem.get))
+        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))
     }
 
   def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
     elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
 
-  def +(elem: A): Linear_Set[A] = _insert_after(last_elem, 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 (!body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
-        else if (body(elem) == last_elem.get) Linear_Set.make(first_elem, Some(elem), body - elem)
-        else Linear_Set.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
+        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(body(first_elem.get)), last_elem, body - first_elem.get)
+        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(!first_elem.isDefined) this
+    if(!rep.first_elem.isDefined) this
     else {
-      val next = if (from == last_elem) None
-                 else if (from == None) first_elem
-                 else from.map(body(_))
+      val next =
+        if (from == rep.last_elem) None
+        else if (from == None) rep.first_elem
+        else from.map(rep.body(_))
       if (next == to) this
       else delete_after(from).delete_between(from, to)
     }
   }
 
-  def -(elem: A): Linear_Set[A] =
-    if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
-    else delete_after(body find (p => p._2 == elem) map (p => p._1))
+
+  /* Set methods */
+
+  override def stringPrefix = "Linear_Set"
+
+  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
 
   def elements = new Iterator[A] {
-    private var next_elem = first_elem
+    private var next_elem = rep.first_elem
     def hasNext = next_elem.isDefined
     def next = {
       val elem = next_elem.get
-      next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
+      next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
       elem
     }
   }
+
+  def contains(elem: A): Boolean =
+    !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+
+  def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, 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] =
+    if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+    else delete_after(prev(elem))
 }
\ No newline at end of file