		Search-engine friendly clone of the ACL2 documentation.

Meta

Transparent-functions

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 books/system/tests/transparent-functions-input.lsp, with corresponding output in file transparent-functions-log.txt in the same directory.

A function is called a “transparent function symbol” when it is declared with :transparent t in a signature of an encapsulate event. By thus declaring a function to be transparent, you are modifying the notion of “ancestor” of a meta-level function as follows, for purposes of the ancestor restriction described in evaluator-restrictions: when a transparent function f has an attachment g (see defattach), then g is the sole ancestor (supporter) of f.

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 f0 is no longer a common ancestor of meta-fn1 and evl. The notion of ancestor doesn't change for the path leading to the evaluator function; but for the path leading to the meta function, a transparent function symbol has its attachment as its ancestor instead of the function symbols in its constraint. In particular, f1 normally has f0 as an ancestor, since f0 occurs in the constraint on f1; but if f1 is transparent and has an attachment, then its attachment is the sole ancestor of f0, as though f1 had been defined to be f0. Thus, if we replace the encapsulate event in our example simply by declaring its signature functions to be transparent, as follows, then the error disappears.

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

If any function is declared with :transparent t in the signatures of an encapsulate event, then all must be.
If any function is declared with :transparent t in the signatures of an encapsulate event, then every signature in a superior or inferior encapsulate event must also specify :transparent t.
The value of the :transparent keyword in a signature must be t or the default, nil.
The signatures of a partial-encapsulate (or of any encapsulate with a call of set-unknown-constraints-supporters) must not specify :transparent t in its signatures.
When a defattach event attaches to a transparent function symbol f, that event must attach to every function symbol constrained in an encapsulate with f, and only to such function symbols. The same holds for unattaching in place of attaching.