This PR makes updates to the K AST, in accordance with the changes in the SMIR AST and generated json output (PR). I also proactively added the
"crates_functions": [ [id, "symbol"] ]
field in the json output and the K AST and parse it.
The parser script has been updated to handle a reduced version of the generated json output from panic.rs, due to the fact that the output was too long to manually write the reference K file. I can continue to handle more cases of different K sorts in a next PR, since a lot are going to be quite similar.
Finally,
a few (mechanical) changes to the execution semantics were necessary, due to the change from Const to MirConst. These should be seamlessly transferred to the memory_impl branch.
this version of the execution semantics rely on the representation of Types where the type is still materialized (ty(Int, TyKind), so I added it back to the ty constructor to make the semantics build. We still plan to remove it, and have the types being interned:
Ty ::= ty(Int)
We will do that with the next iteration of the execution semantics, which ignore the TyKind.
This PR makes updates to the K AST, in accordance with the changes in the SMIR AST and generated json output (PR). I also proactively added the
field in the json output and the K AST and parse it.
The parser script has been updated to handle a reduced version of the generated json output from panic.rs, due to the fact that the output was too long to manually write the reference K file. I can continue to handle more cases of different K sorts in a next PR, since a lot are going to be quite similar.
Finally,
ty(Int, TyKind), so I added it back to thetyconstructor to make the semantics build. We still plan to remove it, and have the types being interned:We will do that with the next iteration of the execution semantics, which ignore the
TyKind.