;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: evaluate.lsp
;;;;    System: FIRE v1
;;;;    Author: Ken Forbus
;;;;   Created: March 14, 2004 10:47:43
;;;;   Purpose: Evaluator for FIRE
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Monday, May 31, 2004 at 23:57:12 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;; Every reasoning system has to have some kind of mechanism 
;;; for getting garden-variety computations done.  The "just do it"
;;; sorts of calculations that happen in the course of figuring things
;;; out.  In FIRE this occurs via the evaluation subsystem, which is
;;; accessed via ASK.

;;; This subsystem is triggered when ask receives a query of the form
;;;      (evaluate ?answer <some expression in terms of an EvaluatableFunction>)

;;; The expression is passed to evaluate-1, which is a simple interpreter driven
;;; by links between constants declared to be instances of the collection 
;;; EvaluatableFunction and procedures in the Lisp environment that carry out
;;; the work of that procedure.  The final result of the evaluation is bound to
;;; ?answer, as well as being justified in the WM.
;;;
;;; The file evalnfs.lsp provides definitions for the built-in EvaluatableFunction
;;; instances supported by FIRE.  The definitions in this file are processed by

;;; (create-evaluation-implementation-files
;;;        <evalfn file name> <flat file name> <lisp source file name>)
;;; which creates, given the definitions in the file given as the first argument,
;;; two files, a KB flat file that must be loaded into the KB and a file of lisp
;;; source that actually provides the code to support those functions.
;;; Both must be created at the same time because the procedure names are
;;; timestamped, to minimize the chance of collisions with human-defined code.
;;; 
;;; For convenience,
;;; (create-fire-default-evaluation-files) creates the files for the
;;; EvaluatableFunctions built into FIRE.

;;; Historical notes: 
;;; 1. We used an eval-source previously for implementing this,
;;; which was a good way to boostrap, but when one considers quotation issues
;;; and special cases that have to be known about in the term optimizer, the
;;; generic methods for handling other kinds of sources didn't scale very well.
;;; Hence this specialized subsystem interface.
;;;
;;; 2. In DTE we actually allowed evaluatable expressions anywhere in a pattern,
;;; and the system would automatically evaluate them wherever they appeared.
;;; This was great for supporting the trafficability domain theory in HPKB, where
;;; a lot of conditional calculations were made based on available GIS data.
;;; But it caused a lot of extra work when doing an ASK, and it isn't clear that
;;; it is worth it.  So we are going the simpler route for now by only limiting
;;; this to evaluate.  We could expand expressions off-line if we wanted to 
;;; allow more freedom in knowledge entry, but this isn't a high priority right now.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Entry point for evaluation subsystem

(defun ask-for-evaluation (query reasoner context number response effort)
  ;; Query is of form (evaluate <answer> <expression>)
  ;; Recall that ask does substitutions, so no binding list to pass in.
  (declare (ignore number))
  (cond ((variable? (cadr query))
         (do-evaluate query reasoner context response effort
           (cadr query) (third query)))
        (t ;; Testing a result
         (do-evaluate-ground query reasoner context response effort
           (cadr query) (third query)))))

(defun do-evaluate (query reasoner context response effort 
                          answer-var expr)
  (multiple-value-bind (answer antecedents)
      (evaluate expr reasoner context response effort)
    (unless (eq answer :eval-error)
      (let* ((binding-list (list (cons answer-var answer)))
             (bound-result (sublis binding-list query)))
        ;; Cache result in reasoner 
        (cond (antecedents 
               (tell `(:implies (:and ,@ antecedents) ,bound-result)
                     reasoner :eval context))
              (t (tell bound-result reasoner :eval context)))
        (list (case response
                (:bindings binding-list)
                (:pattern (sublis binding-list query))
                (t (sublis binding-list response)))))))) 

(defun do-evaluate-ground (query reasoner context response effort 
                                  answer expr)
  (multiple-value-bind (ans antecedents)
      (evaluate expr reasoner context response effort)
    ;; Did we get the same answer?
    (cond ((equal ans answer)
           (cond (antecedents 
                  (tell `(:implies (:and ,@ antecedents) ,query)
                        reasoner :eval context))
                 (t (tell query reasoner :eval context)))
           (list (case response
                   (:bindings '(nil))
                   (:pattern query)
                   (t query))))
          (t (values nil nil)))))

(defmethod predicate-ask-signatures ((pred (eql 'data::evaluate))
                                     (reasoner reasoner))
  :need-arguments)

(defmethod argument-based-predicate-signature ((predicate (eql 'data::evaluate))
                                               (arguments list)
                                               (reasoner reasoner))
  (let ((exp (cadr arguments))
        (var (car arguments)))
    (list 
     (list (if (variable? var) :produces
             :input-only)
           (if (and (listp exp)
                    (introduces-local-variable? (car exp)))
             :input-only ;; Was :can-produce, but I think that's just wrong
             :input-only)))))
         
         
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The core of the subsystem

(defun evaluate (form reasoner context response effort)
  (cond ((null form) nil)
        ((numberp form) form)
        ((atom form) form) ; `(quote ,form)?
        ((listp form)
         (evaluate-expression form reasoner context response effort))
        (t form)))

(defun evaluate-expression (form reasoner context response effort)
  (cond ((or (evaluatable-function? (car form)) ;; Like PlusFn
             (produces-evaluatable-function? (car form))
             (fire-evaluatable-function? (car form)))
         (let* ((given-args (cdr form))
                (given-arity (length given-args))
                (lisp-procedure (get-lisp-handler (car form)
                                                  :kb (kb reasoner)))
                (arity (arity (car form))))
           ;; TODO - Errorchecking by argIsa's
           (cond ((and (or (n-ary? (car form))
                           (and (integerp arity) (eql arity given-arity)))
                       (fboundp lisp-procedure))
                  (multiple-value-bind (arg-values arg-antes)
                      (evaluate-arguments 
                       given-args reasoner context response effort)
                    (cond ((eq arg-values :eval-error) :eval-error)
                          (t ;; Need to put juicier error handling here
                           ;; for runtime systems
                           (multiple-value-bind (the-value the-antes)
                               (apply lisp-procedure arg-values)
                             (values the-value (nconc arg-antes the-antes)))))))
                 (t :eval-error))))
        ((and (listp (car form))
              (produces-evaluatable-function? (caar form))) ;; Like FunctionToArg
         ;; Tried to make this more general, but then realized that one cannot know
         ;; the arity of the function without a lot more information!
         ;; First get the procedure, and apply it to the arguments
         (multiple-value-bind (procedure antes)
             (evaluate (car form) reasoner context
                       response effort)
           (cond ((or (evaluatable-function? procedure)
                      (fire-evaluatable-function? procedure))
                  (multiple-value-bind (the-value the-antes)
                      (evaluate-expression 
                       (cons procedure (cdr form))
                       reasoner context response effort)
                    (values the-value (nconc antes the-antes))))
                 (t :eval-error))))
        ;; We hit something that isnt evaluatable. Various things 
        ;; we could do here -- go ASK, or signal something to say
        ;; that we hit something thats not defined to be evaluated. 
        ;; Right now, we do the simplest thing, just returns the form. 
        ;; (ask form reasoner context number response effort)))
        ;;(return-from evaluate-1 :UNDEFINED-FUNCTION)))
        (t form)))

(defun evaluate-arguments (args reasoner context effort response)
  (let ((antecedents nil))
    (values (mapcar
                #'(lambda (arg)
                    (multiple-value-bind (arg-value arg-antes)
                        (evaluate arg reasoner context effort response)
                      (cond ((eq arg-value :eval-error)
                             (return-from evaluate-arguments (values :eval-error)))
                            (t (setq antecedents (nconc antecedents arg-antes))
                               arg-value))))
              args)
            antecedents)))

(defun quote-if-needed (thing)
  ;; Subtle issue: In the Lisp world, things like symbols and s-expressions need to
  ;; be quoted.  In the Logic world, these represent entities, predicates, and statements,
  ;; which should not be quoted.  So inside the evaluation process, we may need to keep
  ;; wrapping quotes around things to keep from having lisp errors.
  (cond ((symbolp thing) `(quote ,thing))
        ((listp thing)
         (if (eq (car thing) 'quote) thing
           `(quote ,thing)))
        (t thing)))

(defun get-lisp-handler (function-name &key (kb *kb*))
  (let ((entry (find-or-make-sc-function function-name kb)))
    (cond ((sc-function? entry)
           (sc-lisp-handler (sc-details entry)))
          (t nil))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Extending the language

;; There are things for which a sensible procedural interpretation exists
;; e.g., TheSetOf but which aren't in EvaluatableFunction in Cyc.  Since
;; we think there won't be many of these, and new predicates that we add
;; can include EvaluatableFunction as a genl, we use the generic procedure
;; fire-evaluatable-function? to track these special cases.

(defmethod fire-evaluatable-function? ((pred t)) nil)
(defmethod fire-evaluatable-function? ((pred (eql 'data::TheClosedRetrievalSetOf))) t)

;;;* Adding new evaluatable functions
;;; The defEvalFn form enables you to write the definition for a symbol 
;;; that stands for an EvaluatableFunction in the KB. 
;;;      (defEvalFunction <name> 
;;;                 :args ;; list of variables, or :n-ary
;;;                 :lispcode ;; lisp code that implements the function
;;;		 :axioms ;; list of assertions about this function 
;;;		         ;; that will be added to the KB.  
;;;		 :documentation)
;;; For example, (more in fire:*fire-path*\\evalfns.lsp)
;;;  (defEvalFn data::LengthOfListFn 
;;;  	     :args (?list)
;;;	     :lispcode (length ?list)
;;; 	     :documentation "Computes the length of a list"
;;;	     :axioms ((arg1Isa LengthOfListFn List) 
;;;     		      (resultIsa LengthOfListFn NonNegativeInteger)))		 
;;; 
;;; Tips for writing eval functions
;;; 1. Lisp-level errors are best handled locally.  You should always catch
;;; errors yourself, preferably via careful tests on the arguments, and
;;; with error handlers otherwise.  If your code gets an error, the
;;; evaluation subsystem will expect your procedure to return :eval-error,
;;; a special keyword symbol that should only be used for this purpose.
;;; For instance, in the example above, a better definition is
;;;
;;;(fire:defEvalFn LengthOfListFn 
;;;  :documentation "Computes the length of a list"
;;;  :args (?list)
;;;  :lispcode (if (and (listp ?list)
;;;                     (eql (car ?list) 'TheList)
;;;                     (listp (cdr ?list)))
;;;              (1- (length ?list)) ;; dont count TheList
;;;              :eval-error)
;;;  :axioms ((arg1Isa LengthOfListFn List) 
;;;           (resultIsa LengthOfListFn NonNegativeInteger)))
;;; since this will handle non-list inputs correctly without causing a lisp error.

;;; 2. Remember that you are, tacitly, writing a lisp procedure that will
;;; be compiled and executed. Efficiency matters. 

(defun create-fire-default-evaluation-files ()
  (create-evaluation-implementation-files
   (qrg::make-qrg-file-name *fire-path* "evalfns.lsp") 
   (qrg::make-qrg-file-name *fire-path* "evaluate-axioms.lsp")
   (qrg::make-qrg-file-name *fire-path* "evaluate-handlers.lsp")))

(defun create-evaluation-implementation-files
    (evalfn-file-name flat-file-name lisp-source-file-name)
  (let ((file-marker (cons nil nil)))
    (with-open-file (evalfns-ptr evalfn-file-name
                                 :direction :input)
      (with-open-file (flat-file-ptr flat-file-name
                                     :direction :output
                                     :if-exists :supersede)
        (with-open-file (lisp-source-ptr lisp-source-file-name
                                         :direction :output
                                         :if-exists :supersede)
          (write-evalfn-flat-file-header evalfn-file-name flat-file-ptr)
          (write-evalfn-lisp-source-header evalfn-file-name lisp-source-ptr)
          (let ((*package* (find-package :cl-user)))
            (do ((form (read evalfns-ptr nil file-marker)
                       (read evalfns-ptr nil file-marker)))
                ((eq form file-marker) evalfn-file-name)
              (cond ((defevalfn-form-okay? form)
                     (let* ((name (cadr form))
                            (lisp-code (extract-procedure-from-defevalfn form))
                            (axioms (extract-knowledge-from-defevalfn form
                                                                      (cadr lisp-code))))
                       (write-evalfn-lisp-code name lisp-code lisp-source-ptr)
                       (write-evalfn-axioms name axioms flat-file-ptr)))
                    ((and (listp form)
                          (member (car form) '(cl-user::defun cl-user::defvar
                                                  cl-user::defparameter)))
                     (write-evalfn-lisp-code "utilities"
                                             form lisp-source-ptr))))
            (write-evalfn-file-trailer flat-file-ptr)
            (write-evalfn-file-trailer lisp-source-ptr)))))))

(defun write-evalfn-flat-file-header (evalfn-file-name flat-file-ptr)
  (format flat-file-ptr ";;;; Axioms for ~A" evalfn-file-name)
  (format flat-file-ptr "~%;;;; Automatically generated ~A." 
    (generate-file-timestring))
  (format flat-file-ptr "~%;;;; PLEASE DO NOT MANUALLY EDIT.~%~%")
  (format flat-file-ptr "(in-package :data)~%~%"))

(defun write-evalfn-lisp-source-header (evalfn-file-name lisp-source-ptr)
   (format lisp-source-ptr ";;;; Lisp procedures for ~A" evalfn-file-name)
  (format lisp-source-ptr "~%;;;; Automatically generated ~A." 
    (generate-file-timestring))
  (format lisp-source-ptr "~%;;;; PLEASE DO NOT MANUALLY EDIT.~%~%")
  (format lisp-source-ptr "(in-package :data)~%~%"))

(defun write-evalfn-file-trailer (file-ptr)
  (format file-ptr "~%;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;")
  (format file-ptr "~%;; End of file~%"))

(defun generate-file-timestring ()
  (multiple-value-bind (second minute hour date month year)
      (decode-universal-time (get-universal-time))
    (format nil "~D/~D/~D, ~D:~D:~D" month date year hour minute second)))

(defun write-evalfn-lisp-code (name code file-ptr)
  (format file-ptr "~%;;; Lisp procedure for implementing ~A~%" name)
  (let ((*print-pretty* t))
    (format file-ptr "~S~%" code)))

(defun write-evalfn-axioms (name axioms file-ptr)
  (format file-ptr "~%;;; Axioms concerning ~A~%" name)
  (dolist (axiom axioms (format file-ptr "~%"))
    (format file-ptr "~%~S" axiom)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Parsing defevalfn forms

(defun defevalfn-form-okay? (form)
  (let ((winner? t))
    (cond ((and (listp form)
                (listp (cdr form))
                (eq (car form) 'data::defEvalFn))
           (multiple-value-bind (name arity arglist code documentation axioms)
               (parse-defevalfn-form form)
             (unless (symbolp name)
               (warn "defEvalFn: ~A not a symbol." name)
               (setq winner? nil))
             (unless (or (eq arity :n-ary)
                         (integerp arity))
               (warn "defEvalFn: Can't figure out arity for ~A." name)
               (setq winner? nil))
             (unless (or (listp arglist)
                         (symbolp arglist))
               (warn "defEvalFn: Arglist for ~A must be list or symbol." name)
               (setq winner? nil))
             (unless (listp code)
               (warn "defEvalFn: lispcode of ~A must be a list." name)
               (setq winner? nil))
             (unless (stringp documentation)
               (warn "defEvalFn: Documentation for ~A must be a string."
                 name)
               (setq winner? nil))
             (unless (and (listp axioms)
                          (not (null axioms)))
               (warn "defEvalFn: No axioms provided to constrain ~A." 
                 name)
               (setq winner? nil)))
           winner?)
          (t nil))))
  
(defun parse-defevalfn-form (form)
  (let ((keywords (cddr form)))
    (values (cadr form) ;; Name
            (get-arity-from-args (cadr (member :args keywords)))
            (get-arglist-from-args (cadr (member :args keywords)))
            (cadr (member :lispcode keywords))
            (cadr (member :documentation keywords))
            (cadr (member :axioms keywords)))))

(defun extract-procedure-from-defevalfn (defevalfn)
  (multiple-value-bind (name arity arglist lispcode documentation axioms)
      (parse-defevalfn-form defevalfn)
    (declare (ignore documentation axioms arity))
    `(cl-user::defun ,(generate-evalfn-procedure-name name)
       ,(if (listp arglist) arglist `(&rest ,arglist)) ;; Handle n-ary case
       ,lispcode)))

(defun extract-knowledge-from-defevalfn (defevalfn lisp-handler-name)
  (multiple-value-bind (name arity arglist lispcode documentation axioms)
      (parse-defevalfn-form defevalfn)
    (declare (ignore lispcode))
    (push (make-lisp-implementation-assertion name lisp-handler-name)
            axioms)
    (push (make-arity-assertion name :function
                                arglist
                                (if (eq arity :n-ary) '(:n-ary? t) nil))
          axioms)
    (push (make-eval-function-declaration name) axioms)
    (push (make-comment-statement name documentation) axioms)
    axioms))
      
    
(defun generate-evalfn-procedure-name (name)
  (intern (format nil "~A-~A" name (get-universal-time))
          (find-package :data)))

(defun get-arity-from-args (form)
  (if (eql (car form) :n-ary)
    :n-ary
    (length form)))

(defun get-arglist-from-args (form)
  (if (eql (car form) :n-ary)
    (cadr form)
    form))

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

(defun reinstall-fire-default-evaluation-info ()
  ;; Assumes KB, reasoner available
  (clean-out-old-evaluate-lisp-handler-procedures)
  (load-file *fire-path*
             "evaluate-handlers"
             :action :source-if-newer)
  (simple-flat-file->kb
   (qrg::make-qrg-file-name *fire-path* "evaluate-axioms.lsp")))

(defun clean-out-old-evaluate-lisp-handler-procedures (&key (kb *kb*))
  (with-open-file (fin (qrg::make-qrg-file-name *fire-path*
                                                "evaluate-axioms.lsp")
                       :direction :input)
    (let ((eof (cons nil nil)))
      (do ((form (read fin nil eof)
                 (read fin nil eof))
           (count 0))
          ((eq form eof) count)
        (when (and (listp form)
                   (eq (car form) 'data::lispProcedureImplementing))
          (dolist (old (retrieve (list (car form) (cadr form) '?old-code)))
            (incf count)
            (forget old :kb kb)))))))

(defun simple-flat-file->kb (file-name)
  (with-open-file (fin file-name 
                       :direction :input)
    (let ((marker nil)) 
      (do ((form (read fin nil marker)
                 (read fin nil marker))
           (counter 0 (incf counter)))
          ((eq form marker) counter)
        (kb-store form)))))

;;;Good things to trace if this subsystem is acting up:

(defun cl-user::trace-evaluation-subsystem ()
  (trace evaluate-arguments
         evaluate-expression
         evaluate
         do-evaluate-ground
         do-evaluate
         ask-for-evaluation
         produces-evaluatable-function?
         evaluatable-function?
         fire-evaluatable-function?))

(defun cl-user::untrace-evaluation-subsystem ()
  (untrace evaluate-arguments
         evaluate-expression
         evaluate
         do-evaluate-ground
         do-evaluate
         ask-for-evaluation
         produces-evaluatable-function?
         evaluatable-function?
         fire-evaluatable-function?))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End of Code