runtimeverification / mir-semantics

10 stars 3 forks source link

K definition based parser #399

Closed mariaKt closed 2 months ago

mariaKt commented 2 months ago

This PR creates a parser based on the K definition of the MIR semantics. At the moment, it is tested on small examples. The changes made in the semantics are as needed to make them more ammenable to the parser, and are described in the notes.txt included with the parser.

To work on more of the semantics, some additional changes are needed, and these are described in the notes.txt included with the parser. Making these changes and adding more tests, as well as making the parser more usable (so that fewer changes are needed) is ongoing work, and will be part of follow up PRs.