(in-package "USER")

(setq *limit* 2)
(setq *new-macros* nil)
(setq *goodness* 200)

(defun goal-of (stage)
  (car stage))
(defun current-of (stage)
  (cadr stage))
(defun relevants-of (stage)
  (caddr stage))
(defun irrelevants-of (stage)
  (cadddr stage))

(defun state-of (node)
  (cadr node))
(defun moves-of (node)
  (car node))

; returns a custom macro, given the names of operators in a list
(defun mm (name)
  (declare (special OPERATORS))
  (form-macro (mapcar #'(lambda (o) (assoc (list o) OPERATORS :test #'equal))
		      name)
	      nil))

; A move is a-new-move if it is not already in MACROS, if so it is also added
(defun a-new-move (move)
  (cond ((and (cddr move)		; not an identity move
	      (add-new-macro move)))))

; A move is a-good-move if it has less than k assignments
(defun a-good-move (move)
  (declare (special *goodness*))
  (< (length (cddr move)) *goodness*))

(defun strategy (n)
  (declare (special PROBLEMS))
  (nthcdr n (nth 0 problems)))

(defun update (strategy)
  (declare (special *new-macros*))
  (format t "Updating the strategy with ~S new macros~%" (length *new-macros*))
  (format t "updated stages: ~S~%" (update-strategy strategy *new-macros*))
  (setq *new-macros* nil))
  
;returns a node of the form: (path state) if there is a solution
;returns nil if no solution is found
(defun solve (initial-state strategy)
  (declare (special *limit*))
   (format t "number of remaining stages: ~S~%" (length strategy))
  (if strategy
      (do ((depth-bound 0 (1+ depth-bound))
	   (path nil))
	  ((or (> depth-bound *limit*) path) 
	   (if path 
	       (list path 
		     (apply-move-to-state 
		      (form-macro path (current-of (car strategy))) 
		      initial-state))))
	  (setq path (dfs initial-state strategy nil depth-bound)))
    (list nil initial-state)))

; returns a list of moves       
(defun dfs (initial-state strategy path-in-stage depth-bound)
  (declare (special *new-macros*))
  (let ((children nil) 
	(macro-from-path nil)
	(solution-of-rest nil))

    (cond ((= 0 depth-bound)		; bottom of the search tree
	   (setq macro-from-path 
		 (form-macro (reverse path-in-stage)
			     (current-of (car strategy))))
	   (if (and (a-good-move macro-from-path)
		    (a-new-move macro-from-path))
	       (setq *new-macros* (cons macro-from-path *new-macros*)))

	   (if (and (evaluate initial-state (goal-of (car strategy)))
		    (setq solution-of-rest 
			  (solve initial-state (cdr strategy))))
	       (append path-in-stage (moves-of solution-of-rest))))

	  ((= 1 depth-bound)		; last move is a relevant one
	   (setq children               ; list of nodes
		 (expand-state initial-state (relevants-of (car strategy))))
	   (do ((children children (cdr children))
		(solution nil))
	       ((or (null children) solution) solution)
	       (setq solution 
		     (dfs (state-of (car children)) 
			  strategy 
			  (append path-in-stage (moves-of (car children)))
			  0))))

	  (t				; depth-bound > 1
	   (setq children 
		 (expand-state initial-state
			      (append (relevants-of (car strategy))
				      (irrelevants-of (car strategy)))))
	   (do ((children children (cdr children))
		(solution nil))
	       ((or (null children) solution) solution)
	       (setq solution 
		     (dfs (state-of (car children)) 
			  strategy 
			  (append path-in-stage (moves-of (car children)))
			  (1- depth-bound))))))))
	   
;returns a node
(defun expand-state (state moves)
  (mapcan #'(lambda (move)
	      (let ((precond (cadr move)))
		(if (evaluate state precond)
		    (list (list (list move) (apply-move-to-state move state)))
		  nil)))
	  moves))

(defun apply-move-to-state (move state)
  (declare (special VARIABLES))
  (let ((assignments (cddr move))
	(temp-state (copy-list state)))
    (dolist (assign assignments temp-state)
	    (setf (nth (position (car assign) VARIABLES) temp-state)
		  (eval-assignment (cdr assign) state)))))

(defun eval-assignment (expression state)
  (declare (special CONSTANTS))
  (declare (special VARIABLES))
  (if (= 1 (length expression))
      (if (member (car expression) CONSTANTS) (car expression)
	(nth (position (car expression) VARIABLES) state))
    (funcall (car expression) (eval-assignment (cdr expression) state))))
	 
(defun inc-3 (value)
  (if (= value 2) 0 (1+ value)))
              
(defun evaluate (state statement)
  (cond ((null statement) state)
	((evaluate-a-stmt state (car statement))
	 (evaluate state (cdr statement)))
	(t nil)))

(defun evaluate-a-stmt (state a-stmt)
  (let ((arg1 (value-of (nth 1 a-stmt) state))
	(arg2 (value-of (nth 2 a-stmt) state)))
    (case (car a-stmt)
	  (EQ (eql arg1 arg2))
	  (NE (not (eql arg1 arg2)))
	  (otherwise 
	   (format t "I don't know how to test for ~S yet" (car a-stmt))))))

(defun value-of (exp state)
  (declare (special VARIABLES))
  (declare (special CONSTANTS))
  (if (member exp CONSTANTS) exp (nth (position exp VARIABLES) state)))

(defun form-macro (moves current-of-stage)
  (unless (null moves)
	  (let ((new-macro (car moves)))
	    (dolist (move (cdr moves) (if (nth 2 new-macro) new-macro nil))
		    (setq new-macro (extend new-macro move current-of-stage)))
	    new-macro)))