Pyk: KCFG stores aliases for nodes #2647
Conversation
nishantjr
force-pushed
the
pyk-kcfg-aliases
branch
from
6cd3e78 to
fdba4e8
Compare
|
@ehildenb I went for |
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
pyk/src/pyk/kcfg.py
Outdated
| @@ -351,21 +395,25 @@ def _short_label(label): | |||
|
|
|||
| return graph.source | |||
|
|
|||
| def _resolve_all(self, short_id: str) -> List[str]: | |||
| return [node_id for node_id in self._nodes if compare_short_hashes(short_id, node_id)] | |||
| def _resolve_all(self, id_like: str) -> List[str]: | |||
There was a problem hiding this comment.
I'd call this _resolve_hash, and keep its old behavior.
Then _resolve_or_none can be implemented as follows.
- If
id_likeis a hash, then delegate to_resolve_hash, and raise an exception if there are multiple results. - Otherwise, we have an alias. If it starts with
@, drop the first character. - Try to resolve the alias.
As a result, @ is optional, and can be used to enforce strings to be resolved as aliases (as something starting with @ is never a hash). So for example
abcdis resolved as a hash@abcdis resolved as aliasabcdhellois resolved as aliashello@hellois resolved as aliashello
Optionally, we can also refine _resolve to give a more specific error message if resolution fails:
- If
id_likeis a hash:Unknown node hash: ... - Otherwise:
Unknown alias: ...
What do you think?
There was a problem hiding this comment.
I like the refactoring. But wasn't the whole point of adding the @ to avoid confusion between the two?
There was a problem hiding this comment.
But wasn't the whole point of adding the @ to avoid confusion between the two?
My point is that if id_like is not a valid hash, we can omit the @, because we know we have an alias. But this is just a small usability improvement.
In any case, the input should be validated to be either a hash or an alias (if @ is optional, the latter does not have to be checked).
…untimeverification#2042) * haskell-backend/src/main/native/haskell-backend: 9247a969d - Prune unsatisfiable state with unifyStringEq (runtimeverification#2647) * haskell-backend/src/main/native/haskell-backend: 797767163 - modified matchEquation to accept new equation format (runtimeverification#2688)
short_idfunction that returns the alias if present, or else the shortened hash.pretty_printandto_dotuseshort_ids instead ofshorten_hash.