Add precompilation of static queries at compile time
Imagine a function like this:
(defun legal-moves ()
(query (legal ?who ?move)))
The argument to `query` there is constant, so we can compile it into WAM
bytecode once, when the Lisp function around it is compiled. Then running the
query doesn't need to touch the Bones compiler -- it can just load the bytecode
from an array and first up the VM loop.
This saves a lot of time (and consing) compared to compiling the same query over
and over at runtime.
author |
Steve Losh <steve@stevelosh.com> |
date |
Sun, 17 Jul 2016 16:49:06 +0000 |
parents |
6c90a65137d9 |
children |
(none) |
(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))