;; -*- Mode: Lisp; -*-
;;;;  Modified: Ron Ferguson on Tue Jan 20 8:48:40 1998

;;;; JSAINT: A rational reconstruction of Slagel's SAINT program
;;; Last edited 1/29/92, by KDF

;;; Copyright (c) 1991 -- 1992, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, Xerox Corporation
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(defstruct (jsaint 
            (:print-function (lambda (a st ignore)
                               (declare (ignore ignore))
                               (format st "<Agenda ~A>"
                                 (jsaint-title a)))))
  (title "")           ;; Name for printing
  (jtre nil)           ;; Associated JTRE
  (agenda nil)         ;; list of queued subproblems
  (problem nil)        ;; When solved, we are done.
  (solution nil)       ;; Cached answer.
  (n-subproblems 0)    ;; Statistic
  (max-tasks 20)       ;; resource bound
  (debugging nil))     ;; Debugging flag

;; Start with the usual encapsulation

(eval-when (:execute :compile-toplevel :load-toplevel)
  (proclaim '(special *jsaint*)))

(defvar *jsaint* nil)

(defun create-jsaint (title problem &key (debugging nil)
			    (max-tasks nil))
  (let ((ag (make-jsaint
	      :title title
	      :problem problem
	      :jtre (create-jtre 
		      (concatenate 'string "JTRE of " title))
	      :debugging debugging
	      :max-tasks (if (integerp max-tasks) max-tasks 20))))
    (in-jtre (jsaint-jtre ag))
    (change-jtms (jtre-jtms (jsaint-jtre ag))
		 :contradiction-handler #'jsaint-contradiction-handler)
    (use-jsaint ag)))

(defmacro debugging-jsaint (js msg &rest args)
  `(when (jsaint-debugging ,js) (format t ,msg ,@ args)))

(defun change-jsaint (js &key (debugging :NADA) (problem :NADA)
		       (max-tasks :NADA))
  (unless (eq debugging :NADA) (setf (jsaint-debugging js) debugging))
  (unless (eq problem :NADA) (setf (jsaint-problem js) problem))
  (unless (eq max-tasks :NADA) (setf (jsaint-max-tasks js) max-tasks)))

(defun use-jsaint (js) (setq *jsaint* js))

(defmacro with-jsaint (js &rest forms) `(let ((*ag* ,js)) ,@ forms))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; User entry point


(defun solve-integral (integral
		       &key (title (symbol-name (gensym)))
		       (debugging nil)
		       (max-tasks 20))
  ;; Remove redudancies and canonicalize input. 
  (setq integral (eval (quotize (simplifying-form-of integral))))
  (use-jsaint (create-jsaint title integral
			     :debugging debugging
			     :max-tasks max-tasks))
  (queue-problem (jsaint-problem *jsaint*) nil)
  (with-jtre (jsaint-jtre *jsaint*) 
	     (bps-load-file *jtre-path* *jsaint-rules*)
	     (bps-load-file *jtre-path* *jsaint-operators*))
  (run-jsaint *jsaint*))

(defun explain-result (&optional (*jsaint* *jsaint*))
  (cond ((null (jsaint-solution *jsaint*))
	 (format t "~% Problem not solved yet."))
	((eq (jsaint-solution *jsaint*) :failed-problem)
	 (explore-network (get-tms-node `(failed ,(jsaint-problem *jsaint*))
				    (jsaint-jtre *jsaint*)))
	 (format t "~% Failed to find a solution."))
	((eq (jsaint-solution *jsaint*) :failed-empty)
	 (format t "~% Ran out of things to do.")
	 (explore-network (get-tms-node `(failed ,(jsaint-problem *jsaint*))
				    (jsaint-jtre *jsaint*))))
	(t (format t "~% Solved the problem:")
	   (explore-network (get-tms-node
			 `(solution-of ,(jsaint-problem *jsaint*)
				       ,(jsaint-solution *jsaint*))
			 (jsaint-jtre *jsaint*))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Basic algorithm 

(defun run-jsaint (*jsaint*)
  (when (jsaint-solution *jsaint*)
    (return-from run-jsaint ;; Don't re-solve
      (values (jsaint-solution *jsaint*) *jsaint*)))
  (when (> (jsaint-n-subproblems *jsaint*)
	   (jsaint-max-tasks *jsaint*))
    (return-from run-jsaint ;; Respect resource limits
      (values :time-out *jsaint*)))
  (do ((done? nil)
       (solution (fetch-solution (jsaint-problem *jsaint*) *jsaint*)
		 (fetch-solution (jsaint-problem *jsaint*) *jsaint*))
       (failure-signal `(failed (integrate ,(jsaint-problem *jsaint*)))))
      (done? (values (jsaint-solution *jsaint*) *jsaint*))
    (cond (solution (setf (jsaint-solution *jsaint*) solution)
            (debugging-jsaint *jsaint*
             "~% ~A: Solved original problem." (jsaint-title *jsaint*))
	    (setq done? t))
	  ((in? failure-signal (jsaint-jtre *jsaint*))
	   (debugging-jsaint *jsaint*
	     "~% ~A: Failed on original problem."
	     (jsaint-title *jsaint*)) 
	   (setf (jsaint-solution *jsaint*) :failed-problem)
	   (setq done? t))
	  ((null (jsaint-agenda *jsaint*))
	   (debugging-jsaint *jsaint* "~% ~A: Agenda empty."
			     (jsaint-title *jsaint*))
	   (setf (jsaint-solution *jsaint*) :failed-empty)
	   (setq done? t))
	  (t (process-subproblem (cdr (pop (jsaint-agenda *jsaint*))))))))

(defun process-subproblem (item &aux (jtre (jsaint-jtre *jsaint*))
			   (suggestions nil))

  (debugging-jsaint *jsaint* "~%  Trying to solve ~A." item)
  (open-subproblem item)
  (when (fetch-solution item *jsaint*)
	;; Bookkeeping is done by pdis rules
	(debugging-jsaint *jsaint* "~%    ..already solved.")
	(return-from process-subproblem t))
  (when (some #'(lambda (f) (in? f jtre)) ;; Already expanded
	      (fetch `(and-subgoals ,item ?subproblems) jtre))
	(debugging-jsaint *jsaint* "~%   ..already expanded.")
    (return-from process-subproblem t))
  (dolist (suggestion (fetch `(suggest-for ,item ?operator) jtre))
    (when (in? suggestion jtre)
      (queue-problem `(try ,(third suggestion)) item)
      (push `(try ,(third suggestion)) suggestions)))
  ;; Presume extra subgoals don't come along.
  (assert! `(or-subgoals ,item ,suggestions) :or-subgoals jtre)
  (run-rules jtre))

(defun open-subproblem (item &aux (jtre (jsaint-jtre *jsaint*)))
  (assert! `(expanded ,item) :expand-agenda-item jtre)
  (assume! `(open ,item) :expand-agenda-item jtre)
  ;; Look for quick win, extra consequences.
  (run-rules jtre))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Queuing problems
;; Queue entries take the form (<difficulty> . <subproblem>)
;; Difficulty estimates are based on the form of the subproblem
;; alone, since there could be multiple parents for a subproblem.

(defun queue-problem (problem parent &aux entry)
  (setq entry (cons (estimate-difficulty problem) problem))
  (debugging-jsaint *jsaint* "~%   Queueing ~A from ~A, difficulty = ~D"
		    problem parent (car entry))
  (setf (jsaint-agenda *jsaint*)
	(merge 'list (list entry)
	       (jsaint-agenda *jsaint*)
	       #'(lambda (a b) (< (car a) (car b))))))

(defun estimate-difficulty (problem)
  (+ (max-depth problem) (count-symbols problem)))

(defun count-symbols (pr)
  (cond ((null pr) 0)
	((listp pr)
	 (reduce #'+ (mapcar #'count-symbols pr)
		 :initial-value 0))
	(t 1)))

(defun max-depth (pr)
  (cond ((not (listp pr)) 1)
	(t (1+ (reduce #'max (mapcar #'max-depth pr)
		       :initial-value 0)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Auxiliary routines

(defun fetch-solution (problem &optional (*jsaint* *jsaint*)
		       &aux (jtre (jsaint-jtre *jsaint*)))
  (dolist (solution (fetch `(solution-of ,problem ?answer) jtre))
    (when (in? solution jtre)
      (return-from fetch-solution (third solution)))))

(defun jsaint-contradiction-handler (contradictions jtms)
  (ask-user-handler contradictions jtms)) ;; default

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Defining operators

(defmacro defIntegration (name trigger &rest keyed-items
			  &aux subproblems result test)
  (setq subproblems (cadr (member :subproblems keyed-items)))
  (setq result (cadr (member :result keyed-items)))
  (setq test (cadr (member :test keyed-items)))
  (unless result 
    (error "Integration operator must have result form"))
  `(rule ((:in (expanded (integrate ,trigger)) :var ?starter
	  ,@ (if test `(:test ,test) nil)))
	 (rlet ((?integral ,trigger)
		(?problem (integrate ,trigger)))
	       (rlet ((?op-instance (,name ?integral)))
	     (rassert! (Operator-Instance ?op-instance)
		       :op-instance-definition)
	     ;; If no subproblems, just create solution
     ,@ (cond ((null subproblems)
	       `((rlet ((?solution
			 (:eval (simplify ,(quotize result)))))
		  (rassert! (solution-of ?problem ?solution)
		   (,(keywordize name)
		     (Operator-Instance ?op-instance))))))
	      (t ;; Usual case
	       (let ((subs (calculate-subproblem-list subproblems))) 
		 `((rassert! (suggest-for ?problem ?op-instance)
		    (:intopexpander ?starter))
   (rule ((:in (expanded (try ?op-instance)) :var ?try))
	   (rlet ,subs
		 ,@ (mapcar #'(lambda (sub)
				`(queue-problem ,(car sub) ?problem))
			    subs)
		 (rassert! (and-subgoals (try ?op-instance)
					 ,(mapcar #'car subs))
			   (,(keywordize (format nil "~A-def" name))
			    ?try))
		 ;; Solution detector
		 ,(multiple-value-bind (triggers antes)
		      (calculate-solution-rule-parts subs subproblems)
		    `(rule (,@ triggers)
			   (rlet ((?solution
				    (:eval (simplify ,(quotize result)))))
				 (rassert! (solution-of ?problem ?solution)
					   (,(keywordize name)
					     ,@ antes)))))))))))))))

(defvar *test-operator*
	'(defIntegration Integral-of-Sum
	   (integral (+ ?t1 ?t2) ?var)
	   :subproblems ((?int1 (integrate (integral ?t1 ?var)))
			 (?int2 (integrate (integral ?t2 ?var))))
	   :result (+ ?int1 ?int2)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Helpers for operator definition

(defun calculate-subproblem-list (subproblems &aux (counter -1))
  ;; Takes list of entries whose form is (?result-var ?form)
  ;; and returns a list of (?goal-var ?form)
  (mapcar #'(lambda (pair)
	      (incf counter)
	      (list (intern (format nil "?GOAL~D" counter)) 
		    (simplifying-form-of (cadr pair))))
	  subproblems))

(defun simplifying-form-of (alg-goal)
  ;; Run simplifier on subgoals, just in case.
  (cond ((null alg-goal) nil)
	((not (listp alg-goal)) alg-goal)
	((eq (car alg-goal) 'integral) ;; simplify as needed
	 `(integral (:eval (simplify ,(quotize (cadr alg-goal))))
	   ,(caddr alg-goal)))
	(t (cons (simplifying-form-of (car alg-goal))
		 (simplifying-form-of (cdr alg-goal))))))

(defun calculate-solution-rule-parts (sub-pairs res-pairs
				      &aux (counter -1)
				      (antes nil)
				      (triggers nil))
  (setq triggers
	(mapcar #'(lambda (subpair respair)
		    (incf counter)
		    (let ((rvar (intern (format nil "?result~D" counter))))
		      (push rvar antes)
		      `(:in (solution-of ,(car subpair) ,(car respair))
			:var ,rvar)))
		sub-pairs res-pairs))
  (values triggers (nreverse antes)))

(defun keywordize (stuff)
  (cond ((null stuff) (error "Can't keywordize nothing."))
	((listp stuff) (keywordize (car stuff)))
	(t (intern (format nil "~A" stuff) 'keyword))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Interrogatives

;;; SHOW-PROBLEM highlights the assertions relevant to
;;; the given problem.

(defun show-problem (pr &optional (*jsaint* *jsaint*)
			&aux stuff ands ors)
  (format t "~%~A:: (~D)" pr (estimate-difficulty pr))
  (with-jtre (jsaint-jtre *jsaint*)
  (setq stuff (fetch `(parent-of ,pr ?x ?type)))
  (cond (stuff (format t "~% Parent(s): ")
  (dolist (p stuff)
	  (if (in? p)
	      (format t "~%   ~A, ~A."
		      (third p) (fourth p))
	    (format t "~%    BUG: Should be in: ~A" p))))
	(t (format t "~% No parents found.")))
  (if (fetch `(expanded ,pr)) (format t "~% Expanded,")
    (format t "~% Not expanded,"))
  (if (fetch `(open ,pr))
      (if (in? `(open ,pr)) (format t " open,")
	(format t " closed,"))
    (format t " not opened,"))
  (if (in? `(relevant ,pr)) (format t " relevant.")
    (format t " not relevant."))
  (cond ((setq stuff (fetch-solution pr))
	 (format t "~% Solved, solution = ~A" stuff))
	((and (setq stuff (car (fetch `(failed ,pr))))
	      (in? stuff)) (format t "~%  Failed."))
	((not (equal (car pr) 'try))
	 (format t "~% Neither solved nor failed.")))
  (setq ands (fetch `(and-subgoals ,pr ?ands)))
  (when ands (format t "~% And subgoals:")
	(dolist (subg (third (car ands)))
		(format t "~%   ~A" subg))
	(format t "."))
  (setq ors (fetch `(or-subgoals ,pr ?ors)))
  (when ors (format t "~% Or subgoals:")
	(dolist (subg (third (car ors)))
		(format t "~%   ~A" subg))
	(format t "."))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Textual display of an AND/OR graph

(defun show-ao-graph (&optional (*jsaint* *jsaint*))
  (let* (;; (problems (get-problems))
	 (depth-table (update-ao-depth-table 
		       (jsaint-problem *jsaint*)
		       0 (list (cons (jsaint-problem *jsaint*) 0))
		       (list (jsaint-problem *jsaint*)))))
    (setq depth-table
	  (sort depth-table #'(lambda (x y) (< (cdr x) (cdr y)))))
    (dolist (pair depth-table)
	    (format t "~% ~D:" (cdr pair))
	    (show-problem (car pair)))))

(defun update-ao-depth-table (now depth depths path)
  (incf depth)
  (dolist (child (get-children now) depths)
   (unless (member child path :test 'equal) ;; Yes, can loop!
    (let ((entry (assoc child depths :test 'equal)))
      (unless entry 
	      (push (setq entry (cons child 0)) depths))
      (when (> depth (cdr entry))
	    (setf (cdr entry) depth)
	    (setq depths (update-ao-depth-table
			child depth depths (cons child path))))))))

(defun get-children (gp &optional (*jsaint* *jsaint*)
			&aux children)
  (dolist (maybe-kid (fetch `(parent-of ?x ,gp ?type)
			    (jsaint-jtre *jsaint*))
		     children)
	  (if (in? maybe-kid (jsaint-jtre *jsaint*))
	      (push (cadr maybe-kid) children))))

(defun get-problems (&optional (*jsaint* *jsaint*))
  (mapcar 'cadr (fetch '(expanded ?x) (jsaint-jtre *jsaint*))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Debugging

(defun try-jsaint (problem &optional (title "JSAINT Test"))
  (solve-integral problem :debugging t :title title))

(defun jfetch (pattern) (fetch pattern (jsaint-jtre *jsaint*)))

(defvar problem1 '(integrate (integral 1 x)))
(defvar problem2 '(integrate (integral (+ x 5) x)))
(defvar problem3 '(integrate (integral (* 46 (log x %e)) x)))
(defvar problem4 '(integrate
		 (integral (+ 0.63
			    (* 3.2 (sin (* 1.7 x)))
			    (* 4 (expt %e (* 2 x)))) x)))