runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Exporting `get_requires` utils function #1056

Closed Robertorosmaninho closed 6 months ago

Robertorosmaninho commented 6 months ago

This PR introduces a new file, utils.py, which should contain auxiliary functions that need to be converted from and to llvm but don't set any field on an object.

In this context we're using a function from llvm backend's pattern_matching.cpp to avoid reimplement it in Python. This function is exported as Pyhton binding in this PR, and therefore, the current PR can only be merged after we merge the LLVM Backend one.

tothtamas28 commented 6 months ago

In this context we're using a function from llvm backend's pattern_matching.cpp to avoid reimplement it in Python

Hasn't there been a plan to eventually implement it in pyk though?

Robertorosmaninho commented 6 months ago

In this context we're using a function from llvm backend's pattern_matching.cpp to avoid reimplement it in Python

Hasn't there been a plan to eventually implement it in pyk though?

That was revisited, and we decided to move in another direction to avoid having the exact implementation in two different places when we could just export them.

Robertorosmaninho commented 6 months ago

Please add a unit test for this feature. That will also block merging this PR until the binding becomes available.

I've just added a unit test, and I'm waiting for this PR to be approved