src/Pure/General/linear_set.scala
author wenzelm
Tue Apr 04 18:43:58 2017 +0200 (2017-04-04 ago)
changeset 65374 ce09e947c1d5
parent 64370 865b39487b5d
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/General/linear_set.scala
     2     Author:     Makarius
     3     Author:     Fabian Immler, TU Munich
     4 
     5 Sets with canonical linear order, or immutable linked-lists.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.SetLike
    12 import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
    13 import scala.collection.mutable.{Builder, SetBuilder}
    14 import scala.language.higherKinds
    15 
    16 
    17 object Linear_Set extends SetFactory[Linear_Set]
    18 {
    19   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
    20   override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
    21 
    22   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
    23   def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
    24 
    25   class Duplicate[A](x: A) extends Exception
    26   class Undefined[A](x: A) extends Exception
    27   class Next_Undefined[A](x: Option[A]) extends Exception
    28 }
    29 
    30 
    31 final class Linear_Set[A] private(
    32     start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    33   extends scala.collection.immutable.Set[A]
    34   with GenericSetTemplate[A, Linear_Set]
    35   with SetLike[A, Linear_Set[A]]
    36 {
    37   override def companion: GenericCompanion[Linear_Set] = Linear_Set
    38 
    39 
    40   /* relative addressing */
    41 
    42   def next(elem: A): Option[A] =
    43     if (contains(elem)) nexts.get(elem)
    44     else throw new Linear_Set.Undefined(elem)
    45 
    46   def prev(elem: A): Option[A] =
    47     if (contains(elem)) prevs.get(elem)
    48     else throw new Linear_Set.Undefined(elem)
    49 
    50   def get_after(hook: Option[A]): Option[A] =
    51     hook match {
    52       case None => start
    53       case Some(elem) => next(elem)
    54     }
    55 
    56   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
    57     if (contains(elem)) throw new Linear_Set.Duplicate(elem)
    58     else
    59       hook match {
    60         case None =>
    61           start match {
    62             case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map())
    63             case Some(elem1) =>
    64               new Linear_Set[A](Some(elem), end,
    65                 nexts + (elem -> elem1), prevs + (elem1 -> elem))
    66           }
    67         case Some(elem1) =>
    68           if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
    69           else
    70             nexts.get(elem1) match {
    71               case None =>
    72                 new Linear_Set[A](start, Some(elem),
    73                   nexts + (elem1 -> elem), prevs + (elem -> elem1))
    74               case Some(elem2) =>
    75                 new Linear_Set[A](start, end,
    76                   nexts + (elem1 -> elem) + (elem -> elem2),
    77                   prevs + (elem2 -> elem) + (elem -> elem1))
    78             }
    79       }
    80 
    81   def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] =  // FIXME reverse fold
    82     ((hook, this) /: elems) {
    83       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
    84     }._2
    85 
    86   def delete_after(hook: Option[A]): Linear_Set[A] =
    87     hook match {
    88       case None =>
    89         start match {
    90           case None => throw new Linear_Set.Next_Undefined[A](None)
    91           case Some(elem1) =>
    92             nexts.get(elem1) match {
    93               case None => empty
    94               case Some(elem2) =>
    95                 new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
    96             }
    97         }
    98       case Some(elem1) =>
    99         if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
   100         else
   101           nexts.get(elem1) match {
   102             case None => throw new Linear_Set.Next_Undefined(Some(elem1))
   103             case Some(elem2) =>
   104               nexts.get(elem2) match {
   105                 case None =>
   106                   new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
   107                 case Some(elem3) =>
   108                   new Linear_Set[A](start, end,
   109                     nexts - elem2 + (elem1 -> elem3),
   110                     prevs - elem2 + (elem3 -> elem1))
   111               }
   112           }
   113     }
   114 
   115 
   116   /* Set methods */
   117 
   118   override def stringPrefix = "Linear_Set"
   119 
   120   override def isEmpty: Boolean = !start.isDefined
   121   override def size: Int = if (isEmpty) 0 else nexts.size + 1
   122 
   123   def contains(elem: A): Boolean =
   124     nonEmpty && (end.get == elem || nexts.isDefinedAt(elem))
   125 
   126   private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
   127     private var next_elem = from
   128     def hasNext(): Boolean = next_elem.isDefined
   129     def next(): A =
   130       next_elem match {
   131         case Some(elem) =>
   132           next_elem = nexts.get(elem)
   133           elem
   134         case None => Iterator.empty.next()
   135       }
   136   }
   137 
   138   override def iterator: Iterator[A] = make_iterator(start)
   139 
   140   def iterator(elem: A): Iterator[A] =
   141     if (contains(elem)) make_iterator(Some(elem))
   142     else throw new Linear_Set.Undefined(elem)
   143 
   144   def iterator(from: A, to: A): Iterator[A] =
   145     if (contains(to))
   146       nexts.get(to) match {
   147         case None => iterator(from)
   148         case Some(stop) => iterator(from).takeWhile(_ != stop)
   149       }
   150     else throw new Linear_Set.Undefined(to)
   151 
   152   def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
   153 
   154   override def last: A = reverse.head
   155 
   156   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
   157 
   158   def - (elem: A): Linear_Set[A] = delete_after(prev(elem))
   159 }