带引用计数的 C（C with Reference Counting）

有一个实验性的代码生成器可通过 C 语言编译为可执行文件，使用引用计数垃圾回收器。该生成器旨在作为轻量级（即依赖最少）的代码生成器，可移植到多种平台，尤其适用于内存受限的平台。

性能不如基于 Scheme 的代码生成器，一方面是因为引用计数尚未优化，另一方面是 C 语言本身的限制。然而，主要目标是可移植性：生成的代码应能在任何支持 C 编译器的平台上运行。

可通过 REPL 命令访问此代码生成器：

Main> :set cg refc

或者，您可以通过 IDRIS2_CG 环境变量进行设置：

$ export IDRIS2_CG=refc

所调用的 C 编译器由 IDRIS2_CC 或 CC 环境变量决定。如果两者都未设置，则使用 cc。

该代码生成器尚不支持 :exec，仅支持 :c。

另请注意，如果链接了用于 C 语言接口的动态库，运行可执行文件时需确保这些库可通过 LD_LIBRARY_PATH 访问。Idris 2 默认支持库为静态链接。

扩展 RefC（Extending RefC）

RefC 可扩展为支持 C 语言外部函数的其他语言生成新后端。例如：Idris 的 Python 后端。

在您的后端中，使用 Compiler.RefC 的 generateCSourceFile、compileCObjectFile {asLibrary = True} 和 compileCFile {asShared = True} 函数生成 .so 共享对象文件。

_ <- generateCSourceFile defs cSourceFile
_ <- compileCObjectFile {asLibrary = True} cSourceFile cObjectFile
_ <- compileCFile {asShared = True} cObjectFile cSharedObjectFile

要运行已编译的 Idris 程序，请在编译生成的 .so 文件中调用 int main(int argc, char *argv[]) 函数，并传入希望传递给运行程序的参数。

例如，在 Python 中：

import ctypes
import sys

argc = len(sys.argv)
argv = (ctypes.c_char_p * argc)(*map(str.encode, sys.argv))

cdll = ctypes.CDLL("main.so")
cdll.main(argc, argv)

扩展 RefC FFI（Extending RefC FFIs）

如需让生成的 C 代码识别标准 RefC FFI 以外的其他 FFI 语言，请在调用 generateCSourceFile 时传递 additionalFFILangs 选项，并提供后端可识别的语言标识符列表。

_ <- generateCSourceFile {additionalFFILangs = ["python"]} defs cSourceFile

这将在生成的 C 文件中生成 FFI 函数指针桩，您的后端应在调用 main 之前将其指向相应的 C 函数。

每个函数的 %foreign "lang: foreignFuncName, opts" 定义都会生成一个相应类型的函数指针桩。该桩名为 cName $ NS (mkNamespace lang) funcName，其中 funcName 是该函数的 Idris 完全限定名。

因此，%foreign 函数

%foreign "python: abs"
abs : Int -> Int

会生成一个 python_Main_abs 桩，可在 Python 中进行回补：

abs_ptr = ctypes.CFUNCTYPE(ctypes.c_int64, ctypes.c_int64)(abs)
ctypes.c_void_p.in_dll(cdll, "python_Main_abs").value = ctypes.cast(abs_ptr, ctypes.c_void_p).value