# HG changeset patch # User Fabian Huch # Date 1700209408 -3600 # Node ID 47f8533c6887609dd1c7ed9afcba2c0833ac04fc # Parent a80ee3c97aae6b83d59acfe3f3e92f65fb10c095 add position information to toml parser and error messages; diff -r a80ee3c97aae -r 47f8533c6887 src/Pure/General/toml.scala --- a/src/Pure/General/toml.scala Thu Nov 16 15:36:34 2023 +0100 +++ b/src/Pure/General/toml.scala Fri Nov 17 09:23:28 2023 +0100 @@ -7,7 +7,6 @@ package isabelle -import TOML.Parsers.Keys import TOML.Parse_Context.Seen import java.lang.Long.parseLong @@ -21,6 +20,8 @@ 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 @@ -159,7 +160,7 @@ enum Kind { case KEYWORD, VALUE, STRING, MULTILINE_STRING, LINE_SEP, ERROR } - sealed case class Token(kind: Kind, text: Str) { + 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 @@ -244,7 +245,8 @@ def string_failure: Parser[Token] = ("\"" | "'") ~> failure("Unterminated string") def token: Parser[Token] = - line_sep_token | keyword | value | string | string_failure | failure("Unrecognized token") + positioned( + line_sep_token | keyword | value | string | string_failure | failure("Unrecognized token")) } @@ -253,17 +255,42 @@ 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 */ - type Keys = List[Key] - - sealed trait V + 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 + 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 @@ -272,7 +299,7 @@ /* top-level syntax structure */ - def key: Parser[Keys] = rep1sep(keys, $$$(".")) ^^ (_.flatten) + 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)) @@ -293,20 +320,25 @@ token("local time", _.is_value, s => Local_Time(LocalTime.parse(s))) def array: Parser[Array] = - $$$("[") ~>! repsep(opt(line_sep) ~> toml_value, opt(line_sep) ~ $$$(",")) <~! - opt(line_sep) ~! opt($$$(",")) ~! opt(line_sep) <~! $$$("]") ^^ Array.apply + 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] = - $$$("{") ~>! repsep(pair, $$$(",")) <~! $$$("}") ^^ Inline_Table.apply + positioned( + $$$("{") ~>! repsep(pair, $$$(",")) <~! $$$("}") ^^ Inline_Table.apply) def pair: Parser[(Keys, V)] = (key <~! $$$("=")) ~! toml_value ^^ { case ks ~ v => (ks, v) } - def table: Parser[Table] = $$$("[") ~> (key <~! $$$("]") ~! line_sep) ~! content ^^ - { case key ~ content => Table(key, content) } + def table: Parser[Table] = + positioned( + $$$("[") ~> (key <~! $$$("]") ~! line_sep) ~! content ^^ + { case key ~ content => Table(key, content) }) def array_of_tables: Parser[Array_Of_Tables] = - $$$("[") ~ $$$("[") ~>! (key <~! $$$("]") ~! $$$("]") ~! line_sep) ~! content ^^ - { case key ~ content => Array_Of_Tables(key, content) } + 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)) ^^ @@ -327,7 +359,7 @@ s => parser(s.stripPrefix(prefix))) private def is_key(e: Elem): Bool = e.is_value && !e.text.exists("+: ".contains(_)) - private def keys: Parser[Keys] = + 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 = @@ -361,8 +393,10 @@ case "nan" | "+nan" | "-nan" => Double.NaN }) - private def toml_value: Parser[V] = (string | float | integer | boolean | offset_date_time | - local_date_time | local_date | local_time) ^^ Primitive.apply | array | inline_table + 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)) @@ -388,33 +422,29 @@ /* checking and translating parse structure into toml */ - private def prefixes(ks: Keys): Set[Keys] = - if (ks.isEmpty) Set.empty else Range.inclusive(1, ks.length).toSet.map(ks.take) - - class Parse_Context private(var seen_tables: Map[Keys, Seen]) { - private def splits(ks: Keys): List[(Keys, Keys)] = - Range.inclusive(0, ks.length).toList.map(n => (ks.dropRight(n), ks.takeRight(n))) - - private def recent_array(ks: Keys): (Keys, Seen, Keys) = - splits(ks).collectFirst { + class Parse_Context private(var seen_tables: Map[Parsers.Keys, Seen]) { + 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: Keys, elem: Parsers.Def | Parsers.V): Unit = { + 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.dropRight(1)) - (ks, seen, rest ::: ks.takeRight(1), 0) + 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.splitAt(split) - val implicitly_seen = prefixes(rest1.dropRight(1)).map(rest0 ::: _) + val (rest0, rest1) = rest.split(split) + val implicitly_seen = rest1.parent.prefixes.map(rest0 + _) - seen.inlines.find(rest.startsWith(_)).foreach(ks => - error("Attempting to update an inline value at " + Format.keys(ks))) + def error[A](s: Str): A = this.error(s, ks, elem) + + seen.inlines.find(rest.is_child_of).foreach(ks => + error("Attempting to update an inline value")) val (inlines, tables) = elem match { @@ -422,54 +452,58 @@ (seen.inlines, seen.tables ++ implicitly_seen) case _: Parsers.Array => if (seen_tables.contains(ks)) - error("Attempting to append with an inline array at " + Format.keys(ks)) + error("Attempting to append with an inline array") (seen.inlines + rest, seen.tables ++ implicitly_seen) case _: Parsers.Inline_Table => - seen.tables.find(_.startsWith(rest)).foreach(ks => - error("Attempting to add with an inline table at " + Format.keys(ks))) + 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 at " + Format.keys(ks)) + 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 check_add_def(ks: Keys, defn: Parsers.Def): Unit = check_add(0, ks, defn) - def check_add_value(ks0: Keys, ks1: Keys, v: Parsers.V): Unit = - check_add(ks0.length - 1, ks0 ::: ks1, v) + def error[A](s: Str, ks: Parsers.Keys, elem: Positional): A = + isabelle.error(s + " in table " + Format.keys(ks.rep) + " at line " + elem.pos.line) + 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[Keys], tables: Set[Keys]) + case class Seen(inlines: Set[Parsers.Keys], tables: Set[Parsers.Keys]) - def apply(): Parse_Context = new Parse_Context(Map(Nil -> Seen(Set.empty, Set.empty))) + 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) - def convert(ks0: Keys, ks1: Keys, v: Parsers.V): T = { - def to_table(ks: Keys, t: T): Table = - ks.dropRight(1).foldRight(Table(ks.last -> t))((k, v) => Table(k -> v)) - def to_toml(v: Parsers.V): (T, Set[Keys]) = v match { + 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, _) => - error("Duplicate key " + Format.keys(ks) + " in inline table at " + - Format.keys(ks0 ::: ks1))) + context.error("Duplicate key " + Format.keys(ks.rep) + " in inline table", ks0 + ks1, v)) val (tables, pfxs, key_spaces) = elems.map { (ks, v) => val (t, keys) = to_toml(v) - (to_table(ks, t), prefixes(ks), keys.map(ks ::: _) + ks) + (to_table(ks, t), ks.prefixes, keys.map(ks + _) + ks) }.unzip3 - pfxs.foreach(pfx => if (key_spaces.count(pfx.intersect(_).nonEmpty) > 1) - error("Inline table not self-contained at " + Format.keys(ks0 ::: ks1))) + for { + pfx <- pfxs + if key_spaces.count(pfx.intersect(_).nonEmpty) > 1 + } context.error("Inline table not self-contained", ks0 + ks1, v) (tables.foldLeft(Table())(_ ++ _), pfxs.toSet.flatten ++ key_spaces.toSet.flatten) } @@ -477,48 +511,50 @@ to_toml(v)._1 } - def update(map: Table, ks0: Keys, value: T): Table = { - def update_rec(hd: Keys, map: Table, ks: Keys): Table = { + def update(map: Table, ks0: Parsers.Keys, value: T): Table = { + def error[A](s: Str): A = context.error(s, ks0, ks0) + + def update_rec(hd: Parsers.Keys, map: Table, ks: Parsers.Keys): Table = { val updated = if (ks.length == 1) { - map.any.get(ks.head) match { + 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 at " + Format.keys(ks0)) + 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 at " + - Format.keys(ks0)) + error("Attempting to redefine existing value in super-table") else t ++ t2 - case _ => error("Attempting to redefine a table at " + Format.keys(ks0)) + case _ => error("Attempting to redefine a table") } - case Some(_) => error("Attempting to redefine a value at " + Format.keys(ks0)) + case Some(_) => error("Attempting to redefine a value") case None => value } } else { - val hd1 = hd :+ ks.head - map.any.get(ks.head) match { - case Some(t: Table) => update_rec(hd1, t, ks.tail) + 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, ks.tail)) - case Some(_) => error("Attempting to redefine a value at " + Format.keys(hd1)) - case None => update_rec(hd1, Table(), ks.tail) + 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.head) + (ks.head -> updated) + (map - ks.the_head) + (ks.the_head -> updated) } - update_rec(Nil, map, ks0) + + update_rec(Parsers.Keys(Nil), map, ks0) } - def fold(elems: List[(Keys, T)]): Table = + 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(Nil, ks, v)))) + val t = fold(file.elems.map((ks, v) => (ks, convert(Parsers.Keys(Nil), ks, v)))) file.defs.foldLeft(t) { case (t0, defn@Parsers.Table(ks0, elems)) => context.check_add_def(ks0, defn) @@ -558,7 +594,7 @@ } } - def keys(ks: Keys): Str = ks.mkString(".") + def keys(ks: List[Key]): Str = ks.map(key).mkString(".") def inline(t: T, indent: Int = 0): Str = { val result = new StringBuilder