--- a/bones.asd Sat Aug 20 21:56:13 2016 +0000
+++ b/bones.asd Sat Aug 20 21:56:20 2016 +0000
@@ -22,8 +22,7 @@
(:module "src"
:serial t
:components
- ((:file "paip")
- (:file "utils")
+ ((:file "utils")
(:file "circle")
(:module "wam"
:serial t
@@ -68,7 +67,6 @@
:components ((:file "bones")
(:file "utils")
(:file "circle")
- (:file "paip")
(:file "wam")
(:file "99")
(:file "taop")))))
--- a/docs/api.lisp Sat Aug 20 21:56:13 2016 +0000
+++ b/docs/api.lisp Sat Aug 20 21:56:20 2016 +0000
@@ -1,7 +1,7 @@
(ql:quickload "cl-d-api")
(defparameter *document-packages*
- (list "BONES.PAIP"))
+ (list "BONES.WAM"))
(defparameter *output-path*
#p"docs/03-reference.markdown" )
--- a/package-test.lisp Sat Aug 20 21:56:13 2016 +0000
+++ b/package-test.lisp Sat Aug 20 21:56:20 2016 +0000
@@ -20,13 +20,6 @@
#:%append
#:%member))
-(defpackage #:bones-test.paip
- (:use
- #:cl
- #:1am
- #:bones.quickutils
- #:bones.paip))
-
(defpackage #:bones-test.wam
(:use
#:cl
--- a/package.lisp Sat Aug 20 21:56:13 2016 +0000
+++ b/package.lisp Sat Aug 20 21:56:20 2016 +0000
@@ -99,42 +99,6 @@
#:?
#:!))
-(defpackage #:bones.paip
- (:use
- #:cl
- #:bones.quickutils)
- (:documentation "Test?")
- (:export
-
- ;; Unification, constants
- #:unify
- #:fail
- #:no-bindings
- #:*check-occurs*
-
- ;; Destructive unification
- #:unify!
- #:unbound
- #:bound-p
-
- ;; Database management
- #:clear-db
- #:clear-predicate
- #:fact
- #:rule
- #:add-fact
- #:rule-fact
-
- ;; Lisp data structures as results
- #:return-one
- #:return-all
-
- ;; Interactive queries
- #:query
- #:query-one
- #:query-all))
-
-
(defpackage #:bones
(:use #:cl #:bones.wam)
(:export
--- a/src/paip-compiled.lisp Sat Aug 20 21:56:13 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,460 +0,0 @@
-(in-package #:bones.paip)
-
-;;;; Utils
-(defun find-all (item sequence
- &rest keyword-args
- &key (test #'eql) test-not &allow-other-keys)
- "Find all elements of the sequence that match the item.
-
- Does not alter the sequence.
-
- "
- (if test-not
- (apply #'remove
- item sequence :test-not (complement test-not)
- keyword-args)
- (apply #'remove
- 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)))
-
-(defun new-symbol (&rest args)
- (make-symbol (format nil "~{~A~}" args)))
-
-(defun find-if-anywhere (test expr)
- (cond ((funcall test expr) t)
- ((consp expr) (or (find-if-anywhere test (car expr))
- (find-if-anywhere test (cdr expr))))
- (t nil)))
-
-
-;;;; UNIFICATION --------------------------------------------------------------
-;;;; Variables
-(define-constant unbound "Unbound"
- :test #'equal
- :documentation "A magic constant representing an unbound variable.")
-
-(defvar *var-counter* 0
- "The number of variables created so far.")
-
-(defstruct (var (:constructor ? ())
- (:print-function print-var))
- (name (incf *var-counter*)) ; The variable's name (defaults to a new number)
- (binding unbound)) ; The variable's binding (defaults to unbound)
-
-(defun print-var (var stream depth)
- (if (or (and (numberp *print-level*)
- (>= depth *print-level*))
- (var-p (deref var)))
- (format stream "?~A" (var-name var))
- (write var :stream stream)))
-
-(defun bound-p (var)
- "Return whether the given variable has been bound."
- (not (eq (var-binding var) unbound)))
-
-(defmacro deref (expr)
- "Chase all the bindings for the given expression in place."
- `(progn
- (loop :while (and (var-p ,expr) (bound-p ,expr))
- :do (setf ,expr (var-binding ,expr)))
- ,expr))
-
-
-;;;; Bindings
-(defvar *trail* (make-array 200 :fill-pointer 0 :adjustable t)
- "The trail of variable bindings performed so far.")
-
-(defun set-binding! (var value)
- "Set `var`'s binding to `value` after saving it in the trail.
-
- Always returns `t` (success).
-
- "
- (when (not (eq var value))
- (vector-push-extend var *trail*)
- (setf (var-binding var) value))
- t)
-
-(defun undo-bindings! (old-trail)
- "Undo all bindings back to a given point in the trail.
-
- The point is specified by giving the desired fill pointer.
-
- "
- (loop :until (= (fill-pointer *trail*) old-trail)
- :do (setf (var-binding (vector-pop *trail*)) unbound))
- (values))
-
-
-;;;; Unification
-(defun unify! (x y)
- "Destructively unify two expressions, returning whether it was successful.
-
- Any variables in `x` and `y` may have their bindings set.
-
- "
- (cond
- ;; If they're identical objects (taking bindings into account), they unify.
- ((eql (deref x) (deref y)) t)
-
- ;; If they're not identical, but one is a variable, bind it to the other.
- ((var-p x) (set-binding! x y))
- ((var-p y) (set-binding! y x))
-
- ;; If they're both non-empty lists, unify the cars and cdrs.
- ((and (consp x) (consp y))
- (and (unify! (first x) (first y))
- (unify! (rest x) (rest y))))
-
- ;; Otherwise they don't unify.
- (t nil)))
-
-
-;;;; COMPILATION --------------------------------------------------------------
-(deftype relation ()
- 'list)
-
-(deftype clause ()
- '(trivial-types:proper-list relation))
-
-(deftype non-negative-integer ()
- '(integer 0))
-
-
-(defun prolog-compile (symbol &optional (clauses (get-clauses symbol)))
- "Compile a symbol; make a separate function for each arity."
- (when (not (null clauses))
- (let* ((arity (relation-arity (clause-head (first clauses))))
- (matching-arity-clauses (clauses-with-arity clauses #'= arity))
- (other-arity-clauses (clauses-with-arity clauses #'/= arity)))
- (compile-predicate symbol arity matching-arity-clauses)
- (prolog-compile symbol other-arity-clauses))))
-
-(defun clauses-with-arity (clauses test arity)
- "Return all clauses whose heads have the given arity."
- (find-all arity clauses
- :key #'(lambda (clause)
- (relation-arity (clause-head clause)))
- :test test))
-
-
-(defun relation-arity (relation)
- "Return the number of arguments of the given relation.
-
- For example: `(relation-arity '(likes sally cats))` => `2`
-
- "
- (length (relation-arguments relation)))
-
-(defun relation-arguments (relation)
- "Return the arguments of the given relation.
-
- For example:
-
- * (relation-arguments '(likes sally cats))
- (sally cats)
-
- "
- (rest relation))
-
-
-(defun compile-predicate (symbol arity clauses)
- "Compile all the clauses for the symbol+arity into a single Lisp function."
- (let ((predicate (make-predicate symbol arity))
- (parameters (make-parameters arity)))
- (compile
- (eval
- `(defun ,predicate (,@parameters continuation)
- .,(maybe-add-undo-bindings
- (mapcar #'(lambda (clause)
- (compile-clause parameters clause 'continuation))
- clauses)))))))
-
-(defun make-parameters (arity)
- "Return the list (?arg1 ?arg2 ... ?argN)."
- (loop :for i :from 1 :to arity
- :collect (new-symbol '?arg i)))
-
-(defun make-predicate (symbol arity)
- "Returns (and interns) the symbol with the Prolog-style name symbol/arity."
- (values (interned-symbol symbol '/ arity)))
-
-
-(defun make-= (x y)
- `(= ,x ,y))
-
-(defun compile-clause (parameters clause continuation)
- "Transform away the head and compile the resulting body."
- (bind-unbound-vars
- parameters
- (compile-body
- (nconc
- (mapcar #'make-= parameters (relation-arguments (clause-head clause)))
- (clause-body clause))
- continuation
- (mapcar #'self-cons parameters))))
-
-(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 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 bindings))
- (relation-arguments goal))
- (if (null (rest body))
- continuation
- `#'(lambda ()
- ,(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))
-
-(defun prolog-compiler-macro (name)
- "Fetch the compiler macro for a Prolog predicate."
- (get name 'prolog-compiler-macro))
-
-(defmacro def-prolog-compiler-macro (name arglist &body body)
- "Define a compiler macro for Prolog."
- `(setf (get ',name 'prolog-compiler-macro)
- #'(lambda ,arglist .,body)))
-
-(def-prolog-compiler-macro
- = (goal body continuation bindings)
- (let ((args (relation-arguments goal)))
- (if (/= (length args) 2)
- :pass
- (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-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 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 ((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 #'(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?"
- (find-if-anywhere #'variable-p x))
-
-(defun proper-list-p (x)
- "Is x a proper (non-dotted) list?"
- (or (null x)
- (and (consp x) (proper-list-p (rest x)))))
-
-
-(defun maybe-add-undo-bindings (compiled-expressions)
- "Undo any bindings that need undoing.
-
- If there ARE any, also bind the trail before we start.
-
- "
- (if (= (length compiled-expressions) 1)
- compiled-expressions
- `((let ((old-trail (fill-pointer *trail*)))
- ,(first compiled-expressions)
- ,@(loop :for expression :in (rest compiled-expressions)
- :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)))
- (if expr-vars
- `(let ,(mapcar #'(lambda (var) `(,var (?)))
- 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)))
-
-
--- a/src/paip.lisp Sat Aug 20 21:56:13 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,418 +0,0 @@
-(in-package #:bones.paip)
-
-;;;; Types
-(deftype logic-variable ()
- 'symbol)
-
-(deftype binding ()
- '(cons logic-variable t))
-
-(deftype binding-list ()
- '(trivial-types:association-list keyword t))
-
-
-;;;; Constants
-(define-constant fail nil
- :documentation "Failure to unify")
-
-(define-constant no-bindings '((:bones-empty-bindings . t))
- :test 'equal
- :documentation "A succesful unification, with no bindings.")
-
-(defparameter *check-occurs* t
- "Whether to perform an occurs check.")
-
-
-;;;; Unification
-(defun variable-p (term)
- "Return whether the given term is a logic variable."
- (and (symbolp term)
- (equal (char (symbol-name term) 0)
- #\?)))
-
-
-(defun get-binding (variable bindings)
- "Return the binding (var . val) for the given variable, or nil."
- (assoc variable bindings))
-
-(defun has-binding (variable bindings)
- (not (null (get-binding variable bindings))))
-
-
-(defun binding-variable (binding)
- "Return the variable part of a binding."
- (car binding))
-
-(defun binding-value (binding)
- "Return the value part of a binding."
- (cdr binding))
-
-
-(defun lookup (variable bindings)
- "Return the value the given variable is bound to."
- (binding-value (get-binding variable bindings)))
-
-(defun extend-bindings (variable value bindings)
- "Add a binding (var . val) to the binding list (nondestructively)."
- (cons (cons variable value)
- (if (and (equal bindings no-bindings))
- nil
- bindings)))
-
-
-(defun check-occurs (variable target bindings)
- "Check whether the variable occurs somewhere in the target.
-
- Takes the bindings into account. This is expensive.
-
- "
- (cond
- ;; If the target is this variable, then yep.
- ((eql variable target) t)
-
- ;; The empty list doesn't contain anything.
- ((null target) nil)
-
- ;; The the target is a (different) variable that has a binding, we need to
- ;; check if the variable occurs in its bindings.
- ((and (variable-p target)
- (get-binding target bindings))
- (check-occurs variable (lookup target bindings) bindings))
-
- ;; If the target is a list, check if any of the elements contain the variable.
- ((listp target)
- (or (check-occurs variable (first target) bindings)
- (check-occurs variable (rest target) bindings)))
-
- ;; Otherwise we're safe.
- (t nil)))
-
-(defun unify (x y &optional (bindings no-bindings))
- "Unify the two terms and return bindings necessary to do so (or FAIL)."
- (flet ((unify-variable (variable target bindings)
- (cond
- ;; If we've already got a binding for this variable, we can try to
- ;; unify its value with the target.
- ((get-binding variable bindings)
- (unify (lookup variable bindings) target bindings))
-
- ;; If the target is ALSO a variable, and it has a binding, then we
- ;; can unify this variable with the target's value.
- ((and (variable-p target) (get-binding target bindings))
- (unify variable (lookup target bindings) bindings))
-
- ;; If this variable occurs in the target (including in something
- ;; in its bindings) and we're checking occurrence, bail.
- ((and *check-occurs* (check-occurs variable target bindings))
- fail)
-
- ;; Otherwise we can just bind this variable to the target.
- (t (extend-bindings variable target bindings)))))
- (cond
- ;; Pass failures through.
- ((eq bindings fail) fail)
-
- ;; Trying to unify two identical objects (constants or variables) can just
- ;; return the bindings as-is.
- ;;
- ;; ex: (unify :y :y) or (unify 'foo 'foo)
- ((eql x y) bindings)
-
- ;; Unifying a variable with something.
- ((variable-p x) (unify-variable x y bindings))
- ((variable-p y) (unify-variable y x bindings))
-
- ;; Unifying a non-variable with nil should fail, except for nil itself.
- ;; But that was handled with (eql x y).
- ((or (null x) (null y)) fail)
-
- ;; Unifying non-empty compound terms such as
- ;; (likes :x cats) with (likes sally :y).
- ((and (listp x) (listp y))
- (unify (rest x) (rest y) ; Unify the tails with the bindings gotten from...
- (unify (first x) (first y) bindings))) ; unifying the heads.
-
- ;; Otherwise we're looking at different constants, or a constant and a
- ;; compound term, so just give up.
- (t fail))))
-
-
-;;;; Substitution
-(defun substitute-bindings (bindings form)
- "Substitute (recursively) the bindings into the given form."
- (cond ((eq bindings fail) fail)
- ((eq bindings no-bindings) form)
- ((and (variable-p form) (get-binding form bindings))
- (substitute-bindings bindings
- (lookup form bindings)))
- ((atom form) form)
- (t (mapcar (curry #'substitute-bindings bindings) form))))
-
-(defun unifier (x y)
- "Unify x with y and substitute in the bindings to get the result."
- (substitute-bindings (unify x y) x))
-
-
-;;;; Database
-;;; A clause is an assertion in the database. There are two types.
-;;;
-;;; A fact is the "base" clause:
-;;;
-;;; (likes kim cats)
-;;;
-;;; A rule is a way to deduce new facts from existing information:
-;;;
-;;; ((likes sally :x)
-;;; (likes :x cats))
-;;;
-;;; Clauses are stored as lists. The head is the first item in the list, and
-;;; it's "the thing you're trying to prove". You prove it by proving all the
-;;; things in the tail of the list. For facts the tail is empty, so they are
-;;; trivially proven.
-;;;
-;;; A predicate is the named head of a part of a clause. In `(likes sally :x)`
-;;; the predicate is `likes`.
-;;;
-;;; Predicates are stored in the plists of their symbols, which is a little
-;;; insane, but it's how Norvig did it so I'll do it like this for now.
-(defvar *db-predicates* nil
- "A list of all the predicates in the database.")
-
-(defconstant clause-key 'bones.paip-clauses
- "The key to use in the symbol plist for the clauses.")
-
-(defun clause-head (clause)
- (first clause))
-
-(defun clause-body (clause)
- (rest clause))
-
-
-(defun get-clauses (pred)
- (get pred clause-key))
-
-(defun set-clauses (pred clauses)
- (setf (get pred clause-key) clauses))
-
-
-(defun predicate (relation)
- (first relation))
-
-
-(defun wildcard-variable-p (form)
- (and (symbolp form) (string= (symbol-name form) "?")))
-
-(defun replace-wildcard-variables (form)
- (cond
- ((wildcard-variable-p form) (gensym "?"))
- ((atom form) form)
- ((consp form) (cons (replace-wildcard-variables (car form))
- (replace-wildcard-variables (cdr form))))
- (t (mapcar #'replace-wildcard-variables form))))
-
-
-(defun add-clause (clause)
- (let ((pred (predicate (clause-head clause))))
- (assert (and (symbolp pred)
- (not (variable-p pred))))
- (pushnew pred *db-predicates*)
- (set-clauses pred
- (nconc (get-clauses pred) (list clause)))
- pred))
-
-
-(defun add-rule (clause)
- (add-clause (replace-wildcard-variables clause)))
-
-(defmacro rule (&rest clause)
- `(add-rule ',clause))
-
-(defun add-fact (body)
- (add-clause (list (replace-wildcard-variables body))))
-
-(defmacro fact (&rest body)
- `(add-fact ',body))
-
-
-(defun clear-predicate (predicate)
- (setf (get predicate clause-key) nil))
-
-(defun clear-db ()
- (mapc #'clear-predicate *db-predicates*))
-
-
-;;;; Proving
-(defun unique-find-anywhere-if (predicate tree &optional acc)
- (if (atom tree)
- (if (funcall predicate tree)
- (adjoin tree acc)
- acc)
- (unique-find-anywhere-if predicate
- (first tree)
- (unique-find-anywhere-if predicate (rest tree) acc))))
-
-(defun variables-in (expr)
- (unique-find-anywhere-if #'variable-p expr))
-
-(defun rename-variables (form)
- "Replace all variables in the form with new (unique) ones."
- (sublis (mapcar #'(lambda (variable)
- (cons variable (gensym (string variable))))
- (variables-in form))
- form))
-
-
-(defun prove-clause (goal bindings other-goals clause)
- (let ((new-clause (rename-variables clause)))
- (prove-all (append (clause-body new-clause) other-goals)
- (unify goal (clause-head new-clause) bindings))))
-
-(defun prove (goal bindings other-goals)
- "Return a list of possible solutions to the given goal."
- (let ((clauses (get-clauses (predicate goal))))
- (if (listp clauses)
- (some (curry #'prove-clause goal bindings other-goals) clauses)
- (funcall clauses (rest goal) bindings other-goals))))
-
-(defun prove-all (goals bindings)
- "Return a solution to the conjunction of goals."
- (cond
- ;; If something failed further up the pipeline, bail here.
- ((eq bindings fail) fail)
-
- ;; If there's nothing to prove, it's vacuously true. Return the bindings as
- ;; the result.
- ((null goals) bindings)
-
- (t (prove (first goals) bindings (rest goals)))))
-
-
-;;;; Cleaning Solutions
-(defun clean-variables (variables solution)
- (mapcar #'(lambda (var)
- (cons var (substitute-bindings solution var)))
- variables))
-
-
-;;;; Querying Interface
-(defun continue-never ()
- nil)
-
-(defun continue-always ()
- t)
-
-(defun continue-ask ()
- (case (read-char)
- (#\; t)
- (#\. nil)
- (#\newline (continue-ask))
- (otherwise
- (format t " Type ; to see more or . to stop")
- (continue-ask))))
-
-
-(defun show-prolog-vars (variables bindings other-goals continue-p)
- (if (null variables)
- (format t "~&Yes")
- (dolist (var variables)
- (format t "~&~A = ~A"
- var (substitute-bindings bindings var))))
- (finish-output)
- (if (funcall continue-p)
- fail
- (prove-all other-goals bindings)))
-
-
-(defun show-prolog-vars-ask (variables bindings other-goals)
- (show-prolog-vars variables bindings other-goals #'continue-ask))
-
-(defun show-prolog-vars-all (variables bindings other-goals)
- (show-prolog-vars variables bindings other-goals #'continue-always))
-
-(defun show-prolog-vars-one (variables bindings other-goals)
- (show-prolog-vars variables bindings other-goals #'continue-never))
-
-(setf (get 'show-prolog-vars-ask clause-key) 'show-prolog-vars-ask)
-(setf (get 'show-prolog-vars-all clause-key) 'show-prolog-vars-all)
-(setf (get 'show-prolog-vars-one clause-key) 'show-prolog-vars-one)
-
-
-(defun top-level-query (goals primitive)
- (prove-all `(,@(replace-wildcard-variables goals)
- (,primitive
- ,@(remove-if #'wildcard-variable-p (variables-in goals))))
- no-bindings)
- (format t "~&No."))
-
-
-(defmacro query (&rest goals)
- "Perform the query interactively."
- `(top-level-query ',goals 'show-prolog-vars-ask))
-
-(defmacro query-all (&rest goals)
- "Perform the query and automatically show all results."
- `(top-level-query ',goals 'show-prolog-vars-all))
-
-(defmacro query-one (&rest goals)
- "Perform the query and just show the first result."
- `(top-level-query ',goals 'show-prolog-vars-one))
-
-
-;;;; Finding Interface
-(defparameter *results* nil)
-
-
-(defun return-boolean (variables bindings other-goals)
- (declare (ignore variables))
- (setf *results* t)
- (prove-all other-goals bindings))
-
-(defun return-one-result (variables bindings other-goals)
- (setf *results* (clean-variables variables bindings))
- (prove-all other-goals bindings))
-
-(defun return-all-results (variables bindings other-goals)
- (declare (ignore other-goals))
- (push (clean-variables variables bindings) *results*)
- fail)
-
-
-(setf (get 'return-one-result clause-key) 'return-one-result)
-(setf (get 'return-all-results clause-key) 'return-all-results)
-(setf (get 'return-boolean clause-key) 'return-boolean)
-
-(defun top-level-find (goals primitive)
- (let ((*results* (list)))
- (prove-all `(,@(replace-wildcard-variables goals)
- (,primitive
- ,@(remove-if #'wildcard-variable-p (variables-in goals))))
- no-bindings)
- *results*))
-
-
-(defun return-one-for (goals)
- (top-level-find goals 'return-one-result))
-
-(defun return-all-for (goals)
- (top-level-find goals 'return-all-results))
-
-
-(defmacro return-one (&rest goals)
- `(top-level-find ',goals 'return-one-result))
-
-(defun raw-return-one (&rest goals)
- (top-level-find goals 'return-one-result))
-
-(defmacro return-all (&rest goals)
- `(top-level-find ',goals 'return-all-results))
-
-(defun raw-return-all (&rest goals)
- (top-level-find goals 'return-all-results))
-
-
-(defmacro provable-p (&rest goals)
- `(top-level-find ',goals 'return-boolean))
-
-(defun raw-provable-p (&rest goals)
- (top-level-find goals 'return-boolean))
-
--- a/test/paip.lisp Sat Aug 20 21:56:13 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,126 +0,0 @@
-(in-package #:bones-test.paip)
-
-;;;; Utils
-(defun alist-equal (x y)
- (set-equal x y :test #'equal))
-
-(defmacro unifies (x y bindings)
- `(is (alist-equal ,(if (eql bindings 'no-bindings)
- 'no-bindings
- `',bindings)
- (unify ',x ',y))))
-
-(defmacro not-unifies (x y)
- `(is (eql bones.paip:fail (unify ',x ',y))))
-
-
-(defmacro with-db (rules &rest body)
- `(progn
- (clear-db)
- ,@(mapcar (lambda (rule) `(rule ,@rule))
- rules)
- ,@body))
-
-
-(defmacro proves (query)
- `(is (return-all ,query)))
-
-(defmacro not-proves (query)
- `(is (not (return-all ,query))))
-
-(defmacro proves-with (query results)
- `(is (set-equal ',results (return-all ,query)
- :test #'alist-equal)))
-
-
-;;;; Unification
-(test constant-unification
- (unifies 1 1 no-bindings)
- (unifies foo foo no-bindings)
- (unifies (a) (a) no-bindings)
- (unifies (a b c) (a b c) no-bindings)
- (not-unifies 1 2)
- (not-unifies foo bar)
- (not-unifies a (a))
- (not-unifies (a) (a b))
- (not-unifies () (a)))
-
-(test variable-unification
- (unifies ?x 1 ((?x . 1)))
- (unifies ?x a ((?x . a)))
- (unifies ?x ?y ((?x . ?y)))
- (unifies (?x (f ?x)) (2 (f 2)) ((?x . 2)))
- (unifies (likes sally ?thing)
- (likes ?person cats)
- ((?thing . cats)
- (?person . sally)))
- (unifies (?x + ?y)
- (10 + (1 + 2))
- ((?x . 10)
- (?y . (1 + 2))))
- (unifies (?x + (?y + ?z))
- (10 + (1 + 2))
- ((?x . 10)
- (?y . 1)
- (?z . 2)))
- (not-unifies (?x ?x) (1 2))
- (not-unifies (?x ?y ?x) (1 1 3)))
-
-(test occurs-unification
- (not-unifies ?x (f ?x))
- (not-unifies ?x (f (?x 1)))
- (not-unifies ?x (?x ?x))
- (not-unifies ?x (?x ?y))
- (let ((*check-occurs* nil))
- (unifies ?x (f ?x) ((?x . (f ?x))))
- (unifies ?x (f (?x 1)) ((?x . (f (?x 1)))))
- (unifies ?x (?x ?x) ((?x . (?x ?x))))
- (unifies ?x (?x ?y) ((?x . (?x ?y))))))
-
-
-;;;; Basic Proving
-(test prove-facts
- (with-db (((likes kim cats))
- ((likes tom cats)))
- (proves (likes kim cats))
- (proves (likes tom cats))
- (not-proves (likes kim tom))
- (not-proves (likes kim))))
-
-(test prove-rules-simple
- (with-db (((likes kim cats))
- ((likes sally ?x) (likes ?x cats)))
- (proves (likes sally kim))
- (not-proves (likes sally sally))))
-
-(test prove-member
- (with-db (((member ?x (?x . ?tail)))
- ((member ?x (?y . ?tail)) (member ?x ?tail)))
- (proves (member 1 (1 2)))
- (proves (member 2 (1 2)))
- (proves (member (x) (1 (x) 2)))
- (not-proves (member 1 ()))
- (not-proves (member ?x ()))
- (not-proves (member 1 (a b c)))
- (proves-with (member ?x (1 2 3))
- (((?x . 1))
- ((?x . 2))
- ((?x . 3))))
- (proves-with (member ?x (1 1 1))
- (((?x . 1))))
- (proves-with (member (?x ?y) ((a b) (c d) 1))
- (((?x . a) (?y . b))
- ((?x . c) (?y . d))))))
-
-(test prove-last
- (with-db (((last ?x (?x)))
- ((last ?x (?y . ?tail)) (last ?x ?tail)))
- (proves (last 1 (1)))
- (proves (last 2 (1 2)))
- (not-proves (last 1 ()))
- (not-proves (last 1 ((1))))
- (not-proves (last 1 (1 2)))
- (proves-with (last ?x (1 2 3))
- (((?x . 3))))
- (proves-with (last ?x (1 (2 3)))
- (((?x . (2 3)))))))