TOML Encoders

This module contains definitions to assist in encoding Lean types into TOML data values.

class Lake.ToToml (α : Type u) : Type u

• toToml : α → Toml.Value

@[instance_reducible]

instance Lake.instToTomlValue : ToToml Toml.Value

Equations

• Lake.instToTomlValue = { toToml := id }

@[instance_reducible]

instance Lake.instToTomlString : ToToml String

Equations

• Lake.instToTomlString = { toToml := Lake.Toml.Value.string Lean.Syntax.missing }

@[instance_reducible]

instance Lake.instToTomlFilePath : ToToml System.FilePath

Equations

• Lake.instToTomlFilePath = { toToml := fun (x : System.FilePath) => Lake.toToml (Lake.mkRelPathString x) }

@[instance_reducible]

instance Lake.instToTomlName : ToToml Lean.Name

Equations

• Lake.instToTomlName = { toToml := fun (x : Lean.Name) => Lake.toToml x.toString }

@[instance_reducible]

instance Lake.instToTomlInt : ToToml Int

Equations

• Lake.instToTomlInt = { toToml := Lake.Toml.Value.integer Lean.Syntax.missing }

@[instance_reducible]

instance Lake.instToTomlNat : ToToml Nat

Equations

• Lake.instToTomlNat = { toToml := fun (n : Nat) => Lake.Toml.Value.integer Lean.Syntax.missing (Int.ofNat n) }

@[instance_reducible]

instance Lake.instToTomlFloat : ToToml Float

Equations

• Lake.instToTomlFloat = { toToml := Lake.Toml.Value.float Lean.Syntax.missing }

@[instance_reducible]

instance Lake.instToTomlBool : ToToml Bool

Equations

• Lake.instToTomlBool = { toToml := Lake.Toml.Value.boolean Lean.Syntax.missing }

@[instance_reducible]

instance Lake.instToTomlArray {α : Type u_1} [ToToml α] : ToToml (Array α)

Equations

• Lake.instToTomlArray = { toToml := fun (x : Array α) => Lake.Toml.Value.array Lean.Syntax.missing (Array.map Lake.toToml x) }

@[instance_reducible]

instance Lake.instToTomlArrayValue : ToToml (Array Toml.Value)

Equations

• Lake.instToTomlArrayValue = { toToml := fun (x : Array Lake.Toml.Value) => Lake.Toml.Value.array Lean.Syntax.missing x }

@[instance_reducible]

instance Lake.instToTomlTable : ToToml Toml.Table

Equations

• Lake.instToTomlTable = { toToml := Lake.Toml.Value.table Lean.Syntax.missing }

class Lake.ToToml? (α : Type u) : Type u

• toToml? : α → Option Toml.Value

@[instance_reducible, instance 10000]

instance Lake.instToToml?OfToToml {α : Type u_1} [ToToml α] : ToToml? α

Equations

• Lake.instToToml?OfToToml = { toToml? := fun (v : α) => some (Lake.toToml v) }

def Lake.Toml.encodeArray? {α : Type u_1} [ToToml? α] (as : Array α) : Option (Array Value)

Equations

• Lake.Toml.encodeArray? as = Array.foldl (fun (vs? : Option (Array Lake.Toml.Value)) (a : α) => do let vs ← vs? let v ← Lake.toToml? a pure (vs.push v)) (some #[]) as

@[instance_reducible]

instance Lake.instToToml?Array {α : Type u_1} [ToToml? α] : ToToml? (Array α)

Equations

• Lake.instToToml?Array = { toToml? := fun (as : Array α) => Lake.toToml <$> Lake.Toml.encodeArray? as }

@[instance_reducible]

instance Lake.instToToml?Option {α : Type u_1} [ToToml? α] : ToToml? (Option α)

Equations

• Lake.instToToml?Option = { toToml? := fun (x : Option α) => x.bind Lake.toToml? }

@[instance_reducible]

instance Lake.instToToml?OptionOfToToml {α : Type u_1} [ToToml α] : ToToml? (Option α)

Equations

• Lake.instToToml?OptionOfToToml = { toToml? := fun (x : Option α) => Option.map Lake.toToml x }

class Lake.Toml.SmartInsert (α : Type u) : Type u

• smartInsert (k : Lean.Name) : α → Table → Table

  Insert a value into a table unless it represents a nullish value.

@[instance_reducible, instance 100]

instance Lake.Toml.instSmartInsertOfToToml? {α : Type u_1} [ToToml? α] : SmartInsert α

Equations

• Lake.Toml.instSmartInsertOfToToml? = { smartInsert := fun (k : Lean.Name) (v : α) (t : Lake.Toml.Table) => Lake.Toml.RBDict.insertSome k (Lake.toToml? v) t }

@[instance_reducible]

instance Lake.Toml.instSmartInsertTable : SmartInsert Table

Equations

• Lake.Toml.instSmartInsertTable = { smartInsert := fun (k : Lean.Name) (v t : Lake.Toml.Table) => Lake.Toml.RBDict.insertUnless (Lake.Toml.RBDict.isEmpty v) k (Lake.toToml v) t }

@[instance_reducible]

instance Lake.Toml.instSmartInsertArrayOfToToml {α : Type u_1} [ToToml (Array α)] : SmartInsert (Array α)

Equations

• Lake.Toml.instSmartInsertArrayOfToToml = { smartInsert := fun (k : Lean.Name) (v : Array α) (t : Lake.Toml.Table) => Lake.Toml.RBDict.insertUnless v.isEmpty k (Lake.toToml v) t }

@[instance_reducible]

instance Lake.Toml.instSmartInsertString : SmartInsert String

Equations

• Lake.Toml.instSmartInsertString = { smartInsert := fun (k : Lean.Name) (v : String) (t : Lake.Toml.Table) => Lake.Toml.RBDict.insertUnless v.isEmpty k (Lake.toToml v) t }

@[inline]

def Lake.Toml.Table.insert {α : Type u_1} [enc : ToToml α] (k : Lean.Name) (v : α) (t : Table) : Table

Inserts the encoded value into the table.

Equations

• Lake.Toml.Table.insert k v t = Lake.Toml.RBDict.insert k (Lake.toToml v) t

@[macro_inline]

def Lake.Toml.Table.insertSome {α : Type u_1} [enc : ToToml α] (k : Lean.Name) (v? : Option α) (t : Table) : Table

If the value is not none, inserts the encoded value into the table.

Equations

• Lake.Toml.Table.insertSome k v? t = Lake.Toml.RBDict.insertSome k (Option.map Lake.toToml v?) t

@[instance_reducible]

instance Lake.Toml.Table.instSmartInsertOptionOfToToml {α : Type u_1} [ToToml α] : SmartInsert (Option α)

Equations

• Lake.Toml.Table.instSmartInsertOptionOfToToml = { smartInsert := Lake.Toml.Table.insertSome }

@[inline]

def Lake.Toml.Table.smartInsert {α : Type u_1} [SmartInsert α] (k : Lean.Name) (v : α) (t : Table) : Table

Insert a value into the table unless it represents a nullish value.

Equations

• Lake.Toml.Table.smartInsert k v t = Lake.Toml.SmartInsert.smartInsert k v t

@[macro_inline]

def Lake.Toml.Table.insertIf {α : Type u_1} [enc : ToToml α] (p : Bool) (k : Lean.Name) (v : α) (t : Table) : Table

Insert a value into the table if p is true.

Equations

• Lake.Toml.Table.insertIf p k v t = Lake.Toml.RBDict.insertIf p k (Lake.toToml v) t

@[macro_inline]

def Lake.Toml.Table.insertUnless {α : Type u_1} [enc : ToToml α] (p : Bool) (k : Lean.Name) (v : α) (t : Table) : Table

Insert a value into the table if p is false.

Equations

• Lake.Toml.Table.insertUnless p k v t = Lake.Toml.RBDict.insertUnless p k (Lake.toToml v) t

@[inline]

def Lake.Toml.Table.insertD {α : Type u_1} [enc : ToToml α] [BEq α] (k : Lean.Name) (v default : α) (t : Table) : Table

Inserts the value into the table if it is not equal to default.

Equations

• Lake.Toml.Table.insertD k v default t = Lake.Toml.Table.insertUnless (v == default) k (Lake.toToml v) t