副作用与可变性控制

凝华的纪律：默认纯、不可变；副作用与可变性必须显式标注。

纯函数（默认）

fun add(a: Nat, b: Nat): Nat = a + b       // 纯函数，无需标注
fun pure(x: Nat): Nat { return x + 1 }     // 也是纯

纯函数自动获得自然命题 pure<add>，可以参与自动证明。

纯函数必须满足三件事（编译器检查）：

@impure
fun main() { print("hello") }              // print 是副作用，标 @impure

不纯函数的调用是不纯表达式——不承认不纯表达式的相等命题（包括自反）。所以 print("x") = print("x") 证不出。

var n = 0               // 不可变：n 不能再赋值
// n = 1                // ❌ E-IMMUT-ASSIGN

@mut var m = 0
m = m + 1               // ✅ 可变变量需要 @mut 标注

@mut
struct Counter(@mut n: Nat)

var a: @mut Counter = Counter(0)
a.n = 1                  // ✅ 修改可变字段
// var b: Counter = ...; b.n = 1  ❌ 不可变类型不能改

可变/不可变类型之间隐式转换会触发深拷贝：

var a: @mut Counter = Counter(0)
var b: Counter = a         // 深拷贝
a.n = 1
print(b.n)                 // 0（b 是独立拷贝）

想共享同一对象（别名语义）用 @ref：

@ref var a: @mut Counter = Counter(0)
@ref var b: @mut Counter = a
b.n = 1
print(a.n)                 // 1（同一对象，别名共享）

不方便标 @mut/@impure 时可以用 unchecked 显式逃逸（你对此负责）。