search

runtimeverification / k

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

Document munging process for `symbol(_)` attributes #4025

Open tothtamas28 opened 8 months ago

tothtamas28 commented 8 months ago

Characters that are not valid in a KORE identifier (i.e. anything except for digits, letters, - and ') included in the symbol attribute value will be encoded in the corresponding KORE symbol name.

E.g.

symbol(_|->_)

becomes

Lbl'UndsPipe'-'-GT-Unds

in KORE.

In order to ensure that the attribute value (and hence the KLabel of the production) and the KORE symbol are as close to each other as possible (i.e. to make sure the only difference is the Lbl prefix in KORE), consider emitting a warning on such attribute values.

This can be taken one step further by also enforcing a naming convention, e.g. kebab-case (then the symbol would also be a good value for the smtlib attribute, so perhaps we could even drop that one).

A large number of symbols in k-distribution/includes do not conform to this restriction, so those should be cleaned up as well.

Baltoli commented 7 months ago

This will probably be too noisy to implement practically when we migrate away from klabel(_), but we should definitely document how the munging algorithm works and when it will apply.