Hooking into prolog's unification trace output

Question

I'm trying to investigate the feasibility of a project of having a custom type inference language on an untyped language. (The language itself isn't important, but it happens to be PHP). My first idea is to run type unification on this. I've programmed a bit in Haskell, so I know how type unification works from an end-user's point of view, but I've never dug super deep into the details of the algorithm.

At this point, I can parse a PHP code file, build up a corresponding set of rules, and want to start running a unification algorithm against those rules. Rather than re-invent the wheel, I figured I'd use an existing unification algorithm, and AFIAK, Prolog is one of the most robust unification algorithms out there.

I've gotten to the point now where if I pass in a verifiable correct input, Prolog comes back with "true." And if I pass in something that is incorrect, it comes back with "false." Now what I really want in that scenario though is to get an error message indicating why the types did not unify. If I turn on "trace" mode in SWI-Prolog, I get more or less what I am looking for, a step-by-step explanation of why the types did not unify. My core question is, is it possible to get this information programmatically? I am willing to write a C extension and link directly to the Prolog compiler if that's what it takes. Also, I'm not tied to SWI-Prolog in any way, it's just the first one I found on google.

Also, as a complete aside, does anybody know any good tutorials in prolog, either in Web format or as an actual book?

Answer 1

My feeling is that with trace, you don't get detailed information why a unification fails, but you get information which goals fail.

If the latter information is what you want, you can do this by yourself, in that you instrument your code. Just replace every goal

 .. A ..

By the following code:

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

With the following definitions:

 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.

Of course you can replace the write/1 and nl/0 statements with what ever suits you. Here is an example. First the instrumented Prolog text:

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

And now the instrumented query:

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

Bye