diff --git a/tools/metadata.scala b/tools/metadata.scala --- a/tools/metadata.scala +++ b/tools/metadata.scala @@ -1,259 +1,248 @@ package afp import isabelle._ import afp.TOML._ import java.time.LocalDate object Metadata { sealed abstract class Affiliation(val author: Author.ID) case class Unaffiliated(override val author: Author.ID) extends Affiliation(author) case class Email(override val author: Author.ID, id: Email.ID, address: String) extends Affiliation(author) object Email { type ID = Int } case class Homepage(override val author: Author.ID, id: Homepage.ID, url: String) extends Affiliation(author) object Homepage { type ID = Int } case class Author( id: Author.ID, name: String, emails: List[Email], homepages: List[Homepage] ) object Author { type ID = String } case class Topic(id: Topic.ID, name: String, sub_topics: List[Topic]) object Topic { type ID = String } type Date = LocalDate object Isabelle { type Version = String } case class Release(entry: Entry.Name, date: Date, isabelle: Isabelle.Version) type License = String type Change_History = Map[Date, String] type Extra = Map[String, String] case class Entry( short_name: Entry.Name, title: String, authors: List[Affiliation], date: Date, topics: List[Topic], `abstract`: String, notifies: List[Email], contributors: List[Affiliation], license: License, note: String, change_history: Change_History, extra: Extra, releases: List[Release]) object Entry { type Name = String } /* toml */ object TOML { private def by_id[A](elems: List[A], id: Int): A = - elems.applyOrElse(id, error("Elem " + id + " not found in " + quote(elems.mkString(",")))) + elems.lift(id).getOrElse(error("Elem " + id + " not found in " + commas_quote(elems.map(_.toString)))) private def by_id[A](elems: Map[String, A], id: String): A = - elems.getOrElse(id, error("Elem " + id + " not found in " + quote(elems.mkString(",")))) + elems.getOrElse(id, error("Elem " + quote(id) + " not found in " + commas_quote(elems.map(_.toString)))) /* author */ def from_authors(authors: List[Author]): T = { def from_author(author: Author): T = afp.TOML.T( "name" -> author.name, "emails" -> author.emails.map(_.address), "homepages" -> author.homepages.map(_.url)) afp.TOML.T(authors.map(author => author.id -> from_author(author))) } def to_authors(authors: T): List[Author] = { def to_author(id: Author.ID, author: T): Author = { val emails = get_as[List[String]](author, "emails").zipWithIndex.map { case (address, idx) => Email(author = id, id = idx, address = address) } val homepages = get_as[List[String]](author, "homepages").zipWithIndex.map { case (url, idx) => Homepage(author = id, id = idx, url = url) } Author( id = id, name = get_as[String](author, "name"), emails = emails, homepages = homepages ) } split_as[T](authors).map { case (id, author) => to_author(id, author) } } /* topics */ def from_topics(root_topics: List[Topic]): T = afp.TOML.T(root_topics.map(t => t.name -> from_topics(t.sub_topics))) def to_topics(root_topics: T): List[Topic] = { def to_topics_rec(topics: T, root: Topic.ID): List[Topic] = split_as[T](topics).map { case (name, sub_topics) => - val id = root + "/" + name + val id = (if (root.nonEmpty) root + "/" else "") + name Topic(id, name, to_topics_rec(sub_topics, id)) } to_topics_rec(root_topics, "") } /* releases */ def from_releases(releases: List[Release]): T = Utils.group_sorted(releases, (r: Release) => r.entry).view.mapValues { entry_releases => entry_releases.map(r => r.isabelle -> r.date).toMap }.toMap def to_releases(map: T): List[Release] = split_as[T](map).flatMap { case (entry, releases) => split_as[Date](releases).map { case (version, date) => Release(entry = entry, date = date, isabelle = version) } } /* affiliation */ def from_affiliations(affiliations: List[Affiliation]): T = - { - def from_affiliation(affiliation: Affiliation): T = - { - affiliation match { - case Unaffiliated(_) => afp.TOML.T() - case Email(_, id, _) => afp.TOML.T("email" -> id) - case Homepage(_, id, _) => afp.TOML.T("homepage" -> id) - } - } - - Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues { author_affiliations => - Map("affiliations" -> author_affiliations.map(from_affiliation).filter(_.nonEmpty)) - }.toMap - } + Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues(_.collect { + case Email(_, id, _) => "email" -> id + case Homepage(_, id, _) => "homepage" -> id + }.toMap).toMap def to_affiliations(affiliations: T, authors: Map[Author.ID, Author]): List[Affiliation] = { def to_affiliation(affiliation: (String, Int), author: Author): Affiliation = { affiliation match { case ("email", id: Int) => by_id(author.emails, id) case ("homepage", id: Int) => by_id(author.homepages, id) case e => error("Unknown affiliation type: " + e) } } split_as[T](affiliations).flatMap { case (id, author_affiliations) => val author = by_id(authors, id) - val m = get_as[Map[String, Int]](author_affiliations, "affiliations") - if (m.isEmpty) List(Unaffiliated(author.id)) - else m.toList.map(to_affiliation(_, author)) + if (author_affiliations.isEmpty) List(Unaffiliated(author.id)) + else split_as[Int](author_affiliations).map(to_affiliation(_, author)) } } def from_emails(emails: List[Email]): T = afp.TOML.T(emails.map(email => email.author -> email.id)) def to_emails(emails: T, authors: Map[Author.ID, Author]): List[Email] = emails.toList.map { case (author, id: Int) => by_id(by_id(authors, author).emails, id) case e => error("Unknown email: " + quote(e.toString)) } /* history */ def from_change_history(change_history: Change_History): T = change_history.map { case (date, str) => date.toString -> str } def to_change_history(change_history: T): Change_History = change_history.map { case (date, entry: String) => LocalDate.parse(date) -> entry case e => error("Unknown history entry: " + quote(e.toString)) } /* entry */ def from_entry(entry: Entry): T = afp.TOML.T( "title" -> entry.title, "authors" -> from_affiliations(entry.authors), "contributors" -> from_affiliations(entry.contributors), "date" -> entry.date, "topics" -> entry.topics.map(_.id), "abstract" -> entry.`abstract`, "notify" -> from_emails(entry.notifies), "license" -> entry.license, "note" -> entry.note, "history" -> from_change_history(entry.change_history), "extra" -> entry.extra, ) def to_entry(entry: T, authors: Map[Author.ID, Author], topics: Map[Topic.ID, Topic], releases: List[Release]): Entry = Entry( - short_name = get_as(entry, "short_name"), - title = get_as(entry, "title"), - authors = to_affiliations(get_as(entry, "authors"), authors), - date = get_as(entry, "date"), + short_name = get_as[String](entry, "short_name"), + title = get_as[String](entry, "title"), + authors = to_affiliations(get_as[T](entry, "authors"), authors), + date = get_as[Date](entry, "date"), topics = get_as[List[String]](entry, "topics").map(by_id(topics, _)), - `abstract` = get_as(entry, "abstract"), - notifies = to_emails(get_as(entry, "notify"), authors), - contributors = to_affiliations(get_as(entry, "contributors"), authors), - license = get_as(entry, "license"), - note = get_as(entry, "note"), - change_history = to_change_history(get_as(entry, "history")), - extra = get_as(entry, "extra"), + `abstract` = get_as[String](entry, "abstract"), + notifies = to_emails(get_as[T](entry, "notify"), authors), + contributors = to_affiliations(get_as[T](entry, "contributors"), authors), + license = get_as[License](entry, "license"), + note = get_as[String](entry, "note"), + change_history = to_change_history(get_as[T](entry, "history")), + extra = get_as[Extra](entry, "extra"), releases = releases) } } diff --git a/tools/toml.scala b/tools/toml.scala --- a/tools/toml.scala +++ b/tools/toml.scala @@ -1,461 +1,406 @@ package afp import isabelle._ import scala.collection.immutable.ListMap import scala.reflect.{ClassTag, classTag} +import scala.util.Try import scala.util.matching.Regex import scala.util.parsing.combinator.Parsers import scala.util.parsing.combinator.lexical.Scanners import scala.util.parsing.input.CharArrayReader.EofCh import java.time.{LocalDate, LocalDateTime, LocalTime, OffsetDateTime} object TOML { type Key = String type V = Any type T = Map[Key, V] object T { def apply(entries: (Key, V)*): T = ListMap(entries: _*) def apply(entries: List[(Key, V)]): T = ListMap(entries: _*) def unapply(t: Map[_, V]): Option[T] = { if (t.keys.forall(_.isInstanceOf[Key])) Some(t.asInstanceOf[T]) else None } } /* typed access */ def split_as[A: ClassTag](map: T): List[(Key, A)] = map.keys.toList.map(k => k -> get_as[A](map, k)) def get_as[A: ClassTag](map: T, name: String): A = map.get(name) match { case Some(value: A) => value case Some(value) => error("Value " + quote(value.toString) + " not of type " + classTag[A].runtimeClass.getName) case None => error("Field " + name + " not in " + map) } /* lexer */ object Kind extends Enumeration { - val KEYWORD, IDENT, STRING, INTEGER, FLOAT, DATE, ERROR = Value + val KEYWORD, IDENT, STRING, COMMENT, ERROR = Value } sealed case class Token(kind: Kind.Value, text: String) { def is_ident: Boolean = kind == Kind.IDENT - def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name - def is_string: Boolean = kind == Kind.STRING - - def is_integer: Boolean = kind == Kind.INTEGER - - def is_float: Boolean = kind == Kind.FLOAT - - def is_date: Boolean = kind == Kind.DATE - def is_error: Boolean = kind == Kind.ERROR } object Lexer extends Scanners with Scan.Parsers { override type Elem = Char type Token = TOML.Token def errorToken(msg: String): Token = Token(Kind.ERROR, msg) val white_space: String = " \t\n\r" override val whiteSpace: Regex = ("[" + white_space + "]+").r - def whitespace: Parser[Any] = many(character(white_space.contains(_))) - - val letter: Parser[String] = one(character(Symbol.is_ascii_letter)) - val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter)) - - def digits: Parser[String] = many(character(Symbol.is_ascii_digit)) - - def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit)) - - def digitsn(n: Int): Parser[String] = repeated(character(Symbol.is_ascii_digit), n, n) + override def whitespace: Parser[Any] = many(character(white_space.contains(_))) - def chars(chars: String, num: Int = 1, rep_min: Int = 1, rep_max: Int = 1): Parser[String] = - { - chars.toList match { - case Nil => error("No chars given") - case c :: Nil => repeated(character(_ == c), num * rep_min, num * rep_max) - case _ => repeated(character(chars.contains(_)), num * rep_min, num * rep_max) - } - } + override def comment: Parser[String] = + '#' ~>! rep(elem("", c => c != EofCh && c != '\n')) ~ elem("", c => c == EofCh || c == '\n') ^^ + { case s ~ t => s.mkString + t } - - /* keyword */ - - def keyword: Parser[Token] = - ("true" | "false" | "[[" | "]]" | chars("{}[],=.")) ^^ (s => Token(Kind.KEYWORD, s)) - - - /* identifier */ + def keyword: Parser[Token] = ("[[" | "]]" | one(character("{}[],=.".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) def ident: Parser[Token] = - letters1 ^^ (s => Token(Kind.IDENT, s)) - - - /* string */ + many1(character(c => Symbol.is_ascii_digit(c) || Symbol.is_ascii_letter(c) || c == '_' || c == '-')) ^^ + (s => Token(Kind.IDENT, s)) def basic_string: Parser[Token] = '\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) def multiline_basic_string: Parser[Token] = "\"\"\"" ~>! - rep(multiline_string_body | chars("\"", rep_max = 2) ~ multiline_string_body) <~ + rep(multiline_string_body | ("\"" | "\"\"") ~ multiline_string_body) <~ "\"\"\"" ^^ (cs => Token(Kind.STRING, cs.mkString.stripPrefix("\n"))) def multiline_string_body: Parser[Char] = elem("", c => c == '\t' || c == '\n' || c == '\r' || (c > '\u001f' && c != '\"' && c != '\\' && c != EofCh)) | '\\' ~> string_escape def string_body: Parser[Char] = elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape def string_escape: Parser[Char] = elem("", "\"\\/".contains(_)) | elem("", "bfnrt".contains(_)) ^^ { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ (s => Integer.parseInt(s, 16).toChar) def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") - - /* numbers */ - - def integer: Parser[Token] = ("0" ~> letter) ^^ (c => errorToken("Unsupported number format: " + quote(c))) | - integer_body ^^ (i => Token(Kind.INTEGER, i)) - - def integer_body: Parser[String] = zero | opt("-" | "+") ~ nonzero ~ digits ^^ - { case a ~ b ~ c => a.getOrElse("") + b + c } - - def zero: Parser[String] = one(character(c => c == '0')) - - def nonzero: Parser[String] = one(character(c => c != '0' && Symbol.is_ascii_digit(c))) - - def float: Parser[Token] = integer_body ~ opt(number_fract) ~ opt(number_exp) ^^ - { case a ~ b ~ c => Token(Kind.FLOAT, a + b.getOrElse("") + c.getOrElse("")) } - - def number_fract: Parser[String] = "." ~ digits1 ^^ { case a ~ b => a + b } - - def number_exp: Parser[String] = - one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^ - { case a ~ b ~ c => a + b + c } - - - /* date and time (simplified) */ - - def local_date: Parser[Token] = - (digitsn(4) <~ '-') ~ (digitsn(2) <~ '-') ~ digitsn(2) ^^ - { case year ~ month ~ day => Token(Kind.DATE, year + "-" + month + "-" + day) } - - - /* token */ - def token: Parser[Token] = - keyword | ident | local_date | (multiline_basic_string | basic_string | - (string_failure | (integer | float | failure("Illegal character")))) + keyword | ident | (multiline_basic_string | basic_string | string_failure) | failure("Illegal character") } /* parser */ trait Parser extends Parsers { type Elem = Token + def keys: Parser[List[Key]] = rep1sep(key, $$$(".")) + + def string: Parser[String] = elem("string", _.is_string) ^^ (_.text) + + def integer: Parser[Int] = token("integer", _.is_ident, _.toInt) + + def float: Parser[Double] = token("float", _.is_ident, _.toDouble) + + def boolean: Parser[Boolean] = token("boolean", _.is_ident, _.toBoolean) + + def offset_date_time: Parser[OffsetDateTime] = token("offset date-time", _.is_ident, OffsetDateTime.parse) + + def local_date_time: Parser[LocalDateTime] = token("local date-time", _.is_ident, LocalDateTime.parse) + + def local_date: Parser[LocalDate] = token("local date", _.is_ident, LocalDate.parse) + + def local_time: Parser[LocalTime] = token("local time", _.is_ident, LocalTime.parse) + + def array: Parser[V] = $$$("[") ~>! rep(toml_value <~ $$$(",")) <~ $$$("]") + + def table: Parser[T] = $$$("[") ~>! (keys <~ $$$("]")) ~! content ^^ + { case base ~ T(map) => to_map(List(base -> map)) } + + def inline_table: Parser[V] = $$$("{") ~>! (content ^? to_map) <~ $$$("}") + + def array_of_tables: Parser[T] = + $$$("[[") ~>! (keys <~ $$$("]]")) >> { ks => + repsep(content ^^ to_map, $$$("[[") ~! (keys ^? { case ks1 if ks1 == ks => }) ~ $$$("]]")) ^^ + { list => List(ks -> list) } ^? to_map + } + + def toml: Parser[T] = (content ~ rep(table | array_of_tables)) ^? + { case T(map) ~ maps => map :: maps } ^? { case Merge(map) => map } + + + /* auxiliary parsers */ + + private def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name)) + + private def token[A](name: String, p: Token => Boolean, parser: String => A): Parser[A] = + elem(name, p) ^^ (tok => Try { parser(tok.text) }) ^? { case util.Success(v) => v } + + private def key: Parser[Key] = elem("key", e => e.is_ident || e.is_string) ^^ (_.text) + + private def toml_value: Parser[V] = string | integer | float | offset_date_time | local_date_time | local_date | + local_time | array | inline_table + + private def content: Parser[List[(List[Key], V)]] = rep((keys <~ $$$("=")) ~! toml_value ^^ + { case ks ~ v => ks -> v }) + + + /* extractors */ + private object T { def unapply(table: List[(List[Key], V)]): Option[T] = { val by_first_key = table.foldLeft(ListMap.empty[Key, List[(List[Key], V)]]) { case (map, (k :: ks, v)) => map.updatedWith(k) { case Some(value) => Some(value :+ (ks, v)) case None => Some(List((ks, v))) } case _ => return None } val res = by_first_key.map { case (k, (Nil, v) :: Nil) => k -> v case (k, T(map)) => k -> map case _ => return None } Some(res) } } private def to_map: PartialFunction[List[(List[Key], V)], T] = { case T(map) => map } - - def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name)) - - def ident: Parser[String] = elem("ident", _.is_ident) ^^ (_.text) - - def string: Parser[String] = elem("string", _.is_string) ^^ (_.text) - - def date: Parser[LocalDate] = elem("date", _.is_date) ^^ (tok => LocalDate.parse(tok.text)) - - def integer: Parser[Int] = elem("integer", _.is_integer) ^^ (tok => tok.text.toInt) - - def float: Parser[Double] = elem("float", _.is_float) ^^ (tok => tok.text.toDouble) - - def boolean: Parser[Boolean] = $$$("false") ^^^ false | $$$("true") ^^^ true - - def keys: Parser[List[Key]] = rep1sep(ident | string, $$$(".")) - - - /* inline values */ - - def inline_array: Parser[V] = $$$("[") ~>! rep(toml_value <~ $$$(",")) <~ $$$("]") - - def inline_table: Parser[V] = $$$("{") ~>! (content ^? to_map) <~ $$$("}") - - def toml_value: Parser[V] = date | integer | float | string | boolean | inline_array | inline_table - - /* non-inline arrays */ - - def toml_array: Parser[T] = - $$$("[[") ~>! (keys <~ $$$("]]")) >> { ks => - repsep(content ^^ to_map, $$$("[[") ~! (keys ^? { case ks1 if ks1 == ks => }) ~ $$$("]]")) ^^ - { list => List(ks -> list) } ^? to_map - } - - - /* tables */ - - private def content: Parser[List[(List[Key], V)]] = rep((keys <~ $$$("=")) ~! toml_value ^^ - { case ks ~ v => ks -> v }) - - def toml_table: Parser[T] = $$$("[") ~>! (keys <~ $$$("]")) ~! content ^^ - { case base ~ T(map) => to_map(List(base -> map)) } - object Merge { private def merge(map1: T, map2: T): Option[T] = { val res2 = map2.map { case (k2, v2) => map1.get(k2) match { case Some(v1) => (v1, v2) match { case (TOML.T(t1), TOML.T(t2)) => k2 -> merge(t1, t2).getOrElse(return None) case x => return None } case None => k2 -> v2 } } Some(map1.filter { case (k, _) => !map2.contains(k) } ++ res2) } def unapply(maps: List[T]): Option[T] = Some(maps.fold(Map.empty)(merge(_, _).getOrElse(return None))) } - def root_table: Parser[T] = (content ~ rep(toml_table | toml_array)) ^? - { case T(map) ~ maps => map :: maps } ^? { case Merge(map) => map } + /* parse */ def parse(input: CharSequence): T = { val scanner = new Lexer.Scanner(Scan.char_reader(input)) - phrase(root_table)(scanner) match { + phrase(toml)(scanner) match { case Success(toml, _) => toml case NoSuccess(_, next) => error("Malformed TOML input at " + next.pos) } } } object Parser extends Parser /* standard format */ def parse(s: String): T = Parser.parse(s) /* format to a subset of TOML */ object Format { def apply(toml: T): String = { val result = new StringBuilder /* keys */ def key(k: Key): Unit = { val Bare_Key = """[A-Za-z0-9_-]+""".r k match { case Bare_Key() => result ++= k case _ => result += '"' result ++= k result += '"' } } def keys(ks: List[Key]): Unit = Library.separate(None, ks.reverse.map(Some(_))).foreach { case None => result += '.' case Some(k) => key(k) } /* string */ def basic_string(s: String): Unit = { result += '"' result ++= s.iterator.map { case '\b' => "\\b" case '\t' => "\\t" case '\n' => "\\n" case '\f' => "\\f" case '\r' => "\\r" case '"' => "\\\"" case '\\' => "\\\\" case c => if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c }.mkString result += '"' } def multiline_basic_string(s: String): Unit = { result ++= "\"\"\"\n" result ++= s.iterator.map { case '\b' => "\\b" case '\t' => "\t" case '\n' => "\n" case '\f' => "\\f" case '\r' => "\r" case '"' => "\\\"" case '\\' => "\\\\" case c => if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c }.mkString.replace("\"\"\"", "\"\"\\\"") result ++= "\"\"\"" } /* integer, boolean, offset date-time, local date-time, local date, local time */ object To_String { def unapply(v: V): Option[String] = v match { case _: Int | _: Double | _: Boolean | _: OffsetDateTime | _: LocalDateTime | _: LocalDate | _: LocalTime => Some(v.toString) case _ => None } } /* inline: string, float, To_String, value array */ def inline(v: V, indent: Int = 0): Unit = { def indentation(i: Int): Unit = for (_ <- Range(0, i)) result ++= " " indentation(indent) v match { case s: String => if (s.contains("\n") && s.length > 20) multiline_basic_string(s) else basic_string(s) case To_String(s) => result ++= s case list: List[V] => if (list.isEmpty) { result ++= "[]" } else { result ++= "[\n" list.foreach { elem => inline(elem, indent + 1) result ++= ",\n" } indentation(indent) result += ']' } case _ => error("Not inline TOML value: " + v.toString) } } /* array */ def inline_values(path: List[Key], v: V): Unit = { v match { case T(map) => map.foreach { case (k, v1) => inline_values(k :: path, v1) } case _ => keys(path) result ++= " = " inline(v) result += '\n' } } def is_inline(elem: V): Boolean = elem match { case To_String(_) | _: Double | _: String => true case list: List[V] => list.forall(is_inline) case _ => false } def array(path: List[Key], list: List[V]): Unit = { if (list.forall(is_inline)) inline_values(path.take(1), list) else { list.collect { case T(map) => result ++= "\n[[" keys(path) result ++= "]]\n" table(path, map, is_table_entry = true) case _ => error("Array can only contain either all tables or all non-tables") } } } /* table */ def table(path: List[Key], map: T, is_table_entry: Boolean = false): Unit = { val (values, nodes) = map.toList.partition(kv => is_inline(kv._2)) if (!is_table_entry && path.nonEmpty) { result ++= "\n[" keys(path) result ++= "]\n" } values.foreach { case (k, v) => inline_values(List(k), v) } nodes.foreach { case (k, T(map1)) => table(k :: path, map1) case (k, list: List[V]) => array(k :: path, list) case (_, v) => error("Invalid TOML: " + v.toString) } } table(Nil, toml) result.toString } } } diff --git a/tools/utils.scala b/tools/utils.scala --- a/tools/utils.scala +++ b/tools/utils.scala @@ -1,17 +1,27 @@ package afp +import isabelle._ + import scala.collection.immutable.ListMap object Utils { def group_sorted[A, K](l: List[A], f: A => K): ListMap[K, List[A]] = l.foldRight(ListMap.empty[K, List[A]]) { case (a, m) => m.updatedWith(f(a)) { case Some(as) => Some(a :: as) case None => Some(List(a)) } } + + def grouped_sorted[A, K](l: List[A], f: A => K): ListMap[K, A] = + group_sorted(l, f).map { + case (k, v :: Nil) => k -> v + case (k, vs) => error("Not distinct for " + quote(k.toString) + ": " + commas_quote(vs.map(_.toString))) + } + + def the_entry[K, V](m: Map[K, V], k: K): V = m.getOrElse(k, error("Expected key " + quote(k.toString))) } \ No newline at end of file