runtimeverification / mir-semantics

10 stars 3 forks source link

Added ways to handle K lists, along with temporary tests. #403

Closed mariaKt closed 2 months ago

mariaKt commented 2 months ago

This PR adds a way to handle K lists The function _parse_mir_klist_json is able to create a K list of elements of Sort sort, out of the provided json.

There needs to be a way to identify the element sort though. I have provided two alternatives.

  1. We can also encode this in the productions. For this to work, the K lists need to be in a separate production, as in the example below:
syntax TestSort2 ::= testSort2(MIRInt, MyList)     [group(mir), symbol(testSort2)]
syntax MyList ::= List [group(mir-klist-MIRInt)]

We can then use the new group identifier mir-klist to identify a klist, followed by - and the element sort, as shown. Then, the information is tokenized and passed to _parse_mir_klist_json.

  1. To support productions that include the List sort directly, e.g.
syntax TestSort1 ::= testSort1(MIRInt, List)     [group(mir), symbol(testSort1)]

I have made changes to allow for calling the new function _parse_mir_klist_json directly in _parse_mir_nonterminal_json, where the information about the processed production (thus the expected argument sorts) will be known. I have added a function intended to add any hardcoded information necessary (production symbols, argument positions, etc) that will be mapped to sorts.

Both paths have been tested to work, albeit with two random Sorts TestSort1 and TestSort2 (found in ty.k) that I only added for that reason. Please keep in mind that when the List sort is properly used as part of the semantics, these can be removed.

mariaKt commented 2 months ago

Thank you. I agree, I went ahead and removed approach 2, and it can be added back if needed. I also added a description of the new group tag in the parser documentation. Since you are OK with it, let's merge this now, so the new path is tested as part of CI and is not broken unintentionally. Once other rules exist that exercise this path, the TestSort2 rule and test directory will be entirely useless and should be removed.