K Framework: problem with semantic cast in function declarations

Question

I'm trying to update an erlang semantics from K 3.6 to 5.0 and I ran into the following issue:

When I try to write a function declaration without semantic cast, it works fine:

rule Name:Atom(Args) -> Body . =>. ... [structural]

But when I need to write the following, the kompile outputs [Error] Inner Parser: Parse error: unexpected token ')'.

rule Name:Atom(Args:Values) -> Body => . ... [structural]

To reproduce, here is my simplified syntax:

  imports STRING

  syntax UnquotedAtom ::= r"[a-z][_a-zA-Z0-9@]*" [token]
  syntax Atom ::= UnquotedAtom | Bool
  
  syntax Exp ::=  Atom
  syntax Exps ::= List{Exp, ","}              [strict, klabel("exps"), prefer, listexps]
  
  syntax FunCl  ::= Atom"("Exps")" "->" Exps "." [funcl1]

  syntax Value ::=  Atom
  syntax Values ::= List{Value, ","}
  syntax Exp ::= Value
  syntax KResult ::= Value
   
  // Function declaration
  
  //ok
  rule <k>Name:Atom(Args) -> Body . =>. ...</k>     [structural]
  // unexpected token ')'
  rule <k>Name:Atom(Args:Values) -> Body => . ...</k>   [structural]

My K version is: RV-K version 1.0-SNAPSHOT Git revision: adf2f2d Git branch: UNKNOWN Build date: Tue Mar 16 16:43:04 CET 2021

Answer 1

One of the changes from K3 to K5 is that lists are no longer automatically subsorted if the elements are subsorted. If you manually add

syntax Exps ::= Values

Then your rule will kompile again.