Arguments are not sufficiently instantiated in clause/2

Question

i'm trying to write a simple meta-interpreter for the unification in prolog, this is what i got so far

unify(A,B):-var(A),A=B.
unify(A,B):-nonvar(A),var(B),B=A.
unify(A,B):-compound(A),compound(B),A=..[F|ArgsA],B=..[F|ArgsB],unify_args(ArgsA,ArgsB).

unify_args([A|TA],[B|TB]):-unify(A,B),unify_args(TA,TB).
unify_args([],[]).


meta(true).
meta((A,B)):- meta(A),meta(B).
meta(C):-clause(H,B), unify(H,C), meta(B).

the problem that i'm getting is that when i try to unify two variables e.g

meta((A,B)). 

i get the correct result

A = B, B = true .

but when i try to unify anything else for example

meta((a,a)).

or even a compund i get the following error:

ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR:   [12] clause(_4306,_4308)
ERROR:   [11] meta(a) at path_redacted/unify1.pl:22
ERROR:   [10] meta((a,a)) at path_redacted/unify1.pl:21
ERROR:    [9] <user>

i can't understand why clause/2 would need instantiated argouments in this particular case, or maybe i'm missing something else?

Thank you for any help

Answer 1

As Will Ness pointed out in a comment, clause/2 requires the Head to be instantiated.

As written, your meta-interpreter tries to enumerate all clauses of all predicates in the program to find ones that unify with the goal term C. You will have to restrict this to only enumerating clauses that match C. One way to do this would be to call clause(C, Body) directly. I guess you want to avoid this, since this would cheat by doing the unification for you.

The other way is to copy C's functor, but not its arguments. You can use this copy to look up clauses for the predicate of interest, but you will still be able to do the unification yourself.

Here is how you can do such a "skeleton" copy:

?- C = f(x, y), functor(C, Functor, Arity), functor(Skeleton, Functor, Arity).
C = f(x, y),
Functor = f,
Arity = 2,
Skeleton = f(_70, _72).

In the context of your meta-interpreter, something like this gets you closer to what you want:

meta(Goal) :-
    functor(Goal, Functor, Arity),
    functor(Head, Functor, Arity),
    clause(Head, Body),
    unify(Head, Goal),
    meta(Body).

For example, using this example program:

f(x).
g(y).

fg(X, Y) :-
    f(X),
    g(Y).

We get:

?- meta(fg(X, Y)).
X = x,
Y = y ;
ERROR: No permission to access private_procedure `true/0'
ERROR: In:
ERROR:   [12] clause(true,_2750)
...

The solution is found correctly, but backtracking for further answers tries to access a clause for true. This is not allowed by SWI-Prolog. You will have to be more careful about making the clauses of the meta-interpreter mutually exclusive. You will probably need to place cuts.