elab API

elab 包（Luna-Flow/QED/elab）是名称与内核之间的解析边界。它针对局部上下文和内核状态，把项中的每个名称一次性解析为已解析项 RTerm，其中的常量带有其内核标识；它依据状态对已解析项做类型检查；并把它们降级为内核项。它还提供带类型检查的内核项轻量构造器。它只依赖 kernel，不产生任何定理。

冻结标识背后的设计见 elab 设计说明；elab 教程逐步介绍解析和作用域变化。

上下文

`ElabCtx`

ElabCtx 是局部上下文：由变量名及其类型组成的有序列表，最内层在最后。

pub struct ElabCtx {
  locals : Array[(String, @kernel.HolType)]
}

`empty_elab_ctx`、`elab_ctx_from_locals` 和 `elab_ctx_extend`

这些函数用于构造上下文。elab_ctx_extend 返回多一个局部变量的新上下文；参数本身不会改变。

pub fn empty_elab_ctx() -> ElabCtx
pub fn elab_ctx_from_locals(Array[(String, @kernel.HolType)]) -> ElabCtx
pub fn elab_ctx_extend(ElabCtx, String, @kernel.HolType) -> ElabCtx

同名的后一个局部变量会遮蔽前一个。

已解析项

`ResolvedConst`

ResolvedConst 是在解析时冻结的常量出现。

pub struct ResolvedConst {
  name : String
  const_id : Int
  inst_ty : @kernel.HolType
  schema_ty : @kernel.HolType
}

const_id 是名称所解析到的内核标识，schema_ty 是当时声明的模式（schema），inst_ty 是此次出现的类型，即 schema_ty 的一个实例。内置等号的 const_id == -1，其模式为 $\alpha \to \alpha \to \mathit{bool}$ 。

`RTerm`

RTerm 是已解析项：其中每个常量都是 ResolvedConst 的具名项。

pub enum RTerm {
  RVar(String, @kernel.HolType)
  RConst(ResolvedConst)
  RComb(RTerm, RTerm)
  RAbs(String, @kernel.HolType, RTerm)
}

`rterm_var`、`rterm_const`、`rterm_comb` 和 `rterm_abs`

这些函数不加检查地构造已解析项。

pub fn rterm_var(String, @kernel.HolType) -> RTerm
pub fn rterm_const(ResolvedConst) -> RTerm
pub fn rterm_comb(RTerm, RTerm) -> RTerm
pub fn rterm_abs(String, @kernel.HolType, RTerm) -> RTerm

`rconst_name`、`rconst_id`、`rconst_inst_ty` 和 `rconst_schema_ty`

这些函数读取 ResolvedConst 的字段。

pub fn rconst_name(ResolvedConst) -> String
pub fn rconst_id(ResolvedConst) -> Int
pub fn rconst_inst_ty(ResolvedConst) -> @kernel.HolType
pub fn rconst_schema_ty(ResolvedConst) -> @kernel.HolType

`rterm_eq`

rterm_eq 是已解析项的结构相等，包括绑定名称和常量标识。它不是 α 等价。

pub fn rterm_eq(RTerm, RTerm) -> Bool

`rterm_collect_free_vars` 和 `rterm_collect_consts`

rterm_collect_free_vars 按出现顺序列出已解析项的自由变量，允许重复。rterm_collect_consts 列出每一个常量出现。

pub fn rterm_collect_free_vars(RTerm) -> Array[(String, @kernel.HolType)]
pub fn rterm_collect_consts(RTerm) -> Array[ResolvedConst]

`rterm_to_string`

rterm_to_string 渲染已解析项；常量打印为 RConst(name#id : inst <= schema)。

pub fn rterm_to_string(RTerm) -> String

解析

`elab_resolve_name`

elab_resolve_name(state, ctx, name) 解析一个名称：若 ctx 中有该局部变量则取之，否则取 state 中可见的常量，类型为其模式类型。局部变量优先于常量。

pub fn elab_resolve_name(@kernel.KernelState, ElabCtx, String) -> Result[RTerm, ElabError]

当名称既不是局部变量也不是常量时，以 UnknownName(name) 失败。

`elab_resolve_const`、`elab_resolve_const_by_name` 和 `elab_resolve_const_instance`

这些函数解析常量。elab_resolve_const(state, name, ty) 解析类型为 ty 的出现；elab_resolve_const_by_name 使用模式类型；elab_resolve_const_instance 把结果包装为 RConst。

pub fn elab_resolve_const(@kernel.KernelState, String, @kernel.HolType) -> Result[ResolvedConst, ElabError]
pub fn elab_resolve_const_by_name(@kernel.KernelState, String) -> Result[ResolvedConst, ElabError]
pub fn elab_resolve_const_instance(@kernel.KernelState, String, @kernel.HolType) -> Result[RTerm, ElabError]

名称 = 总是解析为内置等号。失败情形：未声明任何常量时为 UnknownConst(name)，类型不是模式的实例时为 InvalidConstInstance(name)，状态的标识表与模式表不一致时为 ScopeResolutionMismatch。

`elab_resolve_var`

elab_resolve_var 不查询上下文，直接构造已解析变量。

pub fn elab_resolve_var(String, @kernel.HolType) -> RTerm

`elab_resolve_app`、`elab_resolve_abs` 和 `elab_resolve_eq`

这些函数由已解析的部分构造应用、抽象或等式，并依据状态和上下文对结果做类型检查。

pub fn elab_resolve_app(@kernel.KernelState, ElabCtx, RTerm, RTerm) -> Result[RTerm, ElabError]
pub fn elab_resolve_abs(@kernel.KernelState, ElabCtx, String, @kernel.HolType, RTerm) -> Result[RTerm, ElabError]
pub fn elab_resolve_eq(@kernel.KernelState, ElabCtx, RTerm, RTerm) -> Result[RTerm, ElabError]

结果类型错误时，它们以 CoreTypingFailure 失败。对于 elab_resolve_abs，函数体在加入绑定子后的 ctx 中检查。

`elab_resolve_named_term` 和 `elab_roundtrip_term`

elab_resolve_named_term(state, ctx, t) 解析一个已有的内核项：自由变量必须是 ctx 中类型相同的局部变量，常量则按名称在 state 中重新查找。elab_roundtrip_term 还会把结果降级，并检查它与 t α 等价（包括常量标识）。

pub fn elab_resolve_named_term(@kernel.KernelState, ElabCtx, @kernel.Term) -> Result[RTerm, ElabError]
pub fn elab_roundtrip_term(@kernel.KernelState, ElabCtx, @kernel.Term) -> Result[RTerm, ElabError]

当 t 中的某个常量现在解析到另一个标识时，elab_roundtrip_term 以 ScopeResolutionMismatch 失败；正是借此可以在发生遮蔽声明之后检测出在某个作用域中构造的项。

test "resolve" {
  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()
  inspect(@elab.rterm_to_string(c), content="RConst(c#1 : A <= A)")
  let eq = @elab.elab_resolve_eq(st, ctx, x, c).unwrap()
  inspect(@elab.elab_check_core_type(st, ctx, eq, @kernel.bool_ty()), content="true")
  inspect(@elab.elab_resolve_name(st, ctx, "nope") is Err(@elab.UnknownName("nope")), content="true")
  // a local named like a constant wins
  let ctx2 = @elab.elab_ctx_extend(ctx, "c", @kernel.bool_ty())
  inspect(@elab.elab_resolve_name(st, ctx2, "c") is Ok(@elab.RVar("c", _)), content="true")
}

核心类型检查

`elab_core_type_of`、`elab_check_core_type` 和 `rterm_well_formed`

elab_core_type_of(state, ctx, t) 计算已解析项的类型。变量必须是 ctx 中类型相同的局部变量；常量在 state 中必须仍具有相同的标识和模式，且其类型必须是该模式的实例。elab_check_core_type 把结果与期望类型比较，rterm_well_formed 测试类型是否存在。

pub fn elab_core_type_of(@kernel.KernelState, ElabCtx, RTerm) -> @kernel.HolType?
pub fn elab_check_core_type(@kernel.KernelState, ElabCtx, RTerm, @kernel.HolType) -> Bool
pub fn rterm_well_formed(@kernel.KernelState, ElabCtx, RTerm) -> Bool

核心类型检查从不重新查找名称：若冻结的标识已不是当前生效的标识，类型检查就会失败，而不会改用新的常量。

降级

`elab_lower_to_term` 和 `elab_lower_to_db`

elab_lower_to_term 把已解析项转为内核项，保留每个常量标识；elab_lower_to_db 则进一步转为内核的 De Bruijn 形式。

pub fn elab_lower_to_term(RTerm) -> Result[@kernel.Term, ElabError]
pub fn elab_lower_to_db(RTerm) -> Result[@kernel.DbTerm, ElabError]

当降级后的项类型错误或无法转换时，两者都以 CoreTypingFailure 失败。

test "freeze" {
  let bool = @kernel.bool_ty()
  let st1 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "c", bool).unwrap()
  let ctx = @elab.empty_elab_ctx()
  let c1 = @elab.elab_resolve_name(st1, ctx, "c").unwrap()
  // a shadowing declaration in an inner scope
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", bool).unwrap()
  inspect(@elab.rterm_well_formed(st1, ctx, c1), content="true")
  inspect(@elab.rterm_well_formed(st2, ctx, c1), content="false")
  // the lowered term keeps the identity resolved in st1
  let t = @elab.elab_lower_to_term(c1).unwrap()
  inspect(@kernel.term_to_string(t), content="Const(c#1 : bool)")
  inspect(@elab.elab_roundtrip_term(st2, ctx, t) is Err(@elab.ScopeResolutionMismatch), content="true")
}

内核项构造器

这些函数带类型检查地直接构造内核 Term 值，供不需要已解析项的调用者使用。

`elab_var`、`elab_const` 和 `elab_const_instance`

elab_var 即 mk_var。elab_const 和 elab_const_instance 分别是 ks_mk_const 和 ks_mk_const_instance。

pub fn elab_var(String, @kernel.HolType) -> @kernel.Term
pub fn elab_const(@kernel.KernelState, String) -> Result[@kernel.Term, @kernel.SigError]
pub fn elab_const_instance(@kernel.KernelState, String, @kernel.HolType) -> Result[@kernel.Term, @kernel.SigError]

`elab_app`、`elab_app2`、`elab_abs` 和 `elab_eq`

这些函数构造应用（一个或两个参数）、抽象或等式，结果类型错误时以 TypeMismatch 失败。

pub fn elab_app(@kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_app2(@kernel.Term, @kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_abs(String, @kernel.HolType, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_eq(@kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

`elab_is_prop` 和 `elab_require_prop`

elab_is_prop 测试一个项是否为类型良好的命题。elab_require_prop 返回该项，否则以 NotBoolTerm 失败（项类型错误时为 TypeMismatch）。

pub fn elab_is_prop(@kernel.Term) -> Bool
pub fn elab_require_prop(@kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

test "builders" {
  let a = @kernel.mk_tyvar("A")
  let f = @elab.elab_var("f", @kernel.fun_ty(a, @kernel.bool_ty()))
  let x = @elab.elab_var("x", a)
  let fx = @elab.elab_app(f, x).unwrap()
  inspect(@elab.elab_is_prop(fx), content="true")
  inspect(@elab.elab_app(x, f) is Err(@kernel.TypeMismatch), content="true")
  inspect(@elab.elab_require_prop(x) is Err(@kernel.NotBoolTerm), content="true")
}

错误

`ElabError`

ElabError 是解析和降级的错误类型。

pub enum ElabError {
  UnknownName(String)
  UnknownConst(String)
  InvalidConstInstance(String)
  ScopeResolutionMismatch
  CoreTypingFailure
}

构造子	含义
`UnknownName(name)`	该名称既不是局部变量，也不是可见常量。
`UnknownConst(name)`	没有声明过此名称的常量。
`InvalidConstInstance(name)`	所请求的类型不是该常量模式的实例。
`ScopeResolutionMismatch`	冻结的标识与状态不再匹配，或状态的各表互相不一致。
`CoreTypingFailure`	已解析项在当前状态和上下文中类型错误。

`elab_err_unknown_name`、`elab_err_unknown_const`、`elab_err_invalid_const_instance`、`elab_err_scope_resolution_mismatch` 和 `elab_err_core_typing_failure`

这些谓词测试某个 ElabError 是哪个构造子，供偏好函数而非模式匹配的调用者使用。

pub fn elab_err_unknown_name(ElabError) -> Bool
pub fn elab_err_unknown_const(ElabError) -> Bool
pub fn elab_err_invalid_const_instance(ElabError) -> Bool
pub fn elab_err_scope_resolution_mismatch(ElabError) -> Bool
pub fn elab_err_core_typing_failure(ElabError) -> Bool

elab API

上下文

ElabCtx

empty_elab_ctx、elab_ctx_from_locals 和 elab_ctx_extend

已解析项

ResolvedConst

RTerm

rterm_var、rterm_const、rterm_comb 和 rterm_abs

rconst_name、rconst_id、rconst_inst_ty 和 rconst_schema_ty

rterm_eq

rterm_collect_free_vars 和 rterm_collect_consts

rterm_to_string

解析

elab_resolve_name

elab_resolve_const、elab_resolve_const_by_name 和 elab_resolve_const_instance

elab_resolve_var

elab_resolve_app、elab_resolve_abs 和 elab_resolve_eq

elab_resolve_named_term 和 elab_roundtrip_term