search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

parsing cells in cell fragment terms #1842

Open daejunpark opened 8 years ago

daejunpark commented 8 years ago

For example, suppose <x> cell consists of <a>, <b>, and <c> cells.

syntax KItem ::= foo(XCellFragment)
rule foo(A:ACell B:BCell) => .

The above rule fails to be parsed, because Cell is not sub-sort of XCellFragment. But if the sub-sort relationship is added, parsing takes unreasonably long.

dwightguth commented 8 years ago

Doesn't cell fragments have its own concrete syntax that is different from this?

bmmoore commented 8 years ago

cell fragments in K3 just had the syntax of bags, I think this is the concrete syntax we want to give them.

What subsort relationship are you adding?

daejunpark commented 8 years ago 
syntax XCellFragment ::= Cell  [avoid]
grosu commented 8 years ago

What is Cell? It does not appear in your original grammar, where you only had ACell and BCell. I still think that we are making things more complicated than they need to be by keeping track of sorts here at all. I would just assume that all cell fragment labels can take any arguments of sort K and produce something of sort K, and then resolve errors due to the too permissive syntax afterwards. In same sense the same like in K3, but with K instead of Bag.

daejunpark commented 8 years ago

@bmmoore, I assigned it to @radumereuta, assuming that you are not working on this.

bmmoore commented 8 years ago

Cell is a sort from kast.k which is used for defining the nice front-end syntax of uncompleted cells. For more than one cell you actually want the name Bag (which is poorly named, I just opened #1942 to rename it to Cells). We should never refer to that in ordinary rules generated by orginary compiler passes, but that seems like the right way to go inside of RuleGrammarGenerator where the complete sugared front-end syntax is being calculated from the input Module.

grosu commented 8 years ago

I agree with Cells over Bag, but I am not sure that we even need to complicate ourselves with Cells at all. We want to allow any operations to be structural, not only cells. And once they are structural, they can take any arbitrary number of arguments and of any sorts that can ever appear underneath them. That is just yelling for one generic sort for their arguments and results, which can be used anywhere, which is what K is for. However, if we are very close to something that works, I would not want to make the transition to 4.0 depend on making the above crystal clear in the implementation. But I'd like to avoid definitions that are very hard to explain to students, especially by other instructors than me (keep it in mind that Elsa will teach CS422 next semester).

grosu commented 8 years ago

Guys, please, take care of this!!! @radumereuta , @bmmoore . It does not matter at this stage what I said above, all it matters is to make it work, so our tutorial definitions pass. Once done, I will get back to this and make sure it is done properly, in terms of theory at least. Please discuss it some more if needed.

@bmmoore : are you working on this or not? Either way, can you concisely tell us what you think would work here, with minimal, hopefully no changes to definitions?

@radumereuta : is there an inherent problem with the parser in terms of performance if we do what @daejunpark recommended, or it is just a matter of fixing some bugs?

daejunpark commented 8 years ago

@radumereuta can you fix this? This seems to be one of road-blockers for our milestone, and I think you are best to fix this issue.

grosu commented 8 years ago

Has this been fixed? I just commented the additional production out below in simple untyped and it seems to work (ktest passes):

  // TODO(KORE): drop the additional production once parsing issue #1842 is fixed
//                 |  (Map,K,K)

@radumereuta , please let us know if this has been fixed and if yes, close this issue.

radumereuta commented 8 years ago

I've been looking over this, and most of the code that handles CellFragments, is written by @bmmoore (parsing and desugaring after that). I think he is the most appropriate to fix it completely since he has the best understanding. I can have a look, but it's going to take me more than a day before I can understand all the details.

Other things: - the issue should not be closed, since there are more aspects to this issue. Some of them seem to work though, so it is ok to delete the comment in simple, but the problem in the original post is not fixed.

Details for the future: there seems to be added a production: XCellFragment ::= Cell, but to parse the first example, the reverse is needed: Bag ::= XCellFragment. Addingi this rule is not enough though, since a CellFragment can be a host to other cells, but as well be stored in other cells/CellFragments. How to do this without creating circularities in sorts? I don't know yet.

daejunpark commented 8 years ago

This issue is still not fixed. See KOOL: https://github.com/kframework/k/pull/2113/files#r50074538