1/*  Title:      Pure/General/linear_set.scala
2    Author:     Makarius
3    Author:     Fabian Immler, TU Munich
4
5Sets with canonical linear order, or immutable linked-lists.
6*/
7
8package isabelle
9
10
11import scala.collection.SetLike
12import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
13import scala.collection.mutable.{Builder, SetBuilder}
14import scala.language.higherKinds
15
16
17object 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
31final 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}
160