A structure that holds data supporting extended meta reasoning

This advanced topic explains the

**WARNING!** This is a data structure that supports the ACL2
implementation. While it is highly stable in practice, there is no guarantee
that future ACL2 implementations will avoid changing it. Use it at your own
(perhaps small) risk! If you want to avoid all such risk, use the interfaces
described in the documentation for extended-metafunctions, such as

The

ancestors : a list of terms assumed true, modified as we backchainbackchain-limit : heuristic limit to backchainingfnstack : functions and terms currently being expanded — of heuristic use onlygeneqv : a generated equivalence relation to maintaingstack : eithernil or a goal stack, as in cw-gstackobj : this ``objective'' is eithert ,nil , or? — of heuristic use only.rcnst : arewrite-constant record that holds many fields to be accessed by the ACL2 rewriter. See the definition(defrec rewrite-constant ...) , including comments therein, in the ACL2 sources.rdepth : maximum allowed rewrite stack depth — of heuristic use onlysimplify-clause-pot-lst : a pot-lst of polynomials (poly records)ttree : the evolving ttree describing the rewritestype-alist : a type-alist, representing assumptions governing the current rewriteunify-subst : eithernil or a unifying substitution used by the rewriterwrld : the current ACL2 world

Here is an example of the use of these fields, which shows how to access the literal of the clause (goal) under which the current rewrite is taking place.

(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) (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))))

Here is some relevant output from the thm call, which shows that 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))