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: Lake.Toml.KeyTy

  A key declared via key = v.

• stdTable: Lake.Toml.KeyTy

  A key declared via [key].

• array: Lake.Toml.KeyTy

  A key declared via [[key]].

• dottedPrefix: Lake.Toml.KeyTy

  A key declared via key.foo.

• headerPrefix: Lake.Toml.KeyTy

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

instance Lake.Toml.instInhabitedKeyTy : Inhabited Lake.Toml.KeyTy

Equations

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

def Lake.Toml.KeyTy.toString (ty : Lake.Toml.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 Lake.Toml.KeyTy

Equations

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

def Lake.Toml.KeyTy.isValidPrefix (ty : Lake.Toml.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 : Lake.Name
• val : Lake.Toml.Value

structure Lake.Toml.ElabState : Type

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

instance Lake.Toml.instInhabitedElabState : Inhabited Lake.Toml.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)) : Lake.Toml.TomlElabM Lake.Name

Equations

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

def Lake.Toml.elabKeyval (kv : Lean.TSyntax `Lake.Toml.keyval) : Lake.Toml.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)) : Lake.Toml.TomlElabM Lake.Name

Equations

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

def Lake.Toml.elabStdTable (x : Lean.TSyntax `Lake.Toml.stdTable) : Lake.Toml.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) : Lake.Toml.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) : Lake.Toml.TomlElabM Unit

Equations

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

def Lake.Toml.mkSimpleTable (items : Array Lake.Toml.Keyval) : Lake.Toml.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 : Lake.Toml.Value → Lake.Toml.Value

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

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

Equations

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

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

Equations

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