kframework / k-legacy

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

Parsing or pretty-printing error? #2097

Open grosu opened 8 years ago

grosu commented 8 years ago

You would expect the following to work:

D:\github\grosu\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static>krun ..\programs\diverse\factorial.simple --pattern "<tasks> T </tasks>"
Search results:

Solution 1:
T:K -->
.TaskCellBag
D:\github\grosu\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static>krun ..\programs\diverse\factorial.simple --pattern "<tasks> .TaskCellBag </tasks>"
[Error] Inner Parser: Parse error: unexpected character '<'.
        Source(<command line>)
        Location(1,22,1,23)

┆Issue is synchronized with this Asana task

radumereuta commented 8 years ago

I tried it this way:

c:\work\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static>krun ..\programs\diverse\factorial.simple --pattern "<tasks> .Bag </tasks>
Search results:

Solution 1:
Empty substitution

Clearly there is a misunderstanding between parsing and pretty printing, but I'm not sure which one is wrong.

cos commented 7 years ago

It seems that parsing is wrong. .TaskCellBag is generated by the configuration expander, so it should be visible during the parsing of patterns as well. I haven't seen any sub-sorting between .Bag and .TaskCellBag so it's curious it works that way. @xianzezhan, I suggest printing the module used for parsing the pattern and checking that is contains the production for .TaskCellBag.

xianzezhan commented 7 years ago

public Rule parsePatternIfAbsent(FileUtil files, KExceptionManager kem, String pattern, Source source) { return cachedParsedPatterns.computeIfAbsent(pattern, p -> new Kompile(kompileOptions, files, kem).parseRule(this, p, source)); }

result = parser.parseString(b.contents(), START_SYMBOL, Source.apply(source), startLine, startColumn); in performParse(DefinitionsParsing.java) this call triggers the error when b.contents()==" .TaskCellBag ".

By the way, could you tell me which module should I look for checking productions? When I try to use system.put.println() in ParseInModule, krun throws errors like [Error] Outer Parser: Encountered <ID_KLABEL>. Was expecting one of: ["("]