TOML Expression Elaboration

Elaborates top-level TOML syntax into a Lean Toml.Table.

inductive Lake.Toml.KeyTy : Type

The manner in which a TOML key was declared.

• value : KeyTy

  A key declared via key = v.

• stdTable : KeyTy

  A key declared via [key].

• array : KeyTy

  A key declared via [[key]].

• dottedPrefix : KeyTy

  A key declared via key.foo.

• headerPrefix : KeyTy

  A key declared via [key.foo] or [[key.foo]].

instance Lake.Toml.instInhabitedKeyTy : Inhabited KeyTy

def Lake.Toml.KeyTy.toString (ty : KeyTy) : String

instance Lake.Toml.instToStringKeyTy : ToString KeyTy

def Lake.Toml.KeyTy.isValidPrefix (ty : KeyTy) : Bool

structure Lake.Toml.Keyval : Type

• ref : Lean.Syntax
• key : Lean.Name
• val : Value

structure Lake.Toml.ElabState : Type

• keyTys : Lean.NameMap KeyTy
• arrKeyTys : Lean.NameMap (Lean.NameMap KeyTy)
• arrParents : Lean.NameMap Lean.Name
• currArrKey : Lean.Name
• currKey : Lean.Name
• items : Array Keyval

instance Lake.Toml.instInhabitedElabState : Inhabited ElabState

@[reducible, inline]

abbrev Lake.Toml.TomlElabM (α : Type) : Type

def Lake.Toml.elabSubKeys (ks : Array (Lean.TSyntax `Lake.Toml.simpleKey)) : TomlElabM Lean.Name

def Lake.Toml.elabKeyval (kv : Lean.TSyntax `Lake.Toml.keyval) : TomlElabM Unit

def Lake.Toml.elabHeaderKeys (ks : Array (Lean.TSyntax `Lake.Toml.simpleKey)) : TomlElabM Lean.Name

def Lake.Toml.elabStdTable (x : Lean.TSyntax `Lake.Toml.stdTable) : TomlElabM Unit

def Lake.Toml.elabArrayTable (x : Lean.TSyntax `Lake.Toml.arrayTable) : TomlElabM Unit

def Lake.Toml.elabExpression (x : Lean.TSyntax `Lake.Toml.expression) : TomlElabM Unit

def Lake.Toml.mkSimpleTable (items : Array Keyval) : Table

Construct a table of simple key-value pairs from arbitrary key-value pairs.

For example:

{a.b := [c.d := 0]}, {a.b := [c.e := 1]}

becomes

{a := {b := [{c := {d := 0, e := 1}}]}}

partial def Lake.Toml.mkSimpleTable.simpVal : Value → Value

partial def Lake.Toml.mkSimpleTable.insert (t : Table) (kRef : Lean.Syntax) (k : Lean.Name) (ks : List Lean.Name) (newV : Value) : Table

def Lake.Toml.TomlElabM.run (x : TomlElabM Unit) : Lean.CoreM Table

def Lake.Toml.elabToml (x : Lean.TSyntax `Lake.Toml.toml) : Lean.CoreM Table