LSR 003 - Lamina C 扩展与插件规范

基本信息

  • LSR 编号 003

  • 标题 Lamina C 扩展与插件规范

  • 作者 Ziyang-Bai

  • 状态 草案

  • 类型 标准规范

  • 创建日期 02-04-2026

  • 归属项目 编译器、虚拟机、包管理器

摘要

定义 C/C++ 扩展的最小交付、接口映射与内存/所有权约束。

技术规范

1. 最小交付物

最小交付:

  • 动态库(编译生成的 .dll/.so/.dylib ,符号建议按C ABI导出)

  • Lamina 模块声明文件(默认文件名为module.lm) [1]

推荐目录(非强制):

  • [root]/module.lm

  • [root]/src/

  • [root]/include/ (可选)

2. 接口映射语法(必需)

在 module.lm 中使用 static 绑定动态库 [1] [2]。 动态库包含 lmx.h,声明文件中的导出符号、调用约定和实际 C 原型必须一致。 量纲剥离按 LSR-008 [3] 处理;剥离量纲不执行数值近似,也不恢复已擦除的量纲。

2.1 数学值、值约束与 ABI

普通源码的基本数学静态类型统一为 num;int、frac、real、complex 分别约束整数、有理数、实标量和复标量,不是四种独立基本类型。 x int、-> real、vector<int> 分别保留对应位置或元素的值约束, 基本类型为 num 或 vector<num>,不使用 num<int> 语法。 约束参与参数和返回校验,不能让基本签名及参数个数相同的函数仅按约束静态分派。 静态可证明时提前检查;其余在运行时检查。确定违反约束报告 DomainError 或 InvalidArgument,无法判定报告 Inconclusive。已证为整数的符号式可满足 int, 但索引、循环计数及原生整数取值仍须得到具体整数。 函数值的兼容检查保留参数值约束和量纲契约,不能只比较底层 num。 原生实参不能具体物化时报告 Inconclusive;确定违反数域或机器范围时报告相应错误。 普通副作用函数的约束未决不得自动变成符号调用。

外部函数声明中的标注同时选择固定 C ABI 表示,不改变上述普通数学类型:

标注

C ABI 表示

边界校验

int

LmInt,即 int64_t

可具体求值的整数,范围为 [-2^63, 2^63-1];禁止截断、环绕或先转浮点

frac

LmValue *,引用运行时有理数值

可具体求值的精确有理数,分母非零;不得降为两个机器整数或 double

real

C double,要求 IEEE 754 binary64

可具体求值的有限实标量;范围和转换规则见下文

complex

LmValue *,引用运行时复标量值

实部与虚部均可具体求值;保留各分量的精确/近似属性

num

LmValue *,引用运行时数学值

保留数值、符号式、关系和近似属性;原生函数须明确支持的数学值域

LmValue 是不透明运行时值,扩展只能经 lmx.h 的公共操作访问; 指针宽度取决于目标平台,不得复制内部布局或把指针强转为机器数。 vector、matrix、set、普通容器及元组也使用运行时值接口; vector<int> 不等于连续 int64_t 数组。裸数组接口必须单独约定元素表示、 长度、布局和借用期间,不得按内部存储猜测。

外部 real 声明选择 double,本身就是用户显式指定的数值 ABI 边界: 精确或近似实数均须先能具体求值,再按 binary64 最近值、同距取偶转换, 检查溢出和非零下溢;不能表示为有限非零数时报告 NumericalFailure。 该边界允许精确输入发生已声明的数值舍入,但不承诺保留超出 binary64 的精度, 也不能用来让普通 sqrt 等标准数学调用经隐藏 FFI 自动失去精确性。 若需先控制近似计算,调用者可显式使用 std.math.approximate [2]。 返回的 double 始终是保留完整 binary64 表示值的近似 num。ABI 的工作精度为 53 个二进制有效位,参与语言传播时按 15 位十进制工作精度记录;精度单位转换不重新舍入该表示值, 也不把工作位数作为认证准确位数。原生返回 NaN 或无穷时报告 NumericalFailure; 数学无穷须使用明确支持它的 num 值接口。 LmInt 返回值可无损导入为精确整数;句柄结果保留原有数学语义,并再次校验声明的值约束。

2.2 借用、修改和结果所有权

  • 实参默认只读借用,仅在调用期间有效。原生代码不得写入、释放或在返回后保存借用句柄。 跨调用保存必须使用公共保留/复制操作取得独立所有权,并最终释放。

  • 容器具有值语义。原地修改只能通过显式可写接口取得独占访问,调用方根路径必须可写, 且不能与其他输入/输出形成冲突别名;否则返回新值或拒绝调用。 let、元组和只读闭包不因经过 FFI 而获得可写子路径。

  • 共享、复制和唯一所有权优化对调用者不可见。修改一份值不得改变仍可观察的其他旧值, 不得用引用计数或地址比较建立数学容器身份。

  • 返回的新句柄把一次所有权交给调用方;返回借用值必须在绑定契约中指明保留者与有效期, 运行时在其失效前取得所需所有权。失败时不得遗留由调用者猜测是否需要释放的半成品。

  • 可写缓冲区须声明容量和实际写入长度。失败后输出保持原值,或回到契约明确的空状态, 不得暴露部分修改后仍标为有效的数学值。

2.3 错误与回调边界

外部接口必须声明可观测的失败协议。可能失败的 C 函数使用状态返回和结果输出参数, 或 lmx.h 提供的等效错误结果接口;绑定将非成功状态映射为带类别、操作和消息的 MathError,沿 LSR-018 [4] 传播。仅在已检查的输入范围内保证无失败的函数, 才可直接以 C 返回值承载结果。void 内核不是无错误协议的豁免, 调用适配层仍须报告分配失败、范围失败和原生运算错误。

不得以零、空集合、NaN 或默认值伪装成功,也不得让 C++ 异常跨越 C ABI。 取消、资源耗尽和内部故障继续向上传播,不能降为数学证明未决。 回调失败必须通过回调错误结果返回原生调用者,完成回调临时值清理并恢复外层执行状态; 原生调用者停止依赖该结果的运算,并传播该错误。不得展开越过不支持展开的 C 帧, 也不得吞掉回调错误后继续返回成功。

3. 接口示例

假设动态库 libidentity.so 导出在整个 LmInt 输入范围内无失败的 LmInt identity(LmInt value):

static "identity"

func so_identity(value int) -> int = "identity"

等号右侧是动态库导出符号。输入整数性和机器范围仍由调用边界检查。

4. 引用