#| ################################################################

Paul Graham's chapter 15 (see http://goo.gl/1OCc5) from Ansi COMMON
LISP (see http://www.paulgraham.com/acl.html) implements a minimal
Prolog system. It can't do everything that Prolog can do but, heh,
what do you expect of 100 lines of code.

################################################################ |#

(defun match (x y &optional binds)
  (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)
  (and (symbolp x) 
       (eql (char (symbol-name x) 0) #\?)))

(defun binding (x binds)
  (let ((b (assoc x binds)))
    (if b
        (or (binding (cdr b) binds)
            (cdr b)))))

(defvar *rules* (make-hash-table))

(defmacro <- (con &optional ant)
  `(length (push (cons (cdr ',con) ',ant)
                 (gethash (car ',con) *rules*))))

(defun prove (expr &optional binds)
  "graham's code, plus 4 extensions"
  (case (car expr)
     ((<= <  > >=) (if (prove-code expr binds) ; # 1
		       (list binds)))
     ((prints say) (prove-code expr binds) ; #2
                   (list binds))
     (is           (list (prove-is (second expr) (third expr) binds))) ; #3
     (do           (prove-code (second expr) binds) ; #4
		   (list binds))
     (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-is (var expr binds)
  (match var (prove-code expr binds) binds))

(defun prove-code (expr binds)
  (labels ((lets (binds want)
	     (mapcar #'(lambda (x) `(,x ',(binding x binds))) want)))
    (let* ((vars (lets binds (vars-in expr)))
	   (code `(let ,vars ,expr)))
      (eval code))))

(defun prove-simple (pred args binds)
  (mapcan #'(lambda (r)
              (multiple-value-bind (b2 yes) 
                                   (match args (car r) 
                                          binds)
                (when yes
                  (if (cdr r) 
                      (prove (cdr r) b2) 
                      (list b2)))))
          (mapcar #'change-vars 
                  (gethash pred *rules*))))

(defun change-vars (r)
  (sublis (mapcar #'(lambda (v) (cons v (gensym "?")))
                  (vars-in r))
          r))

(defun vars-in (expr)
  (if (atom expr)
      (if (var? expr) (list expr))
      (union (vars-in (car expr))
             (vars-in (cdr expr)))))


(defun prove-and (clauses binds)
  (if (null clauses)
      (list binds)
      (mapcan #'(lambda (b)
                  (prove (car clauses) b))
              (prove-and (cdr clauses) binds))))

(defun prove-or (clauses binds)
  (mapcan #'(lambda (c) (prove c binds))
          clauses))

(defun prove-not (clause binds)
  (unless (prove clause binds)
    (list binds)))

(defmacro with-answer (query &body body)
  (let ((binds (gensym)))
    `(dolist (,binds (prove ',query))
       (let ,(mapcar #'(lambda (v)
                         `(,v (binding ',v ,binds)))
		     (vars-in query))
	 (declare (ignorable ,@(vars-in query)))
       ,@body))))

(defun data1 ()
  (clrhash *rules*) ; must start with this
  (<- (= ?x ?x))
  (<- (person matt  m  23  40000))
  (<- (person dean  m  90  90000))
  (<- (person clint m 100 100000000))
  (<- (person marge f  80 100000000))
  (<- (younger ?x ?y) (and (person ?x ?g1   ?age1 ?salary1)
			   (do (format t "~a~%" ?x))
			   (person ?y ?g2 ?age2 ?salary2)
			   (not (= ?x ?y))
			   (is ?factor (/ 11 10))
			   (> (* ?age1 ?factor) ?age2)
			   (say "my isn't ~a too young" ?x)))
  (<- (sameSex ?x ?y) (and (person ?x ?gender ?a1)
			   (person ?y ?gender ?a2)))
  (<- (hates   ?x ?y) (and (sameSex ?x ?y) (younger ?y ?x)))
)


(defun data2 ()
  (clrhash *rules*) ; must start with this
  (<- (person matt  m  23  40000))
  (<- (person dean  m  90  90000))
  (<- (person clint m 100 100000000))
  (<- (person marge f  80 100000000))
  (<- (salary ?x ?salary) (person ?x ?gender ?age ?salary))
  (<- (old ?x)     (and (person ?x ?gender ?age ?salary)
			(> ?age 60)))
  (<- (rich ?x)    (and (salary ?x  ?salary)
			(> ?salary 1000000)))
  (<- (target ?x ?salary) (and (old ?x)
			       (rich ?x)
			       (salary ?x ?salary))))


(deftest !one ()
  (data1)
  (with-answer (younger ?x ?y)
    (format t "~a hates ~a~%" ?x ?y)))


(deftest !two ()
  (let ((out 0))
    (data2)
    (with-answer (target ?x ?sal)
      (incf out ?sal))
    out))



(deftest !three ()
  (data1)
  (<- (age ?x ?age) (person ?x ?gender ?age ?salary))
  (with-answer (and (age ?x ?age) (not (and (age ?y ?older) (> ?older ?age))))
    (print ?x)))