Parsing JSON pairs in JSON obj

Stream: new members

[Andrew Wells]

I'm trying to parse JSON to an AST. I don't want to auto generate the parser with FromJson because I expect I'll need to tweak the parser and to give specific error messages to make sure it matches another implementation. Currently I have:

import Lean.Data.Json.Parser
import Lean.Data.Json.Basic

inductive Primitive where
  | Bool (b: Bool): Primitive
  | Int (i: Int): Primitive
  | String (s: String): Primitive
deriving Repr

inductive Expr where
  | PrimitiveLit (l:Primitive) : Expr
  | If(g : Expr) (t:Expr) (e:Expr) : Expr
  | And(lhs:Expr) (rhs:Expr): Expr
  | Or(lhs:Expr) (rhs:Expr) : Expr
  | GetAttr(e:Expr) (a:Attr) : Expr
  | HasAttr(e:Expr) (a:Attr) : Expr
  | Record(data: Record) : Expr
  | Wrong : Expr

def my_json_expr_str := "{ \"And\" : { \"left\": {\"Lit\": {\"Bool\": true}}, {\"right\": {\"Lit\" : {\"Bool\": true} } } } }"
def my_json_expr := Lean.Json.parse my_json_expr_str

def json_to_expr (json : Lean.Json) : Expr := match json with
  | Lean.Json.null => Expr.Wrong
  | Lean.Json.bool b => Expr.PrimitiveLit (Primitive.Bool b)
  | Lean.Json.num n => match n.exponent with
    | 0 => Expr.PrimitiveLit (Primitive.Int n.mantissa)
    | _ => Expr.Wrong
  | Lean.Json.str s => Expr.PrimitiveLit (Primitive.String s)
  | Lean.Json.arr _ => Expr.Wrong
  | Lean.Json.obj o => match o with -- Can't figure out how to process this case
    | Lean.RBNode.leaf => Expr.Wrong
    | _ => Expr.Wrong

I'd like to do something like iterate through all <key, value> pairs in the Json.obj to make sure the keys are expected and then assuming they are, call different functions processing the value depending on the key. If I knew what all the keys were I see I could call getObjValfor each key, but I can't seem to find a way to iterate through the keys.

[Andrew Wells]

I have a work around, but it looks like it will lead to pretty awful code:

Fix my JSON and define some helpers for unwrapping Except

def my_json_expr_str := "{ \"And\" : { \"left\": {\"Lit\": {\"Bool\": true}}, \"right\": {\"Lit\" : {\"Bool\": true} } } } "
def my_json_expr := Lean.Json.parse my_json_expr_str

structure ErrorStruct where
  error : Bool
deriving Repr, Lean.ToJson

def unwrap_except (e: Except String Lean.Json) : Lean.Json := match e.isOk with
  | true => Option.get! e.toOption
  | false => Lean.Json.bool false

Define new funcs to check that all and any keys in the map match one of my key words:

def is_and_helper (s: String) (f: Lean.Json) : Bool := match s with
  | "And" => true
  | _ => false

def is_and (node : Lean.RBNode String fun x => Lean.Json) : Bool :=
  let contains_and := Lean.RBNode.any is_and_helper node
  let contains_nothing_but_and := Lean.RBNode.all is_and_helper node
  contains_and && contains_nothing_but_and

Use a massive match statement:

def json_to_expr (json : Lean.Json) : Expr := match json with
  | Lean.Json.null => Expr.Wrong
  | Lean.Json.bool b => Expr.PrimitiveLit (Primitive.Bool b)
  | Lean.Json.num n => match n.exponent with
    | 0 => Expr.PrimitiveLit (Primitive.Int n.mantissa)
    | _ => Expr.Wrong
  | Lean.Json.str s => Expr.PrimitiveLit (Primitive.String s)
  | Lean.Json.arr _ => Expr.Wrong
  | Lean.Json.obj o => match is_and o with
    | true =>
      let lhs := unwrap_except ((unwrap_except (json.getObjVal? "And")).getObjVal? "left")
      let rhs := unwrap_except ((unwrap_except (json.getObjVal? "And")).getObjVal? "right")
      Expr.And (json_to_expr lhs) (json_to_expr rhs)
    | false => Expr.Wrong -- Continue for every keyword

Any pointers on how I can do this more cleanly?

[Eric Wieser]

I doubt unwrap_expect is a sensible approach here

[Eric Wieser]

Do you really want invalid json to be treated as bool literals for false?

[Eric Wieser]

You would do much better to propagate the exception, and declare json_to_expr (json : Lean.Json) : Except String Expr

[Eric Wieser]

      let lhs := unwrap_except ((unwrap_except (json.getObjVal? "And")).getObjVal? "left")
      let rhs := unwrap_except ((unwrap_except (json.getObjVal? "And")).getObjVal? "right")
      Expr.And (json_to_expr lhs) (json_to_expr rhs)

would become something like

      let lhs := (<-(<-json.getObjVal? "And").getObjVal? "left")
      let rhs := (<-(<-json.getObjVal? "And").getObjVal? "right")
      return Expr.And (json_to_expr lhs) (json_to_expr rhs)

[Eric Wieser]

(assuming docs4#Lean.Json.getObjVal? is the type I think it is)

[Andrew Wells]

Thanks, I'll clean that up! Is there a better solution to the contains_and && contains_nothing_but_and pattern? Seems like this will get very verbose for more than a few key words

[Andrew Wells]

Hmm, I'm getting invalid use of (<- ...), must be nested inside a 'do' expression

[Eric Wieser]

You need a do after the =>

[Eric Wieser]

You probably need a pure or return before Expr.and too

[Eric Wieser]

Andrew Wells said:

Thanks, I'll clean that up! Is there a better solution to the contains_and && contains_nothing_but_and pattern? Seems like this will get very verbose for more than a few key words

One answer would be to choose a more natural json representation, such as {"_kind": "and", "left": ..., "right":... }