mfc-utils - ACL2 Book

other

(in-package "ACL2")

other

(program)

mfc-rcnstfunction

(defun mfc-rcnst
  (mfc state)
  (declare (xargs :stobjs state)
    (ignore state))
  (access metafunction-context mfc :rcnst))

mfc-current-literalfunction

(defun mfc-current-literal
  (mfc state)
  (declare (xargs :stobjs state))
  (let ((rcnst (mfc-rcnst mfc state)))
    (access rewrite-constant rcnst :current-literal)))

rewriting-positive-literal-fnfunction

(defun rewriting-positive-literal-fn
  (term mfc state)
  (declare (xargs :stobjs state))
  (and (or (equal (mfc-current-literal mfc state) (cons nil term)))
    (or (null (mfc-ancestors mfc)))))

rewriting-positive-literalmacro

(defmacro rewriting-positive-literal
  (term)
  `(syntaxp (rewriting-positive-literal-fn ,TERM mfc state)))

rewriting-negative-literal-fnfunction

(defun rewriting-negative-literal-fn
  (term mfc state)
  (declare (xargs :stobjs state))
  (and (or (equal (mfc-current-literal mfc state) (cons t term)))
    (or (null (mfc-ancestors mfc)))))

rewriting-negative-literalmacro

(defmacro rewriting-negative-literal
  (term)
  `(syntaxp (rewriting-negative-literal-fn ,TERM mfc state)))

print-mfcfunction

(defun print-mfc
  (name mfc state)
  (declare (xargs :stobjs state)
    (ignore state))
  (cw "~x0 mfc: ~X12~%"
    name
    mfc
    (evisc-tuple nil
      nil
      `((,(ACCESS METAFUNCTION-CONTEXT MFC :WRLD) . "<world>") (,(ACCESS REWRITE-CONSTANT (ACCESS METAFUNCTION-CONTEXT MFC :RCNST)
         :CURRENT-ENABLED-STRUCTURE) "<ens>"))
      nil)))