;;; EGGS is an explanation-based generalizer which is capable of generalizing
;;; proofs returned by the DEDUCE deductive retriever (a PROLOG like theorem prover)
;;; and generating macro-rules from the general proofs.  These macro-rules are then
;;; stored and preferentially used in future deductions to increase performance.
;;; The files CUP-DOMAIN and TOY-DOMAIN are sample domain files.

;;;; Copyright (c) 1988 by Raymond Joseph Mooney. This program may be freely 
;;;; copied, used, or modified provided that this copyright notice is included
;;;; in each copy of this code and parts thereof.

(defvar *trace-eggs* nil "Print out specific and general proofs for EGGS")
(defvar *trace-generalizer* nil
  "Print out updated bindings at each step in generalization")
(defvar *learn* t "Generalize proofs and learn operational macro-rules")
(defvar *operational-predicates* nil "List of operational predicates")
(defvar *save-learned-rules* t "Save learned rules for later use")

(defun run-eggs (questions &optional (depth-limit 20))
  ;;; Use the EGGS system to process each of the queries in the list of questions
  ;;; and report total time spent.

  (let ((deduce-time 0) (learn-time 0)(solve-count 0))
    (dolist (question questions)
      (terpri)
      (multiple-value-bind (form d-time l-time) (eggs question depth-limit)
	(incf deduce-time d-time)(incf learn-time l-time)(if form (incf solve-count))))
    (format t "~%~%Number solved: ~A (~A%)" solve-count
	    (round (* 100 (/ solve-count (length questions)))))
    (format t "~%Total Deduce time: ~,2F sec; Learn time: ~,2F sec" deduce-time learn-time)))


(defun eggs (form &optional (depth-limit 20))
  ;;; First use the retriever to retrieve a fact which matches the given form
  ;;; If an answer is found, see if its proof structure can be generalized to 
  ;;; produce a new rule.  If so, generalize it, create a macro-rule from the 
  ;;; generalized proof and add it to the front of the existing rules so that it is
  ;;; preferentially used in future deductions
  
  (let* ((start-time (get-internal-run-time))
	 (answer (gfirst (retrieve form depth-limit)))
	 (deduce-time (/ (- (get-internal-run-time) start-time)
			internal-time-units-per-second))
	 retrieved-form (learn-time 0))
    (format t "~%Deduction time: ~,2F sec" deduce-time)
    (cond (answer (setf retrieved-form (substitute-vars form (first answer)))
	   (format t "~%Retrieved answer:~A" retrieved-form) 
	   (when *trace-eggs* (format t "~%~%Proof:~%~A~%Proof Structure:~%~A"
				      (specific-proof answer)(second answer)))
	   (when *learn*
	     (setf start-time (get-internal-run-time))
	     (let ((proof (prune-operational (second answer))))
	       (when (generalize-p proof)
		 (format t "~%~%Generalizing proof")
		 (let* ((general-bindings (generalize-proof proof))
			(general-rule (general-rule proof general-bindings)))
		   (when *save-learned-rules* ; Add learned rule to front of existing rules
		     (save-brule general-rule))
		   (setf learn-time (/ (- (get-internal-run-time) start-time)
				       internal-time-units-per-second))
		   (when *trace-eggs* (format t "~%~%General proof:~%~A"
					      (instantiate-proof proof general-bindings)))
		   (format t "~%~%Learned rule: ~A" general-rule))))))
	  (t (format t "~%Not able to retrieve: ~A" form)))
    (values retrieved-form deduce-time learn-time)))


(defun save-brule (general-rule)
  (push-brule general-rule))


(defun prune-operational (proof)
  ;;; Prune (i.e. remove from the proof) sub-proofs for predicates which
  ;;; are known to be operational in order to achieve a more general
  ;;; rule which is still operational.
  ;;; TO BE WRITTEN
  proof)

(defun generalize-p (proof)
  ;;; A proof can be generalized if it has at least two rules

  (and (rule-proof-p proof)
       (some #'(lambda (ante-proof) (rule-proof-p (second ante-proof)))
	     (rule-proof-ante-proofs proof))))


(defun generalize-proof (proof &optional (bindings (list t)))
  ;;; Compute the general binding list for this proof structure by simply updating an
  ;;; initially empty binding list to account for all unifications between the consequent
  ;;; of one rule and the antecedent of another. 

  (if (not (rule-proof-p proof))
      bindings
      (dolist (ante-proof (rule-proof-ante-proofs proof) bindings)
	(let ((ante (first ante-proof))(sub-proof (second ante-proof)))
	  (when (rule-proof-p sub-proof)
	      (setf bindings (unify ante (rule-proof-consequent sub-proof)
				    (generalize-proof sub-proof bindings)))
	      (when *trace-generalizer*
		(format t "~%~%~A=~A ~%Updated bindings: ~A"
			ante (rule-proof-consequent sub-proof) bindings)))))))


(defun general-rule (proof &optional (general-bindings
					(generalize-proof proof)))
  ;;; Extract the macro-rule for this proof by applying the general
  ;;; bindings to the consequent and leaves of the proof structure.

    (when (rule-proof-p proof)
      `(<- ,(substitute-vars (rule-proof-consequent proof)
			   general-bindings)
	   ,@(mapcar #'(lambda (leaf) (substitute-vars leaf general-bindings))
		     (proof-leaves proof)))))


(defun proof-leaves (proof)
  ;;; Return the leaves of the proof structure

      (mapcan #'(lambda (ante-proof)
		  (if (rule-proof-p (second ante-proof))
		      (proof-leaves (second ante-proof))
		      (list (first ante-proof))))
	      (rule-proof-ante-proofs proof)))