about the Prolog implementation

I just want to add the capability to handle lisp query into the initial Prolog implementation in OnLisp text. Since this capability is introduced in the following chapater (a new implementation), I just copied from new implementation and made some modification.

Here are the functions/macros I modified/added.

(=defun prove-query (expr binds)
    (case (car expr)
      (and (prove-and (cdr expr) binds))
      (or (prove-or (cdr expr) binds))
      (not (prove-not (cadr expr) binds))
          (lisp (gen-lisp (cadr expr) binds)) ;;; added
      (t (prove-simple expr binds))))

(defmacro with-binds (binds expr)
  `(let ,(mapcar #'(lambda (v) `(,v (fullbind ,v ,binds)))
         (vars-in expr))
     (eval ,expr)))             ;;; copied the whole macro from new implementaion and modified this line.

(=defun gen-lisp (expr binds)  ;;; copied from new implementation but modified
  (if (with-binds binds expr)
       (=values binds)
     (fail)))

But when I run the code below, it complains a variable is not defined.

(<- (ordered (?x)))

(<- (ordered (?x ?y . ?ys))
    (lisp (<= ?x ?y))
    (ordered (?y . ?ys)))

(with-inference (ordered (1 3 6))
  (print t))

*** - EVAL: variable ?G3159 has no value
The following restarts are available:
USE-VALUE      :R1      Input a value to be used instead of ?G3159.
STORE-VALUE    :R2      Input a new value for ?G3159.
ABORT          :R3      Abort main loop

I traced =gen-lisp and expand the macro "with-binds" but found nothing interesting.

(macroexpand '(with-binds '((?G3161 6) (?G3160 . 3) (?G3159 . 1)) '(<= ?G3160 ?G3159)))

(LET
 ((?G3160 (FULLBIND ?G3160 '((?G3161 6) (?G3160 . 3) (?G3159 . 1))))
  (?G3159 (FULLBIND ?G3159 '((?G3161 6) (?G3160 . 3) (?G3159 . 1)))))
 (EVAL '(<= ?G3160 ?G3159))) ;

Any ideas about this?

By the way, here is the complete code

https://drive.google.com/file/d/0B7t_DLbSmjMNRVh5SDBXdUVheDg/view?usp=sharing

Thanks in advance.

Solution

(eval form) evaluates form in the null lexical environment, which means that ?G3160 and ?G3159 are not bound inside the call. Indeed, symbols are resolved during compilation, and there is no information about lexical bindings anymore at runtime. I mention compilation but even if you ran your code in an interpreter, there would be no lexical-symbol-value function available for you to resolve a binding, given a symbol at runtime.

The good news is that you don't need to wrap the form in an eval in your case. The difficulty is that the with-binds introduces another level of quotation (expr is quoted). Here is how I would write gen-lisp:

(=defun gen-lisp (expr binds)
  `(let ,(mapcar #'(lambda (v) `(,v (fullbind ,v ,binds)))
         (vars-in expr))
     (if ,expr
         (=values binds)
         (fail))))