Metafunction-context
A structure that holds data supporting extended meta reasoning
This advanced topic explains the mfc structure documented
elsewhere; see extended-metafunctions for prerequisite background.
This documentation is deliberately minimal, as we consider the mfc
structure to be implementation-level; comments in the source code may serve to
provide more information.
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
mfc-rw.
The mfc (metafunction-context) structure, which is given in the ACL2
sources by the form (defrec metafunction-context ...), currently has the
following fields. Each instance is constructed in the context where it is
needed, for example, during execution of a function that implements the ACL2
rewriter.
- ancestors: a list of terms assumed true, modified as we backchain
- backchain-limit: heuristic limit to backchaining
- fnstack: functions and terms currently being expanded — of
heuristic use only
- geneqv: a generated equivalence relation to maintain
- gstack: either nil or a goal stack, as in cw-gstack
- obj: this ``objective'' is either t, nil, or ? —
of heuristic use only.
- rcnst: a rewrite-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
only
- simplify-clause-pot-lst: a pot-lst of polynomials (poly
records)
- ttree: the evolving ttree describing the rewrites
- type-alist: a type-alist, representing assumptions governing
the current rewrite
- unify-subst: either nil or a unifying substitution used by the
rewriter
- wrld: 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 mv-nth-is-nth above has been applied while rewriting the conclusion
of the proposed theorem — 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))
