src/Pure/update.scala
author wenzelm
Thu, 06 Jun 2024 22:26:40 +0200
changeset 80274 cff00b3dddf5
permissions -rw-r--r--
clarified names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
80274
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/update.scala
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     3
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     4
Update data (with formal name).
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     5
*/
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     6
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     7
package isabelle
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     8
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
     9
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    10
object Update {
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    11
  sealed abstract class Op[A]
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    12
  case class Delete[A](name: String) extends Op[A]
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    13
  case class Insert[A](item: A) extends Op[A]
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    14
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    15
  def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] =
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    16
    updates.foldLeft(old_data) {
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    17
      case (map, Delete(name)) => map - name
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    18
      case (map, Insert(item)) => map + (item.name -> item)
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    19
    }
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    20
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    21
  val empty: Update = Update()
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    22
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    23
  def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update =
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    24
    if (a eq b) empty
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    25
    else {
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    26
      val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x)
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    27
      val insert = List.from(for ((x, y) <- b.iterator if !a.get(x).contains(y)) yield x)
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    28
      Update(delete = delete, insert = insert, kind = kind)
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    29
    }
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    30
}
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    31
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    32
sealed case class Update(
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    33
  delete: List[String] = Nil,
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    34
  insert: List[String] = Nil,
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    35
  kind: Int = 0
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    36
) {
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    37
  def deletes: Boolean = delete.nonEmpty
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    38
  def inserts: Boolean = insert.nonEmpty
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    39
  def defined: Boolean = deletes || inserts
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    40
  lazy val domain: Set[String] = delete.toSet ++ insert
cff00b3dddf5 clarified names;
wenzelm
parents:
diff changeset
    41
}