src/Pure/General/toml.scala

unify error messages;

/*  Title:      Pure/General/toml.scala
    Author:     Fabian Huch, TU Muenchen

Support for TOML: https://toml.io/en/v1.0.0
*/

package isabelle


import TOML.Parse_Context.Seen

import java.lang.Long.parseLong
import java.lang.{String => Str}
import java.time.{LocalDate, LocalDateTime, LocalTime, OffsetDateTime}

import scala.{Boolean => Bool}
import scala.collection.immutable.ListMap
import scala.reflect.{ClassTag, classTag}
import scala.util.Try
import scala.util.matching.Regex
import scala.util.parsing.combinator
import scala.util.parsing.combinator.lexical.Scanners
import scala.util.parsing.input
import scala.util.parsing.input.Positional
import scala.util.parsing.input.CharArrayReader.EofCh


object TOML {
  /* typed representation and access */

  type Key = Str

  sealed trait T
  case class String(rep: Str) extends T
  case class Integer(rep: Long) extends T
  case class Float(rep: Double) extends T
  case class Boolean(rep: Bool) extends T
  case class Offset_Date_Time(rep: OffsetDateTime) extends T
  case class Local_Date_Time(rep: LocalDateTime) extends T
  case class Local_Date(rep: LocalDate) extends T
  case class Local_Time(rep: LocalTime) extends T

  object Scalar {
    def unapply(t: T): Option[Str] =
      t match {
        case s: String => Some(s.rep)
        case i: Integer => Some(i.rep.toString)
        case f: Float => Some(f.rep.toString)
        case b: Boolean => Some(b.rep.toString)
        case o: Offset_Date_Time => Some(o.rep.toString)
        case l: Local_Date_Time => Some(l.rep.toString)
        case l: Local_Date => Some(l.rep.toString)
        case l: Local_Time => Some(l.rep.toString)
        case _ => None
      }
  }

  class Array private(private val rep: List[T]) extends T {
    override def hashCode(): Int = rep.hashCode()
    override def equals(that: Any): Bool = that match {
      case other: Array => rep == other.rep
      case _ => false
    }
    override def toString: Str = "Array(" + length.toString + ")"

    class Values[A](pf: PartialFunction[T, A]) { def values: List[A] = rep.collect(pf).reverse }
    lazy val string = new Values({ case s: String => s })
    lazy val integer = new Values({ case i: Integer => i })
    lazy val float = new Values({ case f: Float => f })
    lazy val boolean = new Values({ case b: Boolean => b })
    lazy val offset_date_time = new Values({ case o: Offset_Date_Time => o })
    lazy val local_date_time = new Values({ case l: Local_Date_Time => l })
    lazy val local_date = new Values({ case l: Local_Date => l })
    lazy val local_time = new Values({ case l: Local_Time => l })
    lazy val array = new Values({ case a: Array => a })
    lazy val table = new Values({ case t: Table => t })
    lazy val any = new Values({ case t => t })

    def +(elem: T): Array = new Array(elem :: rep)
    def ++(other: Array): Array = new Array(other.rep ::: rep)
    def length: Int = rep.length
    def is_empty: Bool = rep.isEmpty
  }

  object Array {
    def apply(elems: Iterable[T]): Array = new Array(elems.toList.reverse)
    def apply(elems: T*): Array = Array(elems)
    val empty: Array = apply()
  }

  class Table private(private val rep: Map[Key, T]) extends T {
    override def hashCode(): Int = rep.hashCode()
    override def equals(that: Any): Bool =
      that match {
        case other: Table => rep == other.rep
        case _ => false
      }
    override def toString: Str =
      rep.map {
        case (k, t: Table) => k + "(" + t.domain.size + ")"
        case (k, a: Array) => k + "(" + a.length + ")"
        case (k, _) => k
      }.mkString("Table(", ", ", ")")

    class Value[A: ClassTag](pf: PartialFunction[T, A]) {
      def values: List[(Key, A)] =
        rep.toList.collect { case (k, v) if pf.isDefinedAt(v) => k -> pf(v) }
      def get(k: Key): Option[A] = rep.get(k).flatMap(v => PartialFunction.condOpt(v)(pf))
      def apply(k: Key): A =
        rep.get(k) match {
          case Some(v) => PartialFunction.condOpt(v)(pf) match {
            case Some(value) => value
            case None =>
              error("Expected" + classTag[A].runtimeClass.getName +
                ", got " + v.getClass.getSimpleName + " for key " + Format.key(k))
          }
          case None => error("Key " + Format.key(k) + " does not exist")
        }
    }

    lazy val string = new Value({ case s: String => s })
    lazy val integer = new Value({ case i: Integer => i })
    lazy val float = new Value({ case f: Float => f })
    lazy val boolean = new Value({ case b: Boolean => b })
    lazy val offset_date_time = new Value({ case o: Offset_Date_Time => o })
    lazy val local_date_time = new Value({ case l: Local_Date_Time => l })
    lazy val local_date = new Value({ case l: Local_Date => l })
    lazy val local_time = new Value({ case l: Local_Time => l })
    lazy val array = new Value({ case a: Array => a })
    lazy val table = new Value({ case t: Table => t })
    lazy val any = new Value({ case t => t })

    def +(elem: (Key, T)): Table = {
      val (k, v) = elem
      val v1 = rep.get(k) match {
        case None => v
        case Some(v0) =>
          (v0, v) match {
            case (t0: Table, t: Table) => t0 ++ t
            case (a0: Array, a: Array) => a0 ++ a
            case _ => v
          }
      }
      new Table(rep + (k -> v1))
    }
    def -(k: Key): Table = new Table(rep - k)
    def ++(other: Table): Table =  other.rep.foldLeft(this)(_ + _)
    def domain: Set[Key] = rep.keySet
    def is_empty: Bool = rep.isEmpty
  }

  object Table {
    def apply(elems: Iterable[(Key, T)]): Table = elems.foldLeft(new Table(ListMap.empty))(_ + _)
    def apply(elems: (Key, T)*): Table = Table(elems)
    val empty: Table = apply()
  }


  /* lexer */

  enum Kind { case KEYWORD, VALUE, STRING, MULTILINE_STRING, LINE_SEP, ERROR }

  sealed case class Token(kind: Kind, text: Str) extends Positional {
    def is_keyword(name: Str): Bool = kind == Kind.KEYWORD && text == name
    def is_value: Bool = kind == Kind.VALUE
    def is_string: Bool = kind == Kind.STRING
    def is_multiline_string: Bool = kind == Kind.MULTILINE_STRING
    def is_line_sep: Bool = kind == Kind.LINE_SEP
  }

  object Lexer extends Scanners with Scan.Parsers {
    override type Elem = Char
    type Token = TOML.Token

    def errorToken(msg: Str): Token = Token(Kind.ERROR, msg)

    val white_space: Str = " \t"
    override val whiteSpace: Regex = ("[" + white_space + "]+").r
    override def whitespace: Parser[Any] = rep(comment | many1(character(white_space.contains(_))))

    def line_sep: Parser[Str] = rep1("\n" | s"\r\n" | EofCh) ^^ (cs => cs.mkString)
    def line_sep_token: Parser[Token] = line_sep ^^ (s => Token(Kind.LINE_SEP, s))

    def is_control(e: Elem): Bool =
      e <= '\u0008' || ('\u000A' <= e && e <= '\u001F') || e == '\u007F'

    override def comment: Parser[Str] = '#' ~>! many(character(c => !is_control(c)))

    def keyword: Parser[Token] = one(character("{}[],=.".contains)) ^^ (s => Token(Kind.KEYWORD, s))

    def is_value(c: Elem): Bool =
      Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || "_-:+".contains(c)
    def value: Parser[Token] =
      many1(character(is_value)) ~
        opt(' ' ~ many1(character(is_value)) ^^ { case ws ~ s => ws.toString + s }) ~
        opt('.' ~ many1(character(is_value)) ^^ { case dot ~ s => dot.toString + s}) ^^
        { case s ~ ss ~ sd => Token(Kind.VALUE, s + ss.getOrElse("") + sd.getOrElse("")) }

    def string: Parser[Token] =
      multiline_basic_string | basic_string | multiline_literal_string | literal_string

    private def trim(s: Str): Str =
      if (s.startsWith("\n")) s.stripPrefix("\n") else s.stripPrefix("\r\n")

    def basic_string: Parser[Token] =
      '"' ~> rep(basic_string_elem) <~ '"' ^^ (cs => Token(Kind.STRING, cs.mkString))

    def multiline_basic_string: Parser[Token] =
      "\"\"\"" ~>
        rep(multiline_basic_string_elem |
          ("\"\"" | "\"") ~ multiline_basic_string_elem ^^ { case s ~ t => s + t }) ~
        repeated(character(_ == '"'), 3, 5) ^^ { case cs ~ q =>
          Token(Kind.MULTILINE_STRING, trim(cs.mkString + q.drop(3))) }

    private def multiline_basic_string_elem: Parser[Str] =
      ('\\' ~ line_sep ~ rep(many1(character(white_space.contains)) | line_sep)) ^^ (_ => "") |
        basic_string_elem ^^ (_.toString) | line_sep

    def literal_string: Parser[Token] =
      '\'' ~> rep(literal_string_elem) <~ '\'' ^^ (cs => Token(Kind.STRING, cs.mkString))

    def multiline_literal_string: Parser[Token] =
      "'''" ~>
        rep(multiline_literal_string_elem |
          ("''" | "'") ~ multiline_literal_string_elem ^^ { case s ~ t => s + t }) ~
        repeated(character(_ == '\''), 3, 5) ^^ { case cs ~ q =>
          Token(Kind.MULTILINE_STRING, trim(cs.mkString + q.drop(3))) }

    private def multiline_literal_string_elem: Parser[Str] =
      line_sep | literal_string_elem ^^ (_.toString)

    private def basic_string_elem: Parser[Elem] =
      elem("", c => !is_control(c) && !"\"\\".contains(c)) | '\\' ~> string_escape

    private def string_escape: Parser[Elem] =
      elem("", "\"\\".contains(_)) |
        elem("", "btnfr".contains(_)) ^^
          { case 'b' => '\b' case 't' => '\t' case 'n' => '\n' case 'f' => '\f' case 'r' => '\r' } |
        ('u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) |
          'U' ~> repeated(character(Symbol.is_ascii_hex), 8, 8)) ^^
          (s => java.lang.Integer.parseInt(s, 16).toChar)

    private def literal_string_elem: Parser[Elem] = elem("", c => !is_control(c) && c != '\'')

    def string_failure: Parser[Token] = ("\"" | "'") ~> failure("Unterminated string")

    def token: Parser[Token] =
      positioned(
        line_sep_token | keyword | value | string | string_failure | failure("Unrecognized token"))
  }


  /* parser */

  trait Parsers extends combinator.Parsers {
    type Elem = Token

    case class Keys(rep: List[Key]) extends Positional {
      def last: Keys = Keys(rep.takeRight(1))
      def the_last: Key = rep.last
      
      def head: Keys = Keys(rep.take(1))
      def the_head: Key = rep.head

      def length: Int = rep.length

      def +(other: Keys): Keys = Keys(rep ::: other.rep)

      def prefixes: Set[Keys] =
        if (rep.isEmpty) Set.empty
        else Range.inclusive(1, length).toSet.map(i => Keys(rep.take(i)))

      def splits: List[(Keys, Keys)] =
        Range.inclusive(0, length).toList.map(n =>
          (Keys(rep.dropRight(n)), Keys(rep.takeRight(n))))
      def split(i: Int): (Keys, Keys) = {
        val (rep0, rep1) = rep.splitAt(i)
        (Keys(rep0), Keys(rep1))
      }

      def parent: Keys = Keys(rep.dropRight(1))
      def is_child_of(parent: Keys): Bool = rep.startsWith(parent.rep)
    }


    /* parse structure */

    sealed trait V extends Positional
    case class Primitive(t: T) extends V
    case class Array(rep: List[V]) extends V
    case class Inline_Table(elems: List[(Keys, V)]) extends V

    sealed trait Def extends Positional
    case class Table(key: Keys, elems: List[(Keys, V)]) extends Def
    case class Array_Of_Tables(key: Keys, elems: List[(Keys, V)]) extends Def

    case class File(elems: List[(Keys, V)], defs: List[Def])


    /* top-level syntax structure */

    def key: Parser[Keys] = positioned(rep1sep(keys, $$$(".")) ^^ (ks => Keys(ks.flatten)))

    def string: Parser[String] =
      elem("string", e => e.is_string || e.is_multiline_string) ^^ (s => String(s.text))
    def integer: Parser[Integer] =
      (decimal_int | binary_int | octal_int | hexadecimal_int) ^^ Integer.apply
    def float: Parser[Float] = (symbol_float | number_float) ^^ Float.apply
    def boolean: Parser[Boolean] = token("boolean", _.is_value, s => Boolean(Value.Boolean.parse(s)))

    def offset_date_time: Parser[Offset_Date_Time] =
      token("offset date-time", _.is_value,
        s => Offset_Date_Time(OffsetDateTime.parse(s.replace(" ", "T"))))
    def local_date_time: Parser[Local_Date_Time] =
      token("local date-time", _.is_value,
        s => Local_Date_Time(LocalDateTime.parse(s.replace(" ", "T"))))
    def local_date: Parser[Local_Date] =
      token("local date", _.is_value, s => Local_Date(LocalDate.parse(s)))
    def local_time: Parser[Local_Time] =
      token("local time", _.is_value, s => Local_Time(LocalTime.parse(s)))

    def array: Parser[Array] =
      positioned(
        $$$("[") ~>! repsep(opt(line_sep) ~> toml_value, opt(line_sep) ~ $$$(",")) <~!
          opt(line_sep) ~! opt($$$(",")) ~! opt(line_sep) <~! $$$("]") ^^ Array.apply)

    def inline_table: Parser[Inline_Table] =
      positioned(
        $$$("{") ~>! repsep(pair, $$$(",")) <~! $$$("}") ^^ Inline_Table.apply)

    def pair: Parser[(Keys, V)] = (key <~! $$$("=")) ~! toml_value ^^ { case ks ~ v => (ks, v) }

    def table: Parser[Table] =
      positioned(
        $$$("[") ~> (key <~! $$$("]") ~! line_sep) ~! content ^^
          { case key ~ content => Table(key, content) })

    def array_of_tables: Parser[Array_Of_Tables] =
      positioned(
        $$$("[") ~ $$$("[") ~>! (key <~! $$$("]") ~! $$$("]") ~! line_sep) ~! content ^^
          { case key ~ content => Array_Of_Tables(key, content) })

    def toml: Parser[File] =
      (opt(line_sep) ~>! content ~! rep(table | array_of_tables)) ^^
        { case content ~ defs => File(content, defs) }


    /* auxiliary */

    private def $$$(name: Str): Parser[Token] = elem(name, _.is_keyword(name))
    private def maybe[A, B](p: Parser[A], f: A => B): Parser[B] =
      p ^^ (a => Try(f(a))) ^? { case util.Success(v) => v }
    private def token[A](name: Str, p: Token => Bool, parser: Str => A): Parser[A] =
      maybe(elem(name, p), s => parser(s.text))
    private def prefixed[A](
      prefix: Str, name: Str, p: Str => Bool, parser: Str => A
    ): Parser[A] =
      token(name, e => e.is_value && e.text.startsWith(prefix) && p(e.text.stripPrefix(prefix)),
        s => parser(s.stripPrefix(prefix)))

    private def is_key(e: Elem): Bool = e.is_value && !e.text.exists("+: ".contains(_))
    private def keys: Parser[List[Key]] =
      token("string key", _.is_string, List(_)) | token("key", is_key, _.split('.').toList)

    private def sep_surrounded(s: Str): Bool =
      !s.startsWith("_") && !s.endsWith("_") && s.split('_').forall(_.nonEmpty)
    private def no_leading_zero(s: Str): Bool = {
      val t = s.replaceAll("_", "").takeWhile(_.isDigit)
      t == "0" || !t.startsWith("0")
    }

    private def is_int(s: Str): Bool =
      no_leading_zero(s.replaceAll("[-+]", "")) && sep_surrounded(s.replaceAll("[-+]", ""))
    private def decimal_int: Parser[Long] =
      token("integer", e => e.is_value && is_int(e.text), _.replace("_", "").toLong)
    private def binary_int: Parser[Long] =
      prefixed("0b", "integer", sep_surrounded, s => parseLong(s.replace("_", ""), 2))
    private def octal_int: Parser[Long] =
      prefixed("0o", "integer", sep_surrounded, s => parseLong(s.replace("_", ""), 8))
    private def hexadecimal_int: Parser[Long] =
      prefixed("0x", "integer", sep_surrounded, s => parseLong(s.replace("_", ""), 16))

    private def is_float(s: Str): Bool =
      s.exists(".eE".contains) && s.count("eE".contains) <= 1 &&
        no_leading_zero(s.replaceAll("[-+]", "")) &&
        sep_surrounded(s.replaceAll("[-+]", "").replaceAll("[.eE][+\\-]?", "_"))
    private def number_float: Parser[Double] =
      token("float", e => e.is_value && is_float(e.text), _.replace("_", "").toDouble)
    private def symbol_float: Parser[Double] =
      token("float", _.is_value, {
        case "inf" | "+inf" => Double.PositiveInfinity
        case "-inf" => Double.NegativeInfinity
        case "nan" | "+nan" | "-nan" => Double.NaN
      })

    private def toml_value: Parser[V] =
      positioned(
        (string | float | integer | boolean | offset_date_time |
          local_date_time | local_date | local_time) ^^ Primitive.apply | array | inline_table)

    private def line_sep: Parser[Any] = rep1(elem("line sep", _.is_line_sep))

    private def content: Parser[List[(Keys, V)]] =
      rep((key <~! $$$("=")) ~! toml_value <~! line_sep ^^ { case ks ~ v => ks -> v })


    /* parse */

    def parse(input: Str): ParseResult[File] =
      phrase(toml)(new Lexer.Scanner(Scan.char_reader(input + EofCh)))
  }

  object Parsers extends Parsers


  /* checking and translating parse structure into toml */

  class Parse_Context private(var seen_tables: Map[Parsers.Keys, Seen], file: Option[Path] = None) {
    private def recent_array(ks: Parsers.Keys): (Parsers.Keys, Seen, Parsers.Keys) =
      ks.splits.collectFirst {
        case (ks1, ks2) if seen_tables.contains(ks1) => (ks1, seen_tables(ks1), ks2)
      }.get

    private def check_add(start: Int, ks: Parsers.Keys, elem: Parsers.Def | Parsers.V): Unit = {
      val (to, seen, rest, split) =
        elem match {
          case _: Parsers.Array_Of_Tables =>
            val (_, seen, rest) = recent_array(ks.parent)
            (ks, seen, rest + ks.last, 0)
          case _ =>
            val (to, seen, rest) = recent_array(ks)
            (to, seen, rest, start - to.length)
        }
      val (rest0, rest1) = rest.split(split)
      val implicitly_seen = rest1.parent.prefixes.map(rest0 + _)

      def error[A](s: Str): A = this.error(s, elem.pos, Some(ks))

      seen.inlines.find(rest.is_child_of).foreach(ks =>
        error("Attempting to update an inline value"))

      val (inlines, tables) =
        elem match {
          case _: Parsers.Primitive =>
            (seen.inlines, seen.tables ++ implicitly_seen)
          case _: Parsers.Array =>
            if (seen_tables.contains(ks))
              error("Attempting to append with an inline array")
            (seen.inlines + rest, seen.tables ++ implicitly_seen)
          case _: Parsers.Inline_Table =>
            seen.tables.find(_.is_child_of(rest)).foreach(ks =>
              error("Attempting to add with an inline table"))
            (seen.inlines + rest, seen.tables ++ implicitly_seen)
          case _: Parsers.Table =>
            if (seen.tables.contains(rest))
              error("Attempting to define a table twice")
            (seen.inlines, seen.tables + rest)
          case _: Parsers.Array_Of_Tables => (Set.empty, Set.empty)
        }

      seen_tables += to -> Seen(inlines, tables)
    }

    def for_file(file: Path): Parse_Context = new Parse_Context(seen_tables, Some(file))

    def error[A](s: Str, pos: input.Position, key: Option[Parsers.Keys] = None): A = {
      val key_msg = if_proper(key, " in table " + Format.keys(key.get.rep))
      val file_msg = if_proper(file, " in " + file.get)
      isabelle.error(s + key_msg + " at line " + pos.line + file_msg)
    }

    def check_add_def(ks: Parsers.Keys, defn: Parsers.Def): Unit = check_add(0, ks, defn)
    def check_add_value(ks0: Parsers.Keys, ks1: Parsers.Keys, v: Parsers.V): Unit =
      check_add(ks0.length - 1, ks0 + ks1, v)
  }

  object Parse_Context {
    case class Seen(inlines: Set[Parsers.Keys], tables: Set[Parsers.Keys])

    def apply(): Parse_Context =
      new Parse_Context(Map(Parsers.Keys(Nil) -> Seen(Set.empty, Set.empty)))
  }

  def parse(s: Str, context: Parse_Context = Parse_Context()): Table = {
    val file =
      Parsers.parse(s) match {
        case Parsers.Success (toml, _) => toml
        case Parsers.Error(msg, next) => context.error("Error parsing toml: " + msg, next.pos)
        case Parsers.Failure (msg, next) =>
          context.error("Malformed TOML input: " + msg, next.pos)
      }

    def convert(ks0: Parsers.Keys, ks1: Parsers.Keys, v: Parsers.V): T = {
      def to_table(ks: Parsers.Keys, t: T): Table =
        ks.parent.rep.foldRight(Table(ks.the_last -> t))((k, v) => Table(k -> v))
      def to_toml(v: Parsers.V): (T, Set[Parsers.Keys]) = v match {
        case Parsers.Primitive(t) => (t, Set.empty)
        case Parsers.Array(rep) => (Array(rep.map(to_toml(_)._1)), Set.empty)
        case Parsers.Inline_Table(elems) =>
          elems.find(e => elems.count(_._1 == e._1) > 1).foreach((ks, _) =>
            context.error(
              "Duplicate key " + Format.keys(ks.rep) + " in inline table", v.pos, Some(ks0 + ks1)))

          val (tables, pfxs, key_spaces) =
            elems.map { (ks, v) =>
              val (t, keys) = to_toml(v)
              (to_table(ks, t), ks.prefixes, keys.map(ks + _) + ks)
            }.unzip3

          for {
            pfx <- pfxs
            if key_spaces.count(pfx.intersect(_).nonEmpty) > 1
          } context.error("Inline table not self-contained", v.pos, Some(ks0 + ks1))

          (tables.foldLeft(Table())(_ ++ _), pfxs.toSet.flatten ++ key_spaces.toSet.flatten)
      }
      context.check_add_value(ks0, ks1, v)
      to_toml(v)._1
    }

    def update(map: Table, ks0: Parsers.Keys, value: T): Table = {
      def error[A](s: Str): A = context.error(s, ks0.pos, Some(ks0))

      def update_rec(hd: Parsers.Keys, map: Table, ks: Parsers.Keys): Table = {
        val updated =
          if (ks.length == 1) {
            map.any.get(ks.the_head) match {
              case Some(a: Array) =>
                value match {
                  case a2: Array => a ++ a2
                  case _ => error("Table conflicts with previous array of tables")
                }
              case Some(t: Table) => value match {
                case t2: Table =>
                  if (t.domain.intersect(t2.domain).nonEmpty)
                    error("Attempting to redefine existing value in super-table")
                  else t ++ t2
                case _ => error("Attempting to redefine a table")
              }
              case Some(_) => error("Attempting to redefine a value")
              case None => value
            }
          }
          else {
            val (head, tail) = ks.split(1)
            val hd1 = hd + head
            map.any.get(ks.the_head) match {
              case Some(t: Table) => update_rec(hd1, t, tail)
              case Some(a: Array) =>
                Array(a.table.values.dropRight(1) :+ update_rec(hd1, a.table.values.last, tail))
              case Some(_) => error("Attempting to redefine a value")
              case None => update_rec(hd1, Table(), tail)
            }
          }
        (map - ks.the_head) + (ks.the_head -> updated)
      }

      update_rec(Parsers.Keys(Nil), map, ks0)
    }

    def fold(elems: List[(Parsers.Keys, T)]): Table =
      elems.foldLeft(Table()) { case (t0, (ks1, t1)) => update(t0, ks1, t1) }

    val t = fold(file.elems.map((ks, v) => (ks, convert(Parsers.Keys(Nil), ks, v))))
    file.defs.foldLeft(t) {
      case (t0, [e-mail](ks0, elems)) =>
        context.check_add_def(ks0, defn)
        update(t0, ks0, fold(elems.map((ks, v) => (ks, convert(ks0, ks, v)))))
      case (t0, [e-mail]_Of_Tables(ks0, elems)) =>
        context.check_add_def(ks0, defn)
        update(t0, ks0, Array(fold(elems.map((ks, v) => (ks, convert(ks0, ks, v))))))
    }
  }

  def parse_files(files: Iterable[Path], context: Parse_Context = Parse_Context()): Table =
    files.foldLeft((Table(), context)) {
      case ((t, context0), file) =>
        val context = context0.for_file(file)
        (t ++ parse(File.read(file), context), context)
    }._1


  /* Format TOML */

  object Format {
    private def basic_string(s: Str): Str =
      "\"" + 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 + "\""

    private def multiline_basic_string(s: Str): Str =
      "\"\"\"\n" + 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("\"\"\"", "\"\"\\\"") + "\"\"\""

    def key(k: Key): Str = {
      val Bare_Key = """[A-Za-z0-9_-]+""".r
      k match {
        case Bare_Key() => k
        case _ => basic_string(k)
      }
    }

    def keys(ks: List[Key]): Str = ks.map(key).mkString(".")

    def inline(t: T, indent: Int = 0): Str = {
      val result = new StringBuilder

      result ++= Symbol.spaces(indent * 2)
      (t: @unchecked) match {
        case s: String =>
          if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
          else result ++= basic_string(s.rep)
        case a: Array =>
          if (a.is_empty) result ++= "[]"
          else {
            result ++= "[\n"
            a.any.values.foreach { elem =>
              result ++= inline(elem, indent + 1)
              result ++= ",\n"
            }
            result ++= Symbol.spaces(indent * 2)
            result += ']'
          }
        case table: Table =>
          if (table.is_empty) result ++= "{}"
          else {
            result ++= "{ "
            Library.separate(None, table.any.values.map(Some(_))).foreach {
              case None => result ++= ", "
              case Some((k, v)) =>
                result ++= key(k)
                result ++= " = "
                result ++= inline(v)
            }
            result ++= " }"
          }
        case Scalar(s) => result ++= s
      }
      result.toString()
    }

    def apply(toml: Table): Str = {
      val result = new StringBuilder

      def inline_values(path: List[Key], t: T): Unit =
        t match {
          case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) }
          case _ =>
            result ++= keys(path.reverse)
            result ++= " = "
            result ++= inline(t)
            result += '\n'
        }

      def is_inline(elem: T): Bool =
        elem match {
          case _: String | _: Integer | _: Float | _: Boolean | _: Offset_Date_Time |
               _: Local_Date_Time | _: Local_Date | _: Local_Time => true
          case a: Array => a.any.values.forall(is_inline)
          case _ => false
        }
      def is_table(elem: T): Bool = elem match { case _: Table => true case _ => false }

      def array(path: List[Key], a: Array): Unit =
        if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table))
          inline_values(path.take(1), a)
        else a.table.values.foreach { t =>
          result ++= "\n[["
          result ++= keys(path.reverse)
          result ++= "]]\n"
          table(path, t, is_table_entry = true)
        }

      def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = {
        val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2))

        if (!is_table_entry && path.nonEmpty) {
          result ++= "\n["
          result ++= keys(path.reverse)
          result ++= "]\n"
        }

        values.foreach { case (k, v) => inline_values(List(k), v) }
        nodes.foreach {
          case (k, t: Table) => table(k :: path, t)
          case (k, arr: Array) => array(k :: path, arr)
          case _ =>
        }
      }

      table(Nil, toml)
      result.toString
    }
  }
}