;;; A strucure copying Prolog interpreter originally written in
;;; Maclisp by Mats Carlsson, UPMAIL, Uppsala University, 1983.
;;;
;;; Written for the Symbolics LISP Machine by Andy Ylikoski 06/11/85
;;; at Nokia Electronics R & D; remodified for Maclisp by AY
;;; 10/05/85. 
;;;
;;; Converted to Common LISP by Andy Ylikoski 12/13/2009 while
;;; carrying out my PhD studies.
;;;
;;;
;;; Syntax:
;;; 
;;; variables are symbols beginning with ?, as
;;;             ?PLANNING-RESTRICTIONS
;;;
;;; terms and predicates are expressed as lists (<functor> . <args>),
;;; as 
;;;             (FATHER ESKO ANTTI)
;;;
;;; assertions are lists (<consequent> . <antecedents>), as
;;;             ((FATHER ?X ?Y) (PARENT ?X ?Y) (MALE ?X))
;;;
;;; top level functions:
;;; (yaq)                       top level read-prove-print loop
;;; (defpredicate <name> . <assertions>)
;;;                             defines predicates
;;;
;;; builtin predicates:
;;; (cut)                       notorious control primitive
;;; (call ?goal)                Tries to prove ?goal.
;;; (bagof ?t ?goal ?b)         ?b is a bag of instances of
;;;                             ?t such that they satisfy ?goal.
;;; (lisp-predicate ?lispform)  ?lispform is evaluated; succeed iff
;;;                             it returns non-NIL.
;;; (lisp-command ?lispform)    ?lispform is evaluated for side
;;;                             effects only; return value ignored.
;;; (lisp-value ?var ?lispform)  ?lispform is evaluated and the return
;;;                             value unified with ?var.
;;; (cl ?clause)                ?clause is instantiated as an
;;;                             assertion in the knowlege base.
;;; (addcl ?clause)             Asserts ?clause into the knowledge
;;;                             base. 
;;; (addcl ?clause ?n)          Asserts ?clause after the ?n'th clause
;;;                             of the procedure it belongs to.
;;; (delcl ?clause)             Retracts clauses matching ?clause.
;;;                             Backtracks.
;;; (delcl ?predicate ?n)       Retracts the ?n'th clause of
;;;                             ?predicate. 
;;;
;;; A number of modifications to convert the program to Common LISP.
;;; Added the (halt) predicate for a better environment for developing
;;; LISP-based Prolog programs.
;;;
;;; This version does not use the the condition system to exit out of
;;; the read-prove-print loop -- because it is written for the GNU
;;; Common LISP.

;;; The variable internal-time-units-per-second gives the number of
;;; "ticks" of the clock per a second of real time.
;;;
;;; The function (get-internal-run-time) (no args) returns as an
;;; integer the current run time in internal time units.  The
;;; difference between two consecutive calls is the used run time.

(defun ticks-to-msec (ticks)
  (* 1000.0 (/ (float ticks) internal-time-units-per-second)))



;;; Definition of MEMQ is missing in Common LISP.

(defun memq (x set)
  (member x set))

;;; So is DELQ.

(defun delq (x set)
  (delete x set))

;;;
;;; YAQ code begins.
;;;



;;;(proclaim '(inline dereference yaq-reset resolve
;;;                   try-assrts try-assertion))

(defvar *cells* () "List of cells used while instantiating.")

(defvar *variables* () "List of all syntactic variables seen.")

(defvar *trail* () "The reset stack to record all variable bindings to
  know what to do upon backtrack")

(defvar *inferences* 0 "Inference counter")

(defvar *failure* 32767 "Just a large integer, used in conjunction
  with the (cut)")

;;; (cell) creates an empty variable cell -- a cons with its CDR
;;; pointing to itself and the atom |var| in the CAR
;;;(proclaim '(inline cell))
(defun cell()
  (let ((x (cons '|var| nil)))
       (rplacd x x)))

;;; (defun consp (x) ...) is unnecessary -- it is there in CLTL2

;;; variables are unified by setting the CDR of the var cell point to
;;; the variable to unify to, and recording this unification to
;;; *trail*

;;;(proclaim '(inline unify-variable))
(defun unify-variable (x y) (progn (push x *trail*) (rplacd x y)))


;;; assrts gets all clauses which may be used to prove a given
;;; goal

;;;(proclaim '(inline assrts))
(defun assrts (goal) (get (car goal) :assrts))


;;; each assertion in the database is represented as a pair of
;;; functions such that the CAR of the assertion constructs its head
;;; and the CDR constructs its body

;;;(proclaim '(inline head body))
(defun head (assertion) (funcall (car assertion)))
(defun body (assertion) (funcall (cdr assertion)))


;;; invoke evaluates continuations

;;;(proclaim '(inline invoke))
(defun invoke (x) (apply (car x) (cdr x)))

;;; define internal functions

(defmacro defbuiltin (name &rest body)
  (let ((g (intern (format nil "~A-builtin-function" name))))
    `(progn 'compile
	    (defun ,g (goal continuation depth)
	      ,@body)
	    (setf (get ',name :assrts) '(:builtin . ,g)))))



;;; instatiate generates a copy of a where unbound variables are
;;; handled by generator

(defun instantiate (x generator)
  (let (*cells*)
    (instantiate-1 x generator)))

;;; Oh, golden ol' DEFUN,
;;; you golden oldie fun!

(defun instantiate-1 (x generator)
  (cond ((syntactic-variable-p x)
	 (cond ((assq x *cells*) (cdr (assq *cells*)))
	       (t (let ((c (funcall generator x)))
		    (push (cons x c) *cells*) c))))
	((consp x) (cons (instantiate-1 (dereference (car x))
                                         generator)
			 (instantiate-1 (dereference (car x))
                                         generator)))
	(t x)))



;;; this generator merely makes a new value cell

(defun copycell (ignore)
  (cell))


;;; this generator creates an uninterned symbol named ?0, ?1, ?2, ...

(defun ?cell (ignore)
  (make-symbol (format nil "~A~A" #\? (code-char 
				       (+ (char-code #\0) (length *cells*))))))





;;;                  The kernel of the interpreter follows



;;; dereference follows a chain of linked variables

(defun dereference (x)
  (cond ((syntactic-variable-p x)
	 (cond ((eq x (cdr x)) x)
	       (t (dereference (cdr x)))))
	(t x)))



;;; Unify two S-expressions

(defun unify (x y)
  (cond ((syntactic-variable-p x) (unify-variable x y)) ; Is x a variable?
	                                      ; Unify with anything
	((syntactic-variable-p y) (unify-variable y x)) ; Is y a variable?
	((consp x)                            ; x and y are general
	 (and (consp y)                       ; expressions:
                                              ; recurse
	      (unify (dereference (car x)) (dereference (car y)))
	      (unify (dereference (cdr x)) (dereference (cdr y)))))
	((equal x y))))                       ; Constants unify
                                              ; whenever EQUAL


;;; Pop all variables up to mark off *trail* and make them empty
;;; variable cells.  Used to undo variable bindings at backrack.

(defun yaq-reset (mark)
  (cond ((not (eq mark *trail*))
	 (let ((cell (pop *trail*)))
	   (rplacd cell cell)
	   (yaq-reset mark)))))

;;; The inference engine.

(defun prove (goals continuation depth)
  (cond ((cdr goals)                          ; Several goals?
	 (resolve (car goals)
		  `(prove ,(cdr goals) ,continuation ,depth)
                                              ; The continuation:
                                              ; prove the rest of the
                                              ; goals
		  depth))
	(goals                                ; One goal?
	 (resolve (car goals)
		  continuation
		  depth))
	(t                                    ; No goals left?
	 (invoke continuation))))


(defun resolve (goal continuation depth)
  (incf *inferences*)                         ; Simple way to count
  (let ((assrts (assrts goal)))
    (cond ((eq :builtin (car assrts))
	   (funcall (cdr assrts) goal continuation depth))
	  (t
	   (try-assrts goal assrts *trail* continuation
			   depth)))))

(defun try-assrts (goal assrts mark continuation depth)
  (cond ((cdr assrts)                     ; Several assrts?
	 (let ((msg (try-assertion goal (car assrts) continuation
				   depth)))
	   (cond ((> msg depth)
		  (yaq-reset mark)
		  (try-assrts goal
				  (cdr assrts)
				  mark
				  continuation
				  depth))
		 ((= msg depth)
		  *failure*)
		 (t msg))))
	(assrts                           ; One assertion?
	 (try-assertion goal (car assrts) continuation depth))
	(t                                    ; No useful assrts
	 *failure*)))

(defun try-assertion (goal assertion continuation depth)
  (cond ((unify (cdr goal) (funcall (car assertion))) ;Is this
                                              ; assertion usable
                                              ; head unifies with
					      ; goal?
	 (prove (funcall (cdr assertion)) continuation (+ 1 depth)))
                                              ; Yes it was
	                                      ; Prove the body.
	(t                                    ; Wasn't useful.
	 *failure*)))



;;; Here come a list of builtin primitives.
;;; The Maclisp version has builtin primitives such as
;;; |cl-delcl|, whereas the Franzl version calls them
;;; cl-delcl0 etc.  Followed this convention in the
;;; Common LISP version.  AY 12/14/2009.

(defbuiltin cl-delcl0
  (let* ((clause (dereference (cadr goal)))
	 (delcl-p (dereference (caddr goal)))
	 (name (caar clause)))
    (cl-delcl-clauses0 clause
		       delcl-p
		       name
		       *trail*
		       (assrts (car clause))
		       continuation
		       depth)))


(defun cl-delcl-clauses0 (clause delcl-p name mark assrts
				 continuation depth)
  (cond ((cdr assrts)
	 (let ((msg
		(cl-delcl-clause0 clause
				  delcl-p
				  name
				  (car assrts)
				  continuation)))
	   (cond ((> msg depth)
		  (yaq-reset mark)
		  (cl-delcl-clauses0 clause
				     delcl-p
				     name
				     mark
				     (cdr assrts)
				     continuation
				     depth))
		 ((= msg depth)
		  *failure*)
		 (t msg))))
	(assrts
	 (cl-delcl-clause0 clause
			   delcl-p
			   (car assrts)
			   continuation))
	(t
	 *failure*)))


(defun cl-delcl-clause0 (clause delcl-p name assertion continuation)
  (cond ((and (unify (cdar clause) (head assertion))
	      (unify (cdr clause) (body assertion)))

	 (cond (delcl-p              ; delcl-p determines 
                                     ; whether really to delete
		(setf (get name :assrts)
		      (delq assertion (get name :assrts)))))
	 (invoke continuation))
	(t
	 *failure*)))


(defbuiltin delcl-1-0
  (let* ((name (dereference (cadr goal)))
	 (n (dereference (caddr goal)))
	 (assrts (get name :assrts)))

    (setf (get name :assrts)
	  (delq (nth (- n 1) assrts) assrts))
    (invoke continuation)))


(defbuiltin addcl0
  (let* ((clause (instantiate (dereference (cadr goal)) '?cell))
	 (n (dereference (caddr goal)))
	 (name (caar clause))
	 (save (get name :assrts)))
    (eval `(defpredicate ,name ,clause))
    (cond ((and (numberp n) (nthcdr n save))
	   (let ((x (nthcdr n save)))
	     (rplacd x (cons (car x) (cdr x)))
	     (rplaca x (car (get name :assrts)))
	     (setf (get name :assrts) save)))
	  (t (setf (get name :assrts)
		      (nconc save (get name :assrts)))))
    (invoke continuation)))


(defbuiltin bagof
  (let ((mark *trail*)
	(reslist (list ()))
	((?t ?p ?b) (cdr goal)))
    (resolve (dereference ?p) `(bagof-aux ,?t ,reslist) depth)
    (yaq-reset mark)
    (cond ((unify (dereference ?b) (nreverse (car reslist)))
	   (invoke continuation))
	  (t *failure*))))

(defun bagof-aux (term reslist)
  (push (instantiate (dereference term) 'copycell) (car reslist))
  *failure*)


;;; The famous control primitives.

(defbuiltin call
 (resolve (dereference (cadr goal)) continuation depth))

(defbuiltin cut (invoke continuation) (- depth 1))

;;; The procedural attachment.

(defbuiltin lisp-predicate
  (cond ((eval (instantiate (cadr goal) 'prog1))
	 (invoke continuation))
	(t *failure*)))

(defbuiltin lisp-predcate-?vars
  (cond ((eval (instantiate (cadr goal) '?cell))
	 (invoke continuation))
	(t *failure*)))

(defbuiltin halt
  (throw 'halt-yaq nil))

;;; The DEFPREDICATE macro and the deniftion of the top level --
;;; the (yaq) function.

;;; Variables are recognized by their first char being a '?'
(defmacro syntactic-variable-p (x)
  `(and (symbolp ,x) (equal '#\? (aref (format nil "~A" ,x) 0)))) ;
								  ; the
								  ; zeroth
								  ; character
								  ; is
								  ; the
								  ; first
								  ; one.......



;;; This begins an (eval-when ....) around a number of DEFUN's
;;; ... DEFPREDICATE calls some functions which have to be defined
;;; at compile time

(eval-when (compile eval load)

;;; VARIABLES-AND-CONSTRUCTOR returns variables occurring in x and a
;;; form that will create x

(defun variables-and-constructor (x)
  (let* ((*variables*)
	 (code (constructor x)))
    (list (nreverse *variables*) code)))

;;; CONSTRUCTOR returns code that will create x
(defun constructor (x)
  (cond ((equal x '?) (cell))
	((syntactic-variable-p x)
	 (or (memq x *variables*) (push x *variables*))
	 x)
	((ground x) `(quote ,x))
	(t `(cons ,(constructor (car x)) ,(constructor (cdr x))))))

;;; GROUND determines whether x is a ground instance
(defun ground (x)
  (cond ((syntactic-variable-p x) nil)     ; variables R not ground
	((atom x) t)                       ; but constants R
	((ground (car x)) (ground (cdr x)))))
                                           ; recurse on CAR & CDR


(defun diffq (x y)
  (mapcan #'(lambda (x1) (and (not (memq x1 y)) (list x1)))
	  x))

;;; ***** MEMQ is undefined in Common LISP *****

(defun make-head-function-name (pred-name)
 (intern (format nil "~A-head-function-~A" pred-name (gensym))))

(defun make-body-function-name (pred-name)
  (intern (format nil "~A-body-function-~A" pred-name (gensym))))

)         ; end of (eval-when .....)


;;; The main user interface: the DEFPREDICATE macro.

(defmacro defpredicate (name &rest assrts)
  `(let ((toplist nil))
     (progn
       (print "Here we print the toplist")
       (print toplist)
       ;; still to do: the compile calls
       ,@(mapcan
	  #'(lambda (a)
	      (destructuring-bind (headvars headcode)
				  (variables-and-constructor (cdar a))
  	        (destructuring-bind (bodyvars bodycode)
				   (variables-and-constructor (cdr a))
	          (let ((head-name (make-head-function-name name))
			(body-name (make-body-function-name name)))
		    (print head-name)
		    (print body-name)
		    (print toplist)
		    (push (cons head-name body-name) toplist)
		    (eval `(defun ,head-name ()
			     ,@(mapcar #'(lambda (v)  ; vars to empty cells
					   `(setf ,v (cell))) headvars)
			     ,headcode))  ; code to generate head
		    (eval `(defun ,body-name ()
			     ,@(mapcar #'(lambda (v)
					   `(setf ,v (cell))) ; all vars
				       (diffq bodyvars headvars))
					; except those
					; among the 
					; head vars to
					; cell
			     ,bodycode))))))  ; code to generate body
	  assrts)  ; MAPCAN this treatment over all assrts
       (setf (get ',name :assrts) ,(nreverse toplist)))))

;;; Still to do: store pretty-printable representation under :pp-pred
;;; property of the symbol name for the (listing ?x) predicate


;;; The main read-prove-print loop, with an exit to LISP via the
;;; HALT-EXCEPTION.

(defun yaq()
  (catch 'halt-yaq
    (yaq-read-prove-print)))

(defun yaq-read-prove-print ()
  (do ((mark *trail*)) (()) ; loop until THROW'n out of loop
      (format t "~%| ?- ")
      (let* ((sexpr (read))) ; Input goal to prove & print
	(destructuring-bind (sexprvars sexprcode)
	    (variables-and-constructor sexpr)
	  (let
	      ((cells
	       (mapcar #'(lambda (x) (set x (cell))) sexprvars)))
	   (unwind-protect
	       (prove
		`(,(eval sexprcode)       ; main goal(s)
		  (lisp-predicate-?vars   ; aux predicate to output &
		   (display ',sexprvars   ; initiate backtracking
			    ',cells
			    ',*inferences*
			    ',(get-internal-run-time))))
		'(+)                    ; this continuation will return
				      ; 0 after all subgoals are done,
				      ; thus causing a return to level
				      ; 0
		0)                    ; depth of top level = zero
	     (yaq-reset mark)))))))

(defun display (names cells inf runtim)
  (let* ((curr-time (get-internal-run-time))
	 (elaps-time (- curr-time runtim))
	 (dt (ticks-to-msec elaps-time)))
    (format t "~%Theorem proving took ~A milliseconds."
	    (fix dt))
    (format t "~%~A inferences were executed."
	    (- *inferences* inf))
    (mapc #'(lambda (n c)
	      (format t "~%~S = " n)
	      (pprint c))
	  names cells)
    (progn (format t "~%Ok ? ")
	   (y-or-n-p))))     ; if this returns NIL, the
                             ; function (display ...) will return NIL,
			     ; and then the goal lisp-predicate-?vars
			     ; will fail, thus initiating
			     ; user-controlled backtracking
			     ; (ie. analogous to giving ";" to the
			     ; Edinbugrh Prolog.)


;;; utility predicates

(defpredicate lisp-command
  ((lisp-command ?X)
   (lisp-predicate (progn ?X t))))

(defpredicate lisp-value
  ((lisp-value ?X ?Y)
   (lisp-predicate (unify '?X ?Y))))

(defpredicate cl
  ((cl ?cl)
   (cl-delcl0 ?cl nil)))

(defpredicate addcl
  ((addcl ?cl)
   (addcl0 ?cl))
  ((addcl ?cl ?n)
   (addcl0 ?cl ?n)))    ; index origin 1

(defpredicate delcl
  ((delcl ?cl)
   (cl-delcl0 ?cl t))
  ((delcl ?pred ?n)
   (delcl-1-0 ?pred ?n)))

;;; Some useful predicates

(defpredicate =
  ((= ?X ?X)))

(defpredicate not
  ((not ?p) (call ?p) (cut) (fail))  ; yes: (get 'fail :assrts) => NIL
  ((not ?p)))

;;; Arithmetic

(defpredicate <
  ((< ?a ?b) (lisp-predicate (< '?a '?b))))

(defpredicate >
  ((> ?a ?b) (lisp-predicate (> '?a '?b))))

(defpredicate >=
  ((>= ?a ?b) (> ?a ?b))
  ((>= ?a ?b) (= ?a ?b)))

(defpredicate =<
  ((=< ?a ?b) (< ?a ?b))
  ((=< ?a ?b) (= ?a ?b)))


;;; The following predicates have a syntax similar to the MRS:
;;; (<operation> <arguments, here two> <result>)

(defpredicate +
  ((+ ?a ?b ?result) (lisp-value ?result (+ '?a '?b))))

(defpredicate -
  ((- ?a ?b ?result) (lisp-value ?result (- '?a '?b))))

(defpredicate *
  ((* ?a ?b ?result) (lisp-value ?result (* '?a '?b))))

(defpredicate /
  ((/ ?a ?b ?result) (lisp-value ?result (/ '?a '?b))))