		Search-engine friendly clone of the ACL2 documentation.

Set-skip-meta-termp-checks

Skip output checks for meta functions and clause-processors

WARNING: Use of this macro may render ACL2 unsound, which is why it requires a trust tag. If you obtained an error during application of a metafunction, a hypothesis metafunction, or a clause-processor, it might well be best to rewrite that function to avoid generating terms with the ``forbidden'' function calls described in that error message. However, judicious use of this macro can be useful during development; the rest of this topic describes its usage.

The result of applying a metafunction (or a hypothesis metafunction) must be a term. Similarly, the result of applying a clause-processor must be a list of clauses, where a clause is a list of terms (see clause). If these conditions fail, then an error occurs; see term-table for how one obtains some assistance towards avoiding such errors.

By default, ACL2 actually enforces a stronger requirement: the resulting term or clause-list cannot contain any calls of ``forbidden'' function symbols: ones that would be illegal when submitting a theorem. These include function symbols that are untouchable (see remove-untouchable) as well as those that are keys of the alist *ttag-fns*.

These two checks — that the results are terms and that they contain no calls of forbidden function symbols — can be expensive for large terms. The macro set-skip-meta-termp-checks provides a way to avoid both checks. Since these checks can be critical for soundness, a trust tag (see defttag) must be active in order to invoke this macro unless the argument is nil. It might be best to avoid using this macro except to skip such checks that you have identified to be expensive, and to skip them only when using ACL2 interactively (as opposed to doing batch certification jobs) — though this macro might also be useful in determining when such checks are indeed expensive.

There are two legal ways to call this macro, as follows. Note that the arguments are not evaluated.

; Skip all such checks:
(set-skip-meta-termp-checks t)

; Skip such checks for functions fn1, ..., fnk (each of which is presumably a
; metafunction, hypothesis metafunction, or clause-processor):
(set-skip-meta-termp-checks (fn1 ... fnk))

A special case of the second form above is to perform all such checks: (set-skip-meta-termp-checks nil). No trust tag is required in this case.

This macro actually generates a local table event, for the table skip-meta-termp-checks-table and its unique key, t. The macro set-skip-meta-termp-checks generates a corresponding non-local table event.

ACL2 !>:trans1 (set-skip-meta-termp-checks (f g))
 (LOCAL (SET-SKIP-META-TERMP-CHECKS! (F G)))
ACL2 !>:trans1 (set-skip-meta-termp-checks! (f g))
 (TABLE SKIP-META-TERMP-CHECKS-TABLE T '(F G))
ACL2 !>

It is probably good practice to use set-skip-meta-termp-checks rather than set-skip-meta-termp-checks!, except when there is a compelling reason to do otherwise.