AddBrackets pass in C++ unparser#334
Conversation
| std::ifstream iassocs(argv[1] + std::string("/assoc-att.txt")); | ||
| std::ifstream icomms(argv[1] + std::string("/comm-att.txt")); | ||
| std::ifstream icolors(argv[1] + std::string("/color-att.txt")); | ||
| std::map<std::string, std::set<std::string>> priorities, leftAssoc, rightAssoc; |
There was a problem hiding this comment.
What are these big tables here? Any way we can load them from the actual information in domains.k and kast.k instead?
There was a problem hiding this comment.
Maybe? it's kinda tricky though. These tables contain the metadata for the stuff that is defined in kast.k and thus doesn't get translated by ModuleToKORE, like kseq, inj, dotk, \or, \and, etc. I'm not sure how I can get this information from the frontend to the backend when there aren't symbols in the definition that I can automatically insert attributes for. I'd like to! I'm just not sure how to go about it. Do you have an idea?
virgil-serbanuta
left a comment
virgil-serbanuta
left a comment
There was a problem hiding this comment.
Thanks to @traiansf for explaining a lot of things in this PR to me.
This looks good, but I still have a few things to understand, so I'll approve a bit later.
| * | ||
| * returns: EMPTY if there are terminals on both sides of this nonterminal | ||
| * BARE_LEFT if there is a terminal only on the right of this nonterminal | ||
| * BARE_LEFT if there is a terminal only on the left of this nonterminal |
| return true; | ||
| } | ||
| if (data.terminals.at(innerName) == "0") { | ||
| return false; |
There was a problem hiding this comment.
How can this line be reached?
There was a problem hiding this comment.
it's reached if you have a symbol that has no terminals and one nonterminal.
There was a problem hiding this comment.
Would that mean that you have an 'inj'? And, if so, would it be filtered out by the if in addBrackets?
Even if that's the case, I'm not saying that you should remove this if+return, I'm just trying to understand the code better.
There was a problem hiding this comment.
No, not all productions with zero terminals and one nonterminal are subsort productions in K.
| /** | ||
| * Compute the right capture of a pattern. | ||
| * | ||
| * If you were to unparse the AST of a term without any parentheses as a |
There was a problem hiding this comment.
I coudn't find where we check that "P" below has a terminal. Other than that, would the following text be more clear?
- If you were to unparse the AST of a term without any parentheses as a
- sequence of terminals, start from the point where a particular pattern P
- (the one at "position" in outer) ends and proceed right until you
- reach the first terminal that is part of a pattern Q (directly) such that
- Q is a parent of P. Then Q would be the right capture of that pattern.
- Not all terms have a right capture; for example, the right capture of the
- top term in an AST does not exist.
Also, do we always have terminals between non-terminals? If not, then this description is likely wrong.
| leftAssoc["\\or"].insert("\\or"); | ||
| leftAssoc["\\rewrites"].insert("\\rewrites"); | ||
| rightAssoc["\\rewrites"].insert("\\rewrites"); | ||
| priorities["\\exists"].insert("\\implies"); |
There was a problem hiding this comment.
btw, unless we're need this to work with older compilers, you should be able to do
priorities["\\exists"] = {\\implies", "\\or", "\\and", "\\equals", "\\floor", ...}
(I'm not sure how readable a map initializer list would be, so I only suggested a set one).
| return false; | ||
| } | ||
| Fixity innerFixity = getFixity(innerComposite->getConstructor(), data); | ||
| if ((innerFixity & BARE_RIGHT) && rightCapture != nullptr) { |
There was a problem hiding this comment.
This if (and the one after, but they are the same thing) was somewhat tricky to understand, so if you'd add an explanation of why it works, it would probably help. Suggestion (the details are probably inaccurate):
"
We are not in one of the cases where we know it's safe to skip adding parentheses.
At this point we know that outer does not have higher priority than inner, so, if the
inversePriority bool is true, then we must have added parentheses somewhere else
(e.g. around outer), so we don't need to add some extra ones here. Otherwise we
add some parentheses around inner because we don't want inner's right
operand to be parsed as a direct child of rightCapture.
"
There was a problem hiding this comment.
I mean, I have no idea how this algorithm works, I just know it does. Somewhere out there on the internet is a master's thesis done by someone in Europe whose algorithm eventually became part of the Maude implementation, from which we took it (and believe me, it was wholly impenetrable to understand in that form). But without access to that paper, I couldn't begin to explain why this particular incantation is the one we use here.
There was a problem hiding this comment.
Ah, ok. Well, I tried to understand it, so that's why I asked most of these questions...
| return true; | ||
| } | ||
| if (data.terminals.at(innerName) == "0") { | ||
| return false; |
There was a problem hiding this comment.
Would that mean that you have an 'inj'? And, if so, would it be filtered out by the if in addBrackets?
Even if that's the case, I'm not saying that you should remove this if+return, I'm just trying to understand the code better.
| return false; | ||
| } | ||
| Fixity innerFixity = getFixity(innerComposite->getConstructor(), data); | ||
| if ((innerFixity & BARE_RIGHT) && rightCapture != nullptr) { |
There was a problem hiding this comment.
Ah, ok. Well, I tried to understand it, so that's why I asked most of these questions...
This reverts commit 1212264.
This reverts commit e5fc2ee.
3 participants
This code is based on
kernel/src/main/java/org/kframework/unparser/AddBrackets.javain kframework/k. It adds feature parity with respect to brackets to thekprinttool which powers unparsing in llvm-krun and gdb.