src/Tools/jEdit/src/utils/LinearSet.scala
author immler@in.tum.de
Thu, 05 Mar 2009 10:53:47 +0100
changeset 34530 de629c23b389
parent 34529 f0e55d9ffe45
child 34531 db1c28e326fc
permissions -rw-r--r--
implemented delete_after
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34528
3c3a23c1eb8c changed title
immler@in.tum.de
parents: 34527
diff changeset
     1
/*  Title:      LinearSet.scala
34527
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     2
    Author:     Makarius
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     3
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     4
Sets with canonical linear order, or immutable linked-lists.
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     5
*/
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     6
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     7
object LinearSet
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     8
{
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
     9
  def empty[A]: LinearSet[A] = new LinearSet[A]
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    10
  def apply[A](elems: A*): LinearSet[A] =
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    11
    (empty[A] /: elems) ((s, elem) => s + elem)
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    12
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    13
  class Duplicate(s: String) extends Exception(s)
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    14
  class Undefined(s: String) extends Exception(s)
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    15
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    16
  private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): LinearSet[A] =
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    17
    new LinearSet[A] {
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    18
      override val first_elem = first
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    19
      override val last_elem = last
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    20
      override val body = b
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    21
    }
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    22
}
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    23
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    24
class LinearSet[A] extends scala.collection.immutable.Set[A]
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    25
{
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    26
  /* representation */
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    27
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    28
  val first_elem: Option[A] = None
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    29
  val last_elem: Option[A] = None
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    30
  val body: Map[A, A] = Map.empty
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    31
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    32
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    33
  /* basic methods */
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    34
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    35
  override def isEmpty: Boolean = !last_elem.isDefined
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    36
  def size: Int = if (isEmpty) 0 else body.size + 1
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    37
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    38
  def empty[B] = LinearSet.empty[B]
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    39
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    40
  def contains(elem: A): Boolean =
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    41
    !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    42
34529
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    43
  def insert_after(hook: Option[A], elem: A): LinearSet[A] =
34527
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    44
    if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
34529
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    45
    else hook match {
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    46
      case Some(hook) =>
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    47
        if (!contains(hook)) throw new LinearSet.Undefined(hook.toString)
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    48
        else if (body.isDefinedAt(hook))
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    49
          LinearSet.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    50
        else LinearSet.make(first_elem, Some(elem), body + (hook -> elem))
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    51
      case None =>
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    52
        if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    53
        else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    54
    }
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    55
    
f0e55d9ffe45 implemented insert_after
immler@in.tum.de
parents: 34528
diff changeset
    56
  def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
34527
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    57
34530
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    58
  def delete_after(elem: Option[A]): LinearSet[A] =
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    59
    elem match {
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    60
      case Some(elem) =>
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    61
        if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    62
        else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    63
        else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    64
        else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    65
      case None =>
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    66
        if (isEmpty) throw new LinearSet.Undefined(null)
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    67
        else if (size == 1) empty
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    68
        else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    69
    }
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    70
    
34527
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    71
  def -(elem: A): LinearSet[A] =
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    72
    if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
34530
de629c23b389 implemented delete_after
immler@in.tum.de
parents: 34529
diff changeset
    73
    else delete_after(body find (p => p._2 == elem) map (p => p._1))
34527
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    74
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    75
  def elements = new Iterator[A] {
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    76
    private var next_elem = first_elem
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    77
    def hasNext = next_elem.isDefined
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    78
    def next = {
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    79
      val elem = next_elem.get
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    80
      next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    81
      elem
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    82
    }
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    83
  }
79ad42a9497f added Makarius' LinearSet
immler@in.tum.de
parents:
diff changeset
    84
}