;;; R. Williams
;;; Artificial Intelligence

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The following routines provide the main user interface allowing a
;;; user to store and inspect facts and rules in a small rule-based deduction
;;; system.  These routines and others in this file were designed to work
;;; with forward and backward chaining code in the files "fchain.lisp",
;;; "bchain.lisp", and "unify.lisp".
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defmacro define-facts (&rest facts)	; initialize the list of facts
  `(store-facts ',facts t))

(defmacro define-rules (&rest rules)	; initialize the list of rules
  `(store-rules ',rules t))

(defmacro add-facts (&rest facts)	; add some more facts to the list
  `(store-facts ',facts nil))

(defmacro add-rules (&rest rules)	; add some more rules to the list
  `(store-rules ',rules nil))

(defmacro add-fact (fact)		; add a single fact to the list
  `(store-facts '(,fact) nil))

(defmacro add-rule (rule)		; add a single rule to the list
  `(store-rules '(,rule) nil))

(defun show-facts ()			; display the entire list of facts
  (dolist (fact *facts* (values))
    (format t "~a~%" fact)))

(defun show-rules (&rest numbers)	; display selected or all rules
  (if (null numbers)
      (let ((counter 0))
	(dolist (rule *rules* (values))
	  (print-rule (incf counter) rule)))
      (dolist (n numbers (values))
	(show-rule n))
      ))

(defun show-rule (number)		; display rule with a specified number
  (print-rule number
	      (nth (1- number) *rules*)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Helpers for the above fact/rule interface routines
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defvar *facts*)			; list of fact formulas
(defvar *rules*)			; list of rule structures

; Used to provide interface to general-purpose fwd and bkwd chaining programs
(defvar *fc-db*)			; list of fc-db-items
(defvar *bc-rules*)			; list of bc-rules

(defstruct fc-db-item
  formula
  from-rule)

(defstruct bc-rule
  formula
  number)

(defun store-facts (facts init)
  (if init (setq *facts* nil))
  (setq *facts* (append *facts* facts))
  'ok
  )

;;; Should add a check here for (or make corrections to) rules where
;;; escape to Lisp could contain an unbound (?x type of) variable
;;; during forward or backward chaining.  Also, could add the quotes
;;; here rather than forcing the user to put them in Lisp forms.

(defun store-rules (rules init)
  (when init 
	(setq *rules* nil)
	(setq *bc-rules* nil)
	(setq *fc-db* nil)
	)
  (let ((stand-rules (mapcar #'standardize rules))
	(fc-rule-counter (length *rules*))
	(bc-rule-counter (length *rules*)))
    (setq *rules* (append *rules* rules))
    (setq *fc-db*
	  (append *fc-db*
		  (mapcar #'(lambda (rule)
			      (make-fc-db-item
			       :formula (convert-to-nested-if rule)
			       :from-rule (incf fc-rule-counter)))
			  stand-rules)))
    (setq *bc-rules*
	  (append *bc-rules*
		  (mapcar #'(lambda (rule)
			      (make-bc-rule
			       :formula (convert-to-conj-antecedent rule)
			       :number (incf bc-rule-counter)))
			  stand-rules)))
    'ok
    ))

(defun print-rule (number rule)
  (format t "Rule ~a:~%" number)
  (dolist (elt rule)
    (case elt
	  ((if)   (format t "  If"))
	  ((then) (format t "  Then"))
	  (t      (format t "~9,0t~a~%" elt)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This function takes a formula of the form (if a1 a2 ... an then c)
; and converts it into the form (if (and a1 a2 ... an) c) needed for
; the general-purpose predicate calculus backward chainer that forms
; the core of "bchain.lisp".
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun convert-to-conj-antecedent (rule)
  (let ((antecedents (butlast (cdr rule) 2))
	(consequent (car (last rule))))
    `(if (and ,@antecedents) ,consequent)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This function takes a formula of the form (if a1 a2 ... an then c)
; and converts it into the form (if a1 (if a2 ... (if an c))) needed
; for the general-purpose predicate calculus forward chainer that forms
; the core of "fchain.lisp".
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun convert-to-nested-if (rule)
  (convert-aux (cdr rule)))

(defun convert-aux (rule-pieces)
  (if (eql (car rule-pieces) 'then)
      (cadr rule-pieces)
      `(if ,(car rule-pieces) ,(convert-aux (cdr rule-pieces)))
      ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Miscellaneous utilities
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun fact? (formula)		; used to distinguish facts from rules
  (not (eql (car formula) 'if)))

(defun rule? (formula)
  (eql (car formula) 'if))

(defun lisp-escape? (formula)
  (eql (car formula) 'lisp-eval))

(defun lisp-form (formula)
  (second formula))

(defun is-true? (form)
  (and (not (contains-var? form)) (eval form)))

(defun contains-var? (form)
  (if (atom form)
      (is-var? form)
      (or (contains-var? (car form))
	  (contains-var? (cdr form)))
      ))