src/Pure/General/linear_set.scala
changeset 48761 6a355b4b6a59
parent 48753 5e57a6f24cdb
child 55618 995162143ef4
equal deleted inserted replaced
48760:4218d7b5d892 48761:6a355b4b6a59
    35   override def companion: GenericCompanion[Linear_Set] = Linear_Set
    35   override def companion: GenericCompanion[Linear_Set] = Linear_Set
    36 
    36 
    37 
    37 
    38   /* relative addressing */
    38   /* relative addressing */
    39 
    39 
    40   // FIXME check definedness??
    40   def next(elem: A): Option[A] =
    41   def next(elem: A): Option[A] = nexts.get(elem)
    41     if (contains(elem)) nexts.get(elem)
    42   def prev(elem: A): Option[A] = prevs.get(elem)
    42     else throw new Linear_Set.Undefined(elem)
       
    43 
       
    44   def prev(elem: A): Option[A] =
       
    45     if (contains(elem)) prevs.get(elem)
       
    46     else throw new Linear_Set.Undefined(elem)
    43 
    47 
    44   def get_after(hook: Option[A]): Option[A] =
    48   def get_after(hook: Option[A]): Option[A] =
    45     hook match {
    49     hook match {
    46       case None => start
    50       case None => start
    47       case Some(elem) =>
    51       case Some(elem) => next(elem)
    48         if (!contains(elem)) throw new Linear_Set.Undefined(elem)
       
    49         next(elem)
       
    50     }
    52     }
    51 
    53 
    52   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
    54   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
    53     if (contains(elem)) throw new Linear_Set.Duplicate(elem)
    55     if (contains(elem)) throw new Linear_Set.Duplicate(elem)
    54     else
    56     else
   136   def iterator(elem: A): Iterator[A] =
   138   def iterator(elem: A): Iterator[A] =
   137     if (contains(elem)) make_iterator(Some(elem))
   139     if (contains(elem)) make_iterator(Some(elem))
   138     else throw new Linear_Set.Undefined(elem)
   140     else throw new Linear_Set.Undefined(elem)
   139 
   141 
   140   def iterator(from: A, to: A): Iterator[A] =
   142   def iterator(from: A, to: A): Iterator[A] =
   141     if (!contains(to)) throw new Linear_Set.Undefined(to)
   143     if (contains(to))
   142     else
       
   143       nexts.get(to) match {
   144       nexts.get(to) match {
   144         case None => iterator(from)
   145         case None => iterator(from)
   145         case Some(stop) => iterator(from).takeWhile(_ != stop)
   146         case Some(stop) => iterator(from).takeWhile(_ != stop)
   146       }
   147       }
       
   148     else throw new Linear_Set.Undefined(to)
   147 
   149 
   148   def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
   150   def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
   149 
   151 
   150   override def last: A = reverse.head
   152   override def last: A = reverse.head
   151 
   153 
   152   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
   154   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
   153 
   155 
   154   def - (elem: A): Linear_Set[A] =
   156   def - (elem: A): Linear_Set[A] = delete_after(prev(elem))
   155     if (!contains(elem)) throw new Linear_Set.Undefined(elem)
       
   156     else delete_after(prev(elem))
       
   157 }
   157 }