--- a/src/paip-compiled.lisp Wed Mar 23 17:43:02 2016 +0000
+++ b/src/paip-compiled.lisp Thu Mar 24 15:17:51 2016 +0000
@@ -17,6 +17,13 @@
item sequence :test (complement test)
keyword-args)))
+(defun find-anywhere (item tree)
+ "Does item occur anywhere in tree?"
+ (if (atom tree)
+ (if (eql item tree) tree)
+ (or (find-anywhere item (first tree))
+ (find-anywhere item (rest tree)))))
+
(defun interned-symbol (&rest args)
(intern (format nil "~{~A~}" args)))
@@ -209,27 +216,37 @@
(nconc
(mapcar #'make-= parameters (relation-arguments (clause-head clause)))
(clause-body clause))
- continuation)))
+ continuation
+ (mapcar #'self-cons parameters))))
-(defun compile-body (body continuation)
+(defun compile-body (body continuation bindings)
"Compile the body of a clause."
(if (null body)
`(funcall ,continuation)
(let* ((goal (first body))
(macro (prolog-compiler-macro (predicate goal)))
(macro-val (when macro
- (funcall macro goal (rest body) continuation))))
+ (funcall macro goal (rest body) continuation bindings))))
(if (and macro (not (eq macro-val :pass)))
macro-val
(compile-call
(make-predicate (predicate goal)
(relation-arity goal))
- (mapcar #'(lambda (arg) (compile-arg arg))
+ (mapcar #'(lambda (arg) (compile-arg arg bindings))
(relation-arguments goal))
(if (null (rest body))
continuation
`#'(lambda ()
- ,(compile-body (rest body) continuation))))))))
+ ,(compile-body (rest body) continuation
+ (bind-new-variables bindings goal)))))))))
+
+(defun bind-new-variables (bindings goal)
+ "Extend bindings to include any unbound variables in goal."
+ (let ((variables (remove-if #'(lambda (v) (assoc v bindings))
+ (variables-in goal))))
+ (nconc (mapcar #'self-cons variables) bindings)))
+
+(defun self-cons (x) (cons x x))
(defun compile-call (predicate args continuation)
`(,predicate ,@args ,continuation))
@@ -244,26 +261,87 @@
#'(lambda ,arglist .,body)))
(def-prolog-compiler-macro
- = (goal body continuation)
+ = (goal body continuation bindings)
(let ((args (relation-arguments goal)))
(if (/= (length args) 2)
:pass
- `(when ,(compile-unify (first args) (second args))
- ,(compile-body body continuation)))))
+ (multiple-value-bind (code1 bindings1)
+ (compile-unify (first args) (second args) bindings)
+ (compile-if code1 (compile-body body continuation bindings1))))))
+
+(defun compile-unify (x y bindings)
+ "Return 2 values: code to test if x any y unify, and a new binding list."
+ (cond
+ ((not (or (has-variable-p x) (has-variable-p y)))
+ (values (equal x y) bindings))
+ ((and (consp x) (consp y))
+ (multiple-value-bind (code1 bindings1)
+ (compile-unify (first x) (first y) bindings)
+ (multiple-value-bind (code2 bindings2)
+ (compile-unify (rest x) (rest y) bindings1)
+ (values (compile-if code1 code2) bindings2))))
+ ((variable-p x) (compile-unify-variable x y bindings))
+ (t (compile-unify-variable y x bindings))))
+
+(defun compile-if (pred then-part)
+ (case pred
+ ((t) then-part)
+ ((nil) nil)
+ (otherwise `(if ,pred ,then-part))))
-(defun compile-unify (x y)
- "Return code that tests if the items unify."
- `(unify! ,(compile-arg x) ,(compile-arg y)))
+(defun compile-unify-variable (x y bindings)
+ "X is a variable, and Y might be."
+ (let* ((xb (follow-binding x bindings))
+ (x1 (if xb (cdr xb) x))
+ (yb (if (variable-p y) (follow-binding y bindings)))
+ (y1 (if yb (cdr yb) y)))
+ (cond
+ ((or (eq x '?) (eq y '?)) (values t bindings))
+ ((not (and (equal x x1) (equal y y1)))
+ (compile-unify x1 y1 bindings))
+ ((find-anywhere x1 y1) (values nil bindings))
+ ((consp y1)
+ (values `(unify! ,x1 ,(compile-arg y1 bindings))
+ (bind-variables-in y1 bindings)))
+ ((not (null xb))
+ (if (and (variable-p y1) (null yb))
+ (values 't (extend-bindings y1 x1 bindings))
+ (values `(unify! ,x1 ,(compile-arg y1 bindings))
+ (extend-bindings x1 y1 bindings))))
+ ((not (null yb))
+ (compile-unify-variable y1 x1 bindings))
+ (t (values 't (extend-bindings x1 y1 bindings))))))
+(defun bind-variables-in (exp bindings)
+ "Bind all variables in exp to themselves, and add that to bindings (except for already-bound vars)."
+ (dolist (var (variables-in exp))
+ (when (not (get-binding var bindings))
+ (setf bindings (extend-bindings var var bindings))))
+ bindings)
-(defun compile-arg (arg)
+(defun follow-binding (var bindings)
+ "Get the ultimate binding of var according to the bindings."
+ (let ((b (get-binding var bindings)))
+ (if (eq (car b) (cdr b))
+ b
+ (or (follow-binding (cdr b) bindings)
+ b))))
+
+(defun compile-arg (arg bindings)
"Generate code for an argument to a goal in the body."
- (cond ((variable-p arg) arg)
+ (cond ((eql arg '?) '(?))
+ ((variable-p arg)
+ (let ((binding (get-binding arg bindings)))
+ (if (and (not (null binding))
+ (not (eq arg (binding-value binding))))
+ (compile-arg (binding-value binding) bindings)
+ arg)))
((not (has-variable-p arg)) `',arg)
((proper-list-p arg)
- `(list .,(mapcar #'compile-arg arg)))
- (t `(cons ,(compile-arg (first arg))
- ,(compile-arg (rest arg))))))
+ `(list .,(mapcar #'(lambda (a) (compile-arg a bindings))
+ arg)))
+ (t `(cons ,(compile-arg (first arg) bindings)
+ ,(compile-arg (rest arg) bindings)))))
(defun has-variable-p (x)
"Is there a variable anywhere in the expression x?"
@@ -289,6 +367,7 @@
:collect '(undo-bindings! old-trail)
:collect expression)))))
+
(defun bind-unbound-vars (parameters expr)
"Bind any variables in expr (besides the parameters) to new vars."
(let ((expr-vars (set-difference (variables-in expr) parameters)))
@@ -297,3 +376,98 @@
expr-vars)
,expr)
expr)))
+
+
+(defmacro <- (&rest clause)
+ "Add a clause to the database."
+ `(add-clause ',(make-anonymous clause)))
+
+
+(defun make-anonymous (exp &optional (anon-vars (anonymous-variables-in exp)))
+ "Replace variables that are only used once with ?."
+ (cond ((consp exp)
+ (cons (make-anonymous (first exp) anon-vars)
+ (make-anonymous (rest exp) anon-vars)))
+ ((member exp anon-vars) '?)
+ (t exp)))
+
+(defun anonymous-variables-in (tree)
+ "Return a list of all variables that appear only once in tree."
+ (let ((seen-once nil)
+ (seen-more nil))
+ (labels ((walk (x)
+ (cond
+ ((variable-p x)
+ (cond ((member x seen-once)
+ (setf seen-once (delete x seen-once))
+ (push x seen-more))
+ ((member x seen-more) nil)
+ (t (push x seen-once))))
+ ((consp x)
+ (walk (first x))
+ (walk (rest x))))))
+ (walk tree)
+ seen-once)))
+
+
+
+;;;; UI -----------------------------------------------------------------------
+(defvar *uncompiled* nil "Prolog symbols that have not been compiled.")
+
+(defun add-clause (clause)
+ "Add a clause to the database, indexed by the head's predicate."
+ (let ((pred (predicate (clause-head clause))))
+ (pushnew pred *db-predicates*)
+ (pushnew pred *uncompiled*)
+ (setf (get pred clause-key)
+ (nconc (get-clauses pred) (list clause)))
+ pred))
+
+
+(defun top-level-prove (goals)
+ "Prove the list of goals by compiling and calling it."
+ (clear-predicate 'top-level-query)
+ (let ((vars (delete '? (variables-in goals))))
+ (add-clause `((top-level-query)
+ ,@goals
+ (show-prolog-vars ,(mapcar #'symbol-name vars)
+ ,vars))))
+ (run-prolog 'top-level-query/0 #'ignorelol)
+ (format t "~&No.")
+ (values))
+
+(defun run-prolog (procedure continuation)
+ "Run an 0-ary Prolog prodecure with the given continuation."
+ (prolog-compile-symbols)
+ (setf (fill-pointer *trail*) 0)
+ (setf *var-counter* 0)
+ (catch 'top-level-prove
+ (funcall procedure continuation)))
+
+(defun prolog-compile-symbols (&optional (symbols *uncompiled*))
+ (mapc #'prolog-compile symbols)
+ (setf *uncompiled* (set-difference *uncompiled* symbols)))
+
+(defun ignorelol (&rest args)
+ (declare (ignore args))
+ nil)
+
+(defun show-prolog-vars/2 (var-names vars cont)
+ (if (null vars)
+ (format t "~&Yes")
+ (loop :for name :in var-names
+ :for var :in vars :do
+ (format t "~&~A = ~A" name (deref-exp var))))
+ (if (continue-ask)
+ (funcall cont)
+ (throw 'top-level-prove nil)))
+
+(defun deref-exp (exp)
+ (if (atom (deref exp))
+ exp
+ (cons (deref-exp (first exp))
+ (deref-exp (rest exp)))))
+
+
+(defmacro ?- (&rest goals)
+ `(top-level-prove ',(replace-wildcard-variables goals)))