batch-approach.lisp

(in-package #:cl-prolog)
;; Prove of 11.2


(defun prove (goal bindings)
  "Return a list of possible solutions to goal."  
  (mapcan #'(lambda (clause)
              (let ((new-clause (rename-variables clause)))
                (prove-all (clause-body new-clause)
                           (unify goal (clause-head new-clause) bindings))))
          (get-clauses (predicate goal))))


(defun prove-all (goals bindings)
  "Return a list of solutions to the conjunction of goals."
  (cond ((eq bindings fail) fail)
        ((null goals) (list bindings))
        (t (mapcan #'(lambda (goal1-solution)
                       (prove-all (rest goals) goal1-solution))
                   (prove (first goals) bindings)))))


;; (defmacro ?- (&rest goals) `(prove-all ',goals no-bindings))

;; (defmacro ?- (&rest goals) `(top-level-prove ',goals))

(defmacro ?- (&rest goals) `(top-level-prove ',(replace-?-vars goals)))

(defun top-level-prove (goals)
  "Prove the goals, and print variables readably."
  (show-prolog-solutions
    (variables-in goals)
    (prove-all goals no-bindings)))


(defun show-prolog-solutions (vars solutions)
  "Print the variables in each of the solutions."  
  (if (null solutions)
      (format t "~&No.")
      (mapc #'(lambda (solution) (show-prolog-vars vars solution))
            solutions))
  (values))


(defun show-prolog-vars (vars bindings)
  "Print each variable with its binding."
  (if (null vars)
      (format t "~&Yes")
      (dolist (var vars)
        (format t "~&~a = ~a" var
                (subst-bindings bindings var))))
  (princ ";"))