;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: make-exp.lsp
;;;;    System: FIRE
;;;;   Version: 1.0
;;;;    Author: Ken Forbus
;;;;   Created: November 17, 2000 21:43:15
;;;;   Purpose: Abstraction for making expressions
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Monday, June 7, 2004 at 10:19:23 by hinrichs
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;; There are two kinds of conventions used for predicates:
;;; :HYPHEN is case-independent, with predicates like geographic-region
;;; :MIXED-CASE is case-dependent, Cyc-style: GeographicRegion
;;; While we are building all of our new systems with mixed case right now, 
;;; we still have a number of systems that use hypens, and KB's built by other
;;; groups often use that convention.  Consequently, we need to live comfortably
;;; with both kinds of predicates. This means abstracting away the constructors 
;;; for expressions inside the system.

(defmethod kb-genls-predicate ((kb knowledge-base)) 'data::genls)

(defun mixed-case? (&optional (kb *kb*)) (eq :mixed-case (predicate-style kb)))
(defun hyphens? (&optional (kb *kb*)) (eq :hyphen (predicate-style kb)))

;;; By far the most common case involves two constants.  This macro
;;; streamlines this situation
(defmacro if-mixed-case (mixed-case-option hyphen-case-option)
  `(if (eq :mixed-case (predicate-style *kb*)) ',mixed-case-option ',hyphen-case-option))


(defun ->data (tree)
  (cond ((null tree) nil)
        ((symbolp tree)
         (if (keywordp tree) tree
           (intern (symbol-name tree) (find-package :data))))
        ((consp tree)
         (cons (->data (car tree)) (->data (cdr tree))))
        (t tree)))

(defun make-keyword (foo)
  (intern (symbol-name foo) (find-package :keyword)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Constructing formulas

(defun make-forall (var expr) `(data::forAll ,var ,expr))
(defun make-thereexists (var expr) `(data::thereExists ,var ,expr))
(defun make-implies (ante conse) `(data::implies ,ante ,conse))
(defun make-conjunction (&rest conjuncts) (cons 'data::and conjuncts))
(defun make-implication (ante conse) (list 'data::implies ante conse))
(defun make-negation (arg) (list 'data::not arg))
(defun make-disjunction (&rest args) (cons 'data::or args))
(defun make-biconditional (ante conse) (list 'data::iff ante conse))
(defun make-functional-term (func args) (cons func args))

(defun variable? (x) (ltre::variable? x))
(defun conjunction? (form) (and (listp form) (eq (car form) 'data::and)))
(defun negation? (form) (and (listp form) (eq (car form) 'data::not)))
(defun disjunction? (form) (and (listp form) (eq (car form) 'data::or)))
(defun implication? (form) (and (listp form) (eq (car form) 'data::implies)))
(defun biconditional? (form) (and (listp form) (eq (car form) 'data::iff)))

(defun quantifier-formula? (formula)
  (or (universal-formula? formula)
      (existential-formula? formula)))

(defun universal-formula? (form) 
  (and (listp form)
       (= (length form) 3)
       (equal (car form) 'data::forAll)
       (variable? (cadr form))
       (listp (third form))))

(defun existential-formula? (form)
  (and (listp form)
       (= (length form) 3)
       (equal (car form) 'data::thereExists)
       (variable? (cadr form))
       (listp (third form))))

(defun existential? (symbol) (eq symbol 'data::thereExists))


(defun new-function-symbol-with-args (args)
  `(,(gensym "SKF-") ,@args))

(defun skolem? (symbol)
  (and (not (numberp symbol)) ;; symbol-name complains when handed a number
       (not (stringp symbol))
       (>= (length (symbol-name symbol)) 4)  
       (string-equal (subseq (symbol-name symbol) 0 4) "SKF-")))

;; Accessing parts of formulas

(defun conjuncts (conjunction) (cdr conjunction))
(defun disjuncts (disjunction) (cdr disjunction))
(defun antecedent (implication) (cadr implication))
(defun consequent (implication) (caddr implication))
(defun quantified-variables (quantified-expression) (cadr quantified-expression))
(defun quantified-formula (quantified-expression) (caddr quantified-expression))
(defun negated-formula (negation) (cadr negation))
(defun biconditional-lhs (biconditional) (second biconditional))
(defun biconditional-rhs (biconditional) (third biconditional))
(defun formula-operator (formula) (car formula))
(defun formula-arg1 (formula) (second formula))
(defun formula-arg2 (formula) (third formula))

(defun formula-predicate (formula)
  ;; Assuming nothing internal is stupid enough to generate nested
  ;; negations
  (if (negation? formula) (formula-operator (negated-formula formula))
    (formula-operator formula)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; MELD support

(defun ist-statement? (statement)
  (and (listp statement) 
       (eq (car statement) 'data::ist)))

(defun make-ist-statement (context statement)
  (list 'data::ist context statement))

;; Structural predicates

;;; For efficiency of retrieval, in inference we will use ISA for
;;; attribute information.  This means that the interfaces
;;; to our analogical processing code will require translations in and out,
;;; or to be subclassed to treat ISA statements as attributes.

(defun make-isa (thing collection)
  `(data::isa ,thing ,collection))

(defun isa-predicate? (pred) 
  (or (eq pred 'data::isa)
      (eq pred 'data::|isa|)))

(defun isa-statement? (form)
  (and (listp form)
       (isa-predicate? (car form))
       (= (length form) 3)))

(defun fn-name-heuristic? (pred)
  (when (symbolp pred)
    (let ((name (symbol-name pred)))
      (string-equal (subseq name (- (length name) 2))
                    "FN"))))

(defun non-atomic-term? (thing)
  (and (listp thing)
       (function? (car thing))))

(defun kappa-form? (thing)
  (and (listp thing)
       (if (mixed-case?)
         (eq (car thing) 'data::Kappa)
         (eq (car thing) 'data::kappa))))

(defun lambda-form? (thing)
  (and (listp thing)
       (if (mixed-case?)
         (eq (car thing) 'data::Lambda)
         (eq (car thing) 'data::lambda))))

(defun unary-predicate? (pred kb)
  (let ((p-arity (arity pred :kb kb)))
    (and (numberp p-arity)  ;; need to handle :unknown arities
         (= 1 p-arity))))

(defun attribute-predicate? (pred kb)
  (with-kb kb
    (cond ((symbolp pred)
           (unless (or (function? pred) (unary-predicate? pred kb))
             ;; 5/29/02 - there appear to be some unary predicates which are not functions
             ;;  eg -   happen   - we don't want these  showing up as attribute 
             ;;  expressions either
             ;; If not a function, then an attribute
             (values t pred)))
          (t (values nil pred)))))

(defun make-genls (sub super) `(data::genls ,sub ,super))

(defun genls-predicate? (thing) (eq thing 'data::genls))

(defun genls-statement? (form)
  (and (listp form)
       (genls-predicate? (car form))
       (= (length form) 3)))

(defun make-genl-preds (sub super)
  (list (if-mixed-case data::genlPreds data::genl-preds) sub super))

(defun constant-term? (obj) 
  (cond ((null obj) t) 
        ((variable? obj) nil) 
        ((not (consp obj)) t) 
        (t (and (constant-term? (car obj)) 
                (constant-term? (cdr obj))))))

(defun constant-genls-statement? (form)
  (and (genls-statement? form) (constant-term? (cadr form))
       (constant-term? (third form))))

(defun make-quantity-term (qtype entity)
  (make-isa `(,qtype ,entity)
            (if (mixed-case?) 'data::quantity 'data::quantity)))

(defun make-continuous-quantity (qtype)
  (make-isa qtype (if-mixed-case data::ContinuousQuantity
                                 data::continuous-quantity)))

(defun make-result-type (function type)
  (list (if-mixed-case data::resultIsa data::result-isa)
      function type))

(defun make-arg-type (predicate type n)
  `(,(if (mixed-case?) (intern (format nil "arg~AIsa" n) (find-package :data))
       (intern (format nil "arg-~AIsa" n) (find-package :data)))
      ,predicate ,type))

(defun make-args-isa (predicate type)
  ;; For n-ary case
  (list (if-mixed-case data::argsIsa data::args-isa) predicate type))

(defun make-individual (entity)
  `(data::isa ,entity 
              ,(if (mixed-case?) 'data::Individual 'data::individual)))

(defun make-arity (predicate arity) `(data::arity ,predicate ,arity))

(defun make-n-ary (predicate &optional (type :relation))
  (ecase type
    ((:relation :logical) (make-n-ary-relation predicate))
    (:function (make-n-ary-function predicate))))

(defun make-n-ary-relation (predicate)
  (make-isa predicate (if (mixed-case?) 
                        'data::VariableArityRelation
                        'data::variable-arity-relation)))

(defun make-n-ary-function (predicate)
  (make-isa predicate (if (mixed-case?) 
                        'data::VariableArityFunction
                        'data::variable-arity-function)))

(defun make-arity-assertion (predicate type arglist keywords)
  (let* ((nary? (member :n-ary? keywords)))
    (cond ((and nary? (not (null (cadr nary?))))
           (make-n-ary predicate type))
          (t (make-arity predicate (length arglist))))))

(defun make-predicate-type-declaration (predicate arglist keywords)
  (declare (ignore arglist)) ;; probably useful later.
  (let ((function? (member :function keywords)))
    (cond ((and function? (not (null (cadr function?))))
           (make-function-declaration predicate))
          (t 
           (make-relation-declaration predicate)))))

(defun structural-assertions-by-type (predicate arglist type)
  (let ((assertions (list (make-arity predicate (length arglist)))))
    (when (every 'listp arglist)
      ;; Add argument type information if it is available.
      (let ((arg 1))
        (dolist (arg-entry arglist)
          (push (make-arg-type predicate (cadr arg-entry) arg)
                assertions)
          (incf arg))))
  (case type
    (data::relation (push (make-relation-declaration predicate)
                          assertions))
    (data::function (push (make-function-declaration predicate)
                          assertions))
    (data::attribute (push (make-attribute-declaration predicate)
                           assertions))
    (t (format t "~%Unknown assertion type: ~A, ~A; ~A."
         type predicate arglist)))))

(defun make-function-declaration (functor)
  ;; *** Should really compute arity and include that as well.
  ;; **** Actually not, this function is used in some places where it would
  ;; **** not be appropriate to automatically include assertions about the 
  ;; **** arity.  (For example, in the function structural-assertions-by-type).
  (make-isa functor (if (mixed-case?) 
                      'data::Function-Denotational 
                      'data::function-denotational)))

(defun make-eval-function-declaration (functor)
  (make-isa functor (if (mixed-case?) 
                      'data::EvaluatableFunction 
                      'data::evaluatable-function)))

(defun make-eval-relation-declaration (functor)
  (make-isa functor (if (mixed-case?) 
                      'data::EvaluatableRelation 
                      'data::evaluatable-relation)))

(defun make-lisp-implementation-assertion (function procedure)
  `(data::lispProcedureImplementing ,function ,procedure))

(defun make-function-expression (form expression)
  `(,(if (mixed-case?) 'data::expressionFor 'data::expression-for)
      ,form ,expression))

(defun evaluate-statement? (form)
  (and (listp form)
       (eq (car form) 'data::evaluate)))

(defun make-creator (expr creator)
  (when creator
    (list (if (mixed-case?) 'data::myCreator 'data::my-creator) expr creator)))

(defun make-creation-time (expr)
  (list (if (mixed-case?)
          'data::myCreationTime
          'data::my-creation-time)
        expr (universal-time->cyc-time)))

(defun make-creation-second (expr)
  (list (if (mixed-case?)
          'data::myCreationSecond
          'data::my-creation-second)
        expr (universal-time->cyc-seconds)))

(defun make-assertion-time (expr)
  (list (if (mixed-case?)
          'data::myAssertionTime
          'data::my-assertion-time)
        expr (universal-time->cyc-time)))

;;; Structural relations
;;; 

(defun make-term-formulas (term formula)
  (list (if-mixed-case data::termFormulas data::term-formulas)
        term formula))

(defun make-formula-arg-fn (formula n term)
  (list (if-mixed-case data::formulaArgFn data::formula-arg-fn)
        formula n term))

(defun make-operator-formulas (term formula)
  (list (if-mixed-case data::operatorFormulas data::operator-formulas)
        term formula))

(defun make-formula-arg-list-fn (formula)
  (list (if-mixed-case data::formulaArgListFn data::formula-arg-list-fn)
        formula))

(defun make-some-argument-has-predicate (formula predicate)
  (list (if-mixed-case data::someArgumentHasPredicate data::some-argument-has-predicate)
        formula predicate))

(defun make-asserted-term-sentences (term sentence)
  (list (if-mixed-case data::assertedTermSentences data::asserted-term-sentences)
        term sentence))

(defun make-nat-argument (nat n term)
  (list (if-mixed-case data::natArgument data::nat-argument)
        nat n term))

(defun make-nat-function (nat function)
  (list (if-mixed-case data::natFunction data::nat-function) 
        nat function))


;;; EvaluatableFunctions
;;;
;;; In Cyc, the collection #$EvaluatableFunction is
;;; associated via #$evaluationDefn to the piece of SubL 
;;; code that computes the result of  applying the funtion 
;;; to the args. For example, (evaluationDefn PlusFn CYC-PLUS)
;;; In FIRE, we maintain the evalfn-table, which is a table 
;;; that maps from predicates to function forms which the 
;;; evaluator can understand. For example, the entries in 
;;; the evalfn-table might look like 
;;; (PlusFn (:n-ary fire::arglist (apply #'+ fire::arglist)))
;;; (ExponentFn (2 (fire::?base fire::?exp) (expt fire::?base fire::?exp)))
;;; This will correspond to the statemement
;;; (lispDefinitionFor PlusFn (:n-ary fire::arglist (apply #'+ fire::arglist)))

(defun make-lisp-definition (form expression)
  `(,(if (mixed-case?) 'data::lispDefinitionFor 'data::lisp-definition-for)
      ,form ,expression))

(defun make-connective-declaration (predicate)
  (make-isa predicate (if (mixed-case?) 'data::LogicalConnective
                        'data::logical-connective)))

(defun make-relation-declaration (predicate)
  (make-isa predicate (if (mixed-case?) 'data::Predicate 'data::predicate)))

(defun make-attribute-declaration (predicate)
  (make-isa predicate (if (mixed-case?) 'data::Collection
                           'data::collection)))

(defun make-commutative (pred)
  (make-isa pred (if (mixed-case?) 'data::CommutativeRelation
                      'data::commutative-relation)))

(defun make-nary (pred)
  (make-isa pred (if (mixed-case?) 'data::VariableArityRelation
                   'data::variable-arity-relation)))

(defun make-pidgin (predicate string)
  `(,(if (mixed-case?) 'data::pidginFor 'data::pidgin-for)
      ,(if (and (listp predicate) (eq (car predicate) 'quote))
           (cadr predicate) predicate) ,string))

(defun make-dimension (predicate dimension)
  ;;***** Don't know what we really need here.
  `(,(if (mixed-case?) 'data::dimensionOfUnit 'data::dimension-of-unit)
      ,predicate ,dimension))

(defun make-units (predicate)
  (make-isa predicate (if (mixed-case?) 'data::UnitOfMeasure
                           'data::unit-of-measure)))

(defun make-model-fragment-type (mf)
  (make-isa mf (if (mixed-case?) 'data::ModelFragment
                    'data::model-fragment)))
(defun make-participants (mf participants)
  `(,(if (mixed-case?) 'data::participantsOf 
                'data::participants-of) ,mf ,participants))
(defun make-conditions (mf conditions)
  `(,(if (mixed-case?) 'data::conditionsOf 'data::conditions-of) ,mf ,conditions))
(defun make-quantities (mf quantities)
  `(,(if (mixed-case?) 'data::quantitiesOf 'data::quantities-of) ,mf ,quantities))
(defun make-consequences (mf consequences)
  `(,(if (mixed-case?) 'data::consequencesOf 'data::consequences-of) ,mf ,consequences))

;;;==================================================================
;;; Chainers

(defun make-chainer-file-name-expr (chainer-term string)
  (list (if-mixed-case data::chainerFileName
                       data::chainer-file-name)
        chainer-term string))

(defun make-current-universal-time-term ()
  `(data::UniversalTimeFn ,(get-universal-time)))

(defun make-chainer-dumped-assertion 
    (chainer
     &optional (time (make-current-universal-time-term)))
  `(data::chainerDumpedAt ,chainer ,time))

(defun make-chainer-updated-assertion
    (chainer
     &optional (time (make-current-universal-time-term)))
  `(data::chainerUpdatedAt ,chainer ,time))

(defun universal-time-term? (thing)
  (and (listp thing) (eq (car thing) 'data::UniversalTimeFn)
       (integerp (cadr thing))))

(defun time-term-later? (t1 t2)
  (and (universal-time-term? t1)
       (universal-time-term? t2)
       (> (cadr t1) (cadr t2))))

(defun retrieve-latest-ut-assertion (relation arg1 &key (kb *kb*))
  (let ((facts (retrieve (list relation arg1 '?time) :kb kb)))
    (setq facts (sort facts 'time-term-later? :key 'third))
    (dolist (other (cdr facts)) (forget other :kb kb))
    (car facts)))  

(defun update-chainer-dumped-timestamp (chainer &key (kb *kb*))
  (let ((last-time (retrieve-latest-ut-assertion 'data::chainerDumpedAt chainer)))
    (forget last-time :kb kb)
    (store (make-chainer-dumped-assertion chainer) kb)))

(defun update-chainer-updated-timestamp (chainer &key (kb *kb*))
  (let ((last-time (retrieve-latest-ut-assertion 'data::chainerUpdatedAt chainer)))
    (forget last-time :kb kb)
    (store (make-chainer-updated-assertion chainer) kb)))

;;; =======================================================================
;;; Suggestions

(defun make-ist-suggestion-stmt (form)
  "Mark all the suggestion assertions as in SuggestionMT so that 
   we can reset/blow them all in one go if we need. Debugging hack, 
   will replace by something more principled soon -- PKP"
  (if (mixed-case?)
    `(data::ist-Asserted data::SuggestionMT ,form)))
        
(defun make-suggestion-type (name)
  (make-isa name (if (mixed-case?) 'data::Suggestion 'data::suggestion))) 
      
(defun make-suggestion-comment-stmt (name documentation)
  (make-comment-statement name documentation))

(defun make-suggestion-goal-form (name goal)
  (if (mixed-case?)
    `(data::suggestionGoalForm ,name ,goal)
    `(data::suggestions-goal-form ,name ,goal)))

(defun make-suggest-for-axiom (name goal test)
  (if (and (not (null name)) (not (null goal)))
    (cond ((null test) 
           (make-suggest-for-stmt name goal))
          (t `(data::implies ,test
                             ,(make-suggest-for-stmt name goal)))))) 

(defun make-suggest-for-stmt (name goal)
  (if (mixed-case?)
    `(data::suggestFor ,goal ,name)
    `(data::suggest-for ,goal ,name)))

(defun make-suggestion-subgoals-stmt (name subgoals)
  "Returns the suggestionSubgoals statement"
  (if (mixed-case?)
    `(data::suggestionSubgoals ,name ,(make-the-list subgoals))
    `(data::suggestion-subgoals ,name ,(make-the-list subgoals))))

(defun make-suggestion-result-step-stmt (name result-step)
  (if (mixed-case?)
    `(data::suggestionResultStep ,name ,result-step)
    `(data::suggestion-result-step ,name ,result-step)))
                                                                            
;;; Scenarios
;;; :INITIALLY :INDIVIDUALS :THROUGHOUT

(defun make-scenario (name)
  `(make-isa ,name ,(if (mixed-case?) 'data::Scenario 'data::scenario)))
(defun make-scenario-initially (name initially)
  `(,(if (mixed-case?) 'data::scenarioInitially 'data::scenario-initially)
      ,name ,initially))
(defun make-scenario-individuals (name is)
  `(,(if (mixed-case?) 'data::scenarioIndividuals 'data::scenario-individuals)
      ,name ,is))

(defun make-scenario-throughout (name th)
  `(,(if (mixed-case?) 'data::scenarioThroughout 'data::scenario-throughout)
      ,name ,th))

(defun make-dt-membership (dt fact)
  `(,(if (mixed-case?) 'data::inDomainTheory 'data::in-domain-theory) ,dt ,fact))

;;;; Analogical reasoning

(defun make-match-query (base target constraints matcher)
  `(,(if (mixed-case?) 'data::matchBetween 'data::match-between)
      ,base ,target ,constraints ,matcher))

(defgeneric make-sme-reference (sme-or-id))
  
(defmethod make-sme-reference ((sme sme:sme))
  ;; This is the WM version.  The idea is to just get quickly to
  ;; the SME internals, and not build any new datastructures that we
  ;; don't have to.
  `(,(if (mixed-case?) 'data::MatcherFn 'data::matcher-fn)
      ,(sme::id sme)))

(defmethod make-sme-reference ((sme-id integer))
  ;; This is the WM version.  The idea is to just get quickly to
  ;; the SME internals, and not build any new datastructures that we
  ;; don't have to.
  `(,(if (mixed-case?) 'data::MatcherFn 'data::matcher-fn) ,sme-id))


(defun make-mapping-reference (mapping)
  `(,(if (mixed-case?) 'data::MappingFn 'data::mapping-fn)
      ,(sme::id mapping) ,(sme::id (sme::sme mapping))))

(defun make-mh-reference (mh)
  `(,(if (mixed-case?) 'data::MhFn 'data::mh-fn)
      ,(sme::id mh) ,(sme::id (sme::sme mh))))

(defun make-ci-reference (ci)
  (let ((mapping (sme::mapping ci)))
    `(,(if (mixed-case?) 'data::CiFn 'data::ci-fn)
        ,(sme::id ci) ,(sme::id mapping)
        ,(sme::id (sme::sme mapping)))))

(defun declare-matcher (sme)
  (make-isa (make-sme-reference sme)
            (if (mixed-case?) 'data::Matcher 'data::matcher)))

(defun declare-match-constraints (sme &key (constraints nil))
  (list (if (mixed-case?) 'data::matchConstraints 'data::match-constraints)
        (make-sme-reference sme)
        (or constraints
            (cons (if (mixed-case?) 'data::TheList 'data::the-list)
                  (sme::filter-list-form (sme::match-filters sme) (mixed-case?))))))
                                     
(defun declare-mapping (m)
  (make-isa (make-mapping-reference m)
            (if (mixed-case?) 'data::Mapping 'data::mapping)))

(defun make-mapping-of (m)
  (list (if (mixed-case?) 'data::mappingOf 'data::mapping-of)
        (make-mapping-reference m)
        (make-sme-reference (sme::sme m))))

(defun make-se-form (m)
  (make-nvalue `(,(if (mixed-case?) 'data::structuralEvaluationScore
                    'data::structural-evaluation-score)
                   ,(make-mapping-reference m)) (sme::score m)))


(defun declare-mh (mh)
  (make-isa (make-mh-reference mh) (if (mixed-case?) 'data::Correspondence
                                     'data::correspondence)))

(defun find-or-make-sme-relevance-assumption (sme)
  (let* ((sme-form (make-sme-reference sme))
         (relevance-asn 
          (car (ltre:fetch-trues (make-sme-relevance-assumption sme-form '?rel)))))
    (cond (relevance-asn relevance-asn)
          (t (make-sme-relevance-assumption sme-form (get-universal-time))))))

(defun make-sme-relevance-assumption (sme-ref time)
    (list (if-mixed-case data::relevantComparison data::relevant-comparison)
          sme-ref time))

(defun make-current-sme-timeclock-assumption (sme)
  (make-sme-timeclock-assumption sme (sme::timeclock sme)))

(defun make-sme-timeclock-assumption (sme value)
  (list (if-mixed-case data::smeTimeclockValue data::sme-timeclock-value)
        (make-sme-reference sme)
        value))

(defun make-current-dgroup-timeclock-assumption (dgroup)
  (make-dgroup-timeclock-assumption dgroup (sme::timeclock dgroup)))

(defun make-dgroup-timeclock-assumption (dgroup value)
  (list (if-mixed-case data::dgroupTimeclockValue data::dgroup-timeclock-value)
        (generate-analogy-term dgroup)
        value)) 

(defun make-best-mapping (sme m)
  (list (if (mixed-case?) 'data::bestMapping 'data::best-mapping)
        (make-sme-reference sme) (make-mapping-reference m)))

(defun make-correspondence-of (mh)
  (list (if (mixed-case?) 'data::correspondenceOf 'data::correspondence-of)
        (make-mh-reference mh) (make-sme-reference (sme::sme mh))))

(defun make-has-correspondence (mh m)
  (list (if (mixed-case?) 'data::hasCorrespondence 'data::has-correspondence)
        (make-mapping-reference m)
        (make-mh-reference mh)))

(defun make-correspondence-between (mh)
  (list (if (mixed-case?) 'data::correspondenceBetween 'data::correspondence-between)
        (make-mh-reference mh)
        (sme::lisp-form (sme::base-item mh))
        (sme::lisp-form (sme::target-item mh))))

(defun declare-ci (ci)
  (make-isa (make-ci-reference ci) (if (mixed-case?) 'data::CandidateInference
                                     'data::candidate-inference)))

(defun declare-ci-mapping (ci m)
  (list (if (mixed-case?) 'data::candidateInferenceOf 'data::candidate-inference-of)
        (make-ci-reference ci) (make-mapping-reference m)))

(defun declare-ci-content (ci)
  (list (if (mixed-case?) 'data::candidateInferenceContent
          'data::candidate-inference-content)
        (make-ci-reference ci)
        (translate-ci-content ci)))

(defun declare-ci-support-score (ci)
  (make-nvalue (list 
                (if (mixed-case?) 'data::SupportScore 'data::support-score)
                (make-ci-reference ci))
               (sme::support-score ci))) 

(defun declare-ci-extrapolation-score (ci)
  (make-nvalue (list 
                (if (mixed-case?) 'data::ExtrapolationScore 'data::extrapolation-score)
                (make-ci-reference ci))
               (sme::extrapolation-score ci)))

(defun analogy-skolem-term? (thing)
  (and (listp thing)
       (eq (car thing)
           (if (mixed-case?) 'data::AnalogySkolemFn
             'data::analogy-skolem-fn))))

(defun make-analogy-skolem-term (argument)
  (list (if-mixed-case data::AnalogySkolemFn data::analogy-skolem-fn) argument))


;;;; Dynamic case construction

(defun make-case-fact (case-name fact)
  (list (if-mixed-case data::ist-Information data::ist--information)
        case-name fact))

(defun case-fact? (thing)
  (and (listp thing)
       (eq (car thing)
           (if-mixed-case data::ist-Information data::ist--information))
       (listp (third thing))
       (null (cdddr thing))))

(defun make-explicit-case-fn (case)
  (list (if-mixed-case data::ExplicitCaseFn data::explicit-case-fn)
      case))

(defun make-minimal-case-fn (case)
  (list (if-mixed-case data::MinimalCaseFn data::minimal-case-fn)
      case))

(defun make-case-fn (case)
  (list (if-mixed-case data::CaseFn data::case-fn) case))

(defun make-event-case-fn (case)
  (list (if-mixed-case data::EventCaseFn
                       data::event-case-fn)
        case))

(defun make-event-no-postlude-case-fn (case)
  (list (if-mixed-case data::EventNoPostludeCaseFn
                       data::event-no-postlude-case-fn)
        case))

;; These two are redundant with the above, but Shawn is using them in
;; his code.  We should streamline this.

(defun encase-explicit (expr)
  (if (fire:mixed-case?)
    `(data::ExplicitCaseFn ,expr)
    `(data::explicit-case-fn ,expr)))

(defun encase-minimal (expr)
  (if (fire:mixed-case?)
    `(data::MinimalCaseFn ,expr)
    `(data::minimal-case-fn ,expr)))

;; Shawn's encase-case method is a good idea, in that it enables
;; the case construction sysem to be extended by other programmers
;; more easily without changing FIRE source.  

(defmethod encase-case (expr (style (eql :ExplicitCaseFn)))
  (make-explicit-case-fn expr))

(defmethod encase-case (expr (style (eql :explicit-case-fn)))
  (make-explicit-case-fn expr))

(defmethod encase-case (expr (style (eql :MinimalCaseFn)))
  (make-minimal-case-fn expr))

(defmethod encase-case (expr (style (eql :minimal-case-fn)))
  (make-minimal-case-fn expr))

(defmethod encase-case (expr (style (eql :CaseFn)))
  (make-case-fn expr))

(defmethod encase-case (expr (style (eql :case-fn)))
  (make-case-fn expr))

(defmethod encase-case (expr (style (eql :EventCaseFn)))
  (make-event-case-fn expr))

(defmethod encase-case (expr (style (eql :event-case-fn)))
  (make-event-case-fn expr))

(defmethod encase-case (expr (style (eql :EventNoPostludeCaseFn)))
  (make-event-no-postlude-case-fn expr))

(defmethod encase-case (expr (style (eql :event-no-postlude-case-fn)))
  (make-event-no-postlude-case-fn expr))

;;;; MAC/FAC

(defun make-case-library-contents (library contents)
  (list 
   (if (mixed-case?) 'data::caseLibraryContents 'data::case-library-contents)
   library 
   contents))

(defun make-case-library (library)
  (list 
   (if (mixed-case?) 'data::CaseLibraryFn 'data::case-library-fn) 
   library))


(defun make-case-library-file-name-expr (library-term string)
  (list (if-mixed-case data::caseLibraryFileName
                       data::case-library-file-name)
        library-term string))

(defun make-reminding (probe case-library case match)
  (list 'data::reminding probe case-library case match))

(defun make-ubiquitous-predicate-query (var)
  (if (mixed-case?)
    `(data::isa ,var data::UbiquitousPredicate)
    `(data::isa ,var data::ubiquitous-predicate)))

;;; Predicates involving similarities and differences

(defun make-entity-similarity (mapping mh)
  (list (if (mixed-case?) 'data::entitySimilarityOf 'data::entity-similarity-of)
        (make-mapping-reference mapping) (make-mh-reference mh)))

(defun make-root-similarity  (mapping mh)
  (list (if (mixed-case?) 'data::rootSimilarityOf 'data::root-similarity-of)
        (make-mapping-reference mapping) (make-mh-reference mh)))

(defun make-role-difference (mapping mh base-isas target-isas)
  (list (if (mixed-case?) 'data::roleDifferenceOf 'data::role-difference-of)
        (make-mapping-reference mapping)
        (make-mh-reference mh) base-isas target-isas))

(defun make-base-alignable-absence (mapping base-exp)
  (list (if (mixed-case?) 'data::baseAlignableAbsenceOf 'data::base-alignable-absence-of)
        (make-mapping-reference mapping) base-exp))

(defun make-target-alignable-absence (mapping target-exp)
  (list (if (mixed-case?) 'data::targetAlignableAbsenceOf 'data::target-alignable-absence-of)
        (make-mapping-reference mapping) target-exp))

(defun make-base-only-nad (mapping base-exp)
  (list (if (mixed-case?) 'data::baseOnlyNADOf 'data::base-only-NAD-of)
        (make-mapping-reference mapping) base-exp))

(defun make-target-only-nad (mapping target-exp)
  (list (if (mixed-case?) 'data::targetOnlyNADOf 'data::target-only-NAD-of)
        (make-mapping-reference mapping) target-exp))

;;;; sets

(defun make-set (elements)
  (cons (if (mixed-case?) 'data::TheSet 'data::the-set) elements))

(defun make-element-statement (el set)
  (list (if (mixed-case?) 'data::elementOf 'data::element-of) el set))

(defun the-set-statement? (thing)
  (and (listp thing) 
       (eq (car thing) (if-mixed-case data::TheSet data::the-set)))) 

(defun closed-retrieval-set-statement? (form)
  (and (evaluate-statement? form)
       (the-set-statement? (cadr form))
       (closed-retrieval-set-of-statement? (third form))))

(defun closed-retrieval-set-of-statement? (thing)
  (and (listp thing)
       (eq (car thing) (if-mixed-case data::TheClosedRetrievalSetOf
                                      data::the-closed-retrieval-set-of))
       (variable? (cadr thing))
       (listp (third thing))
       (contains-term? (cadr thing) (third thing))))

(defun make-closed-retrieval-set-cwa (var statement)
  (list (if-mixed-case data::closedRetrievalSetCWA data::closed-retrieval-set-cwa)
        var statement (make-current-universal-time-term)))

;;; lists

(defun make-the-list (elements)
  (cons (if (mixed-case?) 'data::TheList 'data::the-list) elements))

(defun the-list? (thing) (eq thing (if-mixed-case data::TheList data::the-list)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; CML support

(defun make-nvalue (param value) `(data::nvalue ,param ,value))

;;; String conversion

;;; Assume the result should be capitalized (for mixed case).
;;; If, for some strange reason, you're generating the name of a relation,
;;; then it's up to you to manually downcase the first character.
(defun make-CYC-term (init-str)
  "Convert a string into a Cyc-compatible symbol"
  (let ((string (and (stringp init-str) (string-trim " " init-str))))
    (when (and string (not (equal string "")))
      (cond ((not (mixed-case?))
             (intern (substitute #\- #\Space (string-downcase string)) :data))
            ((find #\Space string)
             (intern (remove #\Space (string-capitalize string)) :data))
            (t
             ;;; Don't downcase internal chars:
             (intern (string-capitalize string :end 1) :data))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Bookkeeping

(defun make-comment-statement (pred comment)
  (list 'data::comment pred comment))

(defun make-documentation (predicate string) 
  ;; *** This function has been DEPRECATED. ***
  ;; Doc-strings should be asserted using make-comment-statement,
  ;; but some of our earlier KBs used make-documentation instead.
  ;; This is not quite correct, so all newer KBs must use
  ;; make-comment-statement.
  `(data::documentation ,predicate ,string))

;; For working memory link

(defun make-in-kb-statement (form)
  (list (if (mixed-case?) 'data::inKB 'data::in-kb) form))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Handling temporal assumptions

(defun make-timestamped-assumption (conclusion)
  (list (if (mixed-case?) 'data::temporalCWA 'data::temporal-cwa)
        conclusion (get-universal-time)))


;;;; ---------------------------------------------------------------------------
;;; END OF CODE