polarity - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "translate")

include-book

(include-book "kestrel/terms-light/sublis-var-simple" :dir :system)

mfc-rcnst2function

(defun mfc-rcnst2
  (mfc)
  (declare (xargs :mode :program))
  (access metafunction-context mfc :rcnst))

mfc-current-literal2function

(defun mfc-current-literal2
  (mfc)
  (declare (xargs :mode :program))
  (let ((rcnst (mfc-rcnst2 mfc)))
    (access rewrite-constant rcnst :current-literal)))

want-to-strengthen-fnmutual-recursion

(mutual-recursion (defun want-to-strengthen-fn
    (term mfc state)
    (declare (xargs :stobjs state
        :mode :program :guard (and (true-listp mfc) (pseudo-termp term))))
    (if (and (consp term) (eq 'not (ffn-symb term)))
      (want-to-weaken-fn (fargn term 1) mfc state)
      (and (not (mfc-ancestors mfc))
        (let* ((term (translate-term term 'want-to-strengthen (w state))) (unify-subst (mfc-unify-subst mfc))
            (term (sublis-var-simple unify-subst term))
            (not-flg/atm (mfc-current-literal2 mfc))
            (not-flg (car not-flg/atm))
            (current-literal-core (cdr not-flg/atm)))
          (and not-flg (equal term current-literal-core))))))
  (defun want-to-weaken-fn
    (term mfc state)
    (declare (xargs :stobjs state
        :mode :program :guard (and (true-listp mfc) (pseudo-termp term))))
    (if (and (consp term) (eq 'not (ffn-symb term)))
      (want-to-strengthen-fn (fargn term 1) mfc state)
      (and (not (mfc-ancestors mfc))
        (let* ((term (translate-term term 'want-to-weaken (w state))) (unify-subst (mfc-unify-subst mfc))
            (term (sublis-var-simple unify-subst term))
            (not-flg/atm (mfc-current-literal2 mfc))
            (not-flg (car not-flg/atm))
            (current-literal-core (cdr not-flg/atm)))
          (and (not not-flg) (equal term current-literal-core)))))))

want-to-strengthenmacro

(defmacro want-to-strengthen
  (term)
  `(want-to-strengthen-fn ',TERM mfc state))

want-to-weakenmacro

(defmacro want-to-weaken
  (term)
  `(want-to-weaken-fn ',TERM mfc state))