;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: formulas.lsp
;;;;    System: FIRE
;;;;   Version: v1
;;;;    Author: Kenneth Forbus
;;;;   Created: December 5, 2001
;;;;   Purpose: Define operators and accessors for formulas
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Wednesday, May 26, 2004 at 11:38:24 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;; These utilities get called a lot, so it is important that they do
;; minimal consing.

(defun formula-variables (formula)
  (formula-variables1 formula nil))

(defun formula-variables1 (formula vars)
  (cond ((null formula) vars)
        ((variable? formula) 
         (if (member formula vars) vars
           (cons formula vars)))
        ((not (listp formula)) vars)
        ((introduces-local-variable? (car formula))
         (let ((local (cadr formula))
               (vars (formula-variables1 (third formula)
                                         vars)))
           (remove local vars)))                                     
        (t (formula-variables1
            (cdr formula)
            (formula-variables1 (car formula) vars)))))

;; Quantifier detection
(defmethod introduces-local-variable? ((pred t)) nil)
(defmethod introduces-local-variable? ((pred (eql 'data::forAll))) t)
(defmethod introduces-local-variable? ((pred (eql 'data::thereExists))) t)
(defmethod introduces-local-variable? ((pred (eql 'data::TheSetOf))) t)
(defmethod introduces-local-variable? ((pred (eql 'data::TheClosedRetrievalSetOf))) t)

(defun ground-formula? (formula) ;; Assumed to be a formula
  (cond ((null formula) t)
        ((variable? formula) nil)
        ((not (listp formula)) t)
        (t (and (ground-formula? (car formula))
                (ground-formula? (cdr formula))))))

(defun contains-term? (term formula)
  (cond ((equal term formula) t)
        ((null formula) nil)
        ((not (consp formula)) nil)
        (t (or (contains-term? term (car formula))
               (contains-term? term (cdr formula))))))

(defun uniquize-variables (formula)
  (let ((substitutions (mapcar #'(lambda (var) (cons var (gensym "?")))
                         (formula-variables formula))))
    ;; ******** This will not be correct for nested logically quantified
    ;; ******** statements where variable shadowing can occur.
    (values (sublis substitutions formula) substitutions)))

(defun uniquize-variables2 (formula vars)
  ;; vars is guarenteed to be the set of variables in the formula.
  ;; Saves a bit of time when dealing with the chainer.
  ;; (Is the space in the chainer worth it?  An empirical
  ;;  question.)
  (let ((substitutions (mapcar #'(lambda (var) (cons var (gensym "?")))
                         vars)))
    (values (sublis substitutions formula) substitutions)))

(defun bindings-equal? (bl1 bl2 &key (equality #'equal))
  ;; Returns t iff bl1 and bl2 have the same
  ;; variables bound to the same values.
  ;; We offer the option of an equality procedure parameter
  ;; in case floats become an issue.
  ;; N.B. We do not assume canonical order in binding lists
  ;; Might be worth it, but that's an empirical question
  (and (listp bl1)
       (listp bl2)
       (every 'consp bl1)
       (every 'consp bl2)
       (bindings-equal?-raw bl1 bl2 equality)))

(defun bindings-equal?-raw (bl1 bl2 equality)
  ;; Assumes all format checking already completed
  (and (= (length bl1) (length bl2))
       (same-elements-in-equal-length-binding-lists? bl1 bl2 :test equality)))

(defun same-elements-in-equal-length-binding-lists? (l1 l2 &key (test #'equal))
  ;; By stipulation these are both lists and have the same length.
  ;; We further assume no duplicates (these are binding lists, recall)
  (every #'(lambda (e1) (member e1 l2 :test test)) l1))

(defun invert-bindings (alist)
  (mapcar #'(lambda (entry) (cons (cdr entry) (car entry)))
    alist))

(defun simplify-bindings (binding-list)
  ;; Snaps variable chains
  (mapcar #'(lambda (pair)
              (cons (car pair)
                    (recursive-lookup (car pair) binding-list nil)))
    binding-list))

(defun recursive-lookup (var binding-list so-far)
  ;; Avoid infinite loops on binding lists with loops.
  ;; There shouldn't be any, but this is defensive programming.
  (cond ((member var so-far :test 'equal) var) 
        ((variable? var)
         (let ((entry (assoc var binding-list)))
           (cond (entry 
                  (recursive-lookup (cdr entry) binding-list
                                    (cons var so-far)))
                 (t var))))
        ((not (consp var)) var)
        ((ground-formula? var) var)
        (t (cons (recursive-lookup (car var) binding-list
                                   (cons var so-far))
                 (recursive-lookup (cdr var) binding-list
                                   (cons var so-far))))))

(defun variant? (f1 f2)
  ;; t iff f1 and f2 are the same, modulo names of variables
  (let ((result (catch 'variant-failure 
                       (variant1 f1 f2 nil))))
    (if (eq result :loser) nil t)))

(defun variant1 (f1 f2 bindings)
  (cond ((null f1)
         (cond ((null f2) bindings)
               (t (throw 'variant-failure :loser))))
        ((null f2) (throw 'variant-failure :loser))
        ((variable? f1)
         (cond ((variable? f2)
                (let ((entry (assoc f1 bindings)))
                  (cond (entry
                         (if (eq (cdr entry) f2) bindings
                           (throw 'variant-failure :loser)))
                        (t (let ((other (rassoc f2 bindings)))
                             (cond (other ;; Already bound to something else
                                    (throw 'variant-failure :loser))
                                   (t (cons (cons f1 f2) bindings))))))))
               (t (throw 'variant-failure :loser))))
        ((variable? f2) (throw 'variant-failure :loser))
        ((or (not (consp f1)) (not (consp f2)))
         (if (equal f1 f2) bindings
           (throw 'variant-failure :loser)))
        (t (variant1 (cdr f1) (cdr f2)
                     (variant1 (car f1) (car f2) bindings)))))