时间戳

首页 > 解决方案 > K 框架：函数声明中的语义转换问题

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

问题描述

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

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

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

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

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

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

  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

解决方案

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

syntax Exps ::= Values

然后你的规则将再次编译。

推荐阅读