解析 TOML🔗

贡献者：Anirudh Gupta, subfish-zhou

要解析一个 TOML 字符串，你首先用 TOML 解析器得到一个 Syntax 对象，然后把该语法精译（elaboration）为一个 Lake.Toml.Table。下面给出一个通用的 TOML 解析器函数示例，你可以在自己的代码中使用。它以一个 TOML 字符串作为输入，返回一个 Table，若解析失败则抛出错误。

def parseToml (input : String) : CoreM Table := do
  let env ← getEnv
  let ictx := mkInputContext input "<string>"
  let pctx := { env, options := {} }
  let s := toml.fn.run ictx pctx {} 
    (mkParserState ictx.inputString)
  if let some err := s.errorMsg then
    throwError s!"Parse error: {err}"
  else
    elabToml ⟨s.stxStack.back⟩

def egTomlParse : CoreM String := do
  let input := "name = \"Cookbook\"\nversion = \"1.0.0\""
  let table ← parseToml input
  return s!"Parsed table with {table.values} entries."

"Parsed table with #[\"Cookbook\", \"1.0.0\"] entries."#eval egTomlParse

上面的 parseToml 同样可以用于嵌套的 TOML 结构。你可以用 ppTable 把解析得到的 Table 格式化输出为一个 TOML 字符串，如下所示：

def egNestedParse : CoreM String := do
  let input := "
[database]
server = \"192.168.1.1\"
ports = [ 8000, 8001, 8002 ]

[[users]]
name = \"Alice\"
role = \"admin\"

[[users]]
name = \"Bob\"
role = \"user\"
"
  -- parseToml handles all the nesting for you
  let table ← parseToml input
  return ppTable table

"\n[database]\nserver = \"192.168.1.1\"\nports = [8000, 8001, 8002]\n\n[[users]]\nname = \"Alice\"\nrole = \"admin\"\n\n[[users]]\nname = \"Bob\"\nrole = \"user\"\n"#eval egNestedParse

关于嵌套 TOML 处理的更多内容，见处理嵌套 TOML 一节。