Closed liyili2 closed 10 years ago
From now on, I will refuse to read messages like this with VERY poor English. You can do better than that, Liyi. Make an effort to use grammatically correct English, at least.
Grigore
From: Liyi Li [notifications@github.com] Sent: Sunday, July 20, 2014 6:02 PM To: kframework/k Subject: [k] A strange behavior for a computation other than K cell when I want to get keys of a map (#738)
Actually, This problem belong to both Java backend and Maude backend. If I have this set of rules:
module TEST
configuration <T><k>$PGM:K</k>
<goto-map-calc color="cyan">
<goto-calc multiplicity="*" color="cyan">
<computation color="cyan"> .K </computation>
</goto-calc>
</goto-map-calc>
<control>
<curr-function color="lightgray">
file-scope
</curr-function>
</control>
<translation-units>
<tu multiplicity="*">
<goto-map color="lightgray"> .Map </goto-map>
</tu>
</translation-units>
</T>
syntax KItem ::= "start"
syntax PureStatement ::= "Label" "(" CId "," K ")" [avoid, klabel('Label)]
syntax PureStatement ::= "Return" "(" K ")" [klabel('Return)]
syntax KItem ::= calculateGotoMap(CId, K)
syntax KItem ::= "waitingOnGotoMap"
syntax CId ::= Identifier(String) | funLabel(CId) | "file-scope"
syntax Value ::= "emptyValue"
syntax KItem ::= map(Map)
syntax KItem ::= abc(Set)
rule <k> start => calculateGotoMap(Identifier("isprint"),
Label(funLabel(Identifier("isprint")),Return(emptyValue))) ...</k>
<translation-units>
(. => <tu>... <goto-map> .Map </goto-map> ...</tu>)
...</translation-units>
rule <computation> Return(emptyValue) => .K ...</computation>
rule <computation> abc(.Set) => .K ...</computation>
rule <computation> abc(SetItem(Identifier("isprint"))) => .K ...</computation>
rule <k> waitingOnGotoMap => .K ...</k>
<goto-map-calc> .Bag </goto-map-calc>
rule <k> calculateGotoMap(F:CId, K:K) => waitingOnGotoMap ...</k>
<curr-function> _ => F </curr-function>
<goto-map> M:Map => M[F <- map(.Map)] </goto-map>
<goto-map-calc>
. => (<goto-calc>...
<computation>
K ~> Return(emptyValue)
</computation>
...</goto-calc>)
</goto-map-calc>
[structural]
rule <computation> (Label(Target:CId, S:K) => abc(keys(M))) ~> K:K </computation>
<curr-function> F:CId </curr-function>
<goto-map>...
F |-> map(
(M:Map => M[Target <- 1]))
...</goto-map>
[structural]
endmodule
After I run the program "start", the output of Java backend and Muade backend krun are both:
That being said, I looked over your message anyway and found the problem quite intriguing. I lot those who know better what's going on figure it out and reply.
Thanks for reporting it, Grigore
From: Rosu, Grigore Sent: Sunday, July 20, 2014 10:43 PM To: kframework/k Subject: RE: [k] A strange behavior for a computation other than K cell when I want to get keys of a map (#738)
From now on, I will refuse to read messages like this with VERY poor English. You can do better than that, Liyi. Make an effort to use grammatically correct English, at least.
Grigore
From: Liyi Li [notifications@github.com] Sent: Sunday, July 20, 2014 6:02 PM To: kframework/k Subject: [k] A strange behavior for a computation other than K cell when I want to get keys of a map (#738)
Actually, This problem belong to both Java backend and Maude backend. If I have this set of rules:
module TEST
configuration <T><k>$PGM:K</k>
<goto-map-calc color="cyan">
<goto-calc multiplicity="*" color="cyan">
<computation color="cyan"> .K </computation>
</goto-calc>
</goto-map-calc>
<control>
<curr-function color="lightgray">
file-scope
</curr-function>
</control>
<translation-units>
<tu multiplicity="*">
<goto-map color="lightgray"> .Map </goto-map>
</tu>
</translation-units>
</T>
syntax KItem ::= "start"
syntax PureStatement ::= "Label" "(" CId "," K ")" [avoid, klabel('Label)]
syntax PureStatement ::= "Return" "(" K ")" [klabel('Return)]
syntax KItem ::= calculateGotoMap(CId, K)
syntax KItem ::= "waitingOnGotoMap"
syntax CId ::= Identifier(String) | funLabel(CId) | "file-scope"
syntax Value ::= "emptyValue"
syntax KItem ::= map(Map)
syntax KItem ::= abc(Set)
rule <k> start => calculateGotoMap(Identifier("isprint"),
Label(funLabel(Identifier("isprint")),Return(emptyValue))) ...</k>
<translation-units>
(. => <tu>... <goto-map> .Map </goto-map> ...</tu>)
...</translation-units>
rule <computation> Return(emptyValue) => .K ...</computation>
rule <computation> abc(.Set) => .K ...</computation>
rule <computation> abc(SetItem(Identifier("isprint"))) => .K ...</computation>
rule <k> waitingOnGotoMap => .K ...</k>
<goto-map-calc> .Bag </goto-map-calc>
rule <k> calculateGotoMap(F:CId, K:K) => waitingOnGotoMap ...</k>
<curr-function> _ => F </curr-function>
<goto-map> M:Map => M[F <- map(.Map)] </goto-map>
<goto-map-calc>
. => (<goto-calc>...
<computation>
K ~> Return(emptyValue)
</computation>
...</goto-calc>)
</goto-map-calc>
[structural]
rule <computation> (Label(Target:CId, S:K) => abc(keys(M))) ~> K:K </computation>
<curr-function> F:CId </curr-function>
<goto-map>...
F |-> map(
(M:Map => M[Target <- 1]))
...</goto-map>
[structural]
endmodule
After I run the program "start", the output of Java backend and Muade backend krun are both:
I will try to take care of the problem in the Java backend.
I think the problem is the same on both backends and it occurs in the collection compilation phase. From what I can see in Maude, apparently the transformation of Collections into builtins is not applied on the values of map updates.
@traiansf can you point me to the exact rule? I will take it from here.
I'm more than happy to... This is the rule:
rule <k> calculateGotoMap(F:CId, K:K) => waitingOnGotoMap ...</k>
<curr-function> _ => F </curr-function>
<goto-map> M:Map => M[F <- map(.Map)] </goto-map>
<goto-map-calc>
. => (<goto-calc>...
<computation>
K ~> Return(emptyValue)
</computation>
...</goto-calc>)
</goto-map-calc>
[structural]
When it gets compiled, the .Map in map(.Map) is not changed instead of probably becoming an injected builtin map.
should be fixed via https://github.com/kframework/k/pull/743
Oh. That is why
Sent from my Huawei Mobile
Traian Florin Șerbănuță notifications@github.com wrote:
I'm more than happy to... This is the rule:
rule
calculateGotoMap(F:CId, K:K) => waitingOnGotoMap ... _ => F M:Map => M[F <- map(.Map)] . => ( [structural]... )K ~> Return(emptyValue) ...When it gets compiled, the .Map in map(.Map) is not changed instead of probably becoming an injected builtin map.
— Reply to this email directly or view it on GitHub.
Actually, This problem belongs to both Java backend and Maude backend. If I have this set of rules:
After I run the program "start", the output of Java backend and Muade backend krun are both:
We can see that the krun does not know how to rewrite the term " keys ( .Map )" even if keys is a function term.
If I change the final rule to:
The Maude backend and Java backend will have different behavior as: Java backend:
Maude backend:
If I change the final rule to:
Both Maude and Java backend can give us the correct behavior:
Even if I define the keys function by myself with a new function, the behavior will be the same:
Java Output:
Maude output: