Here's the issue boiled down to a simpler test case :-) First, swi-prolog:

# cat 


foo(N) :- N.

bar(a(X)) :- a(X).

# swipl -f 
% /root/prolog/ compiled 0.00 sec, 2,800 bytes ...

?- trace.

[trace]  ?- bar(a(Z)).
   Call: (6) bar(a(_G386)) ? creep
   Call: (7) a(_G386) ? creep
   Exit: (7) a(3) ? creep
   Exit: (6) bar(a(3)) ? creep
Z = 3.

[trace]  ?- foo(a(Z)).
   Call: (6) foo(a(_G386)) ? creep
   Call: (7) a(_G386) ? creep
   Exit: (7) a(3) ? creep
   Exit: (6) foo(a(3)) ? creep
Z = 3.

In both cases, Z is correctly bound to 3. (The foo rule is the one we are 
interested in.)

$ cat t.l 

(be a (3))

(be foo (@C)
  (@C -> @C))

(be bar ((a @N))
   (a @N))

$ ./pil  t.l 
: (? a bar (bar (a @X)))
1 (bar (a @N))
1 (a 3)
-> NIL

That is correct:  @X=3  ... however :

: (? a foo (foo (a @X)))
1 (foo (a @X))
-> NIL

But they should be the same, as @X = 3 is a (is the) solution. Moreover, in foo 
(a @X) is never even tried to be proven.   

So I think this test case demonstrates the issue.  

> I still don't understand why this test of @A and/or @F for
> being non-NIL is necessary at all. This looks unusual to me. 

  holds(A,S) :- restoreSitArg(A,S,F), F ;
           \+ restoreSitArg(A,S,F), isAtom(A), A.

Me too. At first, I also thought they simply were testing for non-NIL there. 

But the intent of the 'naked' F and A clauses there seems to be this: If the 
data bound to F (or A) is itself a clause, then that clause gets proved and 
variables in it get unified/bound. 

So after the first restoreSitArg(A,S,F), F starts out as partially bound to a 
clause like on(N,s0) - which itself has an unbound variable, N. 

After F is proven, N is bound to 3 (because on(3,s0) is asserted elsewhere, and 
so N = 3 is a solution). 

A bit tricky, with variables bound to clauses which, in turn, have in them 
other unbound variables that may get bound.

Using call/1 there (not sure if this is the way I should use it) gives similar 
results, where (a @X) is not attempted to be proven. 

$ cat t.l 
(be a (3))

(be foo (@C)
  # (@C -> @C))
  (call @C))

$ ./pil  t.l 
: (? a foo call (foo (a @X)))
1 (foo (a @X))
1 (call (a @X))
-> NIL




Reply via email to