elab 教程
本教程使用 elab 包将名称解析为内核项，并展示解析之后签名发生变化时会怎样。当你在内核之上构建自己的前端，或想理解解析器 (parser) 可能报告的错误 ScopeResolutionMismatch 时，可参阅本教程。
快速开始
在 moon.pkg 中导入内核和 elab：
import {
"Luna-Flow/QED/kernel",
"Luna-Flow/QED/elab",
}解析等式 （其中 x 是局部变量，c 是已声明的常量），并将其降级为内核项：
test "quick start" {
let a = @kernel.mk_tyvar("A")
let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "c", a).unwrap()
let ctx = @elab.elab_ctx_from_locals([("x", a)])
let x = @elab.elab_resolve_name(st, ctx, "x").unwrap()
let c = @elab.elab_resolve_name(st, ctx, "c").unwrap()
let eq = @elab.elab_resolve_eq(st, ctx, x, c).unwrap()
let t = @elab.elab_lower_to_term(eq).unwrap()
inspect(
@kernel.term_to_string(t),
content="Comb(Comb(Const(= : fun(A, fun(A, bool))), Var(x : A)), Const(c#1 : A))",
)
}常量显示为 c#1：其标识在解析时就已固定。
日常任务
自底向上构建项
elab_resolve_app 和 elab_resolve_abs 在构建时检查类型：
test "bottom up" {
let bool = @kernel.bool_ty()
let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "neg", @kernel.fun_ty(bool, bool)).unwrap()
let ctx = @elab.empty_elab_ctx()
let neg = @elab.elab_resolve_name(st, ctx, "neg").unwrap()
// λp. neg p — the body is checked with p in scope
let inner = @elab.elab_ctx_extend(ctx, "p", bool)
let body = @elab.elab_resolve_app(st, inner, neg, @elab.elab_resolve_name(st, inner, "p").unwrap()).unwrap()
let lam = @elab.elab_resolve_abs(st, ctx, "p", bool, body).unwrap()
inspect(@elab.elab_check_core_type(st, ctx, lam, @kernel.fun_ty(bool, bool)), content="true")
// neg applied to itself is rejected
inspect(@elab.elab_resolve_app(st, ctx, neg, neg) is Err(@elab.CoreTypingFailure), content="true")
}在某个实例上使用多态常量
用类型变量声明的常量可以在其模式 (schema) 的任意实例上解析：
test "instances" {
let a = @kernel.mk_tyvar("A")
let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "default", a).unwrap()
let rc = @elab.elab_resolve_const(st, "default", @kernel.bool_ty()).unwrap()
inspect(@kernel.hol_type_to_string(@elab.rconst_inst_ty(rc)), content="bool")
inspect(@kernel.hol_type_to_string(@elab.rconst_schema_ty(rc)), content="A")
// fun(A, A) is not an instance of the schema bool -> bool of `flip`
let bool = @kernel.bool_ty()
let st2 = @kernel.ks_add_const(st, "flip", @kernel.fun_ty(bool, bool)).unwrap()
let bad = @elab.elab_resolve_const(st2, "flip", @kernel.fun_ty(a, a))
inspect(bad is Err(@elab.InvalidConstInstance("flip")), content="true")
}检测作用域漂移
已解析的项会记住每个常量指的是哪个声明。在出现遮蔽声明之后再次检查，会失败，而不会切换到新的常量：
test "scope drift" {
let bool = @kernel.bool_ty()
let st1 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "flag", bool).unwrap()
let ctx = @elab.empty_elab_ctx()
let flag = @elab.elab_resolve_name(st1, ctx, "flag").unwrap()
let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "flag", bool).unwrap()
inspect(@elab.rterm_well_formed(st2, ctx, flag), content="false")
// resolving the name again in st2 gives the new constant
let flag2 = @elab.elab_resolve_name(st2, ctx, "flag").unwrap()
inspect(@elab.rterm_to_string(flag2), content="RConst(flag#2 : bool <= bool)")
// back in the outer scope the old term is fine again
let st3 = @kernel.ks_pop_scope(st2).unwrap()
inspect(@elab.rterm_well_formed(st3, ctx, flag), content="true")
}进一步使用
检查来自别处的项。 elab_roundtrip_term(state, ctx, t) 会重新解析内核项并检查是否有变化；在其他状态中构建的项进入你的代码的边界处使用它。
检查项。 rterm_collect_consts 列出每个常量出现及其标识，rterm_collect_free_vars 列出每个自由变量；两者都适用于诊断。
交给内核。 用 elab_lower_to_term 降级，并把结果传给内核规则。你解析出的标识随之传递，内核的可容许性检查会再次强制执行它们。
改用解析器。 对于文本输入，@parser.parse_term 和 @parser.parse_resolved_term 会替你运行此包；见 parser 教程。
常见陷阱
- 期望类型推断。 绑定子类型从不推断；请把它们传给
elab_resolve_abs，或在上下文中连同类型声明局部变量。 - 用
rterm_eq比较。 它也比较绑定名，所以 α 等价的项可能不相等。请将两者都降级，再使用@kernel.term_alpha_eq。 - 扩展后复用上下文。
elab_ctx_extend返回新上下文；旧的保持不变，离开绑定子时正需要这样。 - 在状态中寻找
=。 等号是内置的，无需声明即可解析；你不能声明或遮蔽它。