src/Pure/General/multi_map.scala
author wenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073 dcecfcc56dce
parent 56744 0b74d1df4b8e
child 63579 73939a9b70a3
permissions -rw-r--r--
more merge operations;
wenzelm@52975
     1
/*  Title:      Pure/General/multi_map.scala
wenzelm@52975
     2
    Module:     PIDE
wenzelm@56744
     3
    Author:     Makarius
wenzelm@52975
     4
wenzelm@52975
     5
Maps with multiple entries per key.
wenzelm@52975
     6
*/
wenzelm@52975
     7
wenzelm@52975
     8
package isabelle
wenzelm@52975
     9
wenzelm@55618
    10
wenzelm@52975
    11
import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
wenzelm@52975
    12
wenzelm@52975
    13
wenzelm@52975
    14
object Multi_Map extends ImmutableMapFactory[Multi_Map]
wenzelm@52975
    15
{
wenzelm@52975
    16
  private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
wenzelm@52975
    17
  override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
wenzelm@52975
    18
wenzelm@52975
    19
  implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
wenzelm@52975
    20
    new MapCanBuildFrom[A, B]
wenzelm@52975
    21
}
wenzelm@52975
    22
wenzelm@52975
    23
wenzelm@59073
    24
final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
wenzelm@52975
    25
  extends scala.collection.immutable.Map[A, B]
wenzelm@52975
    26
  with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
wenzelm@52975
    27
{
wenzelm@52975
    28
  /* Multi_Map operations */
wenzelm@52975
    29
wenzelm@55488
    30
  def iterator_list: Iterator[(A, List[B])] = rep.iterator
wenzelm@55488
    31
wenzelm@52975
    32
  def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
wenzelm@52975
    33
wenzelm@52975
    34
  def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
wenzelm@52975
    35
  {
wenzelm@52975
    36
    val bs = get_list(a)
wenzelm@52975
    37
    if (bs.contains(b)) this
wenzelm@52975
    38
    else new Multi_Map(rep + (a -> (b :: bs)))
wenzelm@52975
    39
  }
wenzelm@52975
    40
wenzelm@52975
    41
  def remove[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
wenzelm@52975
    42
  {
wenzelm@52975
    43
    val bs = get_list(a)
wenzelm@52975
    44
    if (bs.contains(b)) {
wenzelm@52975
    45
      bs.filterNot(_ == b) match {
wenzelm@52975
    46
        case Nil => new Multi_Map(rep - a)
wenzelm@52975
    47
        case bs1 => new Multi_Map(rep + (a -> bs1))
wenzelm@52975
    48
      }
wenzelm@52975
    49
    }
wenzelm@52975
    50
    else this
wenzelm@52975
    51
  }
wenzelm@52975
    52
wenzelm@59073
    53
  def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] =
wenzelm@59073
    54
    if (this eq other) this
wenzelm@59073
    55
    else if (isEmpty) other
wenzelm@59073
    56
    else
wenzelm@59073
    57
      (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
wenzelm@59073
    58
        case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
wenzelm@59073
    59
      }
wenzelm@59073
    60
wenzelm@52975
    61
wenzelm@52975
    62
  /* Map operations */
wenzelm@52975
    63
wenzelm@52975
    64
  override def stringPrefix = "Multi_Map"
wenzelm@52975
    65
wenzelm@52975
    66
  override def empty = Multi_Map.empty
wenzelm@52975
    67
  override def isEmpty: Boolean = rep.isEmpty
wenzelm@52975
    68
wenzelm@52975
    69
  override def keySet: Set[A] = rep.keySet
wenzelm@52975
    70
wenzelm@52975
    71
  override def iterator: Iterator[(A, B)] =
wenzelm@52975
    72
    for ((a, bs) <- rep.iterator; b <- bs.iterator) yield (a, b)
wenzelm@52975
    73
wenzelm@52975
    74
  def get(a: A): Option[B] = get_list(a).headOption
wenzelm@52975
    75
wenzelm@52975
    76
  def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
wenzelm@52975
    77
wenzelm@52975
    78
  def - (a: A): Multi_Map[A, B] =
wenzelm@52975
    79
    if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
wenzelm@52975
    80
}