Подключение к выводу трассы объединения пролога

Question

Я пытаюсь исследовать выполнимость проекта по созданию языка вывода пользовательских типов на нетипизированном языке. (Сам язык не важен, но это PHP). Моя первая идея - запустить унификацию типов на этом. Я немного программировал на Haskell, так что я знаю, как унификация типов работает с точки зрения конечного пользователя, но я никогда не копался в деталях алгоритма.

На этом этапе я могу проанализировать файл кода PHP, создать соответствующий набор правил и начать запуск алгоритма унификации с этими правилами. Вместо того, чтобы заново изобретать колесо, я решил использовать существующий алгоритм объединения, и AFIAK, Prolog, является одним из самых надежных алгоритмов объединения.

Теперь я дошел до того, что если я передам проверяемый корректный ввод, Prolog вернется с "true". И если я передаю что-то неправильное, оно возвращается с "ложным". Теперь я действительно хочу получить в этом сценарии сообщение об ошибке, указывающее, почему типы не были объединены. Если я включаю режим "трассировки" в SWI-Prolog, я получаю более или менее то, что ищу, - пошаговое объяснение того, почему типы не унифицированы. Мой основной вопрос : возможно ли получить эту информацию программно? Я готов написать расширение C и ссылку непосредственно на компилятор Prolog, если это то, что нужно. Кроме того, я никоим образом не привязан к SWI-Прологу, это только первый, который я нашел в Google.

Кроме того, в дополнение к этому, кто-нибудь знает какие-нибудь хорошие учебники по прологу, либо в веб-формате, либо как настоящая книга?

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.

Конечно, вы можете заменить операторы 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.

до свидания