;;; 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 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)
	 ;; rename the variables in goal to avoid conflicts
	 (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))
	 (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-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
		(display*
		 (indent-n depth) "BC-data: " (instantiate-variables* goal bindings) " won")
		;; Try to finish the proof using this match.  If the
		;; proof fails, we'll backup to try the next assertion.
		(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)
	  ((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* ((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!
	(begin
	  (if *verbose* 
	      (display* 
	       (indent-n depth) "Matched rule " (rule-name rule)))
	  (backchain-loop
	   (instantiate-variables* 
	    ;; Put new subgoals in front of the pendings ones (depth first).
	    (append (instantiate-variables* (rule-ifs rule) renaming)
		    ;; assert the result if we get here
		    (list (list '$assert (rule-name rule) renamed-then-part))
		    other-goals)
	    bindings)
	   (+ 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-thing 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-thing 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-thing (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-thing (third goal)))
		(let ((binding 
		       (add-binding (second goal) (scheme-eval (third goal))
				    (empty-bindings))))
		  (display* (indent-n depth) "Created binding: " binding)
		  (backchain-loop (instantiate-variables* other-goals binding) 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-thing 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-thing 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-thing 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)))))

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

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