0

我的主要问题是什么是“意外的连接项”。我对下面的错误有一些背景，尽管似乎还有许多其他问题可能会混淆这个错误。

我有一个foo排序术语Map和一个bar排序术语Map。foo接受一个表达式列表，目标是将它们全部放入Map. 为此，我调用bar它并连接每个表达式。从语法上Map我相信应该足够然后说bar(exp) foo(exps)得到整个Map.

这编译得很好，但是当我尝试在我重写后立即运行它时，bar(exp) foo(exps)我得到了一个 [Error] Critical: unexpected concatenated termfoo(...) while evaluating function _Map_. 为简洁起见，我删除了表达式本身。

我认为问题可能在于Map联合的优先级高于我的foo，bar因此我尝试将其分配bar为一个函数，因为bar它的参数很严格，这导致了排序错误KItem并且Exp不兼容。

4

1 回答 1

0

@ALee 我们需要查看您的代码才能确定，但​​我认为这里的混淆是您正在尝试将两个地图联合在一起，而 K 实际上不支持地图联合。

我们有构造函数 _Map_，例如，它可以让您构建如下所示的内容Map："a" |-> 3 "b" |-> 4但是您不能使用两个任意映射并使用此构造函数将它们放在一起。

这样做的原因是生成的术语可能没有明确定义（如果两个映射定义相同的键，但具有不同的值怎么办？）。

相反，如果您想要这种行为，您需要编写自己的映射联合运算符，它可以选择当两个映射中有重叠键时要做什么。此示例更喜欢第二个Map参数中的键（如果存在相同的键，则覆盖第一个映射的值）：

syntax Map ::= union ( Map , Map ) [function]

rule union(M, .Map) => M
rule union(M, K |-> V M') => union(M [ K <- V ], M')
于 2020-05-12T11:39:38.317 回答