让在合金块之外的声明

Question

最近我遇到了一些合金模型，它们的"let“语句与模型中的任何块无关。合金分析器很好地分析了这些模型，所以我知道这是有效的合金语法。然而，在张贴在v4上的合金https://alloytools.org/download/alloy4-grammar.txt语法中，或者在Daniel的“合金”一书中，没有一条规则说"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]
}

我正在为合金创建一个ANTLR解析器，我想知道是否应该将这个规则添加到我的语法中。这些"let“语句是否只在合金的某些版本(新的/旧的)中有效？

Answer 1

我还没有看过语法，但这在宏下的合金网站上有报道

可以在文件的顶层定义非类型化宏。所有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个参数，就像运行一样。