;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                    -*-
;;;; ---------------------------------------------------------------------
;;;; File name: term.lsp
;;;;    System: FIRE
;;;;    Author: Jesse Alama
;;;;   Created: December 4, 2001
;;;;   Purpose: Operators for terms (literal-polarity pairs)
;;;; ---------------------------------------------------------------------
;;;;  Modified: Wednesday, February 5, 2003 at 09:51:17 by forbus

(in-package :fire)

#|
Terms are elements of clauses.  Terms contain two pieces of information:
a "literal" (a formula), and a "polarity" (one of either :TRUE or :FALSE).
|#

(defconstant *pos-polarity-symbol* :true)
(defconstant *neg-polarity-symbol* :false)

;; Term construction

(defun make-term (literal polarity) (cons literal polarity))

(defun make-formula-from-term (term)
  (if (eq (term-polarity term) *neg-polarity-symbol*)
      (make-negation (term-literal term))
    (term-literal term)))

(defun make-negative-term (formula)
  (make-term formula *neg-polarity-symbol*))

(defun make-positive-term (formula)
  (make-term formula *pos-polarity-symbol*))

;; Accessing parts of terms

(defun term-operator (term)
  "The operator of TERM's literal.  It is an error to call
   this function when TERM's literal is not a formula."
  (formula-operator (term-literal term)))

(defun term-literal (term) (car term))

(defun term-polarity (term) (cdr term))


;; Useful operators for terms

(defun negate-term (term)
  (make-term (term-literal term)
	     (opposite-sign (term-polarity term))))

(defun opposite-sign (sign)
  (if (eq sign *pos-polarity-symbol*)
      *neg-polarity-symbol*
    *pos-polarity-symbol*))


;; Useful predicates

(defun equal-terms? (t1 t2)
  (and (equal (term-literal t1) (term-literal t2))
       (eq (term-polarity t1) (term-polarity t2))))

(defun positive-term? (term)
  (eq (term-polarity term) *pos-polarity-symbol*))

(defun negative-term? (term)
  (eq (term-polarity term) *neg-polarity-symbol*))

(defun term-has-operator-and-polarity? (term operator polarity)
  (when (equal polarity (term-polarity term))
    (let ((my-literal (term-literal term)))
      (unless (variable? my-literal)
	(let ((my-operator (formula-operator my-literal)))
	  (unless (variable? my-operator)
	    (equal operator my-operator)))))))