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