Emit table of return sorts #911
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Baltoli
force-pushed
the
return-sort-table
branch
from
cf8cde1
to
210f819
Compare
Baltoli
requested review from
gtrepta,
Robertorosmaninho,
theo25 and
dwightguth
Baltoli
changed the title
Robertorosmaninho
approved these changes
Dec 1, 2023
I'd be very surprised if this caused any kind of meaningful performance change; the new code-generation step is one new O(symbols) step among a set of similar ones, and the data getting emitted is only a single pointer for each symbol (the sort names are already present in the binary). |
rv-jenkins
pushed a commit
that referenced
this pull request
Dec 1, 2023
A common pattern in the backend's code is to do the following: ```c++ std::ostringstream out; pattern->print(out); do_something(out.str()); ``` In #911, we introduced a helper function `ast_to_string` that wraps this common pattern up; this PR follows up that change by mechanically refactoring the remainder of the codebase to use the helper. After the change, the above code would be: ```c++ do_something(ast_to_string(*pattern)); ``` Each commit in the PR (bar the first) applies the same conceptual refactoring to a single file; no actual behavioural changes other than in the first commit are implemented, and so this should be an easy PR to review. In future work, I'd like to further clean up this code and make better use of `fmt` across the codebase, but for now this is a useful self-contained change to make.
rv-jenkins
pushed a commit
that referenced
this pull request
Dec 18, 2023
This PR adds a new feature to the backend's binding API that allows for function symbols to be evaluated on a set of AST pattern arguments, with the result returned as a pattern also. This is motivated by the proof generation project; the execution trace format generated by the backend to summarise a concrete execution can contain the labels and arguments for function call events, but not the functions' return values without breaking tail-call optimisation. Most of the prerequisite work for this PR was done in #908 and #911; the actual changes here are quite small: * Adds a sort-aware term-to-pattern reification method that uses the new `rawTerm{}` wrapper. * Marshals arguments and returns between pattern and term level in the core bindings API. * Adds a test case demonstrating a few simple cases for this feature; as ever the bulk of the testing ought to be performed in Pyk.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Part of: #905
In #905, we are implementing a Python binding for the backend's function evaluator: given a function label and list of argument
Patterns, construct runtime terms for the arguments, evaluate the function with the given label, and return the result as an AST pattern.To safely reify the runtime term produced by the function call to an AST pattern, we need to know its sort (so that the machinery in #907, #908 can be used correctly). In some places in the bindings, we have to require that callers provide a sort when reifying terms back to patterns. However, when calling a function, the label of the function determines precisely the correct sort to use.
This PR emits a new table of global data into compiled interpreters that maps tags to declared return sorts, along with a function that abstracts away indexing into this table. This change is similar to (but simpler than) an existing table of argument sorts for each symbol that we already emit.
Testing is handled by binding the new function to Python.