示例：最简 Readline 绑定
本节将介绍如何在 Idris 中为 C 库（GNU Readline 库）创建绑定，并将其封装为可用的包。我们只会实现最基础的绑定，但这些内容已经展示了为 C 库创建绑定时需要处理的一些棘手问题，例如 String 的内存分配。
完整示例可在 Idris 2 源码仓库的 samples/FFI-readline 路径下找到。作为最小示例，它可以作为其他 C 库绑定的起点。
我们将为 Readline API 中以下函数提供绑定，可通过 #include <readline/readline.h> 获得：
char* readline (const char *prompt);
void add_history(const char *string);
此外，我们还将支持 Tab 补全。在 Readline API 中，这通过将全局变量设置为回调函数实现（参见 回调 部分，介绍如何处理补全）：
typedef char *rl_compentry_func_t (const char *, int);
rl_compentry_func_t * rl_completion_entry_function;
补全函数接收一个 String``（待补全文本）和一个 ``Int``（当前请求补全的次数）。在 Idris 中，这可以表示为 ``complete : String -> Int -> IO String。例如，若当前文本为 id，可补全项为 idiomatic 和 idris，则 complete "id" 0 返回 idiomatic，complete "id" 1 返回 idris。
我们将在 C 文件 idris_readline.c 中定义 *glue*（胶水）函数，编译为共享对象 libidrisreadline，并编写一个用于定位 C 函数的函数：
rlib : String -> String
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
每个外部绑定都带有 %foreign 说明符，通过 rlib 定位函数。
基本行为：读取输入与历史
我们可以直接为 readline 编写绑定。由于它是交互式的，因此需要返回 PrimIO：
%foreign (rlib "readline")
prim__readline : String -> PrimIO String
然后，我们可以编写一个 IO 包装器：
readline : String -> IO String
readline prompt = primIO $ readline prompt
但这样还不够！C 语言的 readline 函数在遇到文件结尾且无输入时会返回 NULL 字符串。因此我们需要处理这种情况——否则遇到文件结尾时会崩溃（请记住：为 C 绑定指定合适类型是 Idris 程序员的责任！）
因此我们需要使用 Ptr，以表示它可能是 NULL 指针（参见 原语 FFI 类型 章节）：
%foreign (rlib "readline")
prim__readline : String -> PrimIO (Ptr String)
我们还需要提供一种方法来检查返回的 Ptr String 是否为 NULL。为此，我们会在 idris_readline.c 和对应的头文件 idris_readline.h 中编写胶水代码，实现 Ptr String 与 String 的相互转换。在 idris_readline.h 中有：
int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise
char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL)
void* mkString(char* str); // turn a String into a Ptr String
void* nullString(); // create a new NULL String
相应地，在 idris_readline.c 中：
int isNullString(void* str) {
return str == NULL;
}
char* getString(void* str) {
return (char*)str;
}
void* mkString(char* str) {
return (void*)str;
}
void* nullString() {
return NULL;
}
现在，我们可以如下安全地使用 prim__readline，通过 API 检查其返回结果是 NULL 还是具体的 String：
%foreign (rlib "isNullString")
prim__isNullString : Ptr String -> Int
export
isNullString : Ptr String -> Bool
isNullString str = if prim__isNullString str == 0 then False else True
export
readline : String -> IO (Maybe String)
readline s
= do mstr <- primIO $ prim__readline s
if isNullString mstr
then pure $ Nothing
else pure $ Just (getString mstr)
后续处理补全时会用到 nullString 和 mkString。
读取字符串后，我们通常希望将其添加到输入历史中。可以如下为 add_history 提供绑定：
%foreign (rlib "add_history")
prim__add_history : String -> PrimIO ()
export
addHistory : String -> IO ()
addHistory s = primIO $ prim__add_history s
在这种情况下，由于 String 由 Idris 控制，不会为 NULL，因此可以直接添加。
一个简单的 readline 程序，用于读取输入并回显，同时记录非空输入的历史，可以这样编写：
echoLoop : IO ()
echoLoop
= do Just x <- readline "> "
| Nothing => putStrLn "EOF"
putStrLn ("Read: " ++ x)
when (x /= "") $ addHistory x
if x /= "quit"
then echoLoop
else putStrLn "Done"
这样我们就拥有了命令历史和命令行编辑功能，但当加入 Tab 补全后，Readline 会变得更强大。默认的 Tab 补全（即使在上述简单示例中也可用）会补全当前工作目录下的文件名。但在实际应用中，我们通常希望补全其他命令，如函数名、本地数据引用或其他适合应用场景的内容。
补全功能
Readline API 很丰富，支持多种 Tab 补全方式，通常需要将全局变量设置为合适的补全函数。我们将采用如下方式：
typedef char *rl_compentry_func_t (const char *, int);
rl_compentry_func_t * rl_completion_entry_function;
补全函数接收补全前缀和当前前缀下被调用的次数，返回下一个补全项；若无更多补全则返回 NULL。Idris 中的等价类型如下：
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
如果没有更多补全项，函数返回 Nothing；若当前输入还有其他补全项，则返回 Just str。
我们或许以为只需定义一个函数来设置补全函数即可……
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
rl_completion_entry_function = fn;
}
……然后定义 Idris 绑定，需要注意 Readline 库在无更多补全时期望返回 NULL：
%foreign (rlib "idrisrl_setCompletion")
prim__setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
export
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
setCompletionFn fn
= primIO $ prim__setCompletion $ \s, i => toPrim $
do mstr <- fn s i
case mstr of
Nothing => pure nullString // need to return a Ptr String to readline!
Just str => pure (mkString str)
因此，我们将 Nothing 转为 nullString，将 Just str 转为 mkString str。但这样并不完全可行。为了解问题所在，不妨尝试一个最基础的补全函数——无论输入什么都只返回一个补全项：
testComplete : String -> Int -> IO (Maybe String)
testComplete text 0 = pure $ Just "hamster"
testComplete text st = pure Nothing
我们将在上文 echoLoop 的一个小改动中尝试此方案，先设置补全函数：
main : IO ()
main = do setCompletionFn testComplete
echoLoop
运行后，若在未输入任何内容前按下 TAB，会发现存在问题：
Main> :exec main
> free(): invalid pointer
设置补全的 Idris 代码本身没问题，但 C 端胶水代码的内存分配存在问题。
问题的根源在于我们没有明确区分程序中哪些部分负责字符串的分配和释放。当 Idris 调用返回字符串的外部函数时，会将字符串复制到 Idris 堆并立即释放；但如果外部库也释放该字符串，就会导致重复释放。这正是这里发生的情况：传递给 prim__setCompletion 的回调释放字符串并放入 Idris 堆，而 Readline 在处理完 prim__setCompletion 返回的字符串后也会释放一次。解决方法是为补全函数编写一个包装器，重新分配字符串，并在 idrisrl_setCompletion 中使用。
rl_compentry_func_t* my_compentry;
char* compentry_wrapper(const char* text, int i) {
char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap,
// and freed on return
if (res != NULL) {
char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when
// it is finished with it
strcpy(comp, res);
return comp;
}
else {
return NULL;
}
}
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
rl_completion_entry_function = compentry_wrapper;
my_compentry = fn; // fn is an Idris function, called by compentry_wrapper
}
因此，我们在 C 端定义补全函数，调用 Idris 补全函数，并确保 Idris 返回的字符串被复制到 C 堆。
至此，我们已实现一个原始 API，覆盖了 readline API 的最基本功能：
readline : String -> IO (Maybe String)
addHistory : String -> IO ()
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()