runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
451 stars 149 forks source link

Serialize sort parameters in the JSON format #3477

Open tothtamas28 opened 1 year ago

tothtamas28 commented 1 year ago

Right now sort parameters are included in the name field as a flat string: https://github.com/runtimeverification/k/blob/ba7873e2e5daf8ed8be3d010ae8091c832396052/kernel/src/main/java/org/kframework/unparser/ToJson.java#L397

Instead, serialize them in a structured form:

{"node": "KSort", "name": "Foo", "params": [...]}

where params is an optional list of sorts.

This is not a backward compatible change, so it will require incrementing the KAST format version. Before that, consider checking the KAST JSON format for other small inconsistencies.

radumereuta commented 1 year ago

Make a branch with the changes for the front end. Make the changes to the backends to read the serialized format. When the pyk and K front-end accept the new format, we can merge the front end as well.