;;; A SCM implementation of a simple PROLOG-like backward-chaining
;;; interpreter.  This is a translation of Howie Shrobe's Common Lisp
;;; implementation 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 want all possible derivations of a goal
(define *find-all* #f)

;;; 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 . code)
  (fluid-let ((*ask-user* #t))
    (apply backchain (cons goal code))))

;;; Find all answers for a goal
(define (backchain-all goal . code)
  (fluid-let ((*find-all* #t))
    (apply backchain (cons goal code))))

;;; Top-level function for establishing a goal.
(define (backchain igoal . code)
  (fluid-let ((*indent* 1))
    (counter 0)				; resets the counter to 0
    (let* ((goal (process-vars igoal))	; map ?x into (? x)
	   (variables-in-goal (variables-in-thing goal))
	   (renaming (renaming-bindings-for-variables variables-in-goal))
	   (renamed-goal (instantiate-variables goal renaming)))
      (ask renamed-goal 
	   (empty-bindings)
	   (lambda (bindings)
	     ;; if we are doing this, we succeeded.
	     (let ((all-bindings (merge-bindings renaming bindings)))
	       (if (not (null? code))
		   ((first code) all-bindings)
		   (display* 
		    "Success: " (instantiate-variables* goal all-bindings))))
	     #t)))))

;;; The basic inference function, checks the database and then the rules and 
;;; finally asks the user (if that is enabled).
;;; The "continuation" is a function that carries out the pending work to be
;;; done upon success of this goal.
(define (ask goal environment continuation)
  (display* 
   (indent) "Ask: " (instantiate-variables* goal environment))
  (if (eq? (first goal) '$eval)		; generated by AND-IF expression
      (ask-eval (second goal) environment continuation)
      (if *find-all*
	  ;; If we want all the bindings, then even if we find an answer
	  ;; in the database, we need to see if another is deriveable.
	  (begin 
	    (ask-data goal environment continuation)
	    (ask-rules goal environment continuation))
	  ;; Looking for just one answer, so stop after the first.
	  (or (ask-data goal environment continuation)
	      (ask-rules goal environment continuation)
	      (and *ask-user* (ask-user goal environment continuation)))))
  )

;;; Checks whether the goal is present among the assertions in the database.
;;; If it is, execute continuation, otherwise return #f.
(define (ask-data goal environment continuation)
  (define (loop assertions)
    (cond ((null? assertions) #f)
	  ((ask-datum (first assertions) goal environment continuation)
	   (if *find-all* 
	       ;; try to match the rest of the assertions.
	       (loop (rest assertions)))
	   #t)
	  (else
	   (loop (rest assertions)))))
  (display* 
   (indent) "Ask-data: " (instantiate-variables* goal environment))
  (loop (get-assertions)))

;;; If an assertion in the database matches the goal, then do any pending work
;;; by executing the continuation function.  Otherwise, return #f.
(define (ask-datum assertion goal environment continuation)
  (let ((result (unify assertion goal environment)))
    (cond (result
	   (display*
	    (indent) "Ask-data: " (instantiate-variables* goal result) " won")
	   (continuation result))
	  (else #f))))

;;; Check whether any rule can assert the goal, if so, then recursively examine
;;; the IF conditions of the rule.
(define (ask-rules goal environment continuation)
  (define (loop rules)
    (cond ((null? rules) #f)
	  ((ask-rule (first rules) goal environment continuation)
	   (if *find-all* 
	       (loop (rest rules)))
	   #t)
	  (else
	   (loop (rest rules)))))
  (display* 
   (indent) "Ask-rules: " (instantiate-variables* goal environment))
  (loop *rules*))

;;; Check whether the THEN part of the rule is equal to the goal.  If so, call ask-and
;;; which will loop through the IF conditions to make sure they can be satisfied.
(define (ask-rule rule goal bindings continuation)
  (let* ((renaming (renaming-bindings-for-rule rule))
	 (renamed-then-part (instantiate-variables (first (rule-thens rule)) renaming))
	 (extended-bindings (unify goal renamed-then-part bindings)))
    (if extended-bindings
	(fluid-let ((*indent* (+ *indent* 2)))
	  (display* 
	   (indent) "Checking rule " (rule-name rule))
	  (ask-and 
	   (instantiate-variables 
	    (append (rule-ifs rule)
		    ;; signal the and-ifs to be done specially.
		    (map (lambda (and-if) (list '$eval and-if)) (rule-and-ifs rule)))
	    renaming)
	   extended-bindings
	   (lambda (winning-bindings)
	     (let ((new (instantiate-variables* renamed-then-part winning-bindings)))
	       (display* 
		(indent) "Rule " (rule-name rule) " won: " new)
	       ;; remember this if it has no variables.
	       (if (null? (variables-in-thing new))
		   (remember-assertion new))
	       )
	     (continuation winning-bindings))))
	#f)))

;;; Establish each of the goals and then do continuation
(define (ask-and goals bindings continuation)
  (if (null? goals)
      (continuation bindings)
      (ask (first goals)
	   bindings
	   (lambda (extended-bindings)
	     (ask-and (rest goals)
		      extended-bindings
		      continuation)))))

;;; For establishing AND-IF conditions
(define (ask-eval goal bindings continuation)
  (let ((ngoal (instantiate-variables* goal bindings)))
    (let ((ans (scheme-eval ngoal)))
      ;;(print ans)
      (cond ((bindings? ans)
	     (display* (indent) "Eval won with bindings: " ans)
	     (continuation (merge-bindings ans bindings)))
	    (ans
	     (display* (indent) "Eval won.")
	     (continuation bindings))
	    (else
	     (display* (indent) "Eval failed.")
	     #f)))))

;;; Interact with the user.

(define (ask-user goal environment continuation)
  (let ((fact (instantiate-variables* goal environment)))
    (cond ((null? (variables-in-thing fact))
	   ;; Only ask when no variables
	   (cond ((member (list 'not fact) (get-assertions))
		  #f)
		 ((member fact (get-assertions))
		  ;; keep chaining
		  (continuation environment))
		 (else
		  (display* "Is " fact " true? (Type \"y\" or \"n\" and hit enter)")
		  (let ((input (read)))
		    (cond ((eq? input 'y)
			   (remember-assertion fact) ; remember answer
			   (continuation environment))
			  ((eq? input 'n)
			   ;; remember it is false
			   (remember-assertion (list 'not fact))
			   #f)
			  (else
			   (display "Please type only \"y\" or \"n\" and hit enter.\n")
			   (ask-user goal environment continuation)
			   ))))))
	  (else 
	   ;; Could ask the user to provide bindings to make the goal true.
	   #f))))

;;; 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)
  (backchain
   goal
   (lambda (bindings)
     (pretty-print bindings)
     #t)))

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