K 框架：函数声明中的语义转换问题答案

【问题标题】：K Framework: problem with semantic cast in function declarationsK 框架：函数声明中的语义转换问题
【发布时间】：2021-05-09 22:09:46
【问题描述】：

我正在尝试将 erlang 语义从 K 3.6 更新到 5.0，但遇到了以下问题：

当我尝试编写没有语义转换的函数声明时，它工作正常：

规则名称：Atom(Args) -> 正文。 =>。 ... [结构]

但是当我需要编写以下内容时，kompile 会输出 [Error] Inner Parser: Parse error: unexpected token ')'。

规则名称:Atom(Args:Values) -> 正文 => 。 ... [结构]

为了重现，这是我的简化语法：

  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]

我的 K 版本是： RV-K 版本 1.0-SNAPSHOT Git 修订版：adf2f2d Git 分支：未知构建日期：2021 年 3 月 16 日星期二 16:43:04 CET

【问题讨论】：

标签： kframework

【解决方案1】：

从 K3 到 K5 的变化之一是，如果元素被子排序，列表将不再自动子排序。如果你手动添加

syntax Exps ::= Values

那么你的规则将再次编译。

【讨论】：