模式匹配 - inline-function/Sublimation GitHub Wiki

模式匹配

凝华的 when 是真模式匹配——支持构造子解构、嵌套、守卫、区间模板，且编译器能自动证明穷尽性。

基本用法

when (x) {
    0       -> print("零")           // 字面量
    n if n > 10 -> print("大数")     // 带守卫的变量绑定
    else    -> print("其他")          // 兜底分支
}

when 必须穷尽所有可能值，否则编译报 W-NON-EXHAUSTIVE。

构造子解构

enum Color { Red; Green; Blue }
when (color) {
    Red   -> print("红")
    Green -> print("绿")
    Blue  -> print("蓝")        // 枚举必然穷尽，不需要 else
}

对 Optional[T] 解构：

when (maybe) {
    Some(v) -> print(v)            // 绑定 v，作用域在分支内
    None    -> print("缺值")
}

嵌套构造子：

when (result) {
    Ok(Some(v)) -> print(v)        // 两层构造子同时解构
    Ok(None)    -> print("空")
    Err(e)      -> print("错: " + e)
}

区间穷尽（when(n in _)）

这是凝华的杀手特性：把区间分支交给编译器证明覆盖。

fun grade(score: Nat)<score ∈ (0..100)>: Str {
    when(score in _) {                        // _ = 从上下文推断区间
        (0 .. 59)  -> return "不及格"
        (60 .. 69) -> return "及格"
        (70 .. 79) -> return "中等"
        (80 .. 89) -> return "良好"
        (90 .. 100)-> return "优秀"
    }
}

编译器会自动收集每个分支的端点（0, 59, 60, 69, …），排序后检查相邻衔接。这四个分支覆盖了 (0..100)，无需 else 也不需要自己写边界检查。

// 有前置条件告知区间：
+∵ score ∈ (0..30)
when(score in _) {
    (0 .. 10)  -> print("低")
    (11 .. 20) -> print("中")
    (21 .. 30) -> print("高")
}

when(n in _) 的 _ 充当通配符：编译器从 Γ 中的 n ∈ (l..r) 事实推断区间端点。

无主题 when（条件分支）

没有 subject 的 when 按条件链执行，不需要 else：

when {
    n < 0  -> print("负")
    n == 0 -> print("零")
    n > 0  -> print("正")
}

守卫（if 条件）

when (n) {
    x if x > 100 && x <= 200 -> print("大")       // 多条件守卫
    x if x > 0               -> print("正")
    else                     -> print("非正")
}

穷尽性

凝华强制执行穷尽性：每个 when 的 arm 合集必须覆盖所有可能的值。缺失分支报 W-NON-EXHAUSTIVE。

枚举、构造子族、区间 when(n in _)——编译器有专门的穷尽性策略，大多数场景不需要手动写 else。

// ❌ 编译错误：覆盖不完整
when (color) {
    Red -> print("红")
}
// → W-NON-EXHAUSTIVE: 缺少 Green, Blue

// ✅ 穷尽
when (color) {
    Red   -> print("红")
    Green -> print("绿")
    Blue  -> print("蓝")
}
⚠️ **GitHub.com Fallback** ⚠️