;;;; -*- mode:Scheme -*- ;;;; this is back.scm

(load-option 'format)

;;; counter for new variable suffix
(define *counter* 0)

;;; for nice printing
;;;
(define *indenting* 1)

(define (space-substring n)
  (if (= n 0)
      ""
      (string-append " " (space-substring (- n 1)))))

(define (indentit strng)
  (string-append "~%" 
		 (space-substring *indenting*)
		 strng))

;;;; Assertion functions

(define *assertions* '())

(define (clear-assertions) 
  ;; Removes all current assertions.
  (set! *assertions* '()))
 
(define (remember-assertion assertion)
  ;; Adds a single assertions to (front of) *assertions*
  (if (member assertion *assertions*)
      *assertions*
      (set! *assertions* (cons assertion *assertions*))))

(define (remember-assertions . assertions)
  ;; Adds a list of assertions to *assertions*, maintain the order.
  (begin
    (for-each remember-assertion assertions)
    (set! *assertions* (reverse *assertions*))))

(define (display-assertions assertions)
  ;; Print the assertions.
  (if (not (null? assertions))
      (begin (format #t "~%~a" (first assertions))
	     (display-assertions (rest assertions)))
      ))

;;;; Rule functions

(define *rules* '())

(define (clear-rules)
  ;; Removes all current rules.
  (set! *rules* '()))

(define (remember-rule rule)
  ;; Adds a single rules to (end of) *rules*
  (if (member rule *rules*)
      *rules*
      (set! *rules* (append *rules* (list rule)))
      ))

;;; Scheme note: the use of . in the argument list allows a function
;;; to be called with a variable number of arguments.  A list of any
;;; remaining arguments "left over" after binding required arguments
;;; are bound to the variable after the dot.  So, remember-rule can be
;;; called with any number of rules (see examples, e.g. zoo.scm).

(define (remember-rules . rules)
  ;; Adds a list of rules to *rules*
  (for-each remember-rule rules))


(define (rule-name rule) (first rule))
(define (rule-ifs rule) (extract-from-rule 'if rule))
(define (rule-thens rule) (extract-from-rule 'then rule))
(define (rule-then rule) (first (rule-thens rule)))

(define (extract-from-rule marker rule)
  ;; Construct a list of elements in the rule following the specified marker.
  (let ((fragment (member marker rule)))
    ;; (member x l) returns a sublist of l starting with x or #f.
    (if fragment
	(extract-expressions (rest fragment))
	'())))

(define (extract-expressions rule)
  ;; This returns a list of the elements following a marker (such as IF, THEN ...)
  ;; It relies on the fact that markers will fail the list? test.
  (cond ((null? rule) '())
	((list? (first rule))
	 (cons (first rule) (extract-expressions (rest rule))))
	(else '())))


;;;; BASIC MECHANISM FOR BACKWARD CHAINING

(define (backchain hypothesis)
  ;;;
  ;;; Chains backward from an hypothesis
  ;;;
  (set! *indenting* 0)
  (set! *counter* 0)
  (let ((bindings (eval-premise hypothesis '())))
    ;; Note that eval-premises returns either #f or a list containing a single
    ;; bindings list (to avoid () = #f confusion).
    (cond(bindings
	  (for-each (lambda (binding)
		      (format #t "~%We have established that ~a." 
			      (instantiate-variables hypothesis
						     binding)))
		    bindings)
	  (format #t "~%Final data base contents:")
	  (display-assertions *assertions*))
	 (else
	  (format #t  "~%It is not true that ~a." hypothesis)))))


(define (eval-premises patterns bindings)
  ;;;
  ;;; tries to see whether each premise of rule is true (ie assertion exists or rule
  ;;; can infer it) under the current accumulated set of bindings.
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (if (null? patterns)
	 ;; if we got to the end, return bindings
	 ;; to avoid confusing () with #f, return a list of the bindings.
	 bindings
	 (let ((result (eval-premise (first patterns) bindings)))
	   (if result
	       (eval-premises (rest patterns) (first result))
	       #f))))

(define (eval-premise pattern bindings)
  ;;;
  ;;; tries to see if one premise pattern is true. First checks assertions to
  ;;; see if the pattern w/bindings matches any assertion, 
  ;;;     if not tries to see if it can be inferred via a rule
  ;;; finally, asks user
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (format #t (indentit "Trying to establish whether ~a with bindings ~a.")
	  pattern bindings)
  (or (match-pattern-to-assertions pattern bindings)
      (match-pattern-to-rules pattern bindings)
      (ask? pattern bindings)))


(define (match-pattern-to-assertions pattern bindings)
  ;;; 
  ;;; tries to see if a bound pattern matches any assertion
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (there-exists?
   *assertions*
   (lambda (assertion) (try-assertion pattern assertion bindings))))

(define (try-assertion pattern assertion bindings)
  ;;;
  ;;; Tries to match one pattern against one assertion.
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (let ((result (do-match pattern assertion bindings)))
    (cond ((eq? result 'fail)
	   #f)
	  (else
	   (format #t (indentit "Assertion in db indicates ~a.") assertion)
	   ;; To avoid confusion of () with #f, return a list of result.
	   (list result)))))

(define (match-pattern-to-rules pattern bindings)
  ;;; 
  ;;; try each rule in the rule base to see if it will establish pattern
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (set! *indenting* (+ 2 *indenting*))
  (let ((result (map
		 (lambda (rule) (try-rule pattern rule bindings))
		  *rules*)))
    (set! *indenting* (- *indenting* 2))
    (let ((temp (list-transform-positive result
		  (lambda (item)
		    (not (eq? item '()))))))
      (if (eq? temp '())
	  #f
	  temp))
    ))

(define (try-rule hypothesis rule bindings)
  ;;;
  ;;; First see if rule is relevant, ie then-part can be unified with
  ;;; the hypothesis.  If so, take a step backward and try to establish
  ;;; the premises of the rule.
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (let* ((rule (make-variables-unique rule))
         (result (unify hypothesis (rule-then rule) bindings)))
    (cond((eq? 'fail result)
;;;	  (format #t (indentit "[Rule ~a is irrelevant.]") (rule-name rule))
;;;       uncomment the line above for extra tracing info
	  #f)
	 (else 
	  ; first announce backchaining
	  (format #t (indentit "Trying to establish ~a")
		  (instantiate-variables (rule-then rule) result))
	  (format #t " using rule ~a." (rule-name rule))
	  ; then start the process going on the premises
	  (let ((answer 
		 (eval-premises (rule-ifs rule) result)))
	    (cond(answer
		  (format #t (indentit "Rule ~a establishes ~a") 
			  (rule-name rule)
			  (instantiate-variables (rule-then rule) result)))
		 (else
		  (format #t (indentit "Rule ~a fails to establish ~a") 
			  (rule-name rule)
			  (instantiate-variables (rule-then rule) result))))
	    (format #t ".~%")
	    answer)))))

(define (ask? hypothesis bindings)
  ;;;
  ;;; Prompts the user to see whether hypothesis is true
  ;;; This returns either #f or a list of one element (the bindings list).
  ;;;
  (format #t (indentit "Have no assertion or rule to determine whether"))
  (format #t " ~a." (instantiate-variables hypothesis bindings))
  (format #t (indentit "Is this true [y or n]? "))
  (let ((ans (read)))
    (cond ((eq? ans 'y)
	   (remember-assertion (instantiate-variables hypothesis
						      bindings))
	   (list bindings))
	  ((eq? ans 'n)
	   #f)
	  (else 
	   (format #t "~%Answer must be either y or n.")
	   (ask? hypothesis bindings)))))
  
(define (make-variables-unique rule)
  ;;;
  ;;; Avoids conflict resulting from having the same variable
  ;;; names appear in more than one rule.
  ;;;
  (let* ((variables (list-variables rule))
	 (unique-variables (map (lambda (variable)
				  (set! *counter* (+ 1 *counter*))
				  (string->symbol
				   (format #f "~a~a" variable *counter*)))
				variables)))
    (instantiate-variables rule
			   (map (lambda (v l) (list v (list '? l)))
				variables
				unique-variables))))

(define (list-variables pattern)
  ;;;
  ;;; Create a list of the variables appearing in a pattern
  ;;; Ignore anonymous vars and make sure names appear only once
  ;;;
  (define (lv pat vars)
    (if (simple-variable? pat)
	(if (member (second pat) vars)
	    vars
	    (cons (second pat) vars))
	(if (pair? pat)
	    (lv (rest pat) (lv (first pat) vars))
	    vars)))
  (lv pattern '()))