Accessing and Modifying TOML🔗

Contributors: Anirudh Gupta

The Lake.DecodeToml and Lake.ToToml classes allow you to automatically transform TOML tables into Lean structures and vice versa.

Reading values from TOML🔗

To transform TOML into Lean types, we primarily use two methods: high-level type-safe decoding via the Lake.DecodeToml class, and low-level extraction using Lake.Toml.Table methods.

decodeTable: Converts a generic Lake.Toml.Value into a Table. This is how you "open the box" to access the keys inside a nested section.
decode: A high-level method on Table that retrieves a key and immediately converts it to a Lean type (like String).
decodeValue: A low-level method that simply retrieves the raw Lake.Toml.Value for a key.

structure ToolConfig where
  name    : String
  version : String
  active  : Bool := true
deriving Inhabited, Repr

instance : DecodeToml ToolConfig where
  decode v := do
    -- Cast the generic Value to a Table
    let tbl ← v.decodeTable
    -- Decode specific keys into Lean types
    let name ← tbl.decode `name
    let version ← tbl.decode `version
    let active ← tbl.decode? `active
    return { name, version, active := active.getD true }

/-- 
  A general helper to get any type from a Table.
  If the key is missing or the type is wrong, it panics.
-/
def getTomlValue [DecodeToml α] [Inhabited α] 
    (table : Table) (key : String) : α :=
  match (table.decode key.toName).run #[] with
  | .ok v _ => v
  | .error _ errs => panic! 
      s!"Failed to get '{key}': {errs.toList.map (·.msg)}"

/-- Another safe helper to decode a
  specific key into a Lean type. -/
def decodeTomlValue [DecodeToml α] (table : Table) 
    (key : String) : Except String α :=
  match (table.decode key.toName).run #[] with
  | .ok v _ => .ok v
  | .error _ errs => .error 
    s!"Decode error for '{key}': {errs.toList.map (·.msg)}"

def egGetValue : CoreM String := do
  let input := "
name = \"Dragonbot\"
version = 4
is_active = true
"
  let table ← parseToml input
  
  let name : String := getTomlValue table "name"
  let ver  : Int    := getTomlValue table "version"
  let act  : Bool   := getTomlValue table "is_active"
  
  -- You can even get the raw 'Value' box if you want
  let _raw : Value := getTomlValue table "name"
  return s!"{name} v{ver} (Active: {act})"

"Dragonbot v4 (Active: true)"#eval egGetValue

Encoding and Modifying TOML🔗

To convert Lean structures back to TOML, implement the Lake.ToToml class. When creating a table, we use Value.table .missing tbl to wrap our dictionary into a TOML value.

instance : ToToml ToolConfig where
  toToml c :=
    let tbl := Table.empty
      |> Table.insert `name c.name
      |> Table.insert `version c.version
      |> Table.insert `active c.active
    -- We use .missing because this Value 
    -- is being generated programmatically
    Value.table .missing tbl

def egTomlEncode (cfg : ToolConfig) : CoreM String := do
  let val := toToml cfg
  -- If it's a table, we can pretty-print it for a file
  if let .table _ tbl := val then
    return ppTable tbl
  else
    return toString val

"name = \"my-tool\"\nversion = \"0.1.0\"\nactive = true\n"#eval egTomlEncode
  { name := "my-tool", version := "0.1.0", active := true }

For a given Table, if you want to modify it (e.g., add or update keys), you can use Table.insert to create a new table with the desired changes. For default values, you can use the Table.insertD method instead.

def updateValue [ToToml α] (table : Table) (key : String) 
    (newValue : α) : Table :=
  -- If the key exists, this replaces it; else, it adds it
  Table.insert key.toName newValue table

def safeUpdateValue [ToToml α] (table : Table)
  (key : String) (newValue : α) : Table :=
  -- Check if the key exists before updating
  match (table.decodeValue key.toName).run #[] with
  | .ok .. => updateValue table key newValue
  | .error .. => 
    panic! s!"Key '{key}' does not exist in the table."

def egUpdate : CoreM String := do
  let input := "name = \"Lean4\"\nversion = \"4.15.0\""
  let table ← parseToml input
  -- Update existing key
  let table := updateValue table "version" "4.16.0"
  -- Add new key
  let table := updateValue table "active" true
  return ppTable table

"name = \"Lean4\"\nversion = \"4.16.0\"\nactive = true\n"#eval egUpdate