TOML Decoders

This module contains definitions to assist in decoding TOML data values into concrete user types.

structure Lake.Toml.DecodeError : Type

• ref : Lean.Syntax
• msg : String

@[reducible, inline]

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

Monad for decoders that do not abort.

@[reducible, inline]

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

Monad for decoders that may abort.

class Lake.DecodeToml (α : Type) : Type

• decode (v : Toml.Value) : Toml.EDecodeM α

@[reducible, inline]

abbrev Lake.decodeToml {α : Type} [DecodeToml α] (v : Toml.Value) : Toml.EDecodeM α

@[inline]

def Lake.Toml.ensureDecode {α : Type} (x : DecodeM α) : EDecodeM α

Run the decode action. If there were errors, throw. Otherwise, return the result.

@[inline]

def Lake.Toml.tryDecodeD {α : Type} (default : α) (x : EDecodeM α) : DecodeM α

Run the decode action. If it fails, keep the errors but return default.

@[inline]

def Lake.Toml.tryDecode? {α : Type} (x : EDecodeM α) : DecodeM (Option α)

Run the decode action. If it fails, keep the errors but return none.

@[inline]

def Lake.Toml.tryDecode {α : Type} [Inhabited α] (x : EDecodeM α) : DecodeM α

Run the decode action. If it fails, keep the errors but return Inhabited.default.

@[inline]

def Lake.Toml.optDecodeD {β : Type} {α : Type u_1} (default : β) (a? : Option α) (f : α → EDecodeM β) : DecodeM β

If the value is not none, run the decode action. If it fails, add the errors to the state and return default.

@[inline]

def Lake.Toml.optDecode {β : Type} {α : Type u_1} [Inhabited β] (a? : Option α) (f : α → EDecodeM β) : DecodeM β

If the value is not none, run the decode action. If it fails, add the errors to the state and return Inhabited.default.

@[inline]

def Lake.Toml.optDecode? {α : Type u_1} {β : Type} (a? : Option α) (f : α → EDecodeM β) : DecodeM (Option β)

If the value is not none, run the decode action. If it fails, add the errors to the state and return none. Otherwise, return the result in some.

def Lake.Toml.mergeErrors {α β γ : Type} (x₁ : EDecodeM α) (x₂ : EDecodeM β) (f : α → β → γ) : EDecodeM γ

If either action errors, throw the concatenated errors. Otherwise, if no errors, combine the results with f.

@[inline]

def Lake.Toml.throwDecodeErrorAt {α : Type} (ref : Lean.Syntax) (msg : String) : EDecodeM α

def Lake.Toml.decodeArray {α : Type} [dec : DecodeToml α] (vs : Array Value) : EDecodeM (Array α)

Decode an array of TOML values, merging any errors from the elements into a single array.

def Lake.Toml.Value.decodeString (v : Value) : EDecodeM String

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlString : DecodeToml String

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlFilePath : DecodeToml System.FilePath

def Lake.Toml.Value.decodeName (v : Value) : EDecodeM Lean.Name

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlName : DecodeToml Lean.Name

def Lake.Toml.Value.decodeInt (v : Value) : EDecodeM Int

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlInt : DecodeToml Int

def Lake.Toml.Value.decodeNat : Value → EDecodeM Nat

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlNat : DecodeToml Nat

def Lake.Toml.Value.decodeFloat (v : Value) : EDecodeM Float

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlFloat : DecodeToml Float

def Lake.Toml.Value.decodeBool (v : Value) : EDecodeM Bool

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlBool : DecodeToml Bool

def Lake.Toml.Value.decodeDateTime (v : Value) : EDecodeM DateTime

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlDateTime : DecodeToml DateTime

def Lake.Toml.Value.decodeValueArray (v : Value) : EDecodeM (Array Value)

@[inline]

def Lake.Toml.Value.decodeArray {α : Type} [dec : DecodeToml α] (v : Value) : EDecodeM (Array α)

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlArray {α : Type} [DecodeToml α] : DecodeToml (Array α)

@[inline]

def Lake.Toml.Value.decodeArrayOrSingleton {α : Type} [dec : DecodeToml α] (v : Value) : EDecodeM (Array α)

def Lake.Toml.Value.decodeTable (v : Value) : EDecodeM Table

def Lake.Toml.decodeKeyval {α : Type} [dec : DecodeToml α] (k : Lean.Name) (v : Value) : EDecodeM α

def Lake.Toml.Table.decodeValue (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : EDecodeM Value

@[inline]

def Lake.Toml.Table.decode {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : EDecodeM α

@[inline]

def Lake.Toml.Table.decode? {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) : EDecodeM (Option α)

def Lake.Toml.Table.decodeNameMap {α : Type} [dec : DecodeToml α] (t : Table) : EDecodeM (Lean.NameMap α)

@[implicit_reducible]

instance Lake.Toml.Table.instDecodeTomlNameMap {α : Type} [DecodeToml α] : DecodeToml (Lean.NameMap α)

@[inline]

def Lake.Toml.Table.tryDecode {α : Type} [Inhabited α] [dec : DecodeToml α] (t : Table) (k : Lean.Name) (ref : Lean.Syntax := Lean.Syntax.missing) : DecodeM α

@[inline]

def Lake.Toml.Table.tryDecode? {α : Type} [dec : DecodeToml α] (t : Table) (k : Lean.Name) : DecodeM (Option α)

@[inline]

def Lake.Toml.Table.tryDecodeD {α : Type} [dec : DecodeToml α] (k : Lean.Name) (default : α) (t : Table) : DecodeM α