Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Backend refactor #928

Merged
merged 6 commits into from
Oct 13, 2020
Merged

Backend refactor #928

merged 6 commits into from
Oct 13, 2020

Conversation

robdockins
Copy link
Contributor

This PR untangles the Backend class and it's implementation from the Eval module subtree. This separates the concerns of different base-type value representation from the concerns of the evaluator proper and it's datatypes.

This PR consists almost entirely of file moves and module import changes, and other small code motion required to get things to compile again. The largest change that isn't just a file move was the splitting of Cryptol.Eval.SBV into two parts, similar to how the other backends were already split.

This sets the stage for reuse of the Backend class in other settings (e.g., saw-core).

@robdockins
Copy link
Contributor Author

At this point the Backend module subtree is nearly independent of Cryptol. The things that still tether the backend modules to Cryptol are the EvalError datatype and the various EvalOptions settings. It would be fairly easy to sever the options types, I think, but the EvalError type is baked into the evaluation monads in various places.

Copy link
Contributor

@brianhuffman brianhuffman left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks great; thanks for doing this! I'm excited about how much code reuse we should be able to get by using this part of the Cryptol API within saw-core.

of the `Backend` class into a separate module tree that doesn't depend
on the `GenValue` type or the evaluator.

The code doesn't compile at this point.
that created the `Backend` module tree.

The main change here is that the `Cryptol.Eval.SBV` module was split
into two, similar to how the concrete and What4 evaluators were already
split.  Various other small bits of code are rearranged to detangle
module dependencies.
@robdockins robdockins merged commit 6b9cc9a into master Oct 13, 2020
robdockins added a commit to GaloisInc/saw-core that referenced this pull request Oct 13, 2020
robdockins added a commit to GaloisInc/saw-script that referenced this pull request Oct 13, 2020
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this pull request Oct 16, 2020
The `backend-refactor` PR renamed some cryptol modules.
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this pull request Oct 16, 2020
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Oct 16, 2020
The `backend-refactor` PR renamed some cryptol modules.
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Oct 19, 2020
The `backend-refactor` PR renamed some cryptol modules.
robdockins added a commit to GaloisInc/saw-script that referenced this pull request Oct 23, 2020
@RyanGlScott RyanGlScott mentioned this pull request Jan 27, 2022
@RyanGlScott RyanGlScott deleted the backend-refactor branch March 22, 2024 14:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants