bug in java backend

[grosu]

I know I should try to minimize it, but I have to move on to other things now and I think it is better to report it as is instead of not at all. This code in a file .k crashes with the java backend, but works fine with Maude:

module UP_DOWN

  syntax KLabel ::= "#upKItem" [function]
  syntax KLabel ::= "#upK"     [function]
  syntax KLabel ::= "#upKList" [function]
  syntax KLabel ::= "#down"    [function]

/*                                                                                                                 
All these should be KLabels with the attribute [function]:                                                         
  syntax KLabel ::= "#upKItem" [function]                                                                          
  syntax KLabel ::= "#upK"     [function]                                                                          
  syntax KLabel ::= "#upKList" [function]                                                                          
  syntax KLabel ::= "#down"    [function]                                                                          

but that does not work with the current parser.  So the dirty trick:                                               
*/

  syntax KItem ::= upKItem(KItem)  [function, klabel(#upKItem)]
  syntax KItem ::= upK(KItem)      [function, klabel(#upK)]
  syntax KItem ::= upKList(KItem)  [function, klabel(#upKList)]
  syntax KItem ::= down(KItem)     [function, klabel(#down)]

  syntax KToken ::= #klabel(KLabel)
  syntax KItem  ::= KToken
  syntax KLabel ::= "#ktoken" | "#kapp" | "#klist" | "#kseq"

  syntax KLabel ::= "#klist.cons" | "#kseq.cons"
  rule #klist.cons(K:K,,#klist(Kl:KList)) => #klist(K,,Kl)                           [function]
  rule #kseq.cons(K:KItem,,#kseq(Kl:KList)) => #kseq(K,,Kl)                          [function]

syntax KList ::= #splice(KItem)  [function]
rule #splice(#klist(Kl:KList)) => Kl

  syntax KToken ::= "t1" | "t2"
  syntax KLabel ::= "l1" | "l2"
  syntax K ::= "pgm1" [function] | "pgm" [function]

  rule pgm1 => l1(t1,,t1~>t2~>t1,,t2)
  rule pgm => #down(#down(#down(#upKItem(#upKItem(#upKItem(pgm1))))))
//  rule pgm => #upKItem(pgm1)                                                                                     
//  rule pgm => #upKItem(#upKItem(pgm1))       [anywhere]                                                          
//  rule pgm => #upKItem(#upKItem(#upKItem(pgm1)))                                                                 

  rule #upKItem(T:KToken) => #ktoken(T)                                            [function]
  rule #upKItem(L:KLabel(Kl:KList)) => #kapp(#klabel(L),,#upKList(#klist(Kl)))             [function]

  rule #upKList(#klist(K:K,,Kl:KList)) => #klist.cons(#upK(K),,#upKList(#klist(Kl)))               [function]
  rule #upKList(#klist(.KList)) => #klist(.KList)                                            [function]

  rule #upK(K:KItem ~> K':K) => #kseq.cons(#upKItem(K),,#upK(K'))  [function]
  rule #upK(.K) => #kseq(.KList)                                                     [function]

  rule #down(#ktoken(T:KToken)) => T                                                 [function]
  rule #down(#kapp(#klabel(L:KLabel),,MKl:KItem)) => L(#splice(#down(MKl)))          [function]
//  rule #down(#kapp(#klabel(L:KLabel),,MKl:KItem)) => L(?Kl)                                                      
//  when #klist(?Kl) := #down(MKl)  [function]                                                                     

  rule #down(#klist(.KList)) => #klist(.KList)                                       [function]
  rule #down(#klist(K:K,,Kl:KList)) => #klist(#down(K),,#splice(#down(#klist(Kl))))  [function]

  rule #down(#kseq(.KList)) => .K                                         [function]
  rule #down(#kseq(Ki:KItem,,Kl:KList)) => #down(Ki) ~> #down(#kseq(Kl))  [function]

endmodule

[yilongli]

The problem here is that KLabel is not stored in Poset Context#subsorts. Therefore, calling Context#getCommonSubsorts(Set) with set [KItem, KLabel] fails an internal assertion.

Here is what we have in Context#subsorts right now: [Bag, Bool, TCPError, ListItem, #Bot, KResult, K, #Float, TCPAnswer, #String, KToken, #Int, MySet, MyMap, Set, List, Int, #Bool, Float, Nat, MapItem, KList, Map, Char, MyBag, KItem, Stream, String, BagItem, MyList, Id, SetItem]

@andreistefanescu, could you take a look to check if simply adding KLabel to Context#subsorts is the right fix?

[radumereuta]

But Context#subsorts should contain a set of pairs. What you have there is just a set of declared sorts. Are you sure you looked in the right place?

[yilongli]

You are right. I was actually referring to Context#subsorts.elements.