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

;;; Top-level function for establishing a single goal.
(define (backchain igoal)
  (backchain-and (list igoal)))

;;; Top-level function for establishing a list of goals.
(define (backchain-and igoals)
  (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)))

;; Do Depth-First Search for a proof
(define (backchain-loop goals depth)
  (cond ((or (not goals) (null? goals))	; Failure
	 (error "Empty goal list"))
	((only-answer-predicate? goals)	; Success
	 goals)
	(else
	 (let* ((goal (first goals))	; Recursion
		(other-goals (remove goal goals)))
	   (or (backchain-data goal other-goals depth)
	       (backchain-rules goal other-goals depth)))
	 )))

;;; Checks whether we can prove the goal with some assertion
(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)))))
  (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)
  (and (null? (variables-in-thing assertion))
       ;; since we don't have variables in the assertion we can do match instead of unify.
       (let ((bindings (match goal assertion))) 
	 (cond (bindings
		;; 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)))))

;;; Checks whether we can prove the goal with some rule
(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)))))
  (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		; rename variables to avoid conflict
	  (instantiate-variables* (first (rule-thens rule)) renaming))
	 (bindings (unify goal renamed-then-part (empty-bindings))))
    (cond (bindings			; match!
	   (backchain-loop
	    (instantiate-variables* 
	     ;; Put new subgoals in front of the pendings ones (depth first).
	     (append (instantiate-variables* (rule-ifs rule) renaming)
		     other-goals)
	     bindings)
	    (+ depth 1)))
	  (else #f))))

(define (add-answer-predicate goals)	
  ;; add (ans . variables) to the back of the other goals
  (append goals (list (cons 'ans (variables-in-thing goals)))))

(define (only-answer-predicate? goals)	
  (and goals (not (null? goals))
       ;; there should really be only one but this handles the general case.
       (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)))

;;; 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))))

(define (remove x l)
  (if (null? l) l
      (if (equal? x (first l)) 
	  (rest l)
	  (cons (first l) (remove x (rest l))))))