;;-*- Mode: LISP; Syntax: Common-lisp; Package: LOOM; Base: 10. -*-

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                                                                             ;
;  Copyright (c) 1988, 1995, 1999 by the University of Southern California    ;
;  All rights reserved.                                                       ;
;                                                                             ;
;  Permission to use, copy, modify, and distribute this software and its      ;
;  documentation in source and binary forms for non-commercial purposes       ;
;  and without fee is hereby granted, provided that this notice               ;
;  be reproduced in any copy or modification thereof, and that                ;
;  any documentation, advertising materials, and other materials related      ;
;  to such distribution and use acknowledge that the software was             ;
;  developed by the University of Southern California, Information            ;
;  Sciences Institute.  The name of the University may not be used to         ;
;  endorse or promote products derived from this software without             ;
;  specific prior written permission.                                         ;
;                                                                             ;
;  THE UNIVERSITY OF SOUTHERN CALIFORNIA MAKES NO REPRESENTATIONS ABOUT THE   ;
;  SUITABILITY OF THIS SOFTWARE FOR ANY PURPOSE.  THIS SOFTWARE IS PROVIDED   ;
;  "AS IS" AND WITHOUT ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING,          ;
;  WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND          ;
;  FITNESS FOR A PARTICULAR PURPOSE.                                          ;
;                                                                             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; PROPOSITIONS.LISP (TBOX)

(in-package "LOOM")

(export '())


  ;;
;;;;;; "create-proposition"
  ;;    

(defun create-proposition (name &key wff operator arguments truth-value)
  ;; Create a proposition and fill in its slots;
  ;; Assert the truth value "truth-value" and propagate any side-effects
  ;;    of this assertion;
  (let ((proposition (create name 'Proposition :creation-policy :clos-instance)))
    (setf (wff proposition) wff)
    (setf (proposition-operator proposition) operator)
    (setf (proposition-arguments proposition) arguments)
    (when truth-value
      (finalize-definitions)		; Needs to happen before truth value assertion.
      (assert-truth-value proposition truth-value))
    proposition ))


  ;;
;;;;;; "assert-truth-value"
  ;;

(defun assert-truth-value (proposition truthValue)
  ;; Assert that "proposition" has truth value "truthValue";
  ;; Propagate any side-effects that accompany this assertion;
  (let ((oldTruthValue (proposition-truth-value proposition)))
    (when (eq truthValue oldTruthValue)
      (return-from assert-truth-value proposition))
    (when oldTruthValue
      (retract-truth-value proposition truthValue))
    (setf (proposition-truth-value proposition) truthValue)
    (case (proposition-operator proposition)
      (IMPLIES (assert-implies-proposition proposition))
;      (OR (assert-or-proposition proposition))
;      (NOT (assert-not-proposition proposition))
;     (AND (assert-and-proposition proposition))
;     (otherwise (assert-literal-proposition proposition))
      )
    proposition ))

(defun assert-implies-proposition (proposition)
  ;; Install an implication rule into the concept or relation hierarchy;
  (let ((antecedent (first (proposition-arguments proposition)))
        (consequent (second (proposition-arguments proposition))))
    (cond
     ((or (concept-p antecedent)
          (concept-p consequent))
      (define-concept
        :is (if (concept-p antecedent) antecedent `(and ,antecedent))
        :implies consequent
        :characteristics :system-defined))
     ((relation-p consequent)
      (define-relation
        :is consequent
        :antecedents antecedent
        :characteristics :system-defined))
     (t
      (define-relation
        :is antecedent
        :implies consequent
        :characteristics :system-defined))) ))


  ;;
;;;;;; "retract-truth-value"
  ;;

(defun retract-truth-value (proposition truthValue)
  ;; Assert that "proposition" has truth value "truthValue";
  ;; Propagate any side-effects that accompany this assertion;
  (let ((oldTruthValue (proposition-truth-value proposition)))
    (when (eq truthValue oldTruthValue)
      (return-from retract-truth-value proposition))
;    (case (proposition-operator proposition)
;      (IMPLIES (retract-implies-proposition proposition))
;      (OR (retract-or-proposition proposition))
;      (NOT (retract-not-proposition proposition))
;     (AND (retract-and-proposition proposition))
;     (otherwise (retract-literal-proposition proposition))
;      )
    proposition ))
