Refactored saw-core-coq #1928
Refactored saw-core-coq #1928
Conversation
… and pis when they are type-checked, in order to make the Coq translation work in cases where these argument types have identifiers that translate to alternate Coq definitions
… information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927
|
@RyanGlScott you must be using a different architecture than I am (I'm on an X86 MacBook), because I can't even compile mbox_gen.v on my machine: it's creating a very large constant for a symbol called "mem_in_use", that is created from a zero initializer in the LLVM globals. It should be a simple fix, but it will be a slightly weird addition to this PR... |
|
I don't think the architecture has anything to do with it, since I'm also using an x86-64 machine (as are the CI runners). The |
… directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW term rather than a giant vector literal
|
Huh. Well, it seems like that was the culprit. |
…ainst emptyBitSet with the new termIsClosed function
|
The |
|
Do we even have any tests for the Coq translator? What we be a good way to organize them, and where should we put them? |
|
The only "tests" I had was to re-run the Makefile in the |
|
I was also reminded of this issue, which seems to be in very similar territory to what this PR accomplishes. Would you say that this PR resolves the issue? |
Huh, look at that, I guess I don't ever say anything new. Yes, this PR resolves that issue. |
eddywestbrook
added
the
subsystem: saw-core-coq
eddywestbrook
added
the
PR: ready to merge
This PR refactors the saw-core-coq translator so that all the local variable information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound. It also fixes #1927 by invalidating the term sharing cache whenever a binder is entered.