Overhaul NNFParser #367
Merged
Overhaul NNFParser #367
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
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This commit addresses all three issues. This is a combination of 23 commits: Introduce FixpointParser which will serve as the common superclass of NNFParser/FQParser Pull 'fixpoint' up to FixpointParser Pull matchedParen and tok up to FixpointParser Pull lowerId, upperId up to FixpointParser class Consistently name hThing Place parens in symSort (not its senders) for consistency with LF Use naming for hCstr consistent with LF Inline cstrAnd for consistency with LF Parenthesize hBind consistently with LF Inline #forall, #exists for consistency with LF [cosmetic] Add "tag" TODO Use naming for hCstr consistent with LF Use naming for hPred consistent with LF Inline predAnd for consistency with LF Inline kappaApp, use kvSym for consistency with LF Clear up confusion between pred, hPred and decidablePred Inline #constant for consistency with LF Rename qualif to hQualifier for consistency and to avoid confusion with F.qualifierP Inline #constraint for consistency with LF Rename var to hVar for consistency with LF Pull common (i.e. non-Horn) elements from NNFParser to FixpointParser Remove #matchedParen in favor of consistent use of RefinementExpressionParser Route uses of RefinementExpressionParser through DecidableRefinement
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.
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This PR addresses all three issues.