;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: domain-theory.lsp
;;;;    System: FIRE qp-source
;;;;   Version: 2.0
;;;;    Author: Jin Yan
;;;;   Created: April 23, 2003 12:23:11
;;;;   Purpose: Extracting GIZMO domain theory from FIRE facts.
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Thursday, January 15, 2004 at 14:04:35 by jinyan
;;;; ---------------------------------------------------------------------------

(in-package :fire)

(defun get-dt (dt-term source &key (refresh nil))
  (let ((cached-entry (find dt-term (dts source)
                            :test 'equal
                            :key 'gizmo::name)))
    (if cached-entry
      cached-entry
      (create-dt dt-term source))))

(defmethod create-dt ((dt-spec list) (source qp-source))
  (let ((dt-forms
         (gather-dt-facts (car dt-spec) (cdr dt-spec) source))
        (dt (gizmo::create-domain-theory 
             (gensym "domain-theory"))))
    (gizmo::with-domain-theory dt
      (load-embedded-language-forms dt-forms gizmo::*gizmo-modeling-language-table*))
    (push dt (dts source))
    dt))

(defun load-embedded-language-forms (forms syntax-table)
  (dolist (form forms)
    (gizmo::process-embedded-language-form (->data form) syntax-table)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  
;;; carries out dynamic case construction.

(defgeneric gather-dt-facts (type specs source)
  (:documentation "Returns list of facts from the KB that go into making the 
      case for the SPECS using filter-type TYPE"))

(defmethod gather-dt-facts ((type (eql 'data::explicit-case-fn))
                            (specs list)
                            (source qp-source))
  (gather-explicit-case-dt (car specs) source))

(defmethod gather-dt-facts ((type (eql 'data::ExplicitCaseFn))
                                (specs list)
                                (source qp-source))
  (gather-explicit-case-dt (car specs) source))

(defun gather-explicit-case-dt (case-name source)
  ;; (explicit-case-fn <case name>)
  ;; (explicitCaseFn <case name>)
  (ask (make-case-fact case-name '?fact)
       (reasoner source)
       :any ;; context
       :all ;; number
       '?fact 
       :lookup))

(defmethod gather-dt-facts ((type (eql 'data::minimal-case-fn))
                                  (specs list)
                                  (source qp-source))
  (gather-minimal-case-dt (car specs)))

(defmethod gather-dt-facts ((type (eql 'data::minimalCaseFn))
                                  (specs list)
                                  (source qp-source))
  (gather-minimal-case-dt (car specs)))

(defun gather-minimal-case-dt (dt-name)
  (let ((qtype-facts (extract-dt-qtype-facts dt-name))
        (entity-facts (extract-dt-entity-facts dt-name))
        (relation-facts (extract-dt-relation-facts dt-name))
        (constant-facts (extract-dt-constant-facts dt-name))
        (univ-facts (extract-dt-univ-facts dt-name))
        (mf-facts (extract-dt-mf-facts dt-name)))
    (append qtype-facts
            entity-facts 
            relation-facts 
            constant-facts 
            univ-facts 
            mf-facts)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Extracting domain theory informations
;;; quantitiy functions, entities, relations, model fragments...

;;;---------------------
;;; quantity functions
;;;---------------------

(defun extract-dt-qtype-facts (dt-name &aux qtype-facts)
  (let ((qtype-args nil)
        (qtype-arity nil)
        (qtype-terms
         (cdadar (ask-it (->data `(evaluate ?qf (TheSetOf ?q (inDomainTheory ,dt-name (qpQuantity ?q)))))))))
    (dolist (qtype-term qtype-terms)
      (setf qtype-arity (caddar (ask-it (->data `(arity (QpQuantityFn ,qtype-term) ?n)))))
      (setf qtype-args (fetch-qtype-args qtype-term qtype-arity))
      (push (setup-dt-qtype qtype-term qtype-args) qtype-facts))
    qtype-facts))

(defun fetch-qtype-args (qtype-term qtype-arity)
  (cond ((= qtype-arity 1)
         (list (collection->var (caddar (ask-it (->data `(arg1Isa (QpQuantityFn ,qtype-term) ?arg)))))))
        ((= qtype-arity 2)
         (mapcar 'collection->var
           (append (cddar (ask-it (->data `(arg1Isa (QpQuantityFn ,qtype-term) ?arg1))))
                   (cddar (ask-it (->data `(arg2Isa (QpQuantityFn ,qtype-term) ?arg2)))))))
        ((= qtype-arity 3)
         (mapcar 'collection->var
           (append
            (cddar (ask-it (->data `(arg1Isa (QpQuantityFn ,qtype-term) ?arg1))))
            (cddar (ask-it (->data `(arg2Isa (QpQuantityFn ,qtype-term) ?arg2))))
            (cddar (ask-it (->data `(arg3Isa (QpQuantityFn ,qtype-term) ?arg3)))))))))

;;;(defun extract-dt-qtype-facts (dt-name)
;;;  (let ((qtype-facts nil)
;;;        (qtype-args nil)
;;;        (qtype-terms
;;;         (cdadar (ask-it (->data `(evaluate ?qf (TheSetOf ?q (inDomainTheory ,dt-name (qpQuantity ?q)))))))))
;;;    (dolist (qtype-term qtype-terms)
;;;      (setf qtype-arity (caddar (ask-it (->data `(arity (QpQuantityFn ,qtype-term) ?n)))))
;;;      (push (setup-dt-qtype qtype-term qtype-arity) qtype-facts))
;;;    qtype-facts))

;;;----------
;;; entities
;;;----------

(defun extract-dt-entity-facts (dt-name)
  (let ((entity-facts nil)
        (entity-terms
         (cdadar (ask-it (->data `(evaluate ?ef (TheSetOf ?e (inDomainTheory ,dt-name (qpEntity ?e)))))))))
    (dolist (entity-term entity-terms)
      (push (extract-entity-relevant-facts entity-term) entity-facts))
    entity-facts))

;;; for rerep like: (qpEntityQuantity Container TopHeight)
;;;(defun extract-entity-relevant-facts (entity-term &aux quantities-info)
;;;  (let ((subclass (cddar (ask-it (->data `(genls ,entity-term ?class))))) ;;return a list
;;;        (quantities (cdadar (ask-it (->data `(evaluate ?qf (TheSetOf ?q (qpEntityQuantity ,entity-term ?q)))))))
;;;        (consequences (cdadar (ask-it (->data `(evaluate ?cf (TheSetOf ?c (qpEntityConsequence ,entity-term ?c))))))))
;;;    (dolist (quantity quantities)
;;;      (push (extract-entity-quantity-relevant-facts entity-term quantity) quantities-info))
;;;    (setup-qp-dt-entity entity-term subclass quantities-info consequences)))

;;; for rerep like: 
;;;(forAll (?x) 
;;;        (implies (isa ?x Container) 
;;;                 (and (isa ((QpQuantityFn TopHeight) ?x) Quantity)
;;;                      ...)))   
(defun extract-entity-relevant-facts (entity-term &aux quantities consequences)
  (let ((subclass (cddar (ask-it (->data `(qpEntitySubclass ,entity-term ?class)))))) 
    ;;Q:What if some entities previously 
    ;;defined in our kb have more general super class collections besides what we want to extract? Leave it like
    ;;this for now.
    (multiple-value-bind (quantities consequences)
        (collect-quantities-consequences (ask-it (->data `(forAll (?x) (implies (isa ?x ,entity-term) ?y)))))
      (setup-qp-dt-entity entity-term subclass quantities consequences))))

(defun collect-quantities-consequences (lst &aux quantities consequences)
  (let ((q-lst (cdar (cddar (cddar lst))))
        (unified-info nil))
    (dolist (q-info q-lst)
      (setf unified-info (ltre::unify q-info (->data '(isa ((QpQuantityFn ?q) ?x) Quantity))))
      (if (not (equal unified-info ':fail))
        (push (cdr (assoc 'data::?q unified-info)) quantities)
        (push (substitute-for-var ':self (car (fire->gizmo (list q-info)))) consequences)))
    (values quantities consequences)))

(defun substitute-for-var (thing form)
  (cond ((eq form 'data::?x) thing)
        ((not (consp form)) form)
        (t (cons (substitute-for-var thing (car form))
                 (substitute-for-var thing (cdr form))))))

;;; Test Result:
;;;cl-user(17): (fire::ask-it '(forAll (?x)
;;;                                    (implies (isa ?x Container)
;;;                                             ?y)))
;;;((forAll (#:?DB-x2939) (implies (isa #:?DB-x2939 Container) (and (isa # Quantity) (isa # Quantity)))))
;;;t
;;;cl-user(18): (pprint *)
;;;
;;;((forAll (#:?DB-x2939)
;;;  (implies (isa #:?DB-x2939 Container)
;;;   (and (isa ((QpQuantityFn BottomHeight) #:?DB-x2939) Quantity)
;;;        (isa ((QpQuantityFn TopHeight) #:?DB-x2939) Quantity)))))

;;;(defun extract-entity-quantity-relevant-facts (entity quantity &aux type dimension)
;;;  (setf type (cadar (last (car (ask-it (->data `(qpEntityQuantityType ,entity ,quantity ?t)))))))
;;;  (setf dimension (car (last (car (ask-it (->data `(qpEntityQuantityDimension ,entity ,quantity ?d)))))))
;;;  (setup-qp-ent-quantity quantity type dimension))

(defun switch-quantity (quantity)
  (list quantity ':type quantity))

;;;-----------
;;; relations
;;;-----------

;;;(defun extract-dt-relation-facts (dt-name)
;;;  (let ((relation-facts nil)
;;;        (relation-arity nil)
;;;        (relation-terms 
;;;         (cdadar (ask-it (->data `(evaluate ?rf (TheSetOf ?r (inDomainTheory ,dt-name (qpRelation ?r)))))))))
;;;    (dolist (relation-term relation-terms)
;;;      (setf relation-arity (caddar (ask-it (->data `(arity ,relation-term ?a)))))
;;;      (push (extract-relation-relevant-facts relation-term relation-arity) relation-facts))
;;;    relation-facts))

;;;(defun extract-relation-relevant-facts (relation-term relation-arity)
;;;  (let ((imply-info (caddar (ask-it (->data `(qpRelationImplies ,relation-term ?imply))))))
;;;    (setf imply-info (DB->var imply-info))
;;;    (setup-qp-dt-relation relation-term relation-arity imply-info)))

(defun extract-dt-relation-facts (dt-name &aux relation-facts)
  (let ((relation-arity nil)
        (relation-args nil)
        (relation-terms 
         (cdadar (ask-it (->data `(evaluate ?rf (TheSetOf ?r (inDomainTheory ,dt-name (qpRelation ?r)))))))))
    (dolist (relation-term relation-terms)
      (setf relation-arity (caddar (ask-it (->data `(arity ,relation-term ?a)))))
      (setf relation-args (fetch-relation-args relation-term relation-arity))
      (push (extract-relation-relevant-facts relation-term relation-args) relation-facts))
    relation-facts))

(defun fetch-relation-args (relation-term relation-arity)
  (cond ((= relation-arity 1)
         (list (collection->var (caddar (ask-it (->data `(arg1Isa ,relation-term ?arg)))))))
        ((= relation-arity 2)
         (mapcar 'collection->var
           (append (cddar (ask-it (->data `(arg1Isa ,relation-term ?arg1))))
                   (cddar (ask-it (->data `(arg2Isa ,relation-term ?arg2)))))))
        ((= relation-arity 3)
         (mapcar 'collection->var
           (append
            (cddar (ask-it (->data `(arg1Isa ,relation-term ?arg1))))
            (cddar (ask-it (->data `(arg2Isa ,relation-term ?arg2))))
            (cddar (ask-it (->data `(arg3Isa ,relation-term ?arg3)))))))))

(defun extract-relation-relevant-facts (relation-term relation-args)
  (let ((imply-info (caddar (ask-it (->data `(qpRelationImplies ,relation-term ?imply))))))
    (setf imply-info (DB->var imply-info))
    (setup-qp-dt-relation relation-term relation-args imply-info)))

;;;-----------
;;; Constants
;;;-----------

(defun extract-dt-constant-facts (dt-name)
  (let ((constants 
         (cdadar (ask-it (->data `(evaluate ?cf (TheSetOf ?c (inDomainTheory ,dt-name (qpConstant ?c)))))))))
    (mapcar 'setup-qp-dt-constant constants)))

;;;------------------
;;; Universal Facts
;;;------------------

(defun extract-dt-univ-facts (dt-name)
  (let ((univ-facts 
         (cdadar (ask-it (->data `(evaluate ?uf (TheSetOf ?u (inDomainTheory ,dt-name (qpUnivFact ?u)))))))))
    (mapcar #'setup-qp-dt-uf
      (fire->gizmo univ-facts))))

;;;-----------------
;;; Model Fragment
;;;-----------------
(defun extract-dt-mf-facts (dt-name)
  (let ((mf-facts nil)
        (mf-terms
         (cdadar (ask-it (->data `(evaluate ?mf (TheSetOf ?m (inDomainTheory ,dt-name (qpMF ?m)))))))))
    (dolist (mf-term mf-terms)
      (setf mf-term (car (list mf-term)))
      (push (extract-mf-relevant-facts mf-term) mf-facts))
    mf-facts))

(defun extract-mf-relevant-facts (mf-term)
  (let ((subclass (cddar (ask-it (->data `(qpMFSubclass ,mf-term ?class)))))
        (participants (cdadar (ask-it (->data `(evaluate ?pf (TheSetOf ?p (qpMFParticipant ,mf-term ?p)))))))
        (conditions (cdadar (ask-it (->data `(evaluate ?cf (TheSetOf ?c (qpMFCondition ,mf-term ?c)))))))
        (quantities (cdadar (ask-it (->data `(evaluate ?qf (TheSetOf ?q (qpMFQuantity ,mf-term ?q)))))))
        (consequences 
         (cdadar (ask-it (->data `(evaluate ?consef (TheSetOf ?conse (qpMFConsequence ,mf-term ?conse))))))))
    (setf participants (extract-mf-participants-facts mf-term participants)
      conditions (fire->gizmo conditions)
      quantities (extract-mf-quantities-facts mf-term quantities)
      consequences (fire->gizmo consequences))
    ;;;    quantities (DB->var (extract-mf-quantities-facts mf-term quantities))
    (setup-qp-dt-mf mf-term subclass participants conditions quantities consequences)))

;;;(defun extract-mf-relevant-facts (mf-term)
;;;  (let ((subclass (cddar (ask-it (->data `(qpMFSubclass ,mf-term ?class)))))
;;;        (participants (cdadar (ask-it `(qpMFParticipant ,mf-term ?p)))))
;;;        (partidipants-type 
;;;         (cdadar (ask-it (->data `(qpMFParticipantType ,mf-term ?p ?t)))))))
;;;        (conditions 

;;; MF Participants
(defun extract-mf-participants-facts (mf-term participants &aux (type nil) (constraints nil))
  (mapcar #'(lambda (part)
              (setf type (car (last (car (ask-it (->data `(qpMFParticipantType ,mf-term ,part ?t))))))
                constraints
                (cdadar (ask-it (->data `(evaluate ?cf (TheSetOf ?c (qpMFParticipantConstraint ,mf-term ,part ?c)))))))
              (setup-qp-mf-participant part type constraints))
    participants))

;;; MF Quantities
(defun extract-mf-quantities-facts (mf-term quantities &aux quantity-args)
  (mapcar #'(lambda (quantity)
              (setf quantity-args 
                (car (last (car (ask-it 
                                 (->data `(qpMFQuantityArguments ,mf-term ,quantity ?a)))))))
              (setup-qp-mf-quantity quantity quantity-args))
    quantities))