;; -*- Mode: Lisp; Package: LOOM; Syntax: COMMON-LISP; 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.                                          ;
;                                                                             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; RESOLVE.LISP (ABOX)

;;; Procedures for computing resolvents within a context.

(in-package "LOOM")

(export '(resolve))

;;; THIS IS A VERY CRUDE INITIAL VERSION.
;;;    TO DO: AVOID SCANNING *ALL* CONCEPTS, JUST SCAN THOSE VISIBLE
;;;       IN THE CURRENT CONTEXT.
;;;    QUESTION: WHAT IS THE SCOPE OF INSTANCES THAT WE SHOULD CONSIDER?

;;; LOW PRIORITY TO DO: FIGURE OUT HOW WE MIGHT TRUTH-MAINTAIN INFERENCES BASED
;;;    ON RESOLUTION (E.G., BY RECORDING CONFLICT BOMBS?).

(defun resolve ()
  ;; Augment the knowledge base with facts obtained by resolving
  ;;    disjunctive propositions;
  ;; Currently, we only handle disjunctive types;
  (let ((disjunctionConcepts
         (loop for c in (list-concepts)
               when (and (eq (defined-as c) :disjunction)
                         (not (subconcept-p c (loom-constant META-THING))))
               collect c))
        resolvedSomethingP)
    (loop
      do
      (setq resolvedSomethingP nil)
      (loop for dc in disjunctionConcepts
            do
            (loop for i in (generate-instances dc)
                  when (resolve-concept&instance-p dc i)
                  do (setq resolvedSomethingP t)))
      while resolvedSomethingP) ))

(defun list-concepts (&key local-p all-p)
  ;; Return a list of all concepts visible from the current context;
  ;; "local-p" returns only concepts defined in the current context;
  ;; "all-p" returns all concepts;
  ;; BUG: RIGHT NOW "all-p" IS STUCK ON;
  (retrieve ?c (concept ?c)) )

(defun resolve-concept&instance-p (disjunctionConcept ?instance)
  ;; Helping function for "resolve";
  ;; "?instance" satisfies the disjunctive concept "disjunctionConcept";
  ;; Try to prove that only one of the disjuncts in "disjunctionConcept"
  ;;    is compatible with "?instance".  If we succeed, assert that
  ;;    "?instance" satisfies that disjunct;
  (let ((compatibleDisjuncts nil)
        ?resolventConcept)
    ;; return failure if "?instance" belongs to one of the disjuncts:
    (when (loop for ?dc in (disjuncts disjunctionConcept)
                thereis (ask (?dc ?instance)))
      (return-from resolve-concept&instance-p nil))
    (loop for tail on (disjuncts disjunctionConcept)
          as ?dc = (car tail)
          do
          ;; *assume* the "?instance" satisfies "?dc" and see what happens:
          (tellm (?dc ?instance))
          (when (not (ask (incoherent ?instance)))
            (when (and (null (rest tail))
                       (null compatibleDisjuncts))
              ;; we got lucky -- the last disjunct was the first and only
              ;;    compatible disjunct -- return success (before retracting
              ;;    the last assumption):
              (return-from resolve-concept&instance-p t))
            (push ?dc compatibleDisjuncts))
          (forgetm (?dc ?instance))
          ;; return failure if "?instance" is compatible with at least
          ;;    two of the disjuncts:
          (when (rest compatibleDisjuncts)
            (return-from resolve-concept&instance-p nil)))
    (setq ?resolventConcept (first compatibleDisjuncts))
    ;; return t if "?instance" is compatible with exactly one disjunct:
    (when ?resolventConcept
      (tellm (?resolventConcept ?instance))
      t) ))
