Working around restrictions on the use of evaluators in meta-level rules
See evaluator-restrictions for relevant background. For
examples of the use of transparent functions, see community-book file
A function is called a “transparent function symbol” when it is
We illustrate with a (contrived) example, which shows how declaring a function to be transparent can avoid an error. Consider what happens when we submit the following events in a fresh ACL2 session.
(defstub f0 (x) t) (encapsulate (((f1 *) => *) ((f2 *) => *)) (local (defun f1 (x) (f0 x))) (local (defun f2 (x) (f0 x))) (defthm f2-is-f1 (implies (f0 x) (equal (f2 x) (f1 x))) :rule-classes nil)) (defn g0 (x) x) (defattach f0 g0) (with-output :off :all ; avoid noisy output (defevaluator evl evl-list ((f0 x)))) (defn meta-fn1 (x) (if (f1 x) x x)) (defattach (f1 consp) (f2 consp)) (defthm thm1 (equal (evl x a) (evl (meta-fn1 x) a)) :rule-classes ((:meta :trigger-fns (nth))))
The final (defthm) event results in the following error.
ACL2 Error in ( DEFTHM THM1 ...): The proposed :META rule, THM1, is illegal because the attached function F0 is ancestral in both the evaluator and meta functions. See :DOC evaluator-restrictions and see :DOC transparent- functions. The following is an ancestor path from F0 to the meta function META-FN1, i.e., each function symbol is a supporter of the next: (F0 F1 META-FN1) The following is an ancestor path from F0 to the evaluator function EVL, i.e., each function symbol is a supporter of the next: (F0 EVL)
The events above make it clear that the alleged ancestor paths are indeed ancestor paths, in the sense that each function symbol in the path occurs in the definition or constraint for the function symbol immediately after it.
To avoid this error, we need to arrange that
(encapsulate (((f1 *) => * :transparent t) ((f2 *) => * :transparent t)) (local (defun f1 (x) (f0 x))) (local (defun f2 (x) (f0 x))) (defthm f2-is-f1 (implies (f0 x) (equal (f2 x) (f1 x))) :rule-classes nil))
We close with some restrictions pertaining to transparent function symbols.