;;; Wumpus World


(in-package "USER")

;;;----------------------------------------------------------------------
;;; GLOBAL VARIABLES 

;;; current position of agent
(defvar *x-pos* 1)
(defvar *y-pos* 1)

;;; dimension of field: [1 .. *dimension*] X [1 .. *dimension*]
(defvar *dimension* 4)

;;; Fact base is realised as a list of facts
;;; Facts are lists of literals, ie. atomic or negated atomic facts
(defvar *fact-base*)


(defvar *rule-base*)

(setf *rule-base*
      (list
       #'(lambda (p1 p2) (if (known-fact `(breeze ,p1 ,p2))
			     (add-to-fact-base (in-some-adjacent-squares 'pit p1 p2))))
       #'(lambda (p1 p2) (if (known-fact `(not (breeze ,p1 ,p2)))
			     (add-to-fact-base (in-all-adjacent-squares-not 'pit p1 p2))))
       #'(lambda (p1 p2) (if (known-fact `(stench ,p1 ,p2))
			     (add-to-fact-base (in-some-adjacent-squares 'wumpus p1 p2))))
       #'(lambda (p1 p2) (if (known-fact `(not (stench ,p1 ,p2)))
			     (add-to-fact-base (in-all-adjacent-squares-not 'wumpus p1 p2))))
       #'(lambda (p1 p2) (if (known-fact `(bump ,p1 ,p2))
			     (add-to-fact-base (in-some-adjacent-squares 'wall p1 p2))))
       #'(lambda (p1 p2) (if (and (known-fact `(not (pit ,p1 ,p2)))
				  (known-fact `(not (wall ,p1 ,p2)))
				  (known-fact `(not (wumpus ,p1 ,p2))))
			     (add-to-fact-base (list `(or (ok ,p1 ,p2))))))
       #'(lambda (p1 p2) (if (and (known-fact `(not (pit ,p1 ,p2)))
				  (known-fact `(not (wall ,p1 ,p2)))
				  (known-fact `(wumpus ,p1 ,p2))
				  (known-fact 'wumpus-dead))
			     (add-to-fact-base (list `(or (ok ,p1 ,p2))))))
       #'(lambda (p1 p2) (if (known-fact `(OK ,p1 ,p2))
			     (add-to-fact-base
			      (list `(or (not (wumpus ,p1 ,p2)))
				    `(or (not (pit ,p1 ,p2)))))))
       ))


;;;----------------------------------------------------------------------
;;; AUXILIARY FUNCTIONS


(defun make-disjunction (disjuncts)
  (cons 'or disjuncts))

(defun is-or (fact)
  (and (listp fact)
       (eq (first fact) 'or)))

(defun disjuncts (fact)
  (rest fact))

(defun make-negation (atom)
  (list 'not atom))

(defun is-not (fact)
  (and (listp fact)
       (eq (first fact) 'not)))

(defun neg-atom (fact)
  (second fact))

;; expresses the fact that not not literal == literal
(defun negation-of (literal)
  (if (is-not literal)
      (neg-atom literal)
    (make-negation literal)))

(defun is-atomic (fact)
  (and (not (is-not fact))
       (not (is-or fact))))


;; checks whether a position is within acceptable bounds
(defun out-of-bounds (position)
  (or (< (1+ *dimension*) position)
      (< position 0)))


(defun acceptable-adjacent-positions (pos1 pos2)
  (let ((all-list (list
		   (list (1+ pos1) pos2)
		   (list pos1 (1+ pos2))
		   (list (1- pos1) pos2)
		   (list pos1 (1- pos2)))))
    (remove-if #'(lambda (pair)
		   (or (out-of-bounds (first pair))
		       (out-of-bounds (second pair))))
	       all-list)))

;;; construct a disjunctive fact
;;; (like in: a pit is above or below or to the left or right of position (pos1, pos2))
(defun in-some-adjacent-squares (object pos1 pos2)
  (let ((acc-pos (acceptable-adjacent-positions pos1 pos2)))
    (if acc-pos
	(list (make-disjunction (mapcar #'(lambda (p) (cons object p)) acc-pos)))
      nil)))

;;; construct a list of negative facts
;;; (like in: no pit is above and below ....)
(defun in-all-adjacent-squares-not (object pos1 pos2)
  (let ((acc-pos (acceptable-adjacent-positions pos1 pos2)))
    (mapcar #'(lambda (p) `(or (not ,(cons object p))))
		acc-pos)))



;;;----------------------------------------------------------------------
;;; MANIPULATION OF FACT BASE

;;; Tests whether the atomic fact is contained in the fact-base
;;; The atomic-fact is known if (or atomic-fact) is contained in the fact-base
(defun known-fact (atomic-fact)
  (find (make-disjunction (list atomic-fact))
	*fact-base* :test #'equal))

;;; Input: list of facts
;;; Output: new fact base
;;; Side effect: Global variable *fact-base* is set
(defun add-to-fact-base (facts)
  (setf *fact-base* (union facts *fact-base* :test #'equal)))

;;; Input: a fact
;;; Output: new fact base
;;; Side effect: Global variable *fact-base* is set
(defun remove-from-fact-base (fact)
  (let ((new-base (remove fact *fact-base* :test #'equal)))
    (setf *fact-base* new-base)))



;;;----------------------------------------------------------------------
;;; USER INTERACTION


(defun stench-percept (percept)
  (first percept))

(defun breeze-percept (percept)
  (second percept))

(defun gold-percept (percept)
  (third percept))

(defun bump-percept (percept)
  (fourth percept))

(defun scream-percept (percept)
  (fifth percept))

(defun termination-condition (percept)
  (and (not (listp percept))
       (or (eql percept 'pit)
	   (eql percept 'wumpus))))

(defun read-in-percepts ()
  (format T "Enter list of percepts: ")
  (let ((percept (read)))
    (if (not (termination-condition percept))
	;; no termination condition --> add new facts to base
	(progn
	  (add-to-fact-base (list `(or(OK ,*x-pos* ,*y-pos*))))
	  (add-to-fact-base
	   (list
	    (if (stench-percept percept)
		`(or (stench ,*x-pos* ,*y-pos*))
	      `(or (not (stench ,*x-pos* ,*y-pos*))))
	    (if (breeze-percept percept)
		`(or (breeze ,*x-pos* ,*y-pos*))
	      `(or (not (breeze ,*x-pos* ,*y-pos*))))
	    (if (gold-percept percept)
		`(or (gold ,*x-pos* ,*y-pos*))
	      `(or (not (gold ,*x-pos* ,*y-pos*))))
	    (if (bump-percept percept)
		`(or (bump ,*x-pos* ,*y-pos*))
	      `(or (not (bump ,*x-pos* ,*y-pos*))))))
	  (if (scream-percept percept)
	      (add-to-fact-base (list 'wumpus-dead)))
	  ;; continue
	  T)
      ;; otherwise, do not continue
      nil)))

(defun read-in-action ()
  (format T "Enter action: ")
  (let ((action (read)))
    (case action
      (walk-up (when (< *y-pos* *dimension*)  (setf *y-pos* (1+ *y-pos*))))
      (walk-down (when (< 1 *y-pos*)  (setf *y-pos* (1- *y-pos*))))
      (walk-right (when (< *x-pos* *dimension*)  (setf *x-pos* (1+ *x-pos*))))
      (walk-left (when (< 1 *x-pos*)  (setf *x-pos* (1- *x-pos*))))
      (T (read-in-action)))))

(defun output-state ()
  (format T "~%Fact base: ")
  (pprint *fact-base*)
  (format T "~%Current position: ~D ~D~%" *x-pos* *y-pos*))



;;;----------------------------------------------------------------------
;;; INFERENCE OF NEW FACTS


(defun do-inference (old-facts positions)
  ;; infer new facts
  (mapcar
   #'(lambda (pair)
       (mapcar  #'(lambda (rule) (apply rule pair)) *rule-base*))
   positions)
  ;; terminate if no new information can be derived
  (if (equal old-facts *fact-base*)
      (setf *fact-base* (remove-duplicates *fact-base* :test #'equal))
    (do-inference *fact-base* positions)))
    
(defun infer-new-facts ()
  (let ((positions (cons (list *x-pos* *y-pos*)
			 (acceptable-adjacent-positions *x-pos* *y-pos*))))
    (do-inference *fact-base* positions)))
  


;;;----------------------------------------------------------------------
;;; SIMPLIFICATION OF FACTS



;;; resolve fact1 with fact2, return the list of resolvents
;;; the facts have the form (or a1 .. an) and (or b1 .. bm)
(defun resolve-one (fact1 fact2)
  (remove-if #'(lambda (res) (null res))
	     (mapcar #'(lambda (literal)
			 (if (member (negation-of literal) (disjuncts fact2) :test #'equal)
			     (make-disjunction
			      (union (remove literal (disjuncts fact1) :test #'equal)
				    (remove (negation-of literal) (disjuncts fact2) :test #'equal)
				    :test #'equal))))
		     (disjuncts fact1))))


(defun resolve (facts)
  (remove-duplicates
   (append facts 
	   (apply #'append
		  (mapcar
		   #'(lambda (fct1)
		       (apply #'append 
			      (mapcar #'(lambda (fct2)
					  (resolve-one fct1 fct2))
				      facts)))
		   facts)))
   :test #'equal))


(defun simplify-facts (facts)
  (let ((new-facts (resolve facts)))
    (if (equal new-facts facts)
	;; no change --> simplification finished
	(setf *fact-base* new-facts)
      ;; otherwise, simplify again
      (simplify-facts new-facts))))

;;;----------------------------------------------------------------------
;;; RULE INTERPRETER

(defun start ()
  (reset)
  (output-state)
  (loop while  (read-in-percepts) do
	(infer-new-facts)
	(simplify-facts *fact-base*)
	(output-state)
	(read-in-action)))

(defun reset ()
  (setf *x-pos* 1)
  (setf *y-pos* 1)
  (setf *fact-base*  (list `(or (ok ,*x-pos* ,*y-pos*)))))