;;; A SCM implementation of a simple PROLOG-like backward-chaining
;;; interpreter by Tomas Lozano-Perez, Feb 2000

;;; Scheme note:
;;; (fluid-let ((x 1)) ...)
;;; is just like
;;; (let ((x-init x)) (set! x 1) ... (set! x x-init))
;;; that is, x behaves as if dynamically scoped.  Note that x must be defined.

;;; Controls whether we ask the user.
(define *ask-user* #f)

;;; Global counter used to renaming variables to unique names.
;;; (counter) => returns current-value and increments
;;; (counter x) => sets current-value to x, returns current-value (not x)
(define counter
  (let ((counter-value 0))
    (lambda arg
      (let ((val counter-value))
	(if (null? arg)
	    (set! counter-value (+ val 1))
	    (set! counter-value (first arg)))
	val))))

;;; UNIFY - A generalization of equality matching that allows variables in both 
;;; the pattern and the goal.  It returns a bindings list that makes the pattern
;;; equal? to the goal or #f if no set of bindings exist.
;;; (unify '(parent (? x) (? y)) '(parent foo (? z)) (empty-bindings))
;;; => (bindings (y (? z)) (x foo))
;;; This assumes that the variables are "standardized apart", that is, there are 
;;; no coincidental name conflicts.  Same name variables all get the same value:
;;; (unify '(parent (? x) foo) '(parent foo (? x)) (empty-bindings))
;;; => (bindings (x foo))
;;; (unify '(parent (? x) foo) '(parent bar (? x)) (empty-bindings))
;;; => #f

(define (unify pattern goal bindings)
  (cond ((simple-variable? pattern)
	 (unify-variable pattern goal bindings))
	((simple-variable? goal)
	 (unify-variable goal pattern bindings))
	((eq? pattern goal) bindings)
	((and (pair? pattern) (pair? goal))
	 (let* ((result 
		 (unify (first pattern) (first goal) bindings)))
	   (if result
	       (unify (rest pattern) (rest goal) result)
	       #f)))
	(else #f)))

(define (unify-variable variable stuff bindings)
  (let ((variable-value (lookup variable bindings)))
    (if (simple-variable? variable-value)
	(add-binding variable stuff bindings)
	(unify variable-value stuff bindings))))

(define (lookup variable environment)
  (define (loop last-var)
    (let ((binding (find-binding last-var environment)))
      ;; variable is unbound, return it
      (cond ((not binding)		
	     last-var)
	    ;; a value that is not a variable
	    ((not (simple-variable? (binding-value binding))) 
	     (binding-value binding))
	    ;; bound to a variable
	    (else			
	     (loop (binding-value binding))))))
  (loop variable))

;;; TOP LEVEL

;;; Ask questions if can't show a goal is true via data or rules.
(define (backchain-asking-user goal)
  (fluid-let ((*ask-user* #t))
    (backchain goal)))

;;; Top-level function for establishing a list of goals.
(define (backchain igoals)
  (fluid-let ((*indent* 1))
    (counter 0)				; resets the counter to 0
    (let* ((goals (process-vars igoals)) ; map ?x into (? x)
	   (variables-in-goal (variables-in-thing goals))
	   (renaming (renaming-bindings-for-variables variables-in-goal))
	   (renamed-goals 
	    ;; add the answer predicate to keep track of the variable bindings
	    (instantiate-variables (add-answer-predicate goals)
				   renaming)))
      (backchain-loop renamed-goals 1))))

(define *max-depth* 10)

;; Do Depth-First Search for a proof
(define (backchain-loop goals depth)
  (define (remove x l)
    (if (null? l) l
	(if (equal? x (first l)) 
	    (rest l)
	    (cons (first l) (remove x (rest l))))))
  (cond ((only-answer-predicate? goals)
	 (display* "Success: " goals)
	 goals)
	((or (not goals) (> depth *max-depth*)) ; failed
	 (display* (indent) "Failed.")
	 #f)
	(else
	 (let* ((goal (pick-goal goals))
		(other-goals (remove goal goals)))
	   (if (eq? (car goal) '$eval)
	       (backchain-eval (second goal) other-goals depth)
	       (or (backchain-data goal other-goals depth)
		   (backchain-rules goal other-goals depth)
		   (if *ask-user* (backchain-user goal other-goals depth) #f))))
	 )))

;;; For establishing AND-IF conditions
(define (backchain-eval goal other-goals depth)
  (display* (indent) "Eval: " goal)
  (let ((result (scheme-eval goal)))
    (cond ((bindings? result)		; bound a variable
	   (display* (indent) "Eval won with bindings: " ans)
	   (backchain-loop (instantiate-variables* other-goals result) depth))
	  (result
	   (display* (indent) "Eval won.")
	   (backchain-loop other-goals depth))
	  (else
	   (display* (indent) "Eval failed.")
	   #f))))

;;; Checks whether the goal is present among the assertions in the database.
(define (backchain-data goal other-goals depth)
  (define (loop assertions)
    (cond ((null? assertions) #f)
	  ((backchain-datum (first assertions) goal other-goals depth))
	  (else
	   (loop (rest assertions)))))
  (display* (indent) "BC-data: " goal)
  (loop (get-assertions)))

;;; If an assertion in the database matches the goal, then try to
;;; prove the updated other-goals.  Otherwise, return #f.
(define (backchain-datum assertion goal other-goals depth)
  (let ((bindings (unify assertion goal (empty-bindings))))
    (cond (bindings
	   #|
	   (display* (indent)
		     "backchain-datum " assertion goal other-goals depth)
	   |#
	   (display*
	    (indent) "BC-data: " (instantiate-variables* goal bindings) " won")
	   ;; Try to finish the proof using this match.  If the
	   ;; proof fails, we'll fail here and backup to try the
	   ;; next datum in the data list.
	   (backchain-loop (instantiate-variables* other-goals bindings) depth))
	  (else #f))))

;;; Check whether any rule can assert the goal, if so, add the
;;; preconditions to the other-goals.
(define (backchain-rules goal other-goals depth)
  (define (loop rules)
    (cond ((null? rules) #f)
	  ((backchain-rule (first rules) goal other-goals depth))
	  (else
	   (loop (rest rules)))))
  (display* (indent) "BC-rules: " goal)
  (loop (get-rules)))

;;; Check whether the THEN part of the rule is unifiable with the
;;; goal.  If so, add the IF conditions to the other-goals.
(define (backchain-rule rule goal other-goals depth)
  (let* ((renaming (renaming-bindings-for-rule rule))
	 (renamed-then-part (instantiate-variables* (first (rule-thens rule)) renaming))
	 (bindings (unify goal renamed-then-part (empty-bindings))))
    (if bindings			; match!
	(fluid-let ((*indent* (+ *indent* 2)))
	  #|				;
	  (display* (indent)
		    "backchain-rule " (first rule) goal other-goals depth)
	  |#
	  (display* 
	   (indent) "Matched rule " (rule-name rule))
	  (backchain-loop
	   (instantiate-variables* 
	    (append (instantiate-variables* (rule-ifs rule) renaming)
		    other-goals
		    ;; signal the and-ifs to be done specially.
		    (map (lambda (and-if) (list '$eval and-if))
			 (instantiate-variables* (rule-and-ifs rule) renaming)))
	    bindings)
	   (+ depth 1)))
	#f)))

;;; Interact with the user.

(define (ask-user goal other-goals depth)
  (cond ((null? (variables-in-thing goal))
	 ;; Only ask when no variables
	 (cond ((member (list 'not goal) (get-assertions))
		#f)
	       ((member goal (get-assertions))
		;; This should not really happen...
		(backchain-loop other-goals depth))
	       (else
		(display* "Is " goal " true? (Type \"y\" or \"n\" and hit enter)")
		(let ((input (read)))
		  (cond ((eq? input 'y)
			 (remember-assertion goal) ; remember answer
			 (backchain-loop other-goals depth))
			((eq? input 'n)
			 ;; remember it is false
			 (remember-assertion (list 'not goal))
			 #f)
			(else
			 (display "Please type only \"y\" or \"n\" and hit enter.\n")
			 (ask-user goal other-goals depth)
			 ))))))
	(else 
	 ;; Could ask the user to provide bindings to make the goal true.
	 #f)))

(define (add-answer-predicate goals)
  (cons (cons 'ans (variables-in-thing goals)) goals))

(define (pick-goal goals)		; could be smarter...
  (let ((evals (filter (lambda (x) (eq? (car x) '$eval)) goals)))
    (cond ((null? goals) #f)
	  ((eq? (first (first goals)) 'ans)
	   (pick-goal (rest goals)))
	  ((there-exists? evals (lambda (x) (if (null? (variables-in-thing x)) x #f))))
	  (else (first goals)))))

(define (only-answer-predicate? goals)
  (and (not (null? goals))
       (for-all? goals (lambda (g) (eq? (first g) 'ans)))))

;;; Construct bindings that give each distinct variable a unique name.
(define (renaming-bindings-for-variables variables)
  (let ((bindings (empty-bindings)))
    (for-each
     (lambda (v)
       (set! bindings
	     (add-binding
	      v 
	      ;; new variable with a number attached  (? x) -> (? x6)
	      (make-simple-variable
	       (string->symbol (string-append (symbol->string (variable-name v)) 
					      (number->string (counter)))))
	      bindings))
       )
     variables)
    bindings))

;;; Get the bindings that uniquize the variables in a rule
(define (renaming-bindings-for-rule rule)
  (let ((variables (variables-in-thing rule)))
    (renaming-bindings-for-variables variables)))

;;; Repeatedly instantiates variables until none are left.  This is needed because
;;; variables may be bound to other variables.
(define (instantiate-variables* tree bindings)
  (do ((ans (instantiate-variables tree bindings) 
	    (instantiate-variables ans bindings))
       (prev #f ans))
      ((equal? prev ans) ans))
  )

;;; Debugging/Testing

(define (ask-test goal)
  (pretty-print (backchain goal)))

(define (tr)
  (trace lookup unify-variable unify backchain backchain-loop backchain-data backchain-datum 
	 backchain-rules backchain-rule backchain-eval
	 renaming-bindings-for-rule backchain-rule instantiate-variables instantiate-variables*
	 ))