qcert icon indicating copy to clipboard operation
qcert copied to clipboard

Improvements to JSON support

Open jeromesimeon opened this issue 8 years ago • 1 comments

JSON is used both at run time (to parse input data and produce outputs), and at compile time (notably generation of Cloudant Map/Reduce views).

The JSON support is split in two parts, with OCaml used for parsing/serialization, and Coq used for conversion operations between internal data structures (e.g., data/rtype) and JSON.

Work items include:

  • [ ] On the OCaml side, remove ad-hoc parsers/serializer and rely instead on a well supported OCaml library such as yojson
  • [x] On the Coq side, show round-tripping properties for the conversions between JSON and the data model (data)
  • [ ] There is only a way to import RTypes from JSON, not the other way around. Generally speaking this part of the code might be worth reviewing/extending.
  • [ ] The JSON ast in Coq has a special 'jforeign' node that is used to represent foreign data. It is unclear if it is the right approach, and it might be better to handle the serialization from foreign data to JSON in a way that the AST is pure JSON, but an attempt to do that showed it would require further refactoring which may or may not be useful.

jeromesimeon avatar Aug 22 '17 19:08 jeromesimeon

And example of problem with JSON support can be found in Issue #51 and Issue #13.

jeromesimeon avatar Aug 26 '17 13:08 jeromesimeon