連接到prolog的統一跟蹤輸出

Question

我正在嘗試調查在非類型化語言上使用自定義類型推斷語言的項目的可行性。 （語言本身並不重要，但恰巧是PHP）。我的第一個想法是對此進行類型統一。我在Haskell中編寫了一些代碼，所以我知道從最終用戶的角度來看類型統一是如何工作的，但是我從未深入到算法的細節中。

在這一點上，我可以解析一個PHP代碼文件，建立一組相應的規則，並且想要開始針對這些規則運行統一算法。與其重新發明車輪，我想我會使用現有的統一算法，而AFIAK，Prolog是最強大的統一算法之一。

我已經到了現在的地步，如果我通過一個可驗證的正確輸入，Prolog會回來「真實」。如果我傳遞了一些不正確的東西，它會返回「錯誤」。現在我真正想在這種情況下得到一個錯誤消息，指出爲什麼類型不統一。如果我在SWI-Prolog中打開「跟蹤」模式，我或多或少會得到我正在尋找的內容，一步一步解釋爲什麼這些類型沒有統一。我的核心問題是，是否有可能以編程方式獲取此信息？如果需要的話，我願意編寫一個C擴展並直接鏈接到Prolog編譯器。另外，我不以任何方式與SWI-Prolog綁定，它只是我在谷歌上找到的第一個。

此外，作爲一個完整的旁觀者，是否有人知道序言中的任何好的教程，無論是Web格式還是實際的書？

Answer 1

我的感覺是，跟蹤，你沒有得到詳細的信息 爲什麼統一失敗，但你得到的信息，哪些目標 失敗。

如果後者的信息是你想要的，你可以自己做這個 ，因爲你可以測試你的代碼。只需更換 每一個進球

.. 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. 

當然你也可以更換寫/ 1和NL/0聲明與 什麼都適合你。這是一個例子。首先，儀表 Prolog的文本：

?- [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. 

再見