runtimeverification / k

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

`KVariable` class should store sort directly, strip attributes #3120

Open ehildenb opened 1 year ago

ehildenb commented 1 year ago

We are trying to strip attributes out of the KInner class. Currently, the KVariable uses the KAtt class to store sort information about variables. But this is unfortunate, because at least in pyk, we don't have a global ordering on KAtt, so comparing terms that contain these becomes harder. Here (https://github.com/runtimeverification/pyk/pull/167), we remedy this in pyk, but find that there are several attributes carried by KVariable that need to be just stripped out to remove attributes from the KVariable:

If these attributes are compile-pipeline internal, then they should be stripped after the stage that makes use of them, rather than passed on to other tools further down (like pyk library).

Slack discussion: https://runtimeverification.slack.com/archives/C7E701MFG/p1674584350855989

Another part of the discussion was about what to do with Location/Source attributes. These could be optional attributes of the KInner class.

ehildenb commented 1 year ago

LLVM backned is not using any attributes on terms. Pretty sure haskell backend is not as well.

Likely these attributes are just used for informational purposes in frontend.