让 Alloy 块之外的声明

Question

我最近遇到了一些合金模型，其中包含与模型中的任何块无关的“let”语句。 Alloy Analyzer 可以很好地解析这些模型，所以我知道这是有效的 Alloy 语法。但是，https://alloytools.org/download/alloy4-grammar.txt 上发布的 Alloy v4 语法或 Daniel Jackson 关于 Alloy 的书中的语法中没有规定“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 解析器，我想知道是否应该将此规则添加到我的语法中。难道这些“let”语句仅在 Alloy 的某些版本（较新/较旧）中有效？

Answer 1

我没有看过语法，但这在 Alloy 网站的Macros 下有介绍

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

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

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

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

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

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