		Search-engine friendly clone of the ACL2 documentation.

Programming

System-utilities

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

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 quite rare.

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 built-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 utility.

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)
        BODY
        (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 source code.
(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 nil).
(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 terms), respectively.
(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 b a).
(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 follows.
```
ACL2 !>(cons-term 'coerce (list ''"abc" ''list))
'(#\a #\b #\c)
ACL2 !>
```
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 below.
(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 enabled.
(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, returns nil.
(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* below.
(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 nil.
(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): For a pseudo-termp (fn arg1 ... argk), 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 z).
(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 name.
(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 idea across.
```
(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 'known-package-alist w).
(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 body.
(lambda-formals x): For a lambda expression x, return its formal parameters.
(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 constant).
(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 call).
(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 books/system/pseudo-good-worldp.lisp.
(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 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 or :df each symbol that is not a stobj input — generally nil, but :df if the formal parameter is declared to be a df (see df). Note that fn must be a symbol, not a lambda expression.
(stobjs-out fn w): For a function symbol fn of world w, return the stobjs-out of fn, which is the list described below whose length L is the number of return values of fn — that is, L is 1 unless fn returns multiple values. First suppose that L is 1; say the stobjs-out list is (s). If fn returns a stobj then s is that stobj; if fn returns a df then s is :df; and otherwise s is nil. Otherwise, L is greater than 1. Then for each i less than L, 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 :df if calls of fn are df{i} expressions (see df, else 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''), described above.
(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 subsequence.
(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 necessarily equal.
(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 w?
(trans-eval form ctx state aok): Translate and then evaluate form. See trans-eval for discussion and related utilities.
translate, translate1, translate11, translate-cmp, translate1-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 translate-hints1.
(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.

Subtopics

Saving-event-data: Save data stored for subsidiary events
Trans-eval: Evaluate a form
System-utilities-non-built-in: System utilities related to the ACL2 system.
Get-event-data: Obtain data stored after at the conclusion of an event
Untranslate: Show a user-level representation of a term
Constraint-info: Obtaining the constraint on a function symbol