;; From Paul Graham's Ansi Common Lisp book.
;; Minor re-orgs by Tim Menzies

(defun match (x y &optional binds)
  "Return any bindings, and t/nil, after matching x to y."
  (cond 
   ((eql x y)        (values binds t))
   ((assoc x binds)  (match (binding x binds) y binds))
   ((assoc y binds)  (match x (binding y binds) binds))
   ((var? x)         (values (cons (cons x y) binds) t))
   ((var? y)         (values (cons (cons y x) binds) t))
   (t
    (when (and (consp x) (consp y))
      (multiple-value-bind (b2 yes) 
                           (match (car x) (car y) binds)
        (and yes (match (cdr x) (cdr y) b2)))))))

(defun var? (x)
  "Does the symbol 'x' start with a question mark?"
  (and (symbolp x) 
       (eql (char (symbol-name x) 0) #\?)))

(defun binding (x binds)
  "Chase x's bindings in the 'binds' alist." 
  (let ((b (assoc x binds)))
    (if b
        (or (binding (cdr b) binds)
            (cdr b)))))

(defparameter  *rules* (make-hash-table)
  "*rules* are a hash table indexed on functor of hear.")

(defmacro <- (head &optional body)
  "Clauses have at least one head and N>=0 subgoals in the body.
   The cdr of the head are the arguments.
   Clauses are indexed by the car of the heady."
  `(length (push (cons (cdr ',head) ',body)
                 (gethash (car ',head) *rules*))))

(defun prove (expr &optional binds)
  "Return the bindings (if any) after proving expr,
     or nil otherwise."
  (case (car expr)
    (and (prove-and    (reverse (cdr expr))  binds))
    (or  (prove-or     (cdr expr)            binds))
    (not (prove-not    (cadr expr)           binds))
    (t   (prove-simple (car expr) (cdr expr) binds))))

(defun prove-simple (pred args binds)
  "Run down the clause list. If any head matches,
   check the body." 
  (labels  
      ((worker (r)
	 (let ((head (car r))
	       (body (cdr r)))
	   (multiple-value-bind (b2 yes) 
	       (match args head binds)
	     (when yes
	       (if body            ; if the cons has ants...
		   (prove body b2) ; then prove those ands
		   (list b2))))))) ; else, retun the bindings
       (let* ((relevant (gethash pred *rules*))
	      (renames  (mapcar #'change-vars relevant)))
	 (mapcan #'worker renames))))

(defun change-vars (r)
  "Rename all the variables with some gensym-ed name."
  (sublis (mapcar #'(lambda (v) (cons v (gensym "?")))
                  (vars-in r))
          r))

(defun vars-in (expr)
  "Find all the vars."
  (if (atom expr)
      (if (var? expr) (list expr))
      (union (vars-in (car expr))
             (vars-in (cdr expr)))))

(defun prove-and (clauses binds)
  "Prove the car, prove-and the cdr."
  (if (null clauses)
      (list binds)
      (mapcan #'(lambda (b)
                  (prove (car clauses) b))
              (prove-and (cdr clauses) binds))))

(defun prove-or (clauses binds)
  "Find all the ways you can prove any part of the or."
  (mapcan #'(lambda (c) (prove c binds))
          clauses))

(defun prove-not (clause binds)
  "If you can't prove it, succeed."
  (unless (prove clause binds)
    (list binds)))

(defmacro with-answer (query &body body)
  "For all the sets of bindings, replace the
   references to those bindings in the body,
   then call the body."
  (let ((binds (gensym)))
    `(dolist (,binds (prove ',query))
       (let ,(mapcar #'(lambda (v)
                         `(,v (binding ',v ,binds)))
                     (vars-in query))
         ,@body))))