时间戳

首页 > 解决方案 > 让 Alloy 块之外的声明

alloy - 让 Alloy 块之外的声明

问题描述

我最近遇到了一些 Alloy 模型，它们的“let”语句与模型中的任何块都不相关。Alloy Analyzer 可以很好地解析这些模型，所以我知道这是有效的 Alloy 语法。但是，在https://alloytools.org/download/alloy4-grammar.txt上发布的 Alloy v4 语法或 Daniel Jackson 关于合金的书中的语法中没有规定“let”语句可以出现在块之外. 以下摘录显示了这些“let”语句的示例。

let bitXorTable = {
  i: bits,
  j: bits,
  k: bitAndTable[bitOrTable[i, j], bitNotTable[bitAndTable[i, j]]]
}

pred halfAdder(m: Int, n: Int, s: Int, c: Int) {
  s = bitXorTable[m, n]
  c = bitAndTable[m, n]
}

我正在为 Alloy 创建一个 ANTLR 解析器，我想知道是否应该将此规则添加到我的语法中。难道这些“让”语句只在合金的某些版本（新/旧）中有效吗？

标签： alloy

解决方案

我没有看过语法，但这在合金网站上的宏下有所介绍

可以在文件的顶层定义无类型宏。所有 3 种语法都是等价的。（如果无参数，则 [ ] 可以省略。）

 let a[x,y,z]   {...}
 let a[x,y,z] = {...}
 let a[x,y,z] = .....

宏扩展遵循正确的语法，因此宏的每个参数必须是整数/布尔值/集合/关系，或者必须是对谓词/函数/宏的（可能是部分的）调用。

宏是无类型的，所以在一个文件中我们不能有 2 个同名的宏。此外，如果宏在范围内，它总是会覆盖其他可能具有相同名称的 sig/field/fun/pred（就像在段落中如果我们看到 let x=y | F，那么在 F 中我们总是将 x表示 y，即使全局存在其他 sig x 或其他字段 x)

词法作用域：在宏体内，如果您引用的名称不在参数列表中，那么我们将从“定义”宏的文件中解析它，而不是从“调用”宏的文件中解析它。

柯里化：如果你调用一个参数数量不足的宏，那么结果是一个新的宏，前N个参数被填充，就像柯里化一样。

推荐阅读