; ----------------------------SKOLEMIZATION-----------------------------

(defun var-kind (var) (get var 'var-kind))

(defun interest-variable (x)
    (and (symbolp x) (eq (var-kind x) :variable)))

(defun conclusion-variable (x)
    (and (symbolp x) (eq (var-kind x) :variable)))

(defun make-interest-variable ()
    (let ((var (gensym "^@y")))
       (setf (get var 'var-kind) :variable)
       (setf (get var 'i-var) t)
       var))

(defun make-conclusion-variable ()
    (let ((var (gensym "x")))
       (setf (get var 'var-kind) :variable)
       var))

;; This converts interest-variables into conclusion-variables in formula.
(defunction convert-interest-variables (formula variables)
    (let* ((vars nil)
              (substitution
                (mapcar #'(lambda (x)
                                     (let ((var (make-conclusion-variable)))
                                       (push var vars)
                                       (cons x var)))
                               variables)))
      (values (sublis substitution formula) vars)))

;; This converts conclusion-variables into interest-variables in formula.
(defunction convert-conclusion-variables (formula variables)
    (let* ((vars nil)
              (substitution
                (mapcar #'(lambda (x)
                                     (let ((var (make-interest-variable)))
                                       (push var vars)
                                       (cons x var)))
                               variables)))
     ; (setf substitution (mapcar #'(lambda (x) (cons (cdr x) (car x))) substitution))
      (values (sublis substitution formula) vars substitution)))

;; This converts conclusion-variables into interest-variables in a unifier
(defunction convert-unifier-variables (unifier variables)
   ; (when (> *gensym-counter* 78) (setf u unifier v variables) (break))
    (let ((u1 (mem1 unifier)) (u2 (mem2 unifier)))
      (if (eq u2 t) unifier
           (let* ((vars nil)
                     (substitution
                       (mapcar #'(lambda (x)
                                            (let ((var (make-interest-variable)))
                                              (push var vars)
                                              (cons x var)))
                                      variables)))
             (list u1 (mapcar #'(lambda (x) (cons (car x) (sublis substitution (cdr x)))) u2))))))

#| These are changed to allow conses in formulas. |#
(defunction formula-node-variables (p)
    (cond ((and (symbolp p) (eq (get p 'var-kind) :variable)) (list p))
              ((and (listp p) p)
                (union (formula-node-variables (car p)) (formula-node-variables (cdr p))))))

(defun make-skolem-e-function ()
    (let ((fun (gensym "@y")))
       (setf (get fun 'var-kind) :skolem-function)
       fun))

(defun make-skolem-i-function ()
    (let ((fun (gensym "^x")))
       (setf (get fun 'var-kind) :skolem-function)
       fun))

(defun make-skolem-e-constant ()
    (let ((fun (gensym "@y")))
       (setf (get fun 'var-kind) :skolem-function)
       fun))

(defun make-skolem-i-constant ()
    (let ((fun (gensym "^x")))
       (setf (get fun 'var-kind) :skolem-function)
       fun))

(defun skolem-function (x)
    (and (symbolp x) (eq (get x 'var-kind) :skolem-function)))

(defun skolem-functions (p)
    (cond ((symbolp p)
                 (if (skolem-function p) (list p)))
                ((stringp p) nil)
                ((listp p) (unionmapcar= #'skolem-functions p))))

#| P contains no skolem constants, functions, or variables. |#
(defunction skolem-free (P)
    (cond ((symbolp P)
                 (let ((kind (get P 'var-kind)))
                    (and (not (eq kind :variable)) (not (eq kind :skolem-function)))))
                ((listp P) (every #'skolem-free P))
                (t t)))