挂钩 prolog 的统一跟踪输出

Question

我正在尝试调查在无类型语言上使用自定义类型推断语言的项目的可行性。 （语言本身并不重要，但它恰好是 PHP）。我的第一个想法是对此运行类型统一。我在 Haskell 中编写了一些程序，所以我知道从最终用户的角度来看类型统一是如何工作的，但我从未深入研究过算法的细节。

此时，我可以解析一个 PHP 代码文件，建立一组相应的规则，并希望开始针对这些规则运行统一算法。与其重新发明轮子，我想我会使用现有的统一算法，而 AFIAK，Prolog 是目前最强大的统一算法之一。

我现在已经到了，如果我传入一个可验证的正确输入，Prolog 就会返回“true”。如果我传入不正确的内容，它会返回“错误”。现在我在那种情况下真正想要的是得到一条错误消息，指出为什么类型没有统一。如果我在 SWI-Prolog 中打开“跟踪”模式，我或多或少会得到我想要的东西，逐步解释为什么类型没有统一。我的核心问题是，是否可以通过编程方式获取这些信息？如果需要的话，我愿意编写一个 C 扩展并直接链接到 Prolog 编译器。另外，我与 SWI-Prolog 没有任何关系，它只是我在 google 上找到的第一个。

另外，顺便说一句，有人知道 prolog 中有什么好的教程吗，无论是 Web 格式还是作为一本真正的书？

Answer 1

我的感觉是，使用 trace，您无法获得详细信息 为什么统一失败，但您会获得目标的信息 失败。

如果后面的信息是你想要的，你可以这样做 由你自己，因为你检测你的代码。只需更换 每个目标

 .. A ..

通过以下代码：

 .. in(A), A, out(A) ..

具有以下定义：

 in(A) :- write('call '), write(A), nl.
 in(A) :- write('fail '), write(A), nl, fail.

 out(A) :- write('exit '), write(A), nl.
 out(A) :- write('redo '), write(A), nl, fail.

当然，您可以将 write/1 和 nl/0 语句替换为 什么都适合你。这是一个例子。首先是仪表 序言：

?- [user].
mem(X,[X|_]).
mem(X,[_|Y]) :- in(mem(X,Y)), mem(X,Y), out(mem(X,Y)).
^D

现在是检测查询：

?- in(mem(X,[1,2])), mem(X,[1,2]), out(mem(X,[1,2])).
call mem(_G1479,[1,2])
exit mem(1,[1,2])
X = 1 ;
redo mem(1,[1,2])
call mem(_G1479,[2])
exit mem(2,[2])
exit mem(2,[1,2])
X = 2 ;
redo mem(2,[1,2])
redo mem(2,[2])
call mem(_G1479,[])
fail mem(_G1479,[])
fail mem(_G1479,[2])
fail mem(_G1479,[1,2])
false.

再见