I am trying to compile a module using the syntax for doing a global environment lookup in a function rule.
When I try to compile my module using the Java backend, I get the error Conversion of KAs unsupported on Java backend! (_0,(I),_1) #as #Configuration, presumably related to the desugaring (though the pending-documentation states "This is completely desugared by the K frontend and does not require any special support in the backend."...but as it is pending I understand it's probably not always entirely accurate).
So I tried the Haskell backend. This also gives me an error about using #isConcrete, which I noticed is documented as not being supported in the Haskell backend...but I wasn't using #isConcrete. However, I discovered that if I remove the cell from my configuration which uses stdout, then I no longer get this error.
Is it possible to both use this syntax and have stdout? Ideally I could keep using the Java backend, because that's where I seem to run into the fewest issues.
Below is a simple example that produces the error:
module TEST-SYNTAX
imports DOMAINS-SYNTAX
syntax Prog ::= run(Int)
endmodule
module TEST
imports TEST-SYNTAX
imports DOMAINS
syntax KResult
configuration
<k> $PGM:Prog </k>
<bar> 6 </bar>
<log stream="stdout"> .List </log>
syntax Int ::= foo(Int) [function]
rule [[ foo(0) => I ]]
<bar> I </bar>
rule run(I) => foo(I)
endmodule
with the program being simply run(0).