;;; Simplified Deductive Retriever
;;;------------------------------------------------------------
;;; - File: sddr.lisp
;;; - Author: Chris Riesbeck
;;;
;;; 02/05/08: made further simplifications, added more comments [CKR]
;;; 01/31/08: created file [CKR]
;;
;;; SDDR is a simpler but more CONSful version of DDR.
;;; It crawls unless compiled, even on small rule bases.
;;; It support backward-chaining rules, and the functions
;;; ask, tell, and init-kb. There's no ask-trace, but
;;;
;;;   (trace sddr::apply-rules)
;;;
;;; is a workable substitute. 

(defpackage #:sddr
  (:use #:common-lisp)
  (:export #:ask #:init-kb #:tell))

(in-package :sddr)

(defvar *kb* nil)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; PUBLIC FUNCTIONS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun ask (query &optional (form query))
  (mapcar #'(lambda (blist)
              (replace-variables form blist))
    (apply-rules query)))

(defun tell (pat)
  (pushnew (make-rule pat) *kb* :test #'equal))

(defun init-kb (kb)
  (setq *kb* nil)
  (mapc #'tell kb))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; TELL support functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; (MAKE-RULE pat) -> rule
;;;   Returns (<- head . antecedents), given either
;;;   a rule or a simple assertion.

(defun make-rule (pat)
  (if (rule-form-p pat) pat (list '<- pat)))

(defun rule-form-p (pat)
  (and (consp pat)
       (symbolp (car pat))
       (equal (symbol-name (car pat)) "<-"))) ;; avoids exporting

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; ASK support functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; The key data structure for retrieval is a list of binding
;;; lists (blists). Operations that use or create bindings
;;; iterate over the lists of bindings and replace each one with
;;; zero or more lists of bindings. An empty list of binding
;;; lists means unification or retrieval has failed.

;;; (APPLY-RULES query) -> list of binding lists
;;;   Returns the appended list of successful binding lists for
;;;   all rules in the KB that prove the query. Rule variables
;;;   are renamed before use.
;;;
;;; (APPLY-RULE rule query) -> list of binding lists
;;;   Returns the binding lists produced when using rule to
;;;   prove query. 
;;;
;;;   APPLY-RULE starts by unifying query with the rule's head.
;;;   Any binding lists produced are used to recursively 
;;;   prove the antecedent in the rule. 
;;;
;;; (EXTEND-BLISTS blists query) -> list of binding lists
;;;   Returns a list of the binding lists extended by the
;;;   bindings from proving query.
;;;
;;; (EXTEND-BLIST blist query) -> list of binding lists
;;;   Returns the extensions of blist that result from proving
;;;   query. Variables in query are replaced by their var-values
;;;   in blist.
;;;
;;; (RENAME-VARIABLES pat) -> pat
;;;   Returns a copy of pat with all variables replaced by
;;;   variables with new names.
;;;
;;; (REPLACE-VARIABLE pat blist) -> pat
;;;   Returns a copy of pat with all variables replaced by
;;;   their var-values.

(defun apply-rules (query)
  (mapcan #'(lambda (rule)
              (apply-rule (rename-variables rule) query))
          *kb*))

(defun apply-rule (rule query)
  (reduce #'extend-blists (cddr rule)
          :initial-value (unify (cadr rule) query)))

(defun extend-blists (blists query)
  (mapcan #'(lambda (blist)
              (extend-blist blist query))
          blists))

(defun extend-blist (blist query)
  (mapcar #'(lambda (new-blist)
              (append blist new-blist))
    (apply-rules (replace-variables query blist))))

(defun rename-variables (pat)
  (sublis (rename-list pat) pat))

(defun replace-variables (pat blist)
  (sublis (replace-list pat blist) pat))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Unifier
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; (UNIFY pat1 pat2 [list of blists]) -> list of blists
;;;   Returns a list of the binding lists that can be extended
;;;   to unify pat1 and pat2.
;;;
;;; (VAR-UNIFY var pat blists) => list of blists
;;;   Returns a list of the binding lists that can be extended
;;;   to unify a variable with a pattern.
;;;
;;; (BIND-VAR var pat blist) -> list of blists
;;;   Returns NIL if var can't be unified with pat, otherwise
;;;   returns a list of blist extended with bindings for var,
;;;   if needed.
;;;   - A variable unifies with itself with no new binding
;;;   - A bound variable unifies with pat if its binding
;;;     unifies with pat
;;;   - An unbound variable unifies with anything except a
;;;     functional term containing the variable


(defun unify (pat1 pat2 &optional (blists (list nil)))
  (cond ((null blists) nil)
        ((var-p pat1) (var-unify pat1 pat2 blists))
        ((var-p pat2) (var-unify pat2 pat1 blists))
        ((atom pat1) (and (eql pat1 pat2) blists))
        ((atom pat2) nil)
        (t (unify (cdr pat1) (cdr pat2)
                  (unify (car pat1) (car pat2) blists)))))

(defun var-unify (var pat blists)
  (mapcan #'(lambda (blist) (bind-var var pat blist))
    blists))

(defun bind-var (var pat blist)
  (cond ((eql var pat)
         (list blist))
        ((var-bound-p var blist)
         (unify (var-binding var blist) pat (list blist)))
        ((contained-in-p var pat blist) nil)
        (t (list (cons (list var pat) blist)))))

(defun contained-in-p (var pat blist)
  (if (var-p pat)
      (or (eql var pat)
          (contained-in-p var (var-binding pat blist) blist))
      (and (consp pat)
           (or (contained-in-p var (car pat) blist)
               (contained-in-p var (cdr pat) blist)))))

(defun var-p (x)
 (and (symbolp x) (eq (char (symbol-name x) 0) #\?)))

(defun var-binding (var blist) (cadr (assoc var blist)))
(defun var-bound-p (var blist) (not (null (assoc var blist))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Variable replacing functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; (RENAME-LIST pat) -> list of (variable . new-variable) pairs
;;;   Returns a a-list of new names for every variable in pat.
;;;
;;; (REPLACE-LIST pat blist) -> list of (variable . value) pairs
;;;   Returns a a-list of variable values for every variable
;;;   in pat.
;;;
;;; (VAR-LIST pat) -> list of variables
;;;   Returns a list of the variables in pat, with no duplicates.
;;;
;;; (VAR-VALUE var blist) -> value
;;;   Returns the value of a variable in blist. The value is:
;;;    - var if var has no binding or is bound to itself
;;;    - otherwise, the var-binding of var with variables replaced

(defun rename-list (pat)
  (mapcar #'(lambda (var) (cons var (gensym "?")))
          (var-list pat)))

(defun replace-list (pat blist)
  (mapcar #'(lambda (var) (cons var (var-value var blist)))
          (var-list pat)))

(defun var-list (pat &optional vars)
  (cond ((var-p pat) (adjoin pat vars))
        ((atom pat) vars)
        (t
         (var-list (cdr pat)
                   (var-list (car pat) vars)))))

(defun var-value (var blist)
  (if (var-bound-p var blist)
      (let ((value (var-binding var blist)))
        (if (eql var value)
            var
          (replace-variables value blist)))
    var))