变量(Variables)¶
自由变量和约束变量（Free and bound variable）
变量（Variables）¶
MirrorQL中的变量与代数或逻辑中的变量的使用方式相似；它们表示一组值，这些值通常受公式限制。
这与某些其他编程语言中的变量不同，在其他编程语言中，变量表示可能包含数据的内存位置，该数据还可以随着时间变化。
例如，在MirrorQL中，n = n + 1 是一个等式公式，仅当n 等于n + 1 时才成立（因此，实际上它不适用于任何数值）。
在Java中，n = n + 1 不是等式，而是通过添加1 到当前的值n，并进行新的赋值来改变n代表的值。
声明一个变量（Declaring a variable）¶
MirrorQL还支持在谓词体中使用let语句声明自由变量。
let语句有两种语法：let 变量名:变量类型; 或 let 变量名 = 表达式;。
对于第二种语法，MirrorQL编译器将自动推断变量类型。其中变量名是一系列合法的标识符字符；
- 标识符字符是小写
ASCII字母（a到z、U+0061到U+007A）、大写ASCII字母（A到Z、U+0041到U+005A）、十进制数字（0到9、U+0030到U+0039）和下划线（_、U+005F），标识符的第一个字符必须是字母。 - 标识符不能具有与关键字相同的字符序列。
合法的标识符示例如下：
let语句相当于谓词顶层的exists量词。let的用法示例如下：
fn NumberInRange(x:int) {
x == range(1, 10)
}
fn test1() {
let x:int;
NumberInRange(x)
//相当于 exists(|x:int| NumberInRange(x))
}
fn test3() {
let x = range(1, 5)
NumberInRange(x)
//相当于 exists(|x = range(1, 5)| NumberInRange(x))
}
fn test4() {
let y = range(1, 5)
let x = y;
NumberInRange(x)
//相当于 y = range(1, 5) and exists(|x = y| NumberInRange(x))
}
fn test5() {
let x = range(1 ,2)
let y = range(1, 3)
x == y
//相当于 exists(|x = range(1 ,2),y = range(1, 3)| x == y)
}
MirrorQL中的keyword 如下：
use
as
and
or
not
land
lor
class
exists
forall
instanceof
fn
for
if
else
impl
self
super
package
trait
let
mod
range
extends
yes
no
int
str
float
uint
count
min
max
enum
from
where
select
record
in
match
itos
ftos
toInt
toFloat
substr
len
cat
ord
none
ant
yon
inline
no_inline
magic
no_magic
result
自由变量和约束变量（Free and bound variable）¶
变量可以具有不同的作用。
有些变量是free，它们的值直接影响使用它们的表达式的值，或者使用它们的公式是否 成立。
其他变量（称为绑定变量）仅限于特定的值集。
在一个示例中，最容易理解这种区别。看一下以下表达式：
第一个表达式没有任何变量。它找到"l" 字符串中出现位置的（从零开始的）索引"hello" ，因此它的结果为2 和3。
第二个表达式的计算结果为[-3 .. 3] 范围内的最小值-3。尽管此表达式使用变量f ，但它只是一个占位符或“虚拟”变量，不能为其分配任何值。
您可以使用其他变量替换 f 而无需更改表达式的含义。例如，min(float f | f in [-3 .. 3]) 始终等于min(float other | other in [-3 ..3]) 。这是绑定变量的示例。
表达式(i + 7) * 3 和 x.sqrt()有该是怎样的呢？在这两种情况下，表达式的值取决于什么值赋值给变量和分别。
换句话说，变量的值对表达式的值有影响。这些是自由变量的示例。同样，如果一个公式包含自由变量，则该公式可以保留还是不保留，取决于分配给这些变量的值。例如：
"hello".indexOf("l") = 1
min(float f | f in [-3 .. 3]) = -3
(i + 7) * 3 instanceof int
exists(float y | x.sqrt() = y)
第一个公式不包含任何的变量，并且永远不成立（因为它"hello".indexOf("l") = 1 具有值2和3， 从不为1）。
第二个公式仅包含一个绑定变量，因此不受该变量更改的影响。由于等于，所以该公式始终成立。
第三个公式包含一个自由变量i，公式是否成立，取决于分配给的值i。例如，如果i分配了1或者2（或者其他的int），则公式成立。另一方面，如果i已分配3.5，则它不成立。
最后一个公式包含一个自由变量x 和一个绑定变量y。如果x分配了一个非负数，则最终公式成立。另一个方面，例如，如果x指定值-9，则公式不成立。该变量y不影响公式是否成立。