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

Equations

• Lake.Toml.instInhabitedKeyTy = { default := Lake.Toml.KeyTy.value }

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

Equations

• Lake.Toml.KeyTy.value.toString = "value"
• Lake.Toml.KeyTy.stdTable.toString = "table"
• Lake.Toml.KeyTy.array.toString = "array"
• Lake.Toml.KeyTy.dottedPrefix.toString = "dotted"
• Lake.Toml.KeyTy.headerPrefix.toString = "dotted"

instance Lake.Toml.instToStringKeyTy : ToString KeyTy

Equations

• Lake.Toml.instToStringKeyTy = { toString := Lake.Toml.KeyTy.toString }

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

Equations

• Lake.Toml.KeyTy.stdTable.isValidPrefix = true
• Lake.Toml.KeyTy.headerPrefix.isValidPrefix = true
• Lake.Toml.KeyTy.dottedPrefix.isValidPrefix = true
• ty.isValidPrefix = false

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

Equations

• Lake.Toml.instInhabitedElabState = { default := { keyTys := default, arrKeyTys := default, arrParents := default, currArrKey := default, currKey := default, items := default } }

@[reducible, inline]

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

Equations

• Lake.Toml.TomlElabM = StateT Lake.Toml.ElabState Lean.CoreM

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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}}]}}

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• x.run = do let __discr ← StateT.run x { } match __discr with | (fst, s) => pure (Lake.Toml.mkSimpleTable s.items)

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

Equations

• One or more equations did not get rendered due to their size.