Some built-in programming utilities pertaining to the ACL2 system
Since the ACL2 system is written in itself, the source code defines
many utilities that support the ACL2 implementation. Some of these have been
found to be useful not only to the ACL2 developers, but to those who use ACL2
to perform tasks other than the traditional ones: writing and submitting
definitions, and proving theorems about the functions defined.
This topic provides a summary of some of those utilities that are built
into the ACL2 system. It is intended to be a growing document, with
contributions from those in the community who find such utilities that benefit
them. It has already grown substantially from an initial version created by
the ACL2 implementors, and others will likely continue to add to it over
WARNING 1. Some system utilities are in :program mode,
and for many of those, guards are incomplete or missing entirely.
Incorrect use of such utilities can thus lead to scary (though often harmless)
raw Lisp errors! Although this situation may improve over time, for now users
of these utilities must cope with that danger just as the ACL2 implementors
cope with it, which is by understanding the requirements on each utility that
is invoked. For example, if you incorrectly invoke (untranslate (cons 3 4)
nil (w state)), where perhaps (untranslate '(cons '3 '4) nil (w state))
was intended, then the resulting raw Lisp error is your responsibility for
invoking untranslate on the object (3 . 4) instead of the term
(cons '3 '4).
WARNING 2. These utilities are subject to change. They were
developed to support the ACL2 system, and as ACL2 evolves, its developers
claim the right to modify these functions — even their input-output
signatures. That said, changes to these functions are likely to be
The ACL2 system comes with substantial comments. As of Version_7.1 (May,
2015), out of slightly under 10 MB of source code (not including 4.8 MB of
documentation topics), nearly 400 KB (just over 40%) were comment
lines. This topic is not intended to supplant or duplicate those comments,
but rather, only to note system utilities of interest to the community. If
you find the source comments inadequate, please feel free to ask the system
implementors to make corresponding additions to the source code comments.
Note that if you execute the command
egrep -e '^; Essay on' *.lisp
in your ACL2 sources directory, you will see the names of more than 90 long
source comments, or ``Essays'', that can provide additional background.
Also see programming and its subtopics, in particular programming-with-state, which describes many built-in system
utilities. For example, a subsection of programming-with-state,
entitled ``SEQUENTIAL PROGRAMMING'', introduces handy utilities pprogn
and er-progn along with links to their documentation. You may also
wish to see system-attachments for how to make a few changes to the
behavior of ACL2.
Here is another option for finding a buit-in system utility: As ACL2
developers sometimes do, use meta-. or meta-x tags-apropos in Emacs
to find utilities with given substrings in their names. For example, if in
Emacs you submit the command meta-x tags-apropos and reply pwd at
the prompt, you'll find a raw Lisp function our-pwd that ACL2 defines as
an analogue to the Linux pwd command; and, with meta-x tags-search
applied to (our-pwd, you can see how ACL2 source code uses this
List of a few built-in system utilities
Every function mentioned below belongs in the constant *ACL2-system-exports*. Also see ACL2-built-ins for built-in utilities
that are less relevant to the ACL2 system, and see programming for
utilities in general.
- (acl2-unwind-protect expl body cleanup1 cleanup2): This particularly
sophisticated utility (warning: for advanced system hackers) is logically just
the following (where the formals shown above are capitalized).
(mv-let (erp val state)
(cond (erp (pprogn CLEANUP1 (mv erp val state)))
(t (pprogn CLEANUP2 (mv erp val state)))))
However, aborts are typically handled by causing the ``cleanup'' forms to be
executed, in the spirit of Common Lisp's unwind-protect. In typical use
the cleanup forms restore the values of state global variables that
were ``temporarily'' set by body. Note that expl is essentially
ignored. For more information see the Essay on Unwind-Protect in the ACL2
- (add-suffix sym str): Extend a symbol sym with a suffix
expressed as a string str. The resulting symbol is in the same package
as the original symbol. For instance, (add-suffix 'abc "DEF") results
in the symbol 'abcdef, in the same package as 'abc. See add-suffix-to-fn for a variant that may be more appropriate for generating
new function names.
- (add-suffix-to-fn sym suffix): Variant of add-suffix that
puts the new symbol in the "ACL2" package when sym is in the
"COMMON-LISP" package. New function symbols cannot be in the
"COMMON-LISP" package; thus, this utility may be appropriate when
generating new function names from old ones.
- (all-attachments wrld): Return a list of all attachment pairs (f
. g) where g is attached to f (see defattach) in the world, wrld, except for two cases that are ignored for this purpose:
[warrant]s, and attachments introduced with a non-nil value of
:skip-checks. To obtain the attachment to a function symbol f,
without the restrictions above and with value nil if there is no
attachment to f, evaluate (cdr (attachment-pair 'f wrld)). To
obtain the list of all built-in attachments, evaluate (global-val
'attachments-at-ground-zero (w state)).
- (all-calls names term alist ans): Accumulate into ans
(which typically is nil at the top level) all pseudo-terms u/alist
such that for some f in the list, names, u is a subterm of the
pseudo-term, term, that is a call of the symbol, f. Note that
(all-calls-lst names lst alist ans) is similar, except for a list,
lst, of terms in place of a single term, term.
- (all-ffn-symbs term ans): Accumulate into ans
(which typically is nil at the top level) all function symbols called in
the given term. This may become deprecated, and is just a macro expanding to
a corresponding call of all-fnnames1; see all-fnnames,
all-fnnames-lst, and all-fnnames1, below.
- (all-ffn-symbs-lst lst ans): Accumulate into ans
(which typically is nil at the top level) all function symbols called in
the given list of terms. This may become deprecated, and is just a macro
expanding to a corresponding call of all-fnnames1; see all-fnnames,
all-fnnames-lst, and all-fnnames1, below.
- (all-fnnames term): Return a list of all function symbols called in
the given term. This is a macro call expanding to (all-fnnames1 nil term
- (all-fnnames-lst lst): Return a list of all function symbols called
in the given list of terms. This is a macro call expanding to
(all-fnnames1 t lst nil).
- (all-fnnames1 flg x acc): Accumulate into acc the function
symbols called in the given term or list of terms, x, according to
whether flg is nil (for a term) or not nil (for a list of
- (all-vars x): For a pseudo-termp x, return a
duplicate-free list of all variables in x, in reverse print order of
first occurrence. For example, all-vars of '(f (g a b) c) is '(c
- (arglistp lst): Return true iff lst is a nil-terminated
list of distinct, legal variable names, usable as the formal argument
list (hence the name of this utility) of a function.
- (arity fn w): For a function symbol or lambda expression fn
of world w, return the number of its formal parameters.
- (body fn normalp w): Fn should either be a :logic-mode function symbol of world w or a lambda
expression. If fn is a symbol and normalp is nil, then return
the body (translated but unnormalized) of its original definition. If fn
is a lambda expression, return its body. We now discuss the remaining
case, where fn is a :logic-mode function symbol and
normalp is true. In the usual case that no definition rule has
been introduced for fn with a non-nil value of
:install-body (which is the default), return the normalized body
from the defun form that introduced fn, or nil if fn was
not introduced with defun (as with encapsulate, defstub,
or defchoose) — except that in the case that :normalize nil
was specified in that defun form (see xargs), return the
unnormalized body. The remaining case is that at least one definition
rule for fn has been installed. In that case, the latest such rule
provides the body (see source function latest-body for how hypotheses are
handled), with one exception: if the equivalence relation for that rule is
other than equal, then the unnormalized body is returned.
- (conjoin lst): The conjunction of the given list of terms.
- (conjoin2 term1 term2): The conjunction of the given two terms.
- (cons-term fn args): Returns a term with function symbol (or
lambda expression) fn and arguments args. Evaluation may be
performed for calls of primitives — that is, built-in functions without
definitions — on arguments that are quoted constants, for example as
ACL2 !>(cons-term 'coerce (list ''"abc" ''list))
'(#\a #\b #\c)
To avoid such evaluation, use fcons-term (``fast cons-term''), described
below. Also see cons-term* and fcons-term* below.
- (cons-term* fn arg1 arg2 ...): This variant of cons-term
(described above) returns a term with the indicated function and arguments,
where the arguments are ``spread'' into individual actual parameters rather
than provided as a list. Some simplification may be done; to avoid that, use
fcons-term*. Also see cons-term above and fcons-term
- (default-state-vars state-p &key ...): Returns a record suitable as
an argument for some utilities that take the world as an argument but
not the state, such as translate-cmp. That record provides values
for certain state global variables (which are not stored in the world), such
as guard-checking-on (which holds the guard-checking mode). As
described below, default-state-vars provides suitable defaults, which
however can be modified by supplying keyword arguments corresponding to
certain state globals, such as :guard-checking-on. When the required
argument is t, those defaults are the values of those state globals;
thus, t is probably the right value to use for that argument when the
state is available in the calling context. Otherwise, those defaults are the
values commonly found in those state globals.
- (defined-constant name w): If name is t, nil, or
defined using defconst, return (quote val) where val is the
value of name; otherwise return nil.
- (defun-mode fn w): If fn is a function symbol, return the defun-mode of fn: :program if fn is in :program
mode, :logic if fn is in :logic mode. If fn is
not a function symbol, return nil.
- (disabledp name): The list of runes introduced with name
that are currently disabled. See disabledp. Also see
enabled-runep, below, for a more direct test of whether a given rune is
- (disjoin lst): The disjunction of the given list of terms.
- (disjoin2 term1 term2): The disjunction of the given two terms.
- (doublet-listp x): Returns t if lst is a list of
two-element lists (x1 x2), else nil.
- (dumb-negate-lit t1): For the given term t1, return a
term that is propositionally equivalent to (not t1).
- (dumb-occur x y): Return t if the term x occurs free in the
term y, but without looking for x inside of quoted constants; else,
- (dumb-occur-var x y): Return t if the variable x occurs
free in the term y, else nil. This is the same as dumb-occur,
but optimized for the case that x is a variable.
- (enabled-numep nume ens wrld): Return true iff the given
nume (numeric representation of a rune) in the world, wrld,
is enabled with respect to the given enabled structure, ens.
(For example, (ens state) returns the global enabled structure; during a
proof, the enabled structure comes from the so-called rewrite-constant.)
Nil is also a valid first argument, in which case the return value is
t. See also enabled-runep.
- (enabled-runep rune ens wrld): Return true iff the given rune
in the world, wrld, is enabled with respect to the given
enabled structure (as discussed for enabled-numep, just above). See also
enabled-numep, which may be more efficient since enabled-runep is
defined in terms of enabled-numep.
- (fargn x n): For a pseudo-termp x that is a function
call and for a positive integer n, return the n-th argument of
x, where the numbering of arguments starts at 1.
- (fargs x): For a pseudo-termp x that is a function call,
return its arguments.
- (fcons-term fn args): This variant of cons-term (described
above) returns a term with the indicated function and arguments, without any
simplification. Also see cons-term and cons-term* above, and
- (fcons-term* fn arg1 arg2 ...): This variant of fcons-term
(described above) returns a term with the indicated function and arguments,
without any simplification, and where the arguments are ``spread'' into
individual actual parameters rather than provided as a list. Also see
cons-term, cons-term*, and fcons-term above.
- (fdefun-mode fn): For a function symbol fn, return the defun-mode of fn: :program if fn is in :program
mode, :logic if fn is in :logic mode.
- (ffn-symb x): This version of fn-symb (described below) assumes
that x is a pseudo-termp that is a function call, without
checking that x is a function call (the leading ``f'' is for ``fast''),
and returns its called function or lambda expression.
- (ffn-symb-p x sym): For a pseudo-termp x, return t
if it is a function call whose function symbol is sym, else return
- (ffnnamep fn term): Returns t when the function fn
(possibly a lambda expression) is used as a function in term,
which is assumed to be a pseudo-termp; else returns nil.
- (ffnnamep-lst fn lst): Returns t when the function fn
(possibly a lambda expression) is used as a function in a member of the
list lst of pseudo-termps; else returns nil.
- (fix-pkg pkg): Returns pkg, which should be nil or a
non-empty string, with one exception: if pkg is
"COMMON-LISP" then "ACL2" is returned.
- (flambda-applicationp x): For a pseudo-termp x that is
not a variable, return t if it is a function call whose function symbol
is a lambda expression, else return nil.
- (flambdap fn): True when fn is a lambda expression.
- (flatten-ands-in-lit term): Returns a list of terms whose conjunction
is equivalent to the given term (which satisfies pseudo-termp),
obtained by flattening its conjunctive structure. For example,
(flatten-ands-in-lit '(if (if x y 'nil) z 'nil)) is the list (x y
- (fn-rune-nume fn nflg xflg wrld): For a function symbol fn,
return either the rune (case nflg = nil) or nume (numeric
representation of a rune) (case nflg = t) associated with either
(:DEFINITION fn) (case xflg = nil) or
(:EXECUTABLE-COUNTERPART fn) (case xflg = t). If fn is a
constrained function, return nil for all combinations of the flags.
- (fn-symb x): For a pseudo-termp x, return its called
function or lambda expression if x is a function call, otherwise
return nil. Also see ffn-symb, above.
- (formals fn w): For a function symbol fn of world w,
return its list of formal parameters.
- (formula name normalp w): For an event name or rune,
name, of world w, return the corresponding formula if
any (normalized iff normalp is true), else nil. See formula.
- (fquotep x): For a pseudo-termp x that is not a
variable, return true iff x is a quoted constant.
- (fsubcor-var vars terms form): This variant of subcor-var
(described below) also substitutes, in the pseudo-termp form, the
variables in the list of symbolps vars with the corresponding
elements in the list of pseudo-termps terms, but without
performing any simplification.
- (function-symbolp sym w): True when the symbol sym is a function
symbol in the world w.
- (genvar pkg-witness prefix n avoid-lst): Generate a new variable
- (get-brr-local var state): The value of brr-local variable var;
this is the utility used by brr@.
- (get-defun-event name w): For the given name of a defined function in
the current ACL2 world w, return its defun form. Note
that this applies to both :logic-mode and :program-mode functions, in spite of the name, ``logical'' (which is actually
intended to distinguish from ``raw Lisp'').
- (get-event name w): For the given name of an event in the current
ACL2 world w, return that event. Typically there is only one such
event, but for built-in functions the most recent event might be a variant of
a verify-termination event, so consider using get-defun-event for
names of functions (see above).
- (get-skipped-proofs-p name w): For the given name of an event in the
current ACL2 world w, return t if proofs were skipped when
introducing that event, as with skip-proofs or using set-ld-skip-proofsp — that is, with proofs skipped other than by the
system (as with include-book); else return nil. Exception: if
name is a function symbol that is either built in or in :program mode, return nil.
- (guard fn stobj-optp w): For a function symbol or lambda
expression fn of world w, return its guard. Optimize
the stobj recognizers away iff stobj-optp is true.
- (implicate t1 t2): For terms t1 and t2, return a term that
is propositionally equivalent to (implies t1 t2).
- (io? token commentp shape vars body &key ...): This is a complex
macro that may be most fully understood by reading the source code, including
comments in its definition and examples of its use. But the following
example from the definition of source function print-failure1 may get the
(io? summary nil state (channel)
(fms *proof-failure-string* nil channel state nil))
This is essentially just the body argument, which here is the indicated
fms call, but where, going through the other arguments:
- summary — evaluation only takes place when summary
output is enabled (see set-inhibit-output-lst);
- nil — don't enter a wormhole;
- state — the body (which here is the fms call) returns a
single state value; and finally
- channel — this is the list of free variables in the
body (which here is the fms call).
- (known-package-alist state): Returns a list of package entries, as
explained in the definition of make-package-entry in ACL2 sources, which
is followed by simple accessor definitions (all in file axioms.lisp as of
this writing). This list includes entries for hidden packages (see hidden-death-package). As a package is introduced, its package entry is
pushed on the front of the existing known-package-alist. Note that this list
can be accessed directly from a world, w, with: (global-val
- (lambda-applicationp x): For a pseudo-termp x, return
t if it is a function call whose function symbol is a lambda
expression, else return nil.
- (lambda-body x): For a lambda expression x, return its
- (lambda-formals x): For a lambda expression x, return its
- (legal-constantp name): Returns t if name is a legal
constant name, else nil.
- (legal-variablep name): Returns t if name is a legal
variable name, else nil. For example, x is a legal variable name
but the following are not: :abc, t, nil, &a (a lambda
keyword), *c* (syntax of a constant), and pi (a Common Lisp
- (logicp fn w): For a function symbol fn of world
w, return t when the symbol-class of fn in w is not
:program, else nil. (See symbol-class, below.)
- (make-lambda args body): Return the lambda expression with
formal parameters args and body body.
- (make-lambda-application formals body actuals): Return the
lambda application that is essentially ((lambda formals body)
. actuals). However, extra formals and corresponding actuals are added when
body has free variables that do not belong to formals, because
lambdas must be closed in ACL2. A similar function is make-lambda-term,
but that one does not drop unused formals, while make-lambda-application
does drop them.
- (make-lambda-term formals actuals body): Return the lambda
application that is essentially ((lambda formals body) . actuals).
However, extra formals and corresponding actuals are added when body has
free variables that do not belong to formals, because lambdas must be
closed in ACL2. A similar function is make-lambda-application, but that
one drops unused formals, while make-lambda-term does not.
- (maybe-convert-to-mv uterm): Given the untranslated term
uterm, replace each of its top-level calls of list by a call of
mv on the same arguments.
- (nvariablep x): For a pseudo-termp x, return true iff
x is not a variable (i.e. it is a quoted constant or a function
- (partition-rest-and-keyword-args x keys): x should be a list of
the form (a1 ... an :key1 v1 ... :keyk vk), where no ai is a
keyword. The result is (mv erp rest alist), where erp is
non-nil if and only if the keyword section of x (that is, starting
with :key1) is ill-formed, that is: some :keyi is not a keyword,
:keyi and :keyj are the same for some distinct i and j, or some
:keyi is not a member of keys. When erp is nil, then
rest is (a1 ... an) and alist is equivalent (as a mapping) to
((:key1 . v1) ... (:keyk . vk)).
- (plist-worldp alist): Recognizer for when alist is syntactically
well-formed as an ACL2 logical world, sometimes suitable for use in
guards. Note: for a somewhat deeper check, see community book
- (prettyify-clause cl let*-abstractionp wrld): Returns an untranslated
(user-level) term that is equivalent to the clause, cl.
- (programp fn w): For a function symbol fn of world
w, return t when the symbol-class of fn in w is
:program, else nil. (See symbol-class, below.)
- (quotep x): For a pseudo-termp x, return true iff x
is a quoted constant.
- (recursivep fn flg w): Fn should be a :logic-mode
function symbol fn of the world, w. The result is the list
of mutually recursive functions of which fn is a member. The list is
empty iff fn is not recursive. The list contains just fn iff
fn is singly recursive. NOTE: flg should be t or nil. If
flg is nil, the result is based solely on the defun form that
introduced fn and is equal to (getpropc fn 'recursivep nil w). If
flg is t, then the most recent definition rule for fn
with a non-nil value of :install-body — which could be the
original definition — will cause recursivep to return the
:clique specified by that rule; see rule-classes.
- (stobjp x known-stobjs w): Returns a non-nil value when x
is to be treated as a stobj name, else nil. Argument
known-stobjs is a list of all such names, or else t, standing for
all stobj names in the world, w. If you want to know whether
x has been defined as a stobj in w, use known-stobjs = t.
Technicality: if known-stobjs is a list then it is allowed to contain any
number of nil elements (as may be the case for the the stobjs-in or
stobjs-out of a symbol), which are ignored.
- (stobjs-in fn w): For a function symbol fn of world
w, return the stobjs-in of fn, which is the result of modifying the
list of formal parameters of fn by replacing with nil each symbol
that is not a stobj input. Note that fn must be a symbol, not a
- (stobjs-out fn w): For a function symbol fn of world
w, return the stobjs-out of fn, which is a list whose length is the
number of return values of fn — that is, length 1 unless fn
returns multiple values. For each i less than that length, if the
ith return value is a stobj, then that is the ith element of the
stobjs-out; otherwise the ith element of the stobjs-out is nil.
Note that fn must be a symbol, not a lambda expression. Moreover
fn must not be a member of the list value of the constant
*stobjs-out-invalid*, i.e., the list (if return-last do$ read-user-stobj-alist), since for
these functions arbitrary multiple values may be returned.
- (subcor-var vars terms form): For a list vars of symbols, a list
terms of pseudo-termps, and a pseudo-termp form,
substitute, in form, the i-th variable from vars with the
i-th term from terms. Note that vars and terms should
have the same length. ("subcor" stands for "substitute
corresponding elements".) Some simplification may be done; to avoid
that, use fsubcor-var (``fast substitute corresponding elements''),
- (sublis-fn-simple alist term), (sublis-fn alist term
bound-vars): Both of these apply the functional substitution, alist, to
the given term. Thus in both cases, all keys of alist are function
symbols. In the case of sublis-fn-simple, each key of alist is
mapped to a function symbol; but for sublis-fn, a key may instead be
mapped to a legal lambda expression. The other difference between the
two functions is that for sublis-fn, the formal bound-vars is a list
of variables, generally nil at the top level. For details see the Lisp
comments in the ACL2 sources for function sublis-fn-rec (which is more
general than either sublis-fn-simple and sublis-fn, and is called by
both of them to do the real work).
- (sublis-fn-lst-simple alist termlist): Apply the given functional
substitution, alist, to each term in termlist, essentially by
applying sublis-fn-simple to alist and each such term. See the
description of sublis-fn-simple, above.
- (sublis-var alist form): Substitute alist into the term,
form. Alist should be an alist that associates symbols with pseudo-termps, and term should also satisfy pseudo-termp. Note
that the substitution process evaluates calls of primitives on quoted
constants, essentially using cons-term.
- (subsequencep lst1 lst2): Determine whether the list lst1 is a
subsequence of the list lst2, although not necessarily a proper
- (subst-expr new old term): Substitute new for old in
term; all are assumed to be terms. This function provides a
slightly optimized version of equivalent function (subst-expr1 new old
term). Also, the former causes an explicit error if old is a quoted
constant, and neither will search strictly inside a quoted subterm of
old. A more complex function (perhaps a bit less likely to stay forever
unchanged), subst-equiv-expr, may be found in the source code; it can
substitute one expression for another when the two are equivalent, but not
- (subst-var new old term): Substitute new for old in
term; all are assumed to be terms, but moreover, old is
assumed to be a variable.
- (symbol-class name w): For a function symbol, name, of the ACL2
world w, return :program if name is in :program mode, :common-lisp-compliant if name is guard-verified, and otherwise, :ideal. If name is the name of a
theorem (more specifically, has a 'theorem property; see getprop),
return :ideal unless the theorem is guard-verified, in which case return
:common-lisp-compliant. Otherwise return :program.
- (symbol-doublet-listp lst): Returns t if lst is a list of
two-element lists (x1 x2) where x1 is a symbol, else nil.
- (termp x w): Is x a term in logical world
- (trans-eval form ctx state aok): Translate and then evaluate
form. See trans-eval for discussion and related utilities.
- translate, translate1, translate11, translate-cmp, and
translate1-cmp: Functions that translate user-level input to translated
terms, as recognized by termp. Note that these functions perform
macroexpansion, which checks guards on primitives; see safe-mode.
- (translate-hints name-tree lst ctx wrld state): Translate a given
list of user-level hints, lst, to internal form. NOTE: this function
returns an error-triple, and it checks the syntax of lst. Its
documentation essentially resides in a comment in source function
- (untranslate term iff-flg w): see untranslate.
- (value x): This macro call expands to (mv nil x state). For
related discussion, see error-triple.
- (variablep x): For a pseudo-termp x, return true iff
x is a variable, i.e., a symbol.
- Evaluate a form
- System utilities related to the ACL2 system.
- Obtain data stored after at the conclusion of an event
- Show a user-level representation of a term
- Obtaining the constraint on a function symbol