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

**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 buit-in system utility: As ACL2
developers sometimes do, use

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'sunwind-protect . In typical use the cleanup forms restore the values of state global variables that were ``temporarily'' set bybody . Note thatexpl is essentially ignored. For more information see the Essay on Unwind-Protect in the ACL2 source code.(add-suffix sym str) : Extend a symbolsym with a suffix expressed as a stringstr . 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 whensym 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) whereg is attached tof (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 symbolf , without the restrictions above and with valuenil if there is no attachment tof , 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 intoans (which typically isnil at the top level) all pseudo-termsu/alist such that for somef 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 intoans (which typically isnil 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 ofall-fnnames1 ; seeall-fnnames ,all-fnnames-lst , andall-fnnames1 , below.(all-ffn-symbs-lst lst ans) : Accumulate intoans (which typically isnil 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 ofall-fnnames1 ; seeall-fnnames ,all-fnnames-lst , andall-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 intoacc the function symbols called in the given term or list of terms,x , according to whetherflg isnil (for a term) or notnil (for a list of terms), respectively.(all-vars x) : For a`pseudo-termp`x , return a duplicate-free list of all variables inx , 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 ifflst is anil -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 orlambda expressionfn of worldw , return the number of its formal parameters.(body fn normalp w) :Fn should either be a: `logic`-mode function symbol of worldw or alambda expression. Iffn is a symbol andnormalp isnil , then return the body (translated but unnormalized) of its original definition. Iffn is alambda expression, return its body. We now discuss the remaining case, wherefn is a: `logic`-mode function symbol andnormalp is true. In the usual case that no definition rule has been introduced forfn with a non-nil value of:install-body (which is the default), return the normalized body from thedefun form that introducedfn , ornil iffn was not introduced withdefun (as with`encapsulate`,`defstub`, or`defchoose`) — except that in the case that:normalize nil was specified in thatdefun form (see xargs), return the unnormalized body. The remaining case is that at least one definition rule forfn has been installed. In that case, the latest such rule provides the body (see source functionlatest-body for how hypotheses are handled), with one exception: if the equivalence relation for that rule is other thanequal , 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 argumentsargs . 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, usefcons-term (``fast cons-term''), described below. Also seecons-term* andfcons-term* below.(cons-term* fn arg1 arg2 ...) : This variant ofcons-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, usefcons-term* . Also seecons-term above andfcons-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 astranslate-cmp . That record provides values for certain state global variables (which are not stored in the world), such asguard-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 ist , 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) : Ifname ist ,nil , or defined using`defconst`, return(quote val) whereval is the value ofname ; otherwise returnnil .(defun-mode fn w) : Iffn is a function symbol, return the defun-mode offn ::program iffn is in: `program`mode,:logic iffn is in: `logic`mode. Iffn is not a function symbol, returnnil .(disabledp name) : The list of runes introduced withname that are currently disabled. See disabledp. Also seeenabled-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) : Returnst iflst is a list of two-element lists(x1 x2) , elsenil .(dumb-negate-lit t1) : For the given termt1 , return a term that is propositionally equivalent to(not t1) .(dumb-occur x y) : Returnt if the termx occurs free in the termy , but without looking forx inside of quoted constants; else, returnsnil .(dumb-occur-var x y) : Returnt if the variablex occurs free in the termy , elsenil . This is the same asdumb-occur , but optimized for the case thatx 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 ist . See alsoenabled-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 forenabled-numep , just above). See alsoenabled-numep , which may be more efficient sinceenabled-runep is defined in terms ofenabled-numep .(fargn x n) : For a`pseudo-termp`x that is a function call and for a positive integern , return then -th argument ofx , 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 ofcons-term (described above) returns a term with the indicated function and arguments, without any simplification. Also seecons-term andcons-term* above, andfcons-term* below.(fcons-term* fn arg1 arg2 ...) : This variant offcons-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 seecons-term ,cons-term* , andfcons-term above.(fdefun-mode fn) : For a function symbolfn , return the defun-mode offn ::program iffn is in: `program`mode,:logic iffn is in: `logic`mode.(ffn-symb x) : This version offn-symb (described below) assumes thatx is a`pseudo-termp`that is a function call, without checking thatx is a function call (the leading ``f'' is for ``fast''), and returns its called function orlambda expression.(ffn-symb-p x sym) : For a`pseudo-termp`x , returnt if it is a function call whose function symbol issym , else returnnil .(ffnnamep fn term) : Returnst when the functionfn (possibly a lambda expression) is used as a function interm , which is assumed to be a`pseudo-termp`; else returnsnil .(ffnnamep-lst fn lst) : Returnst when the functionfn (possibly a lambda expression) is used as a function in a member of the listlst of`pseudo-termp`s; else returnsnil .(fix-pkg pkg) : Returnspkg , which should benil or a non-empty string, with one exception: ifpkg is"COMMON-LISP" then"ACL2" is returned.(flambda-applicationp x) : For a`pseudo-termp`x that is not a variable, returnt if it is a function call whose function symbol is alambda expression, else returnnil .(flambdap fn) : For a`pseudo-termp`(fn arg1 ... argk) , true whenfn 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 symbolfn , return either the rune (casenflg =nil ) or nume (numeric representation of a rune) (casenflg =t ) associated with either(:DEFINITION fn) (casexflg =nil ) or(:EXECUTABLE-COUNTERPART fn) (casexflg =t ). Iffn is a constrained function, returnnil for all combinations of the flags.(fn-symb x) : For a`pseudo-termp`x , return its called function orlambda expression ifx is a function call, otherwise returnnil . Also seeffn-symb , above.(formals fn w) : For a function symbolfn of worldw , return its list of formal parameters.(formula name normalp w) : For an event name or rune,name , of worldw , return the corresponding formula if any (normalized iffnormalp is true), elsenil . See formula.(fquotep x) : For a`pseudo-termp`x that is not a variable, return true iffx is a quoted constant.(fsubcor-var vars terms form) : This variant ofsubcor-var (described below) also substitutes, in the`pseudo-termp`form , the variables in the list of`symbolp`svars with the corresponding elements in the list of`pseudo-termp`sterms , but without performing any simplification.(function-symbolp sym w) : True when the symbolsym is a function symbol in the worldw .(genvar pkg-witness prefix n avoid-lst) : Generate a new variable name.(get-brr-local var state) : The value of brr-local variablevar ; this is the utility used by brr@.(get-defun-event name w) : For the given name of a defined function in the current ACL2 worldw , 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 worldw , 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 usingget-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 worldw , returnt 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 returnnil . Exception: ifname is a function symbol that is either built in or in: `program`mode, returnnil .(guard fn stobj-optp w) : For a function symbol orlambda expressionfn of worldw , return its guard. Optimize the stobj recognizers away iffstobj-optp is true.(implicate t1 t2) : For termst1 andt2 , 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 functionprint-failure1 may get the idea across.(io? summary nil state (channel) (fms *proof-failure-string* nil channel state nil))

This is essentially just thebody argument, which here is the indicated`fms`call, but where, going through the other arguments:summary — evaluation only takes place whensummary output is enabled (see set-inhibit-output-lst);nil — don't enter a wormhole;state — the body (which here is thefms call) returns a singlestate value; and finallychannel — this is the list of free variables in the body (which here is thefms call).

(known-package-alist state) : Returns a list of package entries, as explained in the definition ofmake-package-entry in ACL2 sources, which is followed by simple accessor definitions (all in fileaxioms.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 , returnt if it is a function call whose function symbol is alambda expression, else returnnil .(lambda-body x) : For alambda expressionx , return its body.(lambda-formals x) : For alambda expressionx , return its formal parameters.(legal-constantp name) : Returnst ifname is a legal constant name, elsenil .(legal-variablep name) : Returnst ifname is a legal variable name, elsenil . 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), andpi (a Common Lisp constant).(logicp fn w) : For a function symbolfn of worldw , returnt when thesymbol-class offn inw is not:program , elsenil . (Seesymbol-class , below.)(make-lambda args body) : Return thelambda expression with formal parametersargs and bodybody .(make-lambda-application formals body actuals) : Return thelambda application that is essentially((lambda formals body) . actuals) . However, extra formals and corresponding actuals are added whenbody has free variables that do not belong toformals , because lambdas must be closed in ACL2. A similar function ismake-lambda-term , but that one does not drop unused formals, whilemake-lambda-application does drop them.(make-lambda-term formals actuals body) : Return thelambda application that is essentially((lambda formals body) . actuals) . However, extra formals and corresponding actuals are added whenbody has free variables that do not belong toformals , because lambdas must be closed in ACL2. A similar function ismake-lambda-application , but that one drops unused formals, whilemake-lambda-term does not.(maybe-convert-to-mv uterm) : Given the untranslated termuterm , 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 iffx 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 noai is a keyword. The result is(mv erp rest alist) , whereerp is non-nil if and only if the keyword section ofx (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 ofkeys . Whenerp isnil , thenrest is(a1 ... an) and alist is equivalent (as a mapping) to((:key1 . v1) ... (:keyk . vk)) .(plist-worldp alist) : Recognizer for whenalist is syntactically well-formed as an ACL2 logical world, sometimes suitable for use in guards. Note: for a somewhat deeper check, see community bookbooks/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 symbolfn of worldw , returnt when thesymbol-class offn inw is:program , elsenil . (Seesymbol-class , below.)(quotep x) : For a`pseudo-termp`x , return true iffx is a quoted constant.(recursivep fn flg w) :Fn should be a: `logic`-mode function symbolfn of the world,w . The result is the list of mutually recursive functions of whichfn is a member. The list is empty ifffn is not recursive. The list contains justfn ifffn is singly recursive. NOTE:flg should bet ornil . Ifflg isnil , the result is based solely on the`defun`form that introducedfn and is equal to(getpropc fn 'recursivep nil w) . Ifflg ist , then the most recent definition rule forfn with a non-nil value of:install-body — which could be the original definition — will causerecursivep to return the:clique specified by that rule; see rule-classes.(stobjp x known-stobjs w) : Returns a non-nil value whenx is to be treated as a stobj name, elsenil . Argumentknown-stobjs is a list of all such names, or elset , standing for all stobj names in the world,w . If you want to know whetherx has been defined as a stobj inw , useknown-stobjs =t . Technicality: ifknown-stobjs is a list then it is allowed to contain any number ofnil elements (as may be the case for thestobjs-in orstobjs-out of a symbol), which are ignored.(stobjs-in fn w) : For a function symbolfn of worldw , return the stobjs-in offn , which is the result of modifying the list of formal parameters offn by replacing withnil each symbol that is not a stobj input. Note thatfn must be a symbol, not a lambda expression.(stobjs-out fn w) : For a function symbolfn of worldw , return the stobjs-out offn , which is a list whose length is the number of return values offn — that is, length 1 unlessfn returns multiple values. For eachi less than that length, if thei th return value is a stobj, then that is thei th element of the stobjs-out; otherwise thei th element of the stobjs-out isnil . Note thatfn must be a symbol, not a lambda expression. Moreoverfn 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 listvars of symbols, a listterms of`pseudo-termp`s, and a`pseudo-termp`form , substitute, inform , the*i*-th variable fromvars with the*i*-th term fromterms . Note thatvars andterms should have the same length. ("subcor " stands for "substitute corresponding elements".) Some simplification may be done; to avoid that, usefsubcor-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 ofalist are function symbols. In the case ofsublis-fn-simple , each key ofalist is mapped to a function symbol; but forsublis-fn , a key may instead be mapped to a legal lambda expression. The other difference between the two functions is that forsublis-fn , the formalbound-vars is a list of variables, generallynil at the top level. For details see the Lisp comments in the ACL2 sources for functionsublis-fn-rec (which is more general than eithersublis-fn-simple andsublis-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 intermlist , essentially by applyingsublis-fn-simple to alist and each such term. See the description ofsublis-fn-simple , above.(sublis-var alist form) : Substitutealist into the term,form .Alist should be an alist that associates symbols with`pseudo-termp`s, andterm should also satisfypseudo-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) : Substitutenew forold interm ; 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 ifold is a quoted constant, and neither will search strictly inside a quoted subterm ofold . 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) : Substitutenew forold interm ; 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 worldw , return:program ifname is in: `program`mode,:common-lisp-compliant ifname is guard-verified, and otherwise,:ideal . Ifname 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) : Returnst iflst is a list of two-element lists(x1 x2) wherex1 is a symbol, elsenil .(termp x w) : Isx a term in logical worldw ?(trans-eval form ctx state aok) : Translate and then evaluateform . See trans-eval for discussion and related utilities.translate ,translate1 ,translate11 ,translate-cmp , andtranslate1-cmp : Functions that translate user-level input to translated terms, as recognized bytermp . 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 oflst . Its documentation essentially resides in a comment in source functiontranslate-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 iffx is a variable, i.e., a symbol.

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