KFramework: Issues with `#isConcrete` and function global configuration lookup

30 Views Asked by At

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).

0

There are 0 best solutions below