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.

Equations

• Lake.Toml.DecodeM = EStateM Empty (Array Lake.Toml.DecodeError)

@[reducible, inline]

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

Monad for decoders that may abort.

Equations

• Lake.Toml.EDecodeM = EStateM Unit (Array Lake.Toml.DecodeError)

class Lake.DecodeToml (α : Type) : Type

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

@[reducible, inline]

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

Equations

• Lake.decodeToml v = Lake.DecodeToml.decode v

@[inline]

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

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

Equations

• Lake.Toml.ensureDecode x es = match x es with | EStateM.Result.ok a es => if es.isEmpty = true then EStateM.Result.ok a es else EStateM.Result.error () es

@[inline]

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

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

Equations

• Lake.Toml.tryDecodeD default x es = match x es with | EStateM.Result.ok a es => EStateM.Result.ok a es | EStateM.Result.error a es => EStateM.Result.ok default es

@[inline]

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

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

Equations

• Lake.Toml.tryDecode? x es = match x es with | EStateM.Result.ok a es => EStateM.Result.ok (some a) es | EStateM.Result.error a es => EStateM.Result.ok none es

@[inline]

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

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

Equations

• Lake.Toml.tryDecode x = Lake.Toml.tryDecodeD default x

@[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.

Equations

• Lake.Toml.optDecodeD default (some a) f = Lake.Toml.tryDecodeD default (f a)
• Lake.Toml.optDecodeD default none f = pure 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.

Equations

• Lake.Toml.optDecode a? f = Lake.Toml.optDecodeD default a? f

@[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.

Equations

• Lake.Toml.optDecode? a? f = Lake.Toml.optDecodeD none a? fun (a : α) => some <$> f a

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.

Equations

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

@[inline]

def Lake.Toml.logDecodeErrorAt (ref : Lean.Syntax) (msg : String) : DecodeM Unit

Equations

• Lake.Toml.logDecodeErrorAt ref msg es = EStateM.Result.ok () (es.push { ref := ref, msg := msg })

@[inline]

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

Equations

• Lake.Toml.throwDecodeErrorAt ref msg es = EStateM.Result.error () (es.push { ref := ref, msg := msg })

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.

Equations

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

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

Equations

• (Lake.Toml.Value.string ref v_2).decodeString = EStateM.Result.ok v_2
• v.decodeString = Lake.Toml.throwDecodeErrorAt v.ref "expected string"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlString : DecodeToml String

Equations

• Lake.Toml.Value.instDecodeTomlString = { decode := Lake.Toml.Value.decodeString }

@[implicit_reducible]

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

Equations

• Lake.Toml.Value.instDecodeTomlFilePath = { decode := fun (x : Lake.Toml.Value) => System.FilePath.mk <$> Lake.decodeToml x }

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

Equations

• v.decodeName = do let __do_lift ← v.decodeString match __do_lift.toName with | Lean.Name.anonymous => Lake.Toml.throwDecodeErrorAt v.ref "expected name" | n => pure n

@[implicit_reducible]

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

Equations

• Lake.Toml.Value.instDecodeTomlName = { decode := Lake.Toml.Value.decodeName }

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

Equations

• (Lake.Toml.Value.integer ref v_2).decodeInt = EStateM.Result.ok v_2
• v.decodeInt = Lake.Toml.throwDecodeErrorAt v.ref "expected integer"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlInt : DecodeToml Int

Equations

• Lake.Toml.Value.instDecodeTomlInt = { decode := Lake.Toml.Value.decodeInt }

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

Equations

• (Lake.Toml.Value.integer ref (Int.ofNat v)).decodeNat = EStateM.Result.ok v
• x✝.decodeNat = Lake.Toml.throwDecodeErrorAt x✝.ref "expected nonnegative integer"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlNat : DecodeToml Nat

Equations

• Lake.Toml.Value.instDecodeTomlNat = { decode := Lake.Toml.Value.decodeNat }

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

Equations

• (Lake.Toml.Value.float ref v_2).decodeFloat = EStateM.Result.ok v_2
• v.decodeFloat = Lake.Toml.throwDecodeErrorAt v.ref "expected float"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlFloat : DecodeToml Float

Equations

• Lake.Toml.Value.instDecodeTomlFloat = { decode := Lake.Toml.Value.decodeFloat }

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

Equations

• (Lake.Toml.Value.boolean ref v_2).decodeBool = EStateM.Result.ok v_2
• v.decodeBool = Lake.Toml.throwDecodeErrorAt v.ref "expected boolean"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlBool : DecodeToml Bool

Equations

• Lake.Toml.Value.instDecodeTomlBool = { decode := Lake.Toml.Value.decodeBool }

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

Equations

• (Lake.Toml.Value.dateTime ref v_2).decodeDateTime = EStateM.Result.ok v_2
• v.decodeDateTime = Lake.Toml.throwDecodeErrorAt v.ref "expected date-time"

@[implicit_reducible]

instance Lake.Toml.Value.instDecodeTomlDateTime : DecodeToml DateTime

Equations

• Lake.Toml.Value.instDecodeTomlDateTime = { decode := Lake.Toml.Value.decodeDateTime }

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

Equations

• (Lake.Toml.Value.array ref vs).decodeValueArray = EStateM.Result.ok vs
• v.decodeValueArray = Lake.Toml.throwDecodeErrorAt v.ref "expected array"

@[inline]

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

Equations

• v.decodeArray = do let __do_lift ← v.decodeValueArray Lake.Toml.decodeArray __do_lift

@[implicit_reducible]

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

Equations

• Lake.Toml.Value.instDecodeTomlArray = { decode := Lake.Toml.Value.decodeArray }

@[inline]

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

Equations

• (Lake.Toml.Value.array ref vs).decodeArrayOrSingleton = Lake.Toml.decodeArray vs
• v.decodeArrayOrSingleton = Array.singleton <$> Lake.DecodeToml.decode v

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

Equations

• (Lake.Toml.Value.table' ref t).decodeTable = EStateM.Result.ok t
• v.decodeTable = Lake.Toml.throwDecodeErrorAt v.ref "expected table"

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

Equations

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

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

Equations

• t.decodeValue k ref = match Lake.Toml.RBDict.find? k t with | some a => pure a | x => Lake.Toml.throwDecodeErrorAt ref (toString "missing required key: " ++ toString (Lake.Toml.ppKey k))

@[inline]

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

Equations

• t.decode k ref = do let a ← t.decodeValue k ref Lake.Toml.decodeKeyval k a

@[inline]

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

Equations

• t.decode? k = Option.mapM (fun (v : Lake.Toml.Value) => Lake.Toml.decodeKeyval k v) (Lake.Toml.RBDict.find? k t)

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

Equations

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

@[implicit_reducible]

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

Equations

• Lake.Toml.Table.instDecodeTomlNameMap = { decode := fun (x : Lake.Toml.Value) => do let __do_lift ← x.decodeTable __do_lift.decodeNameMap }

@[inline]

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

Equations

• t.tryDecode k ref = Lake.Toml.tryDecode (t.decode k ref)

@[inline]

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

Equations

• t.tryDecode? k = Lake.Toml.optDecode? (Lake.Toml.RBDict.find? k t) Lake.DecodeToml.decode

@[inline]

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

Equations

• Lake.Toml.Table.tryDecodeD k default t = Lake.Toml.optDecodeD default (Lake.Toml.RBDict.find? k t) Lake.DecodeToml.decode