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