JSON parsing

Stream: general

[Alexandre Rademaker]

I didn't find in https://reservoir.lean-lang.org any JSON parser that could report for me more than just the error (Except String Lean.Json) but also the position in the string where the error was found.

Does anyone know about a JSON parser for Lean that could be more informative for validation?

[Henrik Böving]

If you look at the impelemtnation of src#Lean.Json.parse you'll see that it does internally know where the offset is so you can write a very thing wrapper similar to parse itself around the internals to extract that information if you want

[Alexandre Rademaker]

Actually, after your pointer, the problem is not in the parser... but in the fromJson?

structure Value where
  description : String
  value       : Float
  unit        : String
 deriving Lean.FromJson, Lean.ToJson, Repr

structure Product where
  description   : String
  material_type : String
  provenance    : String
  energy_source_equipment : String
  conditions : List Value
  reactants  : List Value
  solvents   : List Value
 deriving Lean.FromJson, Lean.ToJson, Repr

structure Annotation where
  input  : String
  output : List Product
 deriving Lean.FromJson, Lean.ToJson, Repr

def test (filename : System.FilePath) : IO (Except String (List Annotation)) := do
  let txt ← IO.FS.readFile filename
  pure $ Lean.Json.parse txt >>= Lean.fromJson?

The output is

Except.error "Annotation.output: Product.conditions: Value.value: Expected a number or a string 'Infinity', '-Infinity', 'NaN'."

I need to understand how the errors are propagated in a nested structure. But if Lean.Json.parse (s : String) : Except String Lean.Json returns a Lean.Json, I believe I lose the offset information of the original string.