Respect the identity of variables, Part 1 #1830
Merged
Conversation
This file contains hidden or 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
ttuegel
force-pushed
the
refactor--VariableName
branch
from
12e78d1 to
d079c24
Compare
The goal of refactoring is to replace type Variable and the wrappers around it with type Variable1, and rename the latter. Note that this will make the SortedVariable class obsolete because all variables will carry a sort field at the top level; therefore, we will modify the SortedVariable class to carry the intermediate definitions we need for refactoring, and remove the class in the end.
ttuegel
force-pushed
the
refactor--VariableName
branch
from
d079c24 to
2ed1195
Compare
ttuegel
requested review from
ana-pantilie,
andreiburdusa and
traiansf
and removed request for
traiansf
traiansf
approved these changes
May 27, 2020
| :: ElementVariable variable1 | ||
| -> Identity (ElementVariable variable2) | ||
| trElemVar = sequenceA . (<*>) (elemVar adj') | ||
| trSetVar = sequenceA . (<*>) (setVar adj') |
There was a problem hiding this comment.
why did you write the signature for trElemVar but not for trSetVar?
| Just (SetVar setVar') -> setVar' | ||
| _ -> setVar | ||
| subst = TermLike.mkVar <$> rename | ||
| let rename = |
There was a problem hiding this comment.
I can't help notice that the complexity of the code has grown by a non-trivial margin. From 10 lines with easy-to-read-and-write code, we got to more than 30 of code with lenses
There was a problem hiding this comment.
Yes, it's unfortunate, but temporary: the lenses are a consequence of switching between representations of variables, and after I finish the next part of the changes, then all the lenses go away.
ana-pantilie
approved these changes
May 27, 2020
andreiburdusa
approved these changes
May 27, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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 pull request begins to fix #1545. Most of the changes in this pull request are simply consequences of the changes in
Kore.Syntax.Variable, so I recommend starting there.Summary
Variable1which carries a variable name and sort, representing an occurrence of a variable in a Kore pattern. UnlikeVariable, this type is parameterized in the variable name type.VariableNametype, representing the basic syntax of variable names.ElementVariableNameandSetVariableNamewrappers.SomeVariableName, which may be anElementVariableNameor aSetVariableName.AdjSomeVariableName, which represents mappings preserving the element- or set-ness of a variable. The name of the type owes to the adjunction betweenSomeVariableNameandAdjSomeVariableName. This is not as complicated as it sounds, but it bears close attention. Most of the changes in the pull request are related to introducing this type.NamedVariablefor variables, representing the isomorphism between_ VariableandVariable1 _.In the follow-up to this pull request,
Variable1 _will replace_ Variableand theNamedVariableclass will be obsolete. I wanted to get this in as a separate pull request because I think addingAdjSomeVariableNameis significant in its own right.Reviewer checklist
stack test --coveragestack haddock