Show attempted unifications of every predicate clause in the graphical debugger?

I’m using: SWI-Prolog version 8.1.9.

When tracing in the graphical debugger, it automatically skips any clauses that can’t be unified with, which is very useful in most cases. Sometimes though, I’d like to see the attempted unifications so I can see the variable state at the time and detect clauses that are structurally wrong for the desired logic. A common example is when I have clause looking for the end of a list to stop processing for the predicate, but when it’s “called”, the element in the position of the empty set is already bound, defeating that clause since it can’t unify with the empty set. There are other use cases besides this.

Is there a way to get the debugger to trace through all clauses of predicate so you can see the variable state at the time for each clause and detect why a certain clause isn’t unifying when you think it should? I tried the “Show Unifications” button in the debugger toolbar, but that didn’t do i.

1 Like

That is quite a common problem, but the way I solve it is not to rely so heavily on the debugger to do the work for me. Note I am doing this off the top of my head so the exact steps may not be exactly correct.

When using the graphical debugger and single stepping (press space bar) a query (which can be a line in a clause) you expect to succeed then fails, use the redo button to restore the state of the variables. Now open a editor, e.g. NotePad++ and then copy the offending value(s) of the current data that is being used in the query to the editor. Now copy the head(s) of the predicate to the editor and look at the patterns while thinking of how the unification will occur and be very diligent even at times highlighting individual characters as you do the comparison. When I do this I often find my mistake which is usually because I forgot to add something like [], misspelled something like opearter or other such mistakes.

If that doesn’t find the problem then again looking at the values after the redo check to see if a variable that should be free was bound, or if part of a pattern was bound that should be free. In other words, you are expecting the unification to take place with a variable, but because it is bound and doesn’t match the given value will not unify. I often make this mistake when threading variables, e.g. S0,S1,S2,S3 … S into a predicate, then add a few more statements to the clause and renumber the state wrong.

Another thing I do to significantly cut down on these problem is (you heard me say it many times) create lots of specific test cases. Usually it is the assertions that fail and then it is even easier to spot the problem because the assertion gives the expected result and the actual result and putting those into an editor with one above the other and comparing is easy. Also when in the editor, the characters can be lined up so that variables can be matched up with bound values. :smiley:

Here is an actual test case that worked and I modified by putting a typo into the expected result.

ERROR: d:/cellular information/source code/prolog/pdf/
        test 5 (forall bindings = ["/a 1 def a type",dict(user,[kv(a,integer(2))]),operand_stack([literal_name(integertype)])]): assertion failed
        Assertion: dict(user,[kv(a,integer(1))])==dict(user,[kv(a,integer(2))])

putting the two lines top to bottom


the mistake becomes obvious.

1 Like

For complex terms that don’t unify as expected, I find it helpful to open a shell and paste the term into it, then wrap it with print_term. Or paste it into a new source window and use the tab key to indent it properly. This is easy to do in emacs; I don’t know about other editors/IDEs.

I was hoping to avoid having to note about complex terms because the details get a lot more complicated. While I have used what you suggested, a current technique that I am using for my PostScript interpreter which carries around a lot of state in an environment variable is this:

environment/1 returns the initial environment.

    ) :-

dictionary_stack(Dictionary_stack) :-
    Dictionary_stack =

dictionary_user(Dictionary_user) :-
    Dictionary_user = dict(user,[]).

dictionary_global(Dictionary_global) :-
    Dictionary_global = dict(global,[]).

dictionary_system(Dictionary_system) :-
    Dictionary_system =


Then there are various PostScript operators that modify the environment, e.g.

executable(Environment0,Environment,operator(dup)) :-
    Environment0 = environment(stacks(operand_stack(Operands0),Dictionary_stack,Execution_stack,Graphics_state_stack,Clipping_path_stack),save_level(Save_level)),
    Environment = environment(stacks(operand_stack(Operands),Dictionary_stack,Execution_stack,Graphics_state_stack,Clipping_path_stack),save_level(Save_level)).

dup([Value|Operands0],Operands) :-
    Operands1 = [Value,Value|Operands0],
        Length =< Maxium_operand_stack_size
        Operands = Operands1
        Operands = [error(stackoverflow),Value|Operands0]

Now in the test case to avoid having to check all parts of the environment it just pulls out the parts that are expected to change and uses assertion/1 on them, e.g.

% Test operator dup
postscript_operand_stack_test_case("3 dup"                            ,operand_stack([integer(3),integer(3)]) ).
postscript_operand_stack_test_case("dup"                              ,operand_stack(error(stackunderflow)) ).
% dup stackoverflow % See test case 002

test(0001, [forall(postscript_operand_stack_test_case(Input,Expected_operand_stack))]) :-
    Environment = environment(stacks(Operand_stack,Dictionary_stack,execution_stack([]),graphics_state_stack([]),clipping_path_stack([])),save_level(0)),
    assertion( Operand_stack == Expected_operand_stack ).

% These test resize the stack to force a stackoverflow error
postscript_operator_with_stack_resize_test_case(3,"1 2 3 dup"          ,operand_stack([error(stackoverflow),integer(3),integer(2),integer(1)]) ).

test(0002, [forall(postscript_operator_with_stack_resize_test_case(Stack_size,Input,Expected_operand_stack))]) :-
    Environment = environment(stacks(Operand_stack,Dictionary_stack,execution_stack([]),graphics_state_stack([]),clipping_path_stack([])),save_level(0)),
    assertion( Operand_stack == Expected_operand_stack ),

There are other test that check other parts of the environment or combinations of changes but it does keep the length of each test case smaller.

It took some time to write the initial test case and get it so that I could build the data in environment in pieces and use it as needed, but now that the foundation is in place, adding and testing new operators is running like a factory production. However I still have to add some more parts to environment and some of them are very large, but this pattern looks like it will handle it without modification to the test cases.

1 Like

There is no trace event between the call and finishing the head unification and thus there is nothing to show. It tries all clauses (logically; it might skip some/most due to indexing). As @EricGT says, retry to get the original arguments. Next, it would be possible to create something more informative. One option would be to use something similar to term_subsumer/3 to find the generalization required to make a clause head match and present this in some clever way to the user. Getting that right and intuitive is probably not trivial. My answer is typically not to make the head too complicated :slight_smile:

1 Like

Thanks Jan and agreed. A lot of my trouble comes from finding out that the the books/articles I have read on difference lists are a bit deceptive. As they say, the concept of adding a variable to the end of one list and then pairing it with another that carries that variable around for unification that ends up appending the primary list is straightforward.

But, really understanding how all the different ways that tail variable can get unified through all of the paths of your code is a very tricky affair. Especially if the control flow of your predicate brachiates frequently (like a Hydra), a fairly common occurrence when building or traversing trees with multiple child nodes that have to be recursively examined. Pretty much all the errors I’ve been struggling with have come from the tail variable unifying somewhere I didn’t expect it to, and thus causing some other goal to fail.

TL;DR (in other words)

I’m going through the school of hard knocks of actually living with difference lists. :slight_smile:

I think my most common mistake is typos, so term_subsumer/3 isn’t going to help a lot. But it seems like a useful thing to try when pretty-printing terms doesn’t.

My problems usually aren’t complicated heads but complicated arguments to predicates. :wink: