Java backend doesn't know how to put back kresult in to a HOLE in this case

[liyili2]

I have the following definition:

module TEST

     configuration <k> $PGM:K </k>

     syntax KItem ::= "toKRList'" "(" SubKRList ")" [strict]

     syntax KItem ::= toKRList(List)

     syntax KResult ::= krlist(List)

     syntax DeclType ::= Prototype(K, K, Bool)
          [strict(1, 2)]

     //might not need this after accosicate matching 
     syntax SubKRItem ::= sItem(K) [strict]
     syntax SubKRList ::= List{SubKRItem,"ss::"} [strict]
     syntax SubKRList ::= toSubKRList(List) [function]

     syntax SubResult ::= srItem(K)
     syntax SubKRItem ::= SubResult
     syntax KResult ::= SubResult

     syntax KItem ::= "abc" | "start"
     syntax Type ::= "skip"
     syntax KResult ::= "good" | Type | Int

     rule toSubKRList(.List) => .SubKRList
     rule toSubKRList(ListItem(K:K) L:List) => sItem(K) ss:: toSubKRList(L)

     rule sItem(V:KResult) => srItem(V) [structural]

     rule toKRList(L:List) => toKRList'(toSubKRList(L)) ~> krlist(.List)
          [structural]

     rule toKRList'((srItem(V:KResult) ss:: S:SubKRList) => S) 
          ~> krlist(_:List (.List => ListItem(V))) 
          when getKLabel(V) =/=KLabel 'krlist
          [structural]
     // Somewhat contrived feature: nested lists are flattened.
     rule toKRList'((srItem(krlist(L:List)) ss:: S:SubKRList) => S) 
          ~> krlist( _:List (.List => L)) 
          [structural]
     rule toKRList'(.SubKRList) => .
          [structural]

     rule abc => skip [structural]

     rule start => Prototype(abc,toKRList(ListItem(1) ListItem(2) ListItem(3)),true)

     rule Prototype(T:Type, krlist(L:List), true) 
          => good [structural]

endmodule

After I run the program "start", I get the result in Maude backend as:

<k>
    good
</k>

However, Java backend gives me the result of:

<k>
    krlist ( ListItem ( 1 ) ListItem ( 2 ) ListItem ( 3 ) ) ~> Prototype ( 
      skip , HOLE , true )
</k>

We can easily see from the definition that the first two arguments of the constructor "Prototype" will be taken out from holes and be evaluated to certain kresults. However, after the java backend evaluate the second argument to a kresult, it does not know how to put it back to the second hole in Prototype constructor.

[liyili2]

Eventually, I found that, once I change the

syntax KResult ::= krlist(List) 

to

     syntax KResult ::= KRList

     syntax KRList ::= krlist(List)

the definition will run programs properly.

[grosu]

This is very very strange. Can somebody explain what's going on here?

[yilongli]

In the Java backend, the cooling rule that is supposed to work is compiled as: rule <generatedTop><k>_135:KItem ~> (# 'Prototype(_136:K,, HOLE,, _137:Bool))(.KList) ~> _134:K</k>_133:Bag</generatedTop> => <generatedTop><k>'Prototype(_136:K,, _135:KItem,, _137:Bool) ~> _134:K</k>_133:Bag</generatedTop> requires [isKResult(_135:KItem)] ensures []

Therefore, it fails to match _135:KItem with krlist(...) which is declared as a KResult but not KItem.

In the past, this caused me some problem in test generation. I worked around by compiling this rule into rule <generatedTop><k>_135:KResult ~> (# 'Prototype(_136:K,, HOLE,, _137:Bool))(.KList) ~> _134:K</k>_133:Bag</generatedTop> => <generatedTop><k>'Prototype(_136:K,, _135:KItem,, _137:Bool) ~> _134:K</k>_133:Bag</generatedTop>, whenever a special flag is passed to kompile.

I didn't think about injection/projection at that time, so I am not sure about the implication of the above solution. Let me think for a while. At the same time, @andreistefanescu any suggestion?

[andreistefanescu]

I'm not sure how this works in Maude. I think KResult should be subsorted to KItem, otherwise one would have to consider all the prefixes of the k cell. @grosu @traiansf what do you guys think?

[grosu]

Definitely, KResult should be subsorted to KItem. Would that solve the problem?

Grigore

[andreistefanescu]

Yes, this solves it.

[dwightguth]

Well but what if the user writes the following rule?

rule isKResult(A:KItem ~> B:KItem)

If KResult is sub sorted to KItem and not K, what will this rule do? On Jul 17, 2014 5:57 AM, "Andrei Stefanescu" notifications@github.com wrote:

Yes, this solves it.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/718#issuecomment-49292129.

[grosu]

Yes, this is tricky, but I still believe that we should have

KResult < KItem < K

Or more generally, for one's Language,

Language_Results < KResult Language_Constructs < KItem < K

Then, when users write membership predicates, to only be allowed to have them syntactically take KItem arguments (parsing error otherwise).

Of course, this is a limitation, but it feels like the right kind of limitation, one which will work well also with the deductive verifier and with the test-case-generator later on. I am not sure of any examples where we would want more than the above. Anybody knows any?

Grigore

---

From: dwightguth [notifications@github.com] Sent: Thursday, July 17, 2014 10:27 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] Java backend doesn't know how to put back kresult in to a HOLE in this case (#718)

Well but what if the user writes the following rule?

rule isKResult(A:KItem ~> B:KItem)

If KResult is sub sorted to KItem and not K, what will this rule do? On Jul 17, 2014 5:57 AM, "Andrei Stefanescu" notifications@github.com wrote:

Yes, this solves it.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/718#issuecomment-49292129.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/718#issuecomment-49322478.

[yilongli]

fixed via https://github.com/kframework/k/pull/728