Quelle update.scala Sprache: Scala

/*  Title:      Pure/update.scala
    Author:     Makarius

Update data (with formal name).
*/

package isabelle

object Update {
  sealed abstract class Op[A]
  case class Delete[A](name: String) extends Op[A]
  case class Insert[A](item: A) extends Op[A]

  def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] =
    updates.foldLeft(old_data) {
      case (map, Delete(name)) => map - name
      case (map, Insert(item)) => map + (item.name -> item)
    }

  val empty: Update = Update()

  def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update =
    if (a eq b) empty
    else {
      val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x)
      val insert = List.from(for ((x, y) <- b.iterator if !a.get(x).contains(y)) yield x)
      Update(delete = delete, insert = insert, kind = kind)
    }
}

sealed case class Update(
  delete: List[String] = Nil,
  insert: List[String] = Nil,
  kind: Int = 0
) {
  def deletes: Boolean = delete.nonEmpty
  def inserts: Boolean = insert.nonEmpty
  def defined: Boolean = deletes || inserts
  lazy val domain: Set[String] = delete.toSet ++ insert
}

quality83%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.