Gambit Scheme 代码生成器

可以通过 REPL 命令访问 Gambit Scheme 代码生成器：

Main> :set cg gambit

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

$ export IDRIS2_CG=gambit

要使用此生成器运行 Idris 程序，您需要安装 Gambit Scheme 。 Gambit Scheme 是免费软件，可通过大多数包管理器获得。

您可以在 REPL 中将类型为 IO () 的表达式 expr 编译为可执行文件，如下所示：

Main> :c execname expr

...其中 execname 是可执行文件的名称。这将生成以下内容：

你也可以直接执行表达式：

Main> :exec expr

同样， expr 必须具有 IO () 类型。这将生成一个临时 Scheme 文件，并在其上执行 Gambit 解释器。

Gambit 指令

--directive extraRuntime=<path>

将来自 <path> 的 Scheme 源代码直接嵌入到生成的输出中。可以多次指定，在这种情况下，所有给定的文件都将按指定的顺序包含。

; extensions.scm
(define (my-mul a b)
  (* a b))

-- Main.idr
%foreign "scheme:my-mul"
myMul : Int -> Int -> Int

$ idris2 --codegen gambit --directive extraRuntime=/path/to/extensions.scm -o main Main.idr