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

;;; Controls whether we ask the user.
(define *ask-user* #f)
;;; Controls whether we try to find all possible proofs
(define *find-all* #f)
;;; Controls whether goals will fail if the depth of recursions is too
;;; large.
(define *max-depth* #f)
;;; Controls printing of failure...
(define *verbose* #f)

;;; TOP LEVEL

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

;;; Top-level function for establishing a list of goals.
(define (backchain-and goals)
  (set! *new-variable-counter* 0)
  (backchain-loop (rename-variables (add-answer-predicate goals)) 1))

;; Do Depth-First Search for a proof
(define (backchain-loop goals depth)
  (cond ((or (not goals) (null? goals))
	 (error "Empty goal list"))
	((only-answer-predicate? goals)
	 (display* (indent-n depth) "Success: " goals)
	 goals)
	((and *max-depth* (> depth *max-depth*))
	 (if *verbose* (display* (indent-n depth) "Too deep, failed."))
	 #f)
	(else
	 (let* ((goal (pick-goal goals))
		(other-goals (remove goal goals)))
	   ;; Check the special cases: $eval, $eq?, $neq?, $bind, $assert...
	   (cond ((member (first goal) '($eval $eq? $neq? $bind $assert $not))
		  (backchain-special goal other-goals depth))
		 (else
		  (or (backchain-data goal other-goals depth)
		      (backchain-rules goal other-goals depth)
		      (if *ask-user* (backchain-user goal other-goals depth) #f)))))
	 )))

;;; Checks whether we can prove the goal with some assertion
(define (backchain-data goal other-goals depth)
  (define (loop assertions)
    (cond ((null? assertions) #f)
	  ((let ((ans (backchain-datum (first assertions) goal other-goals depth)))
	     (if (and ans *find-all*)	; keep going?
		 (loop (rest assertions))
		 ans)))
	  (else
	   (loop (rest assertions)))))
  (if *verbose* (display* (indent-n depth) "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)
  (and (null? (variables-in assertion))
       ;; since we don't have variables in the assertion we can do match instead of unify.
       (let ((bindings (match goal assertion))) 
	 (cond (bindings
		(display*
		 (indent-n depth) "BC-data: " (subst-bindings bindings goal) " won")
		;; Try to finish the proof using this match.  If the
		;; proof fails, we'll backup to try the next assertion.
		(backchain-loop (subst-bindings bindings other-goals) 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)
	  ((let ((ans (backchain-rule (first rules) goal other-goals depth)))
	     (if (and ans *find-all*)	; keep going
		 (loop (rest rules))
		 ans)))
	  (else
	   (loop (rest rules)))))
  (if *verbose* (display* (indent-n depth) depth " 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* ((renamed-rule (rename-variables rule))
	 (renamed-then-part (first (rule-thens renamed-rule)))
	 (bindings (unify goal renamed-then-part)))
    (if bindings			; match!
	(begin
	  (if *verbose* 
	      (display* 
	       (indent-n depth) "Matched rule " (rule-name rule)))
	  (backchain-loop
	   (subst-bindings 
	    bindings
	    ;; Put new subgoals in front of the pendings ones (depth first).
	    (append (rule-ifs renamed-rule)
		    ;; assert the result if we get here
		    (list (list '$assert (rule-name rule) renamed-then-part))
		    other-goals))
	   (+ depth 1)))
	#f)))

;;; For "non-standard" goals.  Most of these require that no variables
;;; exist in the goal; these should really be delayed rather than
;;; producing failure.  That's been delayed until future versions.
(define (backchain-special goal other-goals depth)
  (cond ((eq? (first goal) '$neq?)
	 ;; Check inequality (can't have variables)
	 (cond ((and (null? (variables-in goal))
		     (not (eq? (second goal) (third goal))))
		(display* (indent-n depth) goal " won")
		(backchain-loop other-goals depth))
	       (else
		(if *verbose* (display* (indent-n depth) goal " failed"))
		#f)))
	((eq? (first goal) '$eq?)
	 ;; Check equality (can't have variables)
	 (cond ((and (null? (variables-in goal))
		     (eq? (second goal) (third goal)))
		(display* (indent-n depth) goal " won")
		(backchain-loop other-goals depth))
	       (else
		(if *verbose* (display* (indent-n depth) goal " failed"))
		#f)))
	((eq? (first goal) '$assert)
	 ;; Assert a result so we don't have to prove it again (or
	 ;; just to record answer).  If the result has variables, it
	 ;; won't be used later.
	 (display* (indent-n depth) depth " Rule " (second goal) " won: " (third goal))
	 (remember-assertion (third goal))
	 (backchain-loop other-goals depth))
	((eq? (first goal) '$not)	
	 ;; negation by failure (goal can't have variables)
	 (cond ((null? (variables-in (second goal)))
		(display* (indent-n depth) "Attempting to show: " goal)
		;; Scheme note:
		;; (fluid-let ((x 1)) ...)
		;; is just like (let ((x-init x)) (set! x 1) ... (set! x x-init))
		(cond ((fluid-let ((*max-depth* #f)) ; it has to be a "real" failure.
			 (backchain-and (rest goal)))
		       (display* (indent-n depth) goal " failed")
		       #f)
		      (else
		       (display* (indent-n depth) goal " succeeded")
		       (backchain-loop other-goals depth))))
	       (else
		(if *verbose* (display* (indent-n depth) goal " has variables"))
		#f)))
	((eq? (first goal) '$bind)	
	 ;; ($bind var <expression>), expression is evaluated and
	 ;; can't have variables and the value is bound to the variable.
	 (cond ((null? (variables-in (third goal)))
		(let ((binding 
		       (extend-bindings (second goal) (scheme-eval (third goal))
					*no-bindings*)))
		  (display* (indent-n depth) "Created binding: " binding)
		  (backchain-loop (subst-bindings binding other-goals) depth)))
	       (else
		(if *verbose*
		    (display* (indent-n depth) "Binding cannot have free variables: " goal))
		#f)))
	((eq? (first goal) '$eval)	
	 ;; ($eval <expression>) evals the expression, which must be non-#f
	 (cond ((null? (variables-in goal))
		(let ((result (scheme-eval (second goal))))
		  (cond (result
			 (display* (indent-n depth) "Evaluated: " (second goal) " and won")
			 (backchain-loop other-goals depth))
			(else
			 (if *verbose*
			     (display* (indent-n depth) "Evaluated: " (second goal) " and failed"))
			 #f))))
	       (else
		(if *verbose* 
		    (display* (indent-n depth) "Evaluation cannot have free variables: " goal))
		#f)))
	(else
	 (error "Unknown special goal type:" goal))))

;;; Interact with the user.

(define (ask-user goal other-goals depth)
  (cond ((null? (variables-in goal))
	 ;; Only ask when no variables
	 (cond ((member (list 'not goal) (get-assertions))
		;; check whether this question has been answered
		;; negatively before.
		#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)	; add to the back of the other goals
  (append goals (list (cons 'ans (variables-in goals)))))

(define (pick-goal goals)		; could be smarter...
  (first goals))

(define (only-answer-predicate? goals)	; there should really be only one...
  (and (not (null? goals))
       (for-all? goals (lambda (g) (eq? (first g) 'ans)))))

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

;;; Debugging/Testing

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