[K-Bug] Example of a symbol used in `overload` attributes not appearing.

[gtrepta]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.51-0-g54e7c65508

Operating System

Linux

K Definitions (If Possible)

module TEST
  imports INT

  syntax Val ::= Int

  syntax Val ::= Val Val [left, overload(apply)]

  syntax Exp ::= Val
  syntax Exp ::= Exp Exp [left, overload(apply)]

  syntax priority apply
endmodule

Steps to Reproduce

$ kompile test.k
[Error] Outer Parser: Could not find any productions for tag: apply
        Source(/home/gtrepta/runtimeverification/k/fun-untyped/test.k)
        Location(11,3,11,24)
        11 |      syntax priority apply
           .      ^~~~~~~~~~~~~~~~~~~~~

Omitting the syntax priority line kompiles successfully. And then:

$ krun -cPGM='1 2 3' --output kast
`<generatedTop>`(`<k>`(`___TEST_Val_Val_Val`(`___TEST_Val_Val_Val`(#token("1","Int"),#token("2","Int")),#token("3","Int"))),`<generatedCounter>`(#token("0","Int")))

Expected Results

The syntax priority sentence shouldn't cause an error for kompile, and the krun output should have apply symbols.

[Baltoli]

module TEST
  imports INT

  syntax Val ::= Int

  syntax Val ::= Val Val [left, overload(apply), group(apply), symbol(applyVal)]

  syntax Exp ::= Val
  syntax Exp ::= Exp Exp [left, overload(apply), group(apply), symbol(applyExp)]

  syntax priority apply
endmodule

[gtrepta]

Bruce's comment clears this up. I wrongly expected that the overload attribute also specifies the symbol name.