;;; -*- 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.                                          ;
;                                                                             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; DISJOINTNESS.LISP (TBOX)

(in-package "LOOM")

;;; This file contains procedures which operate on coverings and
;;;    disjoint-coverings

  ;;
;;;;;; Creating and destroying coverings
  ;;

(defun form-name-of-covering (self)
  ;; Helping function for "define-covering" and "define-disjoint-covering";
  ;; Generate a new covering name for "self" with a suffix numbered
  ;;    one higher than the names of covers already possessed by "self";
  ;; If the name of "self" is FOO, then the covering name has the form
  ;;    "FOO-k"
  (let ((count (1+ (length (disjoint-coverings self))))
	(name (name self)))
    (symbol-append (name "-" (format nil "~S" count)) 
		   (symbol-package name)) ))

(defun compute-concept-from-cover-name (coverName referrer)
  ;; Return the concept identified by "coverName"
  (let ((conceptName (remove-suffix coverName)))
    (case (concept-or-relation referrer)
      (:relation
	(eval-relation-id conceptName))
      (otherwise
	(eval-concept-id conceptName))) ))



  ;;
;;;;;; Disjoint-covering
  ;;

(defun define-disjoint-covering (coveredConcept coverComponents)
  ;; Define a disjoint-covering stating that the concepts in "coverComponents"
  ;;    form an exhaustive partition of the concept "coveredConcept";
  ;; Use the same data structures as partitions;
  (let ((partitionName (form-partition-name coveredConcept)))
    (define-partition
      coveredConcept partitionName coverComponents :exhaustive-p t) ))

(defun undefine-disjoint-covering (coveredConcept coverName)
  ;; Remove the disjoint-covering "coverName" owned by "coveredConcept"
  ;;    from the slot "(disjoint-coverings coveredConcept)", and
  ;;    also remove a record of membership in the covering with each
  ;;    component concept;
  ;; TO DO: FIX "delf" FOR ASSOCIATION LISTS;
  (let ((membership (assoc coverName (disjoint-coverings coveredConcept))))
    (loop for component in (cdr membership)
	 do
	 (delete-disjoint-covering-link coverName coveredConcept component))
;    (delf (disjoint-coverings coveredConcept) coverName)
    (setf (disjoint-coverings coveredConcept)
	  (delete membership (disjoint-coverings coveredConcept) :test #'eq)) ))

(defun add-disjoint-covering-link (coverName coveredConcept component)
  ;; Add the component "component" to the disjoint covering with name
  ;;    "coverName" at the concept "coveredConcept" (when necessary,
  ;;    create the new covering list);
  ;; Also, create a disjoint-covering-membership for the
  ;;    covering "coverName" at the concept "component", and establish a
  ;;    dependency on "coveredConcept";
#L:trace-cover (trace-values "add-disjoint-covering-link:" coverName component)
  (let ((matchingMembership
	  (assoc coverName (disjoint-coverings coveredConcept))))
    (cond
      (matchingMembership
       (setf (cdr matchingMembership)
	     (pushnew component (cdr matchingMembership))))
      (t
       (addf (disjoint-coverings coveredConcept)
	     (list coverName component))))
    (add-disjoint-covering-membership-component
      component coverName component) ))

(defun add-disjoint-covering-membership-component (self coverName component)
  ;; If "self" has no local membership with the same cover-name as
  ;;    "coverName", add "(list coverName component)" to
  ;;    "self"s list of disjoint covering memberships;
  ;; Otherwise, add "component" to the matching local membership 
  (let ((matchingLocalMembership
	  (assoc coverName (disjoint-covering-memberships self))))
    (cond
      (matchingLocalMembership
       (setf (cdr matchingLocalMembership)
	     (pushnew component (cdr matchingLocalMembership))))
      (t
       (addf (disjoint-covering-memberships self)
	     (list coverName component)))) ))

(defun delete-disjoint-covering-link (coverName coveredConcept component)
  ;; Remove a disjoint-covering component from the covering "coverName"
  ;;    belonging to "coveredConcept", remove "component" from the
  ;;    disjoint-covering membership at "component", and eliminate
  ;;    the dependency of "component" on "coveredConcept";
  (let ((membership (assoc coverName (disjoint-coverings coveredConcept))))
    (setf (cdr membership)
	  (delete component (cdr membership)))
    (when (null (cdr membership))
	(delf (disjoint-coverings coveredConcept) coverName))
    (delete-disjoint-covering-membership-component
      component coverName component) ))

(defun delete-disjoint-covering-membership-component (self coverName component)
  ;; Remove "component" from the disjoint-covering membership named
  ;;    "coverName" at "self";
  ;; If its the last component, remove the membership;
  (let ((membership (assoc coverName
			   (disjoint-covering-memberships self))))
    (when membership
      (setf (cdr membership)
	    (delete component (cdr membership)))
      (when (null (cdr membership))
	(delf (disjoint-covering-memberships self) coverName))) ))

(defun delete-inherited-covering-membership-components (self)
  ;; Remove all components from disjoint-covering-memberships
  ;;    belonging to "self" except components equal to "self"
  (loop for tail on (disjoint-covering-memberships self)
       do
       (let ((covering (car tail)))
	 (cond
	   ((member self (cdr covering))
	    (setf (cdr covering) (list self)))
	   (t
	    (setf (car tail) nil)))))
  (setf (disjoint-covering-memberships self)
	(delete nil (disjoint-covering-memberships self))) )

  ;;
;;;;;; Completion of coverings
  ;;


;; Not called from anywhere.
(defun install-disjoint-covering-memberships (self)
  ;; Verify that the covering-memberships directly defined for "self"
  ;;    have owners which subsume self;
  ;; Inherit covering-memberships from the parents of "self";
  ;; Detect if "self" is incoherent, and if so, propagate the incoherence
  ;;    to the dependents of "self";
  (loop for membership in (disjoint-covering-memberships self)
       do
       (let ((coveredConcept
	       (compute-concept-from-cover-name 
		 (car membership) self)))
	 (unless (and (neq self coveredConcept)
		      (subconcept-p self coveredConcept))
	   (warn "Concept ~S belonging to the disjoint-covering ~S does not~%~
                   specialize the covered concept ~S~%"
		 self (car membership) coveredConcept))))
  ;; inherit disjoint-covering-memberships:
  (loop for super in (super-concepts self)
       do
       (loop for inheritedMembership in (disjoint-covering-memberships super)
	    do 
	    (loop for component in (cdr inheritedMembership)
		 do (add-disjoint-covering-membership-component
		      self (car inheritedMembership) component))))
  ;; detect incoherence:
  (let ((badMembership
	  (loop for membership in (disjoint-covering-memberships self)
	       when (cddr membership)
               return membership)))
    (when (and badMembership
	       (not (incoherent-p self)))
      (warn-of-incoherent-concept self badMembership)
      (mark-as-incoherent self))) )


#|
 
(initialize-network)
(defconcept a :p
  (:axioms (:disjoint-covering b c) (:disjoint-covering b g)))

(defconcept b (:s a) :p)
(defconcept c (:s a) :p)
(defconcept d (:s b c))
(defconcept e (:res r (:vr d)))
(incoherent-p (fc e))

(defconcept f :p
  (:axioms (:res r (:vr d))))
(incoherent-p (fc f))

|#


#|

IDEAS FOR DISJOINTNESS SYNTAX:

(defprimc Animal)
(define-disjoint-primitive-c Dog (Animal-Species) Animal)

(defconcept Animal
  :partition (Male-Animal Female-Animal)
  :disjointness-index Animal-Species)
(defconcept Horse
  :is-primitive (:and Animal (:disjoint-member Animal-Species)))
		      
|#
