;;Rules	are represented	as (head bodys)	list,
;;	      stored in	the predicate's	plist
;; for example,
;; R1=(Head   Bodys)
;;   =((p ...)(q ...)(r	...)...)
;; Append R into (get p	'rules)

(defvar	*prolog-rules* nil)

(defun add-index (index)
   (setf *prolog-rules*	(adjoin	index *prolog-rules*)) )
(defun clear-index (index)
		 (setf (get index 'rules) nil))
(defun get-index (rule)	(caar rule))

(defmacro <-- (rule) `(add-rule	',rule))
(defmacro fact (&rest facts) `(add-rule	',facts))
(defmacro rule (head sign &rest	rules)
			    `(<-- (,head ,@rules)))

(defun add-rule	(rule)
  (let*	((index	   (get-index rule))
	 (oldrules (get	index 'rules)))
	(add-index index)
	(setf (get index 'rules)
	      (nconc oldrules (list rule)))
	(format	t "~&Add ~a to ~a --> ~a " rule	index (get index 'rules))
) )
(defun clear-rules ()
   (dolist  (x *prolog-rules*)
      (clear-index x))
   (setf *prolog-rules*	nil)
)


(defun my-prove	(goal binds)
 ;(format t "~&Prove ~a" (get (get-index goal) 'rules))
  (let ((result	nil))
    (dolist (rule (get (get-index goal)	'rules)	result)
       (let* ((nr (rename-var rule))
	      (tmp (my-prove-all (cdr nr)
		      (unify-binds (car	goal)(car nr) binds)
	     ))	   )
	     (setf result (append tmp result))
) ) )  )

(defun my-prove-all (goals binds)
  (cond
	((null binds) nil)
	((null goals) (list binds))
	(t (let	((result nil))
	    (dolist (x (my-prove goals binds) result)
	      (setf result
		    (append (my-prove-all (rest	goals) x) result)
) )	)  )) )

(defun my-prove-one-by-one (goals binds)
  (cond
       ((null binds) nil)
       ((null goals) binds)
       (t (my-prove-one	(first goals) binds (rest goals))
) )    )

(defun my-prove-one (goal binds	rest-goals)
  (let ((clauses (get (first goal) 'rules)))
    (cond
       ((listp clauses)
	(some #'(lambda	(rule)
		 (format t "~&Try rule ~a" rule)
		 (let ((nr (rename-var rule)))
		      (my-prove-one-by-one
			(append	(rest nr) rest-goals)
			(unify-binds goal (first nr) binds)
		))    )
	      clauses
       ))
       ((eql '!	clauses) nil)
       ((eql '$	clauses)
	(show-result (rest goal) binds)
	(if (continue-p)
	    nil
	    (my-prove-one-by-one rest-goals binds)
       ))
) ) )

(defun one-by-one-with-cut (goals binds)
  (cond
       ((null binds) (values nil nil))
       ((null goals) (values binds nil))
       (t (multiple-value-bind (bs cut?)
	     (one-with-cut (first goals) binds (rest goals))
	     (values bs	cut?)
) )    )  )

(defun one-with-cut (goal binds	rest-goals)
  (let ((clauses (get (first goal) 'rules)))
    (cond
       ((listp clauses)
	(let ((cutvalue	nil)(bs2 nil))
	 (dolist (rule clauses)
	    (format t "~&Try rule ~a" rule)
	    (let ((nr (rename-var rule)))
		 (multiple-value-bind (bs cut?)
		   (one-by-one-with-cut
		     (append (rest nr) rest-goals)
		     (unify-binds goal (first nr) binds)
		   )
		   (setf cutvalue cut?)
		   (setf bs2 bs)
	    )	 )
	    (when cutvalue (return))
	 )
	 (values bs2 cutvalue)
       ))
       ((eql '!	clauses)
	(format	t "~&* Cut here! *")
	(multiple-value-bind (bs cut?)
	   (one-by-one-with-cut	rest-goals binds)
	   (values bs t)
       ))
       ((eql '$	clauses)
     ;	(format	t "~&$..binds= ~a" binds)
	(show-result (rest goal) binds)
	(if (continue-p)
	    (values nil	nil)
	    (multiple-value-bind (bs cut?)
	      (one-by-one-with-cut rest-goals binds)
	      (values bs cut?)
	)   )
       )
) ) )

(defun continue-p ()
   (case (read-char)
       (#\; t)
       (#\. nil)
       (#\newline (continue-p))
       (otherwise
	  (format t " Enter ; to see more or . to stop")
	  (continue-p)
)  )   )

(defun rename-var (x)
  "replace all variables in x with new ones."
  (sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
		  (vars-in x))
	  x
) )

(defun vars-in (exp)
   (let* ((tmp1	(DF-search exp))
	  (tmp2	(remove-if-not #'var-p tmp1))
	  (result nil))
	 (dolist (x tmp2 result)
	   (setf result	(adjoin	x result))
)  )	 )

(defun DF-search (L)
   (cond ((null	L) ())
	 ((atom	L) (list L))
	 (t `(,@(DF-search (car	L))
	      ,@(DF-search (cdr	L)))
)  )	 )

;(defmacro ?- (&rest goals) `(my-prove-all ',goals '(())))
(defmacro ??  (&rest goals) `(top-level-prove ',goals))
(defmacro ?1  (&rest goals) `(top-level-prove-one-by-one ',goals))
(defmacro ?1c (&rest goals) `(top-level-one-by-one-with-cut ',goals))


(defun unify-binds (x y	binds)
   (cond
      ((and (null x)(null y))
       (if (null binds)	t binds	))
      ((or  (null x)(null y)) nil)
      ((eql x y) binds)
      ((eql (car x)(car	y))
       (unify-binds (cdr x)(cdr	y) binds))
      ((header-p (car x) #\?)
       (let ((new-binds	(extend-binds (car x) (car y) binds)))
	   (if (null new-binds)
	       nil
	       (unify-binds (cdr x)(cdr	y) new-binds)
      ))   )
      ((header-p (car y) #\?)
       (let ((new-binds	(extend-binds (car y) (car x) binds)))
	   (if (null new-binds)
	       nil
	       (unify-binds (cdr x)(cdr	y) new-binds)
      ))   )
)  )

(defun header-p	(x head)
   (and	(symbolp x)
	(char= (char (symbol-name x) 0)	head )))

(defun extend-binds (x y b)
   (let	((xpair	(assoc x b))
	 (ypair	(assoc y b)))
	(cond
	    ((eql x y) b)
	    ;binding of	x exist
	    ((not (null	xpair))
	     (extend-binds (second xpair) y b))
	    ;binding of	x not exist
	    ((and (var-p y) ypair)
	     (extend-binds x (second ypair) b))
	    ;neither x nor y is	variable
	    ((and (not (var-p x))(not (var-p y)))
	      (if (eql x y) b nil))
	    (t (if (var-p x)
		   (cons (list x y) b)
		   (cons (list y x) b)))
)  )	)

(defun do-binds	(binds x)
   "Replace all	bindings of variables in x"
   (cond
     ((null binds) x)
     ((and (var-p x)(assoc x binds))
      (do-binds	binds (second (assoc x binds))))
     ((atom x) x)
     (t	(cons (do-binds	binds (car x))
	      (do-binds	binds (cdr x))
)  ) )	)

(defun var-p (x) (header-p x #\?))

(defun unify (x	y)
  (let ((bindings nil))
       (do-binds (unify-binds x	y bindings) y)
) )


(defun top-level-prove (goals)
  "Prove the goals, and	print variables	readably."
  (let ((solutions (my-prove-all goals '(()) ))
	(vars	   (vars-in goals)) )
       (cond
	   ((null solutions) (format t "~&No."))
	   (t (dolist (x solutions)
		 (show-result vars x))
       )   )
  )
  (values)
)

(defun top-level-prove-one-by-one (goals)
  (my-prove-one-by-one `(,@goals ($ ,@(vars-in goals)))	'(()) )
  (format t "~&No.")
  (values)
)

(defun top-level-one-by-one-with-cut (goals)
  (one-by-one-with-cut `(,@goals ($ ,@(vars-in goals)))	'(()) )
  (format t "~&No.")
  (values)
)

(defun show-result (vars binds)
  "Print each variable with its binding."
  (if (null vars)
      (format t "~&Yes")
      (dolist (x vars)
	(format	t " ~a = ~a" x (do-binds binds x)
  )   )	)
  (format t ";~&")
)

(setf (get '$ 'rules) '$)
(setf (get '! 'rules) '!)

(clear-rules)

(fact (girl mary))
(fact (girl joy))
(fact (boy  john))
(fact (boy  tom))
(fact (pet  cat))
(fact (pet  dog))
(fact (love john mary))
(fact (like john dog))
(fact (like tom	 car))
(fact (like mary cat))

(rule (like joy	 ?x) if	(pet ?x))
(rule (love mary ?x) if	(boy ?x)(like ?x ?y)(pet ?y))
(rule (like ?x	car) if	(boy ?x))
(rule (like ?x	?y)  if	(boy ?x)(girl ?y))
(rule (like ?x	?y)  if	(girl ?x)(boy ?y))

;Occur-check!!
;(rule (like ?x	?y) if (like ?x	?z)(like ?y ?z))

(fact (smaller 0 3))
(fact (smaller 1 3))
(fact (smaller 2 3))
(fact (smaller 6 8))
(fact (smaller 6 9))

(rule (smaller ?x 6) if	(smaller ?x 3))
(rule (f ?x 0) if (smaller ?x 3) (!))
(rule (f ?x 2) if (smaller ?x 6) (!))
(rule (f ?x 4) if (smaller 6 ?x))

(rule (g ?x 0) if (smaller ?x 3))
(rule (g ?x 2) if (smaller ?x 6))
(rule (g ?x 4) if (smaller 6 ?x))

(fact (u 1)) (fact (u 2)) (fact	(u 3))
(fact (v 4)) (fact (v 5))
(fact (w 6)) (fact (w 7)) (fact	(w 8))

(rule (combin ?x ?y ?z)	if (u ?x)(v ?y)(w ?z))
(rule (combin-cut2 ?x ?y ?z) if	(u ?x)(v ?y)(!)(w ?z))
(rule (combin-cut1 ?x ?y ?z) if	(u ?x)(!)(v ?y)(w ?z))









;(defun	prove (goal binds)
;  (format t "~&Prove ~a" (get (get-index goal)	'rules))
;  (mapcan #'(lambda (rule)
;	       (let ((nr (rename-var rule)))
;		 (prove-all (cdr nr)
;			    (unify-binds (car goal) (car nr) binds)
;	     ) ) )
;	     (get (get-index goal) 'rules)
;) )

;(defun	prove-all (goals binds)
;  (cond
;	 ((null	binds) nil)
;	 ((null	goals) (list binds))
;	 (t (mapcan #'(lambda (one-solution)
;			(prove-all (rest goals)	one-solution))
;		    (prove goals binds)
;) )	 )  )