You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
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.
The text was updated successfully, but these errors were encountered:
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:
data
)The text was updated successfully, but these errors were encountered: