JSON object representation

Stream: lean4

[Bhakti Shah]

I'm working with the JSON library and this probably has an obvious answer but why is a JSON object represented as an RBNode? why do we need the dependent type there?

[Henrik Böving]

RBNode is mostly a dependent type because we can, not because it is strictly necessary.

[Henrik Böving]

That is. RBNode is not written strictly for JSON. It is a general purpose RBtree and we just happen to also use it for JSON.

[Bhakti Shah]

is there a way to get rid of that dependency? I'm just trying to flatten an object to a list of its value fields, but the dependent type is making it annoying to get rid of the keys despite there being no actual dependency in the JSON object type (it's just (Lean.RBNode String fun x => Lean.Json))

[Henrik Böving]

Can you show me a #mwe ? I can't quite imagine what you are doing

[Adam Topaz]

I think this should work?

import Lean

open Lean

def Lean.Json.toList! : Json → List (String × Json)
  | .obj e => e.fold (fun l s j => (s,j) :: l) []
  | _ => []

[Adam Topaz]

For non-object json's this will give back an empty list.

[Bhakti Shah]

sure. I have something in JSON that looks like this:

{
    "key0" : {
        "v0" : 0
    },
    "key1" : {
        "v1" : 0
    }
}

trying to get something like

[
  { "v0" : 0 },
  { "v1" : 0 }
]

assuming the first is parsed into Lean.Json and the second is a list of Lean.Json.

import Lean.Data.Json

def jsonToList (json : Lean.Json) : List Lean.Json :=
match json.getObj? with
| .ok obj => List.map Prod.snd obj.toArray.toList -- where i want something like this to typecheck
| .error _ => sorry

[Adam Topaz]

so use my toList! and map with Prod.snd.

[Bhakti Shah]

Adam Topaz said:

I think this should work?

import Lean

open Lean

def Lean.Json.toList! : Json → List (String × Json)
  | .obj e => e.fold (fun l s j => (s,j) :: l) []
  | _ => []

That does in fact work!! Thank you so much :)