Incorrect variable sort inference

[denis-bogdanas]

The sort of variables of type Map and Set (at least) is incorrectly inferred.

issue.k:

module ISSUE

configuration <T color="yellow">
                <k color="green"> Start </k>
              </T>

syntax KItem ::= "Start"

rule Start => kListToSet("a", .Set)

syntax KItem ::= kListToSet ( KList,  //a list of some K Terms
                              Set     //the result set
                          )
//Not working:
//rule kListToSet((K:K => .KList),,_, (_     (.Set => SetItem(K) )))

//Working:
  rule kListToSet((K:K => .KList),,_, (_:Set (.Set => SetItem(K) )))

endmodule

issue.prog:
Start

Note the different output for the two versions of the rule.

Maude backend, windows, Git Revision: 5c50846

[grosu]

It is hard to read your code, probably because github's viewer hides certain characters. Why don't you use the triple backtick convention for code, namely

   here is your code

But anyway, if it i just a soft inference problem, why not casting things yourself to the sorts you want?

[denis-bogdanas]

I corrected the example, now it is readable.

Regarding your suggestion, it is just a workaround. Isn't sort inference on the feature list anymore? I don't want to change the whole semantics once in a while because of K bugs.

I would have avoided migrating to this version actually, if I wouldn't need the latex line breaking feature.

[grosu]

Denis, if you expect people to give quick attention to your bug reports, you should make an effort to help them get to point immediately. Right now, I have no chance to understand what the problem is unless I run your example. That means I have to switch to another machine where I run things, etc. You should make your bug report self-contained. What are the two outputs?

[denis-bogdanas]

Thank you for suggestion.

Expected output (the rule "working"):

kListToSet ( .KList , SetItem ( "a" ) )

Actual output (the rule "not working"):

kListToSet ( "a" , .Set )

[grosu]

@radumereuta this is your territory. Looks like a simple bug, where you infer the sort of _ to be K instead of Set.

[denis-bogdanas]

@radumereuta , could you give us a status update on this bug?

[radumereuta]

I'm busy with the new parser, so this is not a priority for me. You can always type your variable and move on.

I will get to this issue when I need to revisit the part of the code responsible for this, but it's not going to be in the near future.

[grosu]

Radu, in general, simple bug fixes have priority. Is this a simple fix or not? If yes, you should fix it then. If not, can you at least tell us what the problem is, why you are not inferring the correct sort for the anonymous variable?

[radumereuta]

This is one of those things in which if I change something, it is very likely to break a lot of definitions, and end up spending close to one week to get it right. It is not a pressing issue, since you could always make the tool do what you want by typing the variable.