时间戳

首页 > 解决方案 > 无法计算最少种类的术语（其中术语是列表）

kframework - 无法计算最少种类的术语（其中术语是列表）

问题描述

我有以下作品：

syntax Id
syntax Exp ::= Id
syntax Exps ::= List{Exp, ","}
syntax Ids ::= List{Id, ","}

这个错误是什么意思？

[错误] 严重：无法计算最少种类的术语：
_,__KOOL-UNTYPED-SYNTAX(Id(#"x"),, .List{"_,__KOOL-UNTYPED-SYNTAX"}(.KList))。
可能的排序是 [Ids, Exps]，但它们最不常见的子排序是
GeneratedListBottom{_,__KOOL-UNTYPED-SYNTAX}，这是不可能的排序。所有
术语必须具有唯一的最小排序；考虑将唯一的 KLabels 分配给
重载产品/完成子排序格。
  同时评估功能项目：Stmts
  在评估函数 initKCell 时
  在评估函数 initThreadCell 时
  在评估函数 initThreadsCell 时
  在评估函数 initTCell 时

标签： kframework

解决方案

K 不确定该术语x, .List是 Id 列表还是 Exps 列表。

我们想告诉 K：

  1. 所有 ID 列表都是 Exp 列表：

    syntax Exps ::= Ids

  2. 与 Exp 列表具有相同元素的 Id 列表是相同的。我们告诉 KExps并使用属性Ids解析到同一个 AST 节点：klabel

    syntax Exps ::= List{Exp, ","} [klabel(exps)]
syntax Ids ::= List{Id, ","} [klabel(exps)]

推荐阅读