Nested TOML & Arrays of Tables🔗

Contributors: Anirudh Gupta

TOML supports nested structures through tables (sections like [server]) and arrays of tables (indicated by [[endpoints]]). These are handled by nesting DecodeToml and ToToml instances.

In Lake.Toml, you may see both Value.table and Value.table'. They are almost identical:

Value.table': The raw constructor for the Lake.Toml.Value inductive type.
Value.table: A shorthand for table' that is often used for clarity.

Both take two arguments: a Lean.Syntax (usually .missing for manual creation) and a Lake.Toml.Table.

Defining Nested Structures🔗

First, we define our Lean structures and provide the logic to convert them to and from TOML.

structure Address where
  host : String
  port : Nat
deriving Inhabited, Repr

instance : DecodeToml Address where
  decode v := do
    let tbl ← v.decodeTable
    return { 
      host := ← tbl.decode `host, 
      port := ← tbl.decode `port 
    }

instance : ToToml Address where
  toToml e := Value.table' .missing <| Table.empty
    |> Table.insert `host e.host
    |> Table.insert `port e.port

structure ServiceConfig where
  name      : String
  addresses : Array Address
deriving Inhabited, Repr

instance : DecodeToml ServiceConfig where
  decode v := do
    let tbl ← v.decodeTable
    return { 
      name := ← tbl.decode `name, 
      addresses := ← tbl.decode `addresses 
    }

instance : ToToml ServiceConfig where
  toToml c := Value.table' .missing <| Table.empty
    |> Table.insert `name c.name
    |> Table.insert `addresses c.addresses

Encoding (Representing as TOML)🔗

To see what the nested structure looks like in TOML format, we use Lake.Toml.ppTable.

def egEncodeNested : CoreM String := do
  let config : ServiceConfig := {
    name := "Production",
    addresses := #[
      { host := "api1.io", port := 80 },
      { host := "api2.io", port := 8080 }
    ]
  }
  let val := toToml config
  if let .table' _ tbl := val then
    return ppTable tbl
  else
    return toString val

"name = \"Production\"\n\n[[addresses]]\nhost = \"api1.io\"\nport = 80\n\n[[addresses]]\nhost = \"api2.io\"\nport = 8080\n"#eval egEncodeNested

Decoding (Reading and Accessing)🔗

When reading, you can either decode the entire file at once or target a specific nested section.

def egDecodeNested : CoreM String := do
  let input := "
name = \"Staging\"

[[addresses]]
host = \"localhost\"
port = 3000
"
  let table ← parseToml input
  let val := Value.table' .missing table
  
  let result : EStateM.Result Unit (Array DecodeError) 
    ServiceConfig := decodeToml val #[]
  match result with
  | .ok cfg _ => return s!"Config '{cfg.name}' 
      has {cfg.addresses.size} addresses."
  | .error _ e => 
      throwError s!"Error: {e.toList.map (·.msg)}"

"Config 'Staging' \n      has 1 addresses."#eval egDecodeNested

If you only want one part of a complex TOML file, you can extract the raw Value first and then decode just that part.

def egDecodeSection : CoreM String := do
  let input := "
[server]
name = \"Backend\"
[[addresses]]
host = \"127.0.0.1\"
port = 80
"
  let table ← parseToml input
  
  -- Extract the [server] section as a raw Value
  let serverVal : Value := getTomlValue table "server"
  
  -- Decode that Value into a specific structure
  let result : EStateM.Result Unit (Array DecodeError) 
    Address := decodeToml serverVal #[]
    
  match result with
  | .ok addr _ => return s!"Server host is {addr.host}"
  | .error _ e => 
      throwError s!"Error: {e.toList.map (·.msg)}"

Modifying Nested TOML🔗

To modify a nested structure, you can either update the Lean object and re-encode it, or use helper functions like decodeTomlValue and updateValue to manipulate the Table directly.

def egModifyNested : CoreM String := do
  let input := "name = \"Dev\"\naddresses = []"
  let table ← parseToml input

  -- Retrieve the existing array of addresses
  let addresses : Array Address ← 
    match (decodeTomlValue table "addresses" : 
    Except String (Array Address)) with
    | .ok v => pure v
    | .error _ => pure #[]

  -- Add a new address to the array
  let newAddress : Address := 
    { host := "127.0.0.1", port := 5000 }
  let updatedAddresses := addresses.push newAddress
    
  -- Update the table and pretty-print
  let finalTable := updateValue 
    (updateValue table "addresses" updatedAddresses) 
    "name" "Dev-Local"
  
  return ppTable finalTable

"name = \"Dev-Local\"\n\n[[addresses]]\nhost = \"127.0.0.1\"\nport = 5000\n"#eval egModifyNested