#|

=head1 Inside LIAR (Logic Inference and Rules)

This  code  reviews and extend's Graham's Lisp-based inference system
(see http://goo.gl/1OCc5) taken from Chapter 17 of Ansi COMMON LISP
(see http://www.paulgraham.com/acl.html). That chapter should be read
before this page.

=head2 About this Document

LIAR is an extension to Graham's code that implements forward and
backward chaining rules.

=over 8

=item *

I<Backward rules> try to prove the consequence by
proving the conditions. This, in turn, might recursively lead
to the a condition becoming a sub-goal to be proved by
running its own rule(s).

=item *

I<Forward rules> run the rule condition
before running the rule consequence. LIAR's forward rules
also seperate state up-date from state querying (rule conditions
cannot update state, but other parts of the rule can)

=back

=head2 Conventions

A function named
C<x%> or
C<x%%> is a preliminary version of a function that will be refined,
later.

Anything starting with C<$> is a UNIX shell command; e.g.

 $ ls
 abcd.lisp       counts.lisp     dist.lisp       macros.lisp     nb.lisp
 bounded.lisp    data.lisp       gold.lisp       make.lisp       random.lisp
 class.lisp      deftest.lisp    knn.lisp        misc.lisp       rbst.lisp

Anything starting with C<E<gt>> is a LISP REPL command; e.g.

 > (+ 1 1)
 2

=head1 Load Code

|#

(defun make ()
   (handler-bind ((style-warning #'muffle-warning))
     (load "tricks.lisp")
     (load "liar.lisp")))



(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)))))

(defun xpand (x binds)
  (cond ((var? x)  (xpand (binding x binds) binds))
	((listp x) (mapcar #'(lambda (y) (xpand y binds)) x))
	(t         x)))

(defun xpands (binds)
  (mapcar #'(lambda (bind)
	      (cons (car bind)
		    (xpand (cdr bind) binds)))
	  binds))

(defun quoted (binds)
  (mapcar #'(lambda (x) `(,(car x) . ',(cdr x))) binds))

(defparameter *brules* (make-hash-table))

(defun brules ()
  (showh *brules*))

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

(defun head? (x)
  (gethash x *brules*))

(defun prove (expr &optional binds)
  (case (car expr)
     (debug        (prints :bindings binds) (list binds))
     ((<= <  > >=) (if (prove-code expr binds)
		       (list binds)))
     ((prints say)
                   (prove-code expr binds)  (list binds))
     (is           (list
		    (prove-is   (second expr) (third expr) 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)
  (let* ((code  (sublis (xpands (quoted binds)) 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 *brules*))))

(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)))


(defun retract (rule)
  (let* ((head (first rule))
	 (args (rest rule))
	 (old  (gethash head *brules*))
	 (new  (remove-if #'(lambda (x) (equal x (list args))) old)))
    (setf (gethash head *brules*) new)))


(defmacro with-answer (query &body body)
  (let* ((binds '%bindings%)
	 (lets  (mapcar #'(lambda (v) `(,v (xpand ',v ,binds)))
			(vars-in query))))   
    `(dolist (,binds (prove ',query))
       (let (,@lets)
         ,@body))))


(defmacro ?? (query)
  `(with-answer ,query
     (print ',query) (print %bindings%)))

(defmacro ? (query)
  `(with-answer ,query
     (when %bindings%
       (return
	 (progn
	   (print ',query) (print %bindings%))))))

;; rules 
(defstruct rule label if uses (then t) then-compiled adds deletes)

(defmacro make-if (label iff uses)
  `'(and (= ?name ,label)
	,iff
	(= ?wme ,uses)
	(not (used ?name ?wme))))

(defmacro make-then (code &optional quotep)
  (let* ((binds (gensym "BINDINGS-"))
	 (lets  (mapcar #'(lambda (v) `(,v (binding ',v ,binds)))
		        (vars-in code)))
	 (source     `(lambda (,binds)
			(let  (,@lets)
			  ,code))))
    (if quotep
	`',source
	source)))
  
(defparameter *frules* nil)

(defmacro rule (label &key if uses then adds deletes)
  `(push
    (make-rule
     :label          ',label
     :if             (make-if    ',label ,if ,uses)
     :then-compiled  (make-then ,then)
     :then           (make-then  ,then t)
     :adds           (append ',adds '((used ?name ?wme)))
     :deletes        ',deletes
     :uses ',uses
     )
    *frules*))
  
(defun $reset ()
  (clrhash *brules*)
  (setf *frules* nil))


(defun run (&optional (frules (reverse *frules*)))
  (if frules
      (let ((frule (car frules)))
	(if ($step frule)
	    (run)
	    (run (cdr frules))))))

(defun $step (rule)
  (with-slots (label if then-compiled adds deletes) rule
    ;(format t "testing ~a~%" label)
    (let* ((binds (prove if)))
      (when binds
	(setf binds (xpands (first binds)))
	(format t "~&; FIRING ~a~%" label)
	(mapcar #'defrule (sublis binds adds))
	(mapcar #'retract (sublis binds deletes))
	(funcall then-compiled binds))
      binds)))
      

(defmacro defrelation (relation key &rest fields)
  `(defrelation-worker ',relation ',key ',fields))

(defun defrelation-worker (relation key fields)
  (let (body)
     (labels ((q (x) (intern (string-upcase (format nil "?~a" x))))
	      (r (x) (defrule (list x (q key) (q x))  body)))
       (setf body (cons relation (mapcar #'(lambda (x) (q x)) (cons key fields))))
       (mapc #'r (cons key fields)))))

(defun !one ()
  (clrhash *brules*)
  (<- (person matt m 23))
  (<- (person dean m 30))
  (<- (person clint m 100))
  (<- (younger ?x ?y) (and (person ?x ?g1   ?age1) (person ?y ?g2 ?age2) (< ?age1 ?age2)))
  (<- (sameSex ?x ?y) (and (person ?x ?gender ?a1) (person ?y ?gender ?a2)))
  (<- (hates   ?x ?y) (and (sameSex ?x ?y) (younger ?y ?x)))
  (with-answer (hates ?x ?y)
      (format t "~a hates ~a~%" ?x ?y)))

(defun !two ()
  (clrhash *brules*)
  (defrelation person name age gender)
  (<- (person nancy  23 f))
  (<- (person betty  40 f))
  (<- (person donald 60 m))
  (<- (parent donald nancy))
  (<- (parent donald betty))
  (<- (parent donald suzie))  
  (<- (male ?x)   (person ?x ?_ m))
  (<- (older  ?x ?y) (and (age ?x ?age1)
			  (age ?y ?age2)
			  (> ?age1 ?age2)
			  (say "---- ~a ~a~%" ?age1 ?age2)))
  (<- (father ?x ?y) (and (parent ?x  ?y) (male ?x)))
  (<- (= ?x ?x)) 3
  (<- (sibling ?x ?y) (and (parent ?z ?x)
			   (parent ?z ?y)
			   (not (= ?x ?y))))
  (with-answer (father ?x ?y) nil
      (format t "the father of ~a is ~a~%" ?x ?y))
  (with-answer (sibling ?x ?y) nil ;((?x . suzie))
    (format t "the sibling of ~a is ~a~%" ?x ?y))
  (with-answer (older ?x ?y) nil
    (format t " ~a is older than ~a~%" ?x ?y)))
  
(defun !rule ()
  ($reset)
  (!rule-brules) (!rule-frules)
  (run)
  )

(defun !rule-brules ()
  (<- (= ?x ?x))
  (<- (item bread))
  (<- (item pop))
  (<- (item sad))
  (<- (item bread))
  (<- (grocery pop   water))
  (<- (grocery breod wheat)))

(defun !rule-frules ()
  (rule missing-grocery
	:if      (and (item ?x) (not (grocery ?x ?y)) (is ?z (+ 1 2)))
	:then    (prints 'bad ?x ?z)
	:adds    ((item fred))
	:deletes ((item ?x))
	:uses    (?x ?z)))


#|

=head1 Installation

=head2 Download

Source code: 

 $ wget http://goo.gl/iDD0B

This doco:

 $ wget http://goo.gl/z6Nyw

=head2 Execute

First load into LISP:

 > (load "liar.lisp") ; ignore warning messages

Reloads:

 > (make)

|#