meta-extract.tex

Next we explain meta-extract by first giving two examples and then
summarizing the general forms of meta-extract hypotheses.

\subsection{Tutorial Examples}

We present two examples for the two kinds of meta-extract hypotheses,
corresponding to evaluation of calls of {\tt
  meta-extract-contextual-fact} and of {\tt meta-extract-global-fact}.
(Since a call {\tt (meta-extract-global-fact obj state)} is an
abbreviation for
% I tweaked the wording to fix an "Overfull \hbox" warning.
{\tt (meta-extract-global-fact+ obj state state)}, we are
thus effectively illustrating {\tt meta-extract-global-fact+} as
well.)

\subsubsection{Meta-extract-contextual-fact}

Our first example is intentionally contrived and quite trivial,
intended only to provide an easy introduction to meta-extract.  It
illustrates the use of {\tt meta-extract-contextual-fact}.  The intent
is to simplify any term of the form {\tt (nth $x$ $lst$)}, when $x$ is
easily seen by ACL2 to be a symbol in the current context, to {\tt
  (car $lst$)}.

In ACL2, the use of metafunctions is always supported by an evaluator,
called a {\em pseudo-evaluator} in the preceding section.  Let us
introduce an evaluator that ``knows'' about the functions relevant to
this example.

\begin{verbatim}
(defevaluator nthmeta-ev nthmeta-ev-lst
  ((typespec-check ts x)
   (nth n x)
   (car x)))
\end{verbatim}

\noindent Next we define a metafunction, intended to replace any term
{\tt (nth n x)} by a corresponding term {\tt (car x)} when {\tt n} is
known to be a symbol using
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_TYPE-SET}{\underline{type-set}}
reasoning.\footnote{For details such as the meaning of {\tt :forcep
    nil}, see the documentation for \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_META-EXTRACT}{\underline{meta-extract}}.}

\begin{verbatim}
(defun nth-symbolp-metafn (term mfc state)
  (declare (xargs :stobjs state))
  (case-match term
    (('nth n x)
     (if (equal (mfc-ts n mfc state :forcep nil)
                *ts-symbol*)
         (list 'car x)
       term))
    (& term)))
\end{verbatim}

\noindent When the input term matches {\tt (nth $n$ $x$)}, this calls
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_MFC-TS}{\underline{\tt
    mfc-ts}}
to deduce the possible types of $n$.  If that type-set equals {\tt
  *ts-symbol*} then that term must evaluate to a symbol, and the term
can be reduced to {\tt (car $x$)}.\footnote{Requiring the type-set to
  equal \texttt{*ts-symbol*} is an an unnecessarily strong check,
  chosen merely for ease of presentation: it requires that ACL2's
  determination of the term's possible types include all three of the
  basic
  types {\tt T}, {\tt NIL}, and non-Boolean symbols.}

Now we can present a meta rule with a meta-extract
hypothesis.  Without that hypothesis the formula below is
not a theorem, because the function {\tt mfc-ts} has no axiomatic
properties; all we know about it below is what we are told by the
meta-extract hypothesis, as discussed further below.

\begin{verbatim}
(defthm nth-symbolp-meta
    (implies (nthmeta-ev (meta-extract-contextual-fact `(:typeset ,(cadr term))
                                                       mfc
                                                       state)
                         a)
             (equal (nthmeta-ev term a)
                    (nthmeta-ev (nth-symbolp-metafn term mfc state) a)))
    :rule-classes ((:meta :trigger-fns (nth))))
\end{verbatim}

\noindent To see what the meta-extract hypothesis above gives us, consider the
following theorem provable by ACL2.

\begin{verbatim}
(equal (meta-extract-contextual-fact `(:typeset ,x)
                                      mfc
                                      state)
       (list 'typespec-check
             (list 'quote
                   (mfc-ts x mfc state :forcep nil))
             x))
\end{verbatim}

\noindent At a high level, this theorem shows us that {\tt
% Added words below to fix problem with right margin.
  meta-extract-contextual-fact} returns a term of the form {\tt
  (\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_TYPESPEC-CHECK}{\underline{typespec-check}} (quote $ts$) x)}, which asserts that the term {\tt
  x} belongs to the set of values represented by $ts$.  The
meta-extract hypothesis applies the pseudo-evaluator to this term, and
since {\tt typespec-\allowbreak{}check} is one of its known functions, the
hypothesis reduces to
\begin{verbatim}
  (typespec-check (mfc-ts (cadr term) mfc state :forcep nil)
                  (nthmeta-ev (cadr term) a)).
\end{verbatim}
\noindent The interesting case in proving our metafunction correct is
when this {\tt mfc-ts} call equals {\tt *ts-symbol*}.  In this case the hypothesis becomes
\begin{verbatim}
  (typespec-check *ts-symbol* (nthmeta-ev (cadr term) a))
\end{verbatim}
\noindent which, when expanded, implies that the evaluation of {\tt
  (cadr term)} must be a
symbol, which enables the proof of {\tt nth-symbolp-meta}.

% \begin{comment}
%   Do we need to discuss the application of the meta rule?  As
%   indicated in the introduction, nothing about the application of
%   metafunctions or clause processors has changed.

%   [Matt] Excellent point.  I've made this much shorter and explained
%   that it's just business as usual, since I think that's worth
%   emphasizing.  But if you want to delete all of it, please feel free;
%   in particular, we should delete it without a moment's thought if we
%   need the space.
% \end{comment}

Recall that meta-extract hypotheses do not affect the {\em
  applications} of meta rules; they only support their proofs.
Therefore, the following test of the example above yields no surprises.

\begin{verbatim}
(defstub foo (x) t)
(thm (implies (symbolp (foo x))
              (equal (nth (foo x) y) (car y)))
     :hints (("Goal" :in-theory '(nth-symbolp-meta))))
\end{verbatim}

%%% \noindent Indeed, the summary shows the use of the meta rule, {\tt
%%%   nth-symbolp-meta}.  We can even trace our metafunction: after
%%% evaluating the form
%%%
%%% \begin{verbatim}
%%% (trace$ (nth-symbolp-metafn
%%%          :entry
%%%          (list 'nth-symbolp-metafn term '<mfc> 'state)))
%%% \end{verbatim}
%%%
%%% \noindent we see the following in the proof log for the {\tt thm} call
%%% above.
%%%
%%% \begin{verbatim}
%%% 1> (NTH-SYMBOLP-METAFN (NTH (FOO X) Y)
%%%                        <MFC> STATE)
%%% <1 (NTH-SYMBOLP-METAFN (CAR Y))
%%% \end{verbatim}

\subsubsection{Meta-extract-global-fact}

Our second example is from community book
  ``demos/nth-update-nth-meta-extract.lisp'', which uses {\tt
% Reviewer 3 wanted to replace "by seeing" with "by understanding".
% That's OK, but for some reason I don't like the "sound" of that.  So
% I've changed it to "by considering", but feel free to change to
% whatever wording you prefer.
  meta-extract-global-fact}.  Let us begin by considering what problem this
book is attempting to solve.

% \begin{comment}
%   I like this section but it's pretty long --- about 3.5 pages.  Could
%   we omit the details about the macro that generalizes this to an
%   arbitrary stobj and just assert that it's easy to do?  I think most
%   people who will understand this paper could figure out how to do
%   that.

%   [Matt] Good idea -- I've done that, leaving only a brief description
%   of the macro.
% \end{comment}

Consider a
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_DEFSTOBJ}{\underline{\tt
    defstobj}} event, {\tt (defstobj st fld$_1$ fld$_2$ ... fld$_n$)}.
A common challenge in reasoning about stobjs is the simplification of
{\em read-over-write} terms, of the form {\tt (fld$_i$ (update-fld$_j$
  $v$ st))}, which indicate that we are to read {\tt fld$_i$} after
updating {\tt fld$_j$}.  That term simplifies to {\tt (fld$_i$ st)}
when $i \neq j$, and otherwise it simplifies to $v$.  How do we get
ACL2 to do such simplification automatically?  The following two
approaches are standard.

\begin{itemize}

\item Disable the stobj accessors and updaters after proving
  rewrite rules to simplify terms of the form {\tt (fld$_i$
    (update-fld$_j$ val st))}, to {\tt val} if $i = j$ and to {\tt
    (fld$_i$ st)} if $i \neq j$.

\item Let the stobj accessors and updaters remain enabled, relying on
  a rule such as the built-in rewrite rule {\tt nth-update-nth} to
  rewrite terms, obtained after expanding calls of the accessors and
  updaters, of the form {\tt (nth $i$ (update-nth $j$ val st))}.

\end{itemize}

\noindent The first of these requires $n^2$ rules, which is generally feasible
but can perhaps get somewhat unwieldy.  The second of these provides a
simple solution, but when proofs fail, the resulting checkpoints can
be more difficult to comprehend.

Here, we outline a solution that addresses both of these concerns: a
macro that generates a suitable meta rule.  Details of this proof
development may be found in community book
``demos/\allowbreak{}nth-update-nth-meta-extract.lisp''.
First we introduce our metafunction.  Next, we prove a meta rule for a
specific stobj.  Finally, we mention a macro that generates a version
of this rule that is suitable for an arbitrary specified stobj.

Our metafunction returns the input term unchanged unless it is of the
form {\tt ($r$ ($w$ $v$ $x$))}, where $r$ and $w$ are {\em reader}
(accessor) and {\em writer} (updater) functions defined to be calls of
{\tt nth} and {\tt update-nth}, on explicit indices: {\tt ($r$ $x$)}
$=$ {\tt (nth '$i$ $x$)} and {\tt ($w$ $v$ $x$)} $=$ {\tt (update-nth
  '$i$ $v$ $x$)}.  In that case, the function {\tt
  nth-update-nth-meta-fn-new-term} computes a new term: $v$ if $i =
j$, and otherwise, {\tt ($r$ $x$)}.

\begin{verbatim}
(defun nth-update-nth-meta-fn (term mfc state)
  (declare (xargs :stobjs state)
           (ignore mfc))
  (or (nth-update-nth-meta-fn-new-term term state)
      term))
\end{verbatim}

Notice below that in computing the new term, the definitions of the
reader and writer are extracted from the logical world using the
function, {\tt meta-extract-formula}, which returns the function's
definitional equation.  For example:

\begin{verbatim}
ACL2 !>(meta-extract-formula 'atom state)
(EQUAL (ATOM X) (NOT (CONSP X)))
ACL2 !>
\end{verbatim}

\noindent We thus rely on the correctness of {\tt
  meta-extract-formula} for the equality of the input term and the
term returned by the following function.

\begin{Verbatim}[commandchars=\\\{\},fontsize=\small]
(defun nth-update-nth-meta-fn-new-term (term state)
  (declare (xargs :stobjs state))
  (case-match term
    ((reader (writer val x))
     (and (not (eq reader 'quote))
          (not (eq writer 'quote))
          (let* ((reader-formula (and (symbolp reader)
                                      (meta-extract-formula reader state)))
                 (i-rd (fn-nth-index reader reader-formula)))
            (and
             i-rd {\em ; the body of reader is (nth 'i-rd ...)}
             (let* ((writer-formula (and (symbolp writer)
                                         (meta-extract-formula writer state)))
                    (i-wr (fn-update-nth-index writer writer-formula)))
               (and
                i-wr {\em ; the body of writer is (update-nth 'i-wr ...)}
                (if (eql i-rd i-wr)
                    val
                  (list reader x))))))))
    (& nil)))
\end{Verbatim}

Next we introduce a (pseudo-)evaluator to use in our meta rule.

\begin{verbatim}
(defevaluator nth-update-nth-ev nth-update-nth-ev-lst
  ((nth n x)
   (update-nth n val x)
   (equal x y)))
\end{verbatim}

We need to define one more function before presenting our meta rule.
It takes as input a term {\tt ($f$ $t_1$ $\ldots$ $t_n$)} with list of
formals {\tt ($v_1$ $\ldots$ $v_n$)}, and builds an alist that maps
each $v_i$ to the value of $t_i$ in a given alist.  Like our
metafunction, it consults {\tt meta-extract-formula} to obtain the
formal parameters of $f$.  An earlier attempt to use the function,
{\tt formals}, failed: the meta rule's proof needs these formals to
connect to those found by our metafunction.

\begin{Verbatim}[commandchars=\\\{\},fontsize=\small]
(defun meta-extract-alist-rec (formals actuals a)
  (cond ((endp formals) nil)
        (t (acons (car formals)
                  (nth-update-nth-ev (car actuals) a)
                  (meta-extract-alist-rec (cdr formals) (cdr actuals) a)))))

(defun meta-extract-alist (term a state)
  (declare (xargs :stobjs state :verify-guards nil))
  (let* ((fn (car term))
         (actuals (cdr term))
         (formula (meta-extract-formula fn state)) {\em ; (equal (fn ...) ...)}
         (formals (cdr (cadr formula))))
    (meta-extract-alist-rec formals actuals a)))
\end{Verbatim}

\noindent We now define a stobj and prove a corresponding meta rule.

\begin{Verbatim}[commandchars=\\\{\},fontsize=\small]
(defstobj st
  fld1 fld2 fld3 fld4 fld5 fld6 fld7 fld8 fld9 fld10
  fld11 fld12 fld13 fld14 fld15 fld16 fld17 fld18 fld19 fld20)

(defthm nth-update-nth-meta-rule-st
  (implies
   (and (nth-update-nth-ev {\em ; (f (update-g val st))}
         (meta-extract-global-fact (list :formula (car term)) state)
         (meta-extract-alist term a state))
        (nth-update-nth-ev {\em ; (update-g val st)}
         (meta-extract-global-fact (list :formula (car (cadr term)))
                                   state)
         (meta-extract-alist (cadr term) a state))
        (nth-update-nth-ev {\em ; (f st) -- note st is (caddr (cadr term))}
         (meta-extract-global-fact (list :formula (car term)) state)
         (meta-extract-alist (list (car term)
                                   (caddr (cadr term)))
                             a state)))
   (equal (nth-update-nth-ev term a)
          (nth-update-nth-ev (nth-update-nth-meta-fn term mfc state) a)))
  :hints ...
  :rule-classes ((:meta :trigger-fns (fld1 fld2 ... fld20))))
\end{Verbatim}

\noindent The proof of the theorem below takes no measurable time, and
applies the metafunction proved correct above.

\begin{verbatim}
   (in-theory (disable fld1 ... fld20 update-fld1 ... update-fld20))

   (defthm test1
     (equal (fld3 (update-fld1 1
                   (update-fld2 2
                    (update-fld3 3
                     (update-fld4 4
                      (update-fld3 5
                       (update-fld6 6 st)))))))
            3))
\end{verbatim}

Notice that there is nothing about the meta rule above that is
specific to the particular stobj, {\tt st}, except for the {\tt
  :trigger-fns} that it specifies.  In the community book mentioned
above (``demos/nth-\allowbreak{}update-\allowbreak{}nth-\allowbreak{}meta-\allowbreak{}extract.lisp''), we define a macro
that automates the generation of such a meta rule for an
arbitrary stobj.  Our macro takes the name of a stobj, $s$, and does two
things: it disables all of the stobj's accessors and updaters, and it
proves a meta rule that simplifies every term of the form {\tt ($r$
  ($w$ $v$ $s$))}, where $r$ and $w$ are an accessor and updater,
respectively, for the stobj $s$.

The meta rule above uses three \texttt{meta-extract-global-fact}
hypotheses corresponding to uses of three particular facts.
Enumerating all of the facts potentially used in the metafunction in
this way could easily become unwieldy; in Section \ref{sec:user} we
discuss a utility that solves this problem, allowing one
\texttt{meta-extract-global-fact} hypothesis and one
\texttt{meta-extract-contextual-fact} hypothesis to cover all of the
facts that might be used.

%%% We omit some details here, including
%%% the definition of function {\tt stobj-accessors-and-updaters}, which
%%% as its name suggests, returns a list of all stobj accessors and
%%% updaters for a given stobj.
%%%
%%% \begin{Verbatim}[commandchars=\\\{\},fontsize=\small]
%%% (defthm nth-update-nth-meta-level
%%%   {\em{<same formula as in meta rule above>}}
%%%   :hints (("Goal" :in-theory (enable nth-update-nth-ev-constraint-0)))
%%%   :rule-classes nil)
%%%
%%% (defmacro make-nth-update-nth-meta-stobj (stobj-name)
%%%   `(make-event
%%%     (let ((fns (and (symbolp ',stobj-name)
%%%                     (stobj-accessors-and-updaters ',stobj-name (w state))))
%%%           (theorem-name ...))
%%%       (cond
%%%        ((null fns) {\em <error>})
%%%        (t (value `(progn
%%%                     (in-theory (disable ,@fns))
%%%                     (defthm ,theorem-name
%%%                       {\em{<same formula as in meta rule above>}}
%%%                       :hints (("Goal" :by nth-update-nth-meta-level))
%%%                       :rule-classes ((:meta :trigger-fns ,fns))))))))))
%%% \end{Verbatim}
%%%
%%% The following test succeeds, proving almost instantly by application
%%% of our metafunction.
%%%
%%% \begin{verbatim}
%%% (defstobj st$
%%%   fld$1 fld$2 fld$3 fld$4 fld$5 fld$6 fld$7 fld$8 fld$9 fld$10)
%%%
%%% (make-nth-update-nth-meta-stobj st$)
%%%
%%% (defthm test2
%%%   (equal (fld$3 (update-fld$1 1
%%%                  (update-fld$2 2
%%%                   (update-fld$3 3
%%%                    (update-fld$4 4
%%%                     (update-fld$3 5
%%%                      (update-fld$6 6 st$)))))))
%%%          3))
%%% \end{verbatim}

\subsection{General Forms}
\label{sec:general}

In this section we summarize briefly the forms of meta-extract
hypotheses.  Additional details may be found in the documentation for
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_META-EXTRACT}{\underline{meta-extract}}.
% These forms correspond to the theorems described at the end of
% Section~\ref{sec:user}.

Below, let {\tt evl} be the pseudo-evaluator (see
Section~\ref{sec:intuitive}) used in a meta rule.  The two primary
forms of meta-extract hypotheses that can be used in a meta rule are
as follows.  In the first, {\tt aa} represents an arbitrary term; in
the second, {\tt a} must be the second argument of the two calls of
the pseudo-evaluator in the conclusion of the theorem.

\begin{verbatim}
    (evl (meta-extract-global-fact obj state) aa)
    (evl (meta-extract-contextual-fact obj mfc state) a)
\end{verbatim}

The second form above is only legal for meta rules about extended
metafunctions (which take arguments {\tt mfc} and {\tt state}).  The
first form above is actually equivalent to the first form below, which
in turn is a special case of the second form below.

\begin{verbatim}
    (evl (meta-extract-global-fact+ obj state state) aa)
    (evl (meta-extract-global-fact+ obj st state) aa)
\end{verbatim}

The last form supports clause processors that modify state as long as
they do not change the logical world; it produces the same value as
the previous form as long as both {\tt st} and {\tt state} have equal
world fields.

If the arguments to the meta-extract-* function are somehow malformed,
then it returns the trivial term {\tt 'T}, which is not of any use in
proving a metafunction correct.  Otherwise, each invocation produces a
term that states the ``correctness'' of an invocation of some
utility, such as {\tt mfc-rw+} or {\tt meta-\allowbreak{}extract-\allowbreak{}formula}.  The
terms produced for different kinds of invocation vary according to the
particular concept of correctness appropriate to the utility in
question.


%%% \begin{comment}
%%%   I think it would be nice to explain a little bit more in these
%%%   listings rather than just describing exactly the term that each
%%%   invocation produces.  Ideally I think we should convey for each form:
%%%   \begin{itemize}
%%%   \item what utility it allows metafunctions to use
%%%   \item how the term that is produced implies the ``correctness'' of
%%%     an invocation of that utility
%%%   \item why we believe the term produced to always be true.
%%%   \end{itemize}
%%%   I've done a pass to move toward this, but you can revert to your
%%%   previous version if you'd rather continue from that point...
%%% \end{comment}
% -- Agreed!  Nicely done; thanks.

We now describe the allowed {\tt obj} arguments to {\tt
  meta-extract-global-fact} and the terms they produce.  The
documentation for
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_EXTENDED-METAFUNCTIONS}{\underline{extended-metafunctions}}
explains meta-level functions discussed below, such as {\tt mfc-rw}
and {\tt mfc-ap}.

\begin{itemize}

\item {\tt (:formula $f$)} produces the value of {\tt
    (meta-extract-formula $f$ state)}, which allows metafunctions to
  assume that any invocation of {\tt meta-extract-formula} produces a
  true formula.  {\tt Meta-extract-formula} looks up various kinds of
  formulas from the world:
  \begin{itemize}
  \item the body of $f$ if it is a theorem name
  \item the definitional equation of $f$ if it is a defined function
  \item the constraint of $f$ if it is a constrained function
  \item the defchoose axiom of $f$ if it is a \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_DEFCHOOSE}{\underline{\tt defchoose}} function.
  \end{itemize}

% Reviewer 1 says this about the next item:
%%% page 8, (:lemma f n): is there a reason why this only applies to rewrite rules,
%%% and not to other kinds of rules?
% I think the answer is that :formula (above) already obtains
% theorems, but sometimes one wants to grab a rewrite rule.  I confess
% that I don't know why offhand.  Sol, if you have a quick explanation
% for why :lemma gives us something useful that :formula doesn't
% easily give us, that might be good to add below.

\item {\tt (:lemma $f$ $n$)} produces a term corresponding to the
  $n$th rewrite rule stored in the {\tt lemmas} property of function
  $f$, which allows any such rule to be assumed correct in a
  metafunction.  The term returned is the value of
  \begin{lstlisting}[basicstyle=\linespread{0.4}\normalsize\ttfamily]
    (rewrite-rule-term (nth '<$n$> (getpropc '<$f$> 'lemmas nil (w state))))<\textrm{,}>
  \end{lstlisting}
  assuming that $n$ is a valid index (does not exceed
  the length of the indicated list).  Here {\tt rewrite-\allowbreak{}rule-\allowbreak{}term}
  transforms a {\tt rewrite-rule} record structure into a term such as
  \begin{lstlisting}[basicstyle=\linespread{0.4}\normalsize\ttfamily]
    (implies <$\var{hyps}$> (<$\var{equiv}$> <$\var{lhs}$> <$\var{rhs}$>))<\textrm{.}>
  \end{lstlisting}
  The rewrite rules stored in {\tt :lemmas} are not simply theorem
  bodies, which could be accessed using {\tt meta-extract-formula},
  but rewrite rule structures, which separately store the left-hand
  side, right-hand side, equivalence relation, and hypotheses, and
  also contain heuristic information such as the backchain limits and
  match-free mode.

\item {\tt (:fncall $f$ $L$)} produces a term {\tt (equal $c$ '$v$)}, where
    $c$ is the call that applies $f$ to the quotations of the values in argument list $L$, and $v$ is
    the value of that call computed by
    \href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_MAGIC-EV-FNCALL}{\underline{\tt
        magic-\allowbreak{}ev-\allowbreak{}fncall}}.  This allows
    metafunctions to assume that {\tt magic-ev-fncall}
    correctly evaluates function applications.

\end{itemize}

The allowed {\tt obj} arguments to {\tt meta-extract-contextual-fact} are as follows.

\begin{itemize}

\item {\tt (:typeset $\var{term}$)} produces a term stating the correctness of
    the type-set produced by {\tt mfc-ts} for $\var{term}$.  Specifically, it produces the term
    {\tt (typespec-check '$\var{ts}$ $\var{term}$)}, where $\var{ts}$ is
    the result of {\tt (mfc-ts $\var{term}$ mfc state :forcep nil :ttreep nil)} and
    {\tt (typespec-check ts val)} is true when {\tt val}'s actual type is in the type-set {\tt ts}.

  \item {\tt (:rw+ $\var{term}\ \var{alist}\ \var{obj}\ \var{equiv}$)}
    produces a term stating that {\tt mfc-rw+} correctly rewrites
    $\var{term}$ under substitution $\var{alist}$ with objective
    $\var{obj}$ under equivalence relation $\var{equiv}$.  The form of the term produced is
  \begin{lstlisting}[basicstyle=\linespread{0.4}\normalsize\ttfamily]
    (<$\var{equiv}$> <$\var{term}'$> <$\var{rw}$>)
  \end{lstlisting}
  where $\var{term}'$ is the new term formed by substituting
  $\var{alist}$ into $\var{term}$ and $\var{rw}$ is the result of the call
  {\tt (mfc-rw+ $\var{term}\ \var{alist}\ \var{obj}\ \var{equiv}$ mfc state :forcep nil :ttreep nil)}.
% Modified words below to fix problem with right margin, though I
% changed it a bit more than just for that.
  The $\var{equiv}$ argument may also be {\tt T}, meaning
  {\tt IFF}, or {\tt NIL}, meaning {\tt EQUAL}.

\item {\tt (:rw $\var{term}\ \var{obj}\ \var{equiv}$)} is similar to the
  {\tt :rw+} form above, but instead of {\tt mfc-rw+} it supports {\tt
    mfc-rw}, which takes no $\var{alist}$ argument.  Instead, {\tt
    NIL} is used for the substitution.

\item {\tt (:ap $\var{term}$)} uses {\tt mfc-ap} to derive a linear
  arithmetic contradiction indicating that $\var{term}$ is false, and
  produces {\tt (not $\var{term}$)} if that is successful, that is, if
  {\tt (mfc-ap $\var{term}$ mfc state :forcep nil)} returns true;
  otherwise it just produces {\tt 'T}.

\item {\tt (:relieve-hyp $\var{hyp}\ \var{alist}\ \var{rune}\
    \var{target}\ \var{backptr}$)} uses {\tt mfc-relieve-hyp} to
  attempt to prove that $\var{hyp}$ holds under substitution
  $\var{alist}$, and produces the substitution of
  $\var{alist}$ into $\var{hyp}$ if successful, that is, if
  {\tt (mfc-relieve-hyp $\var{hyp}\ \var{alist}\ \var{rune}\
    \var{target}\ \var{backptr}$ mfc state :forcep nil :ttreep nil)}
  returns true; otherwise, {\tt 'T}.

\end{itemize}

%%%\begin{comment}
%%%
%%%  We had discussed including some sort of correctness argument here.
%%%  But Section~\ref{sec:intuitive} already gives a nice high-level
%%%  correctness argument, and a detailed argument is given in the ACL2
%%%  sources, in the Essay on Correctness of Meta Reasoning.  With some
%%%  effort I could probably write a few remarks here on some of the
%%%  issues addressed in that correctness argument.  But I'm not sure
%%%  anyone would care.  Instead,
%%%
%%%  [Sol] -- I agree; I don't think we need to include a more detailed
%%%  proof of correctness here.  If we do our job right above then
%%%  readers can see why we believe each term produced by the
%%%  meta-extract-* functions to be true.
%%%\end{comment}

We have seen there are two forms of meta-extract hypotheses: {\tt
  meta-extract-contextual-fact} and {\tt meta-extract-global-fact+}
(and its less general form, {\tt meta-extract-global-fact}).  We could
have split each of these into several forms, resulting in eight forms
for the eight kinds of values of {\tt obj} listed above.  However, in
the next section we describe a utility that essentially generalizes
the two supported forms, which eliminates the need for the user to
think about the precise values of {\tt obj}; it was convenient to
generalize two supported forms rather than eight.