This repository has been archived by the owner on Jun 9, 2021. It is now read-only.
Recursors #27
Merged
Recursors #27
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
added 30 commits
September 9, 2017 12:58
…lations back into primitives, but added additional "__def" forms and "__eq" axioms asserting the equality of each primitive to its "__def" form
…f to not use patterns
…by the Cryptol translation
…ith primitives that happen to be types; changed all of the SAW internals that deal with types that used to be primitive data types to handle this change
…ype and recursor stuff, to a new module called CtxTerm
…s, though it does not yet typecheck...
…rgsLength in SCTypeCheck when a constructor or datatype has the wrong number of arguments
…heses around the arguments of applications
…mulator, Conversion engine, and related machinery to work with this change, including adding a VBoolType value for the simulator
…ecords) instead of the old ones
…es as constructor applications
…t be distinguished from applications of the Zero and Succ constructors
…es will eventually handle...
…objects that are local to a given module
# Conflicts: # prelude/Prelude.sawcore # src/Verifier/SAW/Recognizer.hs # src/Verifier/SAW/Simulator/Prims.hs
Currently this is implemented by calling rewriteSharedTerm with a flipped version of the original rewrite rule. However this would fail if the original rewrite rule had variables on the left-hand-side that did not occur on the right. It would be better to have a more flexible alternative to scReduceRecursor, so that we could directly instantiate the recursive calls the way we want.
…to use these instead of looking through all ctors and datatypes in the entire module map
|
This branch is almost completely ready to merge into saw-script. But there are still some test suite failures, specifically some in llvm-verifier. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
This branch includes the following list of changes:
Expanded term type, including recursors and a new record type
The new file CtxTerm.hs, which is used to type-check and reduce recursors
A new type-checker infrastructure that unifies SCTypeCheck.hs (for typed terms) and Typechecker.hs (for untyped terms)
Updated the TH in ParserUtils.hs to deal with the fact that the new type-checker requires a SharedContext (and so cannot happen at TH time)
Replaced the scModule field in SharedContext with scModuleMap, a HashMap of all the loaded modules in the current SharedContext
A refactoring of the Term pretty-printer that used to be split across SharedTerm.hs and Pretty.hs, but is now contained in Pretty.hs