Exercise (perhaps a trick question!): Provide a way to access the
current literal in an extended metafunction.

Solution:

We can already access the current literal.  Here's an example showing
how.

==================== Begin example ====================

(defevaluator my-ev my-ev-lst ((if x y z)))

(defun my-metafn (x mfc state)
  (declare (xargs :stobjs state
                  :verify-guards nil)
           (ignore state))
  (let* ((rcnst (access metafunction-context mfc :rcnst))
         (not-flg/atm (access rewrite-constant rcnst :current-literal))
         (atm (access current-literal not-flg/atm :atm)))
    (prog2$ (cw "Current literal:~%~x0~%Current term:~%~x1~%"
                atm
                x)
            x)))

(defthm my-meta-correct
  (equal (my-ev x a)
         (my-ev (my-metafn x mfc state) a))
  :rule-classes ((:meta :trigger-fns (nth))))

(defthmd mv-nth-is-nth
  (equal (mv-nth x y)
         (nth x y)))

(set-gag-mode nil)

; The following fails, but produces output of interest.
(thm (implies (and (true-listp x)
                   (true-listp y))
              (equal (mv-nth n (append (car (cons x x)) y))
                     uuu))
     :hints (("Goal" :do-not '(preprocess))
             ("Goal'" :in-theory (enable mv-nth-is-nth))))

==================== End example ====================

Here's some relevant output, which in fact shows that the rule
mv-nth-is-nth above has been applied while rewriting the conclusion of
the THM above -- the meta function's printing happens while in the
course of rewriting the NTH call resulting from the application of the
rule (i.e., an instance of the right-hand side of the rule).

Goal'
(IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y))
         (EQUAL (MV-NTH N (APPEND X Y)) UUU)).
Current literal:
(EQUAL (MV-NTH N (BINARY-APPEND X Y)) UUU)
Current term:
(NTH N (BINARY-APPEND X Y))