An exception error when using .K in #if #then #else #fi rule

[liyili2]

If I have the following definition:

module TEST

     syntax KItem ::= "start"

     syntax KItem ::= Call(List,K)

     rule start => Call(.List,1)

     rule Call(P:List,A:K) => #if P ==K .List #then .K #else 1 #fi 

endmodule

When I compile it by Java backend and run the program "start", I will get the following error:

File: /home/qangel/project/k-unified/bin/test.k,(7,6,7,32)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please file a bug report at https://github.com/kframework/k/issues

If I run it in Maude backend, it will be fine:

<k>
    .K
</k>

[traiansf]

Isn't this because you are not sort-decreasing? You are attempting to transform a KItem into .K which is not KItem. I thought the Java engine is not happy with this.

[liyili2]

I use a constructor KItem ::= "dotK" and the rule for dotK is like:

rule dotK => .K [structural]

This works in Java backend, tell me the reason I need to add this step.

[yilongli]

The full stacktrace is the following:

java.lang.AssertionError: unexpected kind K of term .K;expected kind KItem instead
    at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:320)
    at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:287)
    at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:253)
    at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:139)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:584)
    at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:226)
    at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:165)
    at org.kframework.backend.java.kil.KSequence.accept(KSequence.java:140)
    at org.kframework.backend.java.rewritemachine.KAbstractRewriteMachine.rewrite(KAbstractRewriteMachine.java:103)
    at org.kframework.backend.java.rewritemachine.KAbstractRewriteMachine.rewrite(KAbstractRewriteMachine.java:63)
    at org.kframework.backend.java.symbolic.FastDestructiveRewriter.computeRewriteStep(FastDestructiveRewriter.java:120)
    at org.kframework.backend.java.symbolic.FastDestructiveRewriter.rewrite(FastDestructiveRewriter.java:60)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.javaKILRun(JavaSymbolicExecutor.java:100)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.internalRun(JavaSymbolicExecutor.java:79)
    at org.kframework.backend.java.symbolic.JavaSymbolicExecutor.run(JavaSymbolicExecutor.java:74)
    at org.kframework.krun.tools.Executor$Tool.execute(Executor.java:151)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:103)
    at org.kframework.krun.tools.Executor$Tool.run(Executor.java:1)
    at org.kframework.transformation.TransformationCompositionProvider$2.run(TransformationCompositionProvider.java:120)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:77)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:44)
    at org.kframework.main.Main.main(Main.java:43)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please file a bug report at https://github.com/kframework/k/issues

@traiansf is right about this. The Java backend is expecting the result to be a KItem. However, we should definitely give a better error message. @andreistefanescu can you take a look at this issue? Should I detect this problem at kompile time or just give a better error message at runtime?

[liyili2]

I know that Traian is right. I am trying to figure out why the following definition works and what is the difference between the one above and the one below:

module TEST

     syntax KItem ::= "start"

     syntax KItem ::= Call(List,K)

     rule start => Call(.List,1)

     rule Call(P:List,A:K) => #if P ==K .List #then dotK #else 1 #fi 

     syntax KItem ::= "dotK"

     rule dotK => .K [structural]

endmodule

The Java backend output is:

<k>
    .K
</k>