Parsing TOML🔗

Contributors: Anirudh Gupta

To parse a TOML string, you first use the TOML parser to get a Syntax object, and then elaborate that syntax into a Lake.Toml.Table. A general purpose TOML parser function example that you can use in your own code is given below. It takes a TOML string as input and returns a Table or throws an error if parsing fails.

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

The above parseToml you can use for nested TOML structures as well. You can use ppTable to pretty-print the parsed Table back into a TOML string, like below:

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

More about Nested TOML handling in Handling Nested TOML section.