S2Etop(knd=0; …)是什么？如何提取顶层域中的证明值？

通过FFI调用C库时，foo_init初始化函数可能返回空指针。为捕获该不变性，在.sats文件中定义了以下类型：

absvt@ype foo
vtypedef foo_ptr = [l: agz] (foo @ l | ptr l)
vtypedef foo_opt_ptr = [l: addr] (option_v (foo? @ l, l > null) | ptr l)

在检查p > 0后，尝试通过prval Some_v(pf) = pf_opt匹配值来创建非可选类型，代码如下：

(* … *)
val (pf_opt | p): foo_opt_ptr = foo_init(p_options)
if p > 0 then {
    prval Some_v(pf) = pf_opt
    // 此处也会触发类型断言失败：
    // val x: {l: agz}(foo @ l) = pf
    val nc: foo_ptr = (pf | p)
    (* … *)
    val _ = foo_stop(foo_ptr) // 释放foo_ptr
else
    prval None_v(pf) = pf_opt
    (* … *)
    val () = $raise FooFailedInit()
end

遇到pf侧的类型不匹配错误，错误信息：

mismatch of static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Ecst(foo_ptr))
The needed term is: S2Ecst(foo_ptr)

同时存在疑问：

• 如何获取被包装的正确类型？
• 尝试使用vtakeout0（来自prelude/basics_sta.sats）但编译器无法识别
• S2Etop(knd=0; …)是什么，如何从顶层域提取证明值？

1. 修正类型匹配问题 #

问题出在foo_opt_ptr的定义和匹配后的证明值提取上。需要显式拆分option_v中的证明对，同时断言地址相等来关联p的静态信息，调整代码如下：

val (pf_opt | p): foo_opt_ptr = foo_init(p_options)
if p > 0 then {
    // 拆分option_v中的两个证明：foo存在性、地址非空
    prval Some_v(pf_foo, pf_nonnull) = pf_opt
    // 断言运行时地址p与静态地址l相等
    prval () = addr_eq(p, l)
    // 此时可正确构造foo_ptr类型
    val nc: foo_ptr = (pf_foo | p)
    (* … *)
    val _ = foo_stop(nc) // 注意传入实例nc而非类型名foo_ptr
} else {
    prval None_v(pf_null) = pf_opt
    (* … *)
    val () = $raise FooFailedInit()
}

2. 关于vtakeout0的问题 #

vtakeout0用于从顶层环境包裹的静态项中提取原始值，若要使用需确保导入对应模块，在文件顶部添加：

#include "prelude/basics_sta.sats"

不过在当前场景下，通过显式拆分证明和地址断言已能解决问题，无需依赖vtakeout0。

S2Etop(knd=0; …)是ATS编译器内部的静态项表示：

• S2Etop代表顶层环境包裹的静态项，knd=0说明这是值类型的包裹
• 内部的S2Ecst(foo_ptr)才是你需要的原始静态常量类型

错误出现的原因是你直接将被顶层环境包裹的证明值，赋值给了需要原始静态类型的变量。通过拆分option_v中的证明对并断言地址相等，编译器就能正确识别静态类型，自动消除包裹层。

内容的提问来源于stack exchange，提问作者toastal