Developers-guide-utilities
Data Structures and Utilities
This topic introduces some of the data structures and utilities
built into ACL2. Also see system-utilities and programming-with-state. Those topics have lots of useful information not
covered in this overview topic. Just to give one example: someone once needed
a utility to print clauses nicely, so the utility prettyify-clause, not
mentioned below, was added to the list of utilities in system-utilities.
Much of this is covered in developers-guide-background.
The state is, logically, a data structure with many fields. However,
it is represented in ACL2 by a symbol, which is the value of
*the-live-state*:
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? state
ACL2_INVISIBLE::|The Live State Itself|
? *the-live-state*
ACL2_INVISIBLE::|The Live State Itself|
?
For technical reasons involving (as best recalled at this writing) tail
recursion removal in some host Lisps, state is not declared as a Common
Lisp special variable. So raw Lisp code (say, conditioned by
#-acl2-loop-only) should reference *the-live-state* when state
is not lexically bound, to avoid compiler warnings.
? (defun foo () state)
;Compiler warnings :
; In FOO: Undeclared free variable STATE
FOO
? (defun foo () *the-live-state*)
FOO
?
As discussed in an earlier chapter of this Guide (see developers-guide-background), a key logical field of state is the
global-table, which is an alist associating state global variables with
their values. Also see programming-with-state, which explains this
idea further along with many other key data structures and programming idioms
that pertain to state.
The logical world is the value of state global variable
current-acl2-world, but is normally accessed using the function,
w.
ACL2 !>(equal (f-get-global 'current-acl2-world state)
(w state))
T
ACL2 !>(set-guard-checking nil)
Masking guard violations but still checking guards except for self-
recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE. See :DOC set-guard-checking.
ACL2 >(eq (f-get-global 'current-acl2-world state)
(w state))
T
ACL2 >
Enabled structures
THIS SECTION IS WORTH COVERING IN ITS ENTIRETY.
ACL2 handles theories using enabled structures. Ideally you
could learn about enabled structures by visiting the defrec form for
enabled-structure. As of this writing, there are virtually no comments
in that defrec form! Fortunately, the field names are suggestive of
their meaning; but that is not really adequate documentation. This is one of
those place in the ACL2 sources where additional comments would be useful. In
the meantime, you can learn about enabled structures by seeing how they are
used, by doing an Emacs tags-search for ``enabled-structure'' or perhaps
``(access enabled-structure''. Another option is to follow the
definition of disabledp to find the definition of enabled-runep,
where you'll see that (enabled-runep rune ens wrld) is
(enabled-numep (fnume rune wrld) ens). Note that ens is a variable
that is commonly used for enabled structures, and fnume returns the
nume of a rune, which is a unique number corresponding to the
rune. The definition of enabled-numep helps to explain the fields of an
enabled structure.
Function: enabled-numep
(defun enabled-numep (nume ens)
(declare (type (or null (unsigned-byte 60)) nume)
(xargs :guard (enabled-structure-p ens)))
(cond ((null nume) t)
((> nume
(the-fixnum (access enabled-structure
ens :index-of-last-enabling)))
t)
(t (aref1 (access enabled-structure ens :array-name)
(access enabled-structure ens :theory-array)
(the-fixnat nume)))))
An ACL2 developer sometimes needs to be able to follow definitions like
this to learn about ACL2 data structures — sad, but true.
Tag trees
PERHAPS WE'LL JUST LOOK AT A CALL OF PUSH-LEMMA IN REWRITE.
A tag tree, or ttree (pronounced ``tee-tree''), is a
structure that is used for recording information generated by the prover.
There is no defrec form for tag trees, but fortunately, there is a long
comment in the ACL2 sources labeled ``; Essay on Tag-Trees''. Here is a
high-level introduction that may be helpful before you read that Essay.
Abstractly a tag-tree represents a list of sets, each member set having a
name given by one of the ``tags'' (which are symbols) of the ttree. The
elements of the set named tag are all of the objects tagged tag in
the tree. Definitions of primitives in the source code for manipulating tag
trees are labeled with the comment ``; Note: Tag-tree primitive''.
Many ACL2 prover functions take and return tag trees. The function
rewrite, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.
Term' is provably equivalent to the input term (under the current
assumptions) and ttree' is an extension of the input ttree. If we focus
just on the set associated with the tag LEMMA in the ttrees, then the set
for ttree' is the extension of that for the input ttree, which is
obtained by unioning into it all the runes used by the rewriter. The
set associated with tag LEMMA can be obtained by (tagged-objects
'LEMMA ttree). Tag trees contain useful prover information based not only
on lemmas used but also on hints, assumptions generated by force,
forward-chaining, and so on. It is critical not to avoid tag trees
that contain assumptions (see developers-guide-pitfalls).
The Essay on Tag-Trees describes some of the legal tags for a ttree, but
the definitive list is the one enforced by function
all-runes-in-ttree. Here for example is an interesting clause from a
case expression in the body of that definition.
(assumption
; Shape: assumption record
ans)
If you see this, then you might be curious about the notion of an
``assumption record''. Then you can simply go to the definition of
assumption (typically, using the Emacs command, meta-.). You'll see
quite a few lines of comments in that vicinity, which may help to get your
head around these records.
Macros
Many macros that are useful in the ACL2 source code are also helpful to
users, and hence are documented. Among these are defrec (already
discussed in the chapter, developers-guide-background)), defabbrev, er-progn, pprogn, state-global-let*, and
revert-world. Others could reasonably have their own documentation
topics but are discussed in other topics; for example, see programming-with-state for a discussion of er-let*. Still others are
not mentioned in the xdoc documentation but have Lisp comments in the source
code, for example, revert-world-on-error, with-ctx-summarized,
io?, and acl2-unwind-protect. Perhaps the best way to learn about
the variety of available macros for ACL2 system programming is to notice their
usage in existing ACL2 source code, then looking them up in the xdoc
documentation and/or in the source code (typically with the Emacs command,
meta-.).
Evaluators
Source code often contains calls that evaluate terms. A prime example is
the implementation of the read-eval-print loop, as explained in the chapter,
developers-guide-background. There are several evaluators available.
The most familiar to users may be trans-eval, which is actually a
combination of translation and evaluation. If you look at the source code and
drill down (following definitions) from trans-eval, you'll see that there
are several optimizations, in part to support lazy treatment of if calls:
based on the test, perhaps only one of the two branches will need to be
translated, let alone evaluated. If you keep drilling down, you may
ultimately see a call of ev, which is an evaluator for (translated)
terms. In a sense ev is the most basic term evaluator. Note that
ev takes and returns state. A related evaluator, ev-w, may be
used if state and stobjs are not involved.
There is more to evaluation, such as the handling of stobjs via so-called
``latches'' and the user-stobj-alist, which pertain to the subtle notion
that user-defined stobjs are actually part of the ACL2 state; you can read
comments in the sources to learn more about that when the need arises. Also
see the chapter, developers-guide-evaluation.
THIS SECTION IS WORTH COVERING IN ITS ENTIRETY.
There are occasions in which a utility is naturally defined as a function
in ACL2 but as a macro in Common Lisp. Consider mbe. Even though
mbe is itself a macro, it must expand to a function call involving its
:logic and :exec arguments, so that a suitable guard proof
obligation can be generated. However, in raw Lisp we want an mbe call to
be fast, by simply running the :exec argument. Let's see how this is all
arranged.
ACL2 !>:trans (mbe :logic (zp n) :exec (= n 0))
(RETURN-LAST 'MBE1-RAW (= N '0) (ZP N))
=> *
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? (macroexpand '(mbe :logic (zp n) :exec (= n 0)))
(= N 0)
T
?
The key, obviously, is to use return-last, which is the only
ACL2 utility that is defined to be a function in the ACL2 loop but is defined
to be a macro in raw Lisp. Before you add a new utility that, like mbe,
needs to operate as a function in the ACL2 loop but as a macro in raw Lisp,
commit yourself to defining it using return-last. The reason is that
handling any such utility is tricky (see for example the definition of
ev-rec-return-last), so it would be ill-advised to replicate all the work
done already for return-last in handling any additional such utility. Of
course, the first step then is to become familiar with return-last. The
xdoc documentation on return-last is quite extensive, and may suffice;
of course, it is also advisable to read the comments in the source code
definition of return-last.
The use of return-last provides an example of the suggestion to use
precedents (see developers-guide-maintenance). Imagine that you want
to add a function to ACL2 that is implemented under-the-hood as a macro in raw
Lisp. Ideally, you would look at an existing such utility, such as mbe,
to see how it is implemented. This would lead you to return-last, which
you would then use similarly to implement your new utility.
Type-alists
A fundamental data structure in the ACL2 prover is the type-alist.
Since some user-level utilities display the type-alist, there is user-level
documentation for this data structure; see type-alist, which contains
important system-level background. Perusal of the source code will reveal
utilities for computing with type-alists. Two key such utilities are
type-set, which computes the type-set of a term with respect to a given
type-alist, and which again has user-level documentation (see type-set)
that also serves to provide important system-level background; and
assume-true-false, which extends a type-alist as one dives into the true
or false branch of a call of IF. Before creating type-alists with
lower-level or new utilities, be sure to read the ``Essay
on the Invariants on Type-alists, and Canonicality.'' In general,
look for essays on any topic that is relevant to changes that you are making,
unless you are reasonably confident that the essay is at a lower level than
you need. For example, if you call
assume-true-false to extend an existing type-alist, then you are using a
well-worn interface and you needn't be concerned about the well-formedness of
the resulting type-alists.
NEXT SECTION: developers-guide-logic
