Lean 语言参考手册

12.4. 外部函数接口🔗

当前接口是为 Lean 内部使用而设计的，应视为不稳定接口。 未来将对其加以改进和扩展。

Lean 能与任何支持 C ABI 的语言高效互操作。 不过，目前这种支持仅限于传递 Lean 数据类型；尤其是，尚无法在 Lean 与 C 之间按值传入或返回 C struct 等复合数据结构。

与其他语言互操作主要使用两个属性：

  • @[export sym] def leanSym : ...

属性外部符号
attr ::= ...
    | extern str

将 Lean 声明绑定到指定的外部符号。

属性导出的符号
attr ::= ...
    | export ident

以未经名称修饰的符号名 sym 导出 Lean 常量。

有关如何从 Lean 调用外部代码以及反向调用的简单示例，请参阅 Lean 源码仓库中的 FFI 和反向 FFI 示例。

12.4.1. Lean ABI🔗

Lean 的应用二进制接口（ABI）描述了如何按照平台原生调用约定对 Lean 声明的签名进行编码。 它以目标平台的标准 C ABI 和调用约定为基础。 可以用属性 extern "sym" 或 export sym 标记 Lean 声明，使其与外部函数交互：前者令编译后的代码使用 C 声明 sym 作为实现，后者则使该声明以 sym 的名称供 C 使用。

在这两种情况下，C 声明的类型都从带该属性之声明的 Lean 类型推导而来。 设 α₁ → ... → αₙ → β 是该声明经过规范化的类型。 若 n 为 0，则相应的 C 声明为

extern s sym;

其中，s 是按照下一节所述规则将 β 转换成的 C 类型。 对于标有 extern 的定义，只有在调用该 Lean 模块或某个导入它的模块的初始化器之后，才能保证符号的值已经初始化。 有关初始化的一节将更详细地介绍初始化器。

若 n 大于 0，则相应的 C 声明为

s sym(t₁, ..., tₙ);

其中，形参类型 tᵢ 是类型 αᵢ 转换成的 C 类型。 对于 extern，会先移除所有不相关类型。

12.4.1.1. 将 Lean 类型转换为 C 类型🔗

在ABI 中，Lean 类型按以下方式转换为 C 类型：

  • 整数类型 UInt8、……、UInt64、USize 分别由 C 类型 uint8_t、……、uint64_t、size_t 表示。 若其运行时表示需要装箱，则会在 FFI 边界处将其拆箱。

  • Char 由 uint32_t 表示。

  • Float 由 double 表示。

  • Nat 和 Int 由 lean_object * 表示。 它们的运行时值要么是指向不透明大整数对象的指针；要么在“指针”的最低位为 1（lean_is_scalar）时，是经过编码的自然数或整数（lean_box/lean_unbox）。

  • 宇宙 Sort u、类型构造器 ... → Sort u 或命题 p​ :Prop 都是不相关的，它们要么被静态擦除（见上文），要么由运行时值为 lean_box(0) 的 lean_object * 表示。

  • 其他没有编译器特殊支持的归纳类型采用何种 ABI，取决于该类型的具体情况。 其 ABI 与这些类型的运行时表示相同。 其运行时值要么是指向 lean_object 某个子类型对象的指针（见下文“归纳类型”一节）；要么，当归纳类型的第 cidx 个构造器没有任何相关参数时，是值 lean_box(cidx)。

ABI 中的 Unit

u​:Unit 的运行时值始终为 lean_box(0)。

12.4.1.2. 借用🔗

默认情况下，extern 函数的所有 lean_object * 形参都被视为拥有。 外部代码会收到一个“虚拟引用计数令牌”，并负责将该令牌传递给另一个消耗型函数（恰好一次），或通过 lean_dec 释放它。 为减少引用计数开销，可以在形参类型前加上 Lean.Parser.Term.borrowed : term@&，将其标记为借用。 借用对象只能传给其他非消耗型函数（次数不限），或使用 lean_inc 将其转换为拥有值。 在 lean.h 中，lean_object * 的别名 lean_obj_arg 和 b_lean_obj_arg 用于在 C 端标示这种区别。 目前，返回值和 @[export] 形参始终是拥有的。

语法借用形参
term ::= ...
    | @& term

在形参类型前加上 @&，即可将其标记为借用。

12.4.2. 初始化🔗

将 Lean 代码纳入更大的程序时，必须先对模块进行初始化，然后才能访问其中的任何声明。 模块初始化包括：

  • 初始化所有“常量定义”（零元函数），其中包括从其他函数中提升出来的闭项；

  • 执行所有标有 init 属性的代码；以及

  • 如果设置了模块初始化器的 builtin 形参，则执行所有标有 builtin_init 属性的代码。

对于从 Lean 代码编译出的可执行文件，以及通过 lean --plugin 加载的“插件”，模块初始化器会自动带 builtin 标志运行。 对于 lean 导入的所有其他模块，初始化器运行时不带 builtin。 换言之，无论模块是否有可用的原生代码，当且仅当模块被导入时，才会运行其 init 函数；而无论模块是否被导入，builtin_init 函数都只会为原生可执行文件或插件运行。 Lean 编译器使用内置初始化器来完成诸如注册基础解析器之类的工作；即使不导入这些解析器所属的模块，它们也应当可用，这是自举所必需的。

包 foo 中模块 A.B 的初始化器名为 initialize_foo_A_B。 对于 Lean 核心中的模块（例如 Init.Prelude），其初始化器名为 initialize_Init_Prelude。 模块初始化器会自动初始化所有已导入的模块。 使用相同的 builtin 标志运行时，它们还具有幂等性，但并非线程安全。

关于进程相关功能的重要事项：使用 libuv 中进程相关函数（例如 Std.IO.Process.getProcessTitle 和 Std.IO.Process.setProcessTitle）的应用程序，必须在调用任何模块初始化器之前调用 lean_setup_args(argc, argv)（它会返回一个可能经过修改的 argv，必须用其替代原始的 argv）。 这样可以正确设置进程处理能力，而 Lean 运行时所依赖的某些系统级操作离不开这些能力。

综上所述，在访问任何 Lean 声明之前，应当恰好运行一次如下代码：

char ** lean_setup_args(int argc, char ** argv);

lean_object * initialize_A_B(uint8_t builtin);
lean_object * initialize_C(uint8_t builtin);
...

argv = lean_setup_args(argc, argv); // 使用进程相关功能时

lean_object * res;
// 使用与 Lean 可执行文件相同的默认值
uint8_t builtin = 1;
res = initialize_foo_A_B(builtin);
if (lean_io_result_is_ok(res)) {
    lean_dec_ref(res);
} else {
    lean_io_result_show_error(res);
    lean_dec(res);
    return ...;  // 初始化失败时，不得访问 Lean 声明
}
res = initialize_bar_C(builtin);
if (lean_io_result_is_ok(res)) {
...

//lean_init_task_manager();  // （间接）使用 `Task` 的代码需要调用此函数
lean_io_mark_end_initialization();

此外，凡不是由 Lean 运行时自身生成的线程，都必须调用以下函数进行初始化，才能供 Lean 使用：

void lean_initialize_thread();

并且应当调用以下函数终结线程，以释放所有线程局部资源：

void lean_finalize_thread();

12.4.3. 解释器中的 @[extern]🔗

Lean 解释器可以运行符号存在于已加载共享库中的 Lean 声明，其中包括标有 extern 的声明。 要运行此类代码（例如使用 Lean.Parser.Command.eval : command#eval），必须完成以下步骤：

  1. 将包含该声明的模块及其依赖项编译为共享库

  2. 通过 lean --load-dynlib= 提供该共享库，以运行导入此模块的代码。

仅加载包含外部符号的外部库并不足够，因为解释器还依赖于为每个 extern 声明生成的代码。 因此，无法在同一文件中解释 extern 声明。 Lean 源码仓库的 tests/compiler/foreign 中包含这种用法的示例。