World
ACL2 property lists and the ACL2 logical database
The ACL2 logical world is a data structure that includes all
logical content resulting from the commands evaluated, back through and
including initialization, but not including commands that have been
undone (see ubt). Thus in particular, the world includes a
representation of the current logical theory, as well as some extra-logical
information such as the values of ACL2 tables. The rest of this topic
focuses on the structure of the ACL2 world and, more generally, the
``world'' data structure.
A ``world'' is a list of triples, each of the form (sym prop . val),
implementing the ACL2 notion of property lists. ACL2 permits the simultaneous
existence of many property list worlds. ``The world'' is often used as a
shorthand for ``the ACL2 logical world'' which is the particular property list
world used within the ACL2 system to maintain a database that contains rules,
tables, and so on.
Common Lisp provides the notion of ``property lists'' by which one can
attach ``properties'' and their corresponding ``values'' to symbols. For
example, one can arrange for the 'color property of the symbol
'box-14 to be 'purple and the 'color property of the symbol
'triangle-7 to be 'yellow. Access to property lists is given via
the Common Lisp function get. Thus, (get 'box-14 'color) might
return 'purple. Property lists can be changed via the special form
setf. Thus, (setf (get 'box-14 'color) 'blue) changes the Common
Lisp property list configuration so that (get 'box-14 'color) returns
'blue. It should be obvious that ACL2 cannot provide this facility,
because Common Lisp's get ``function'' is not a function of its argument,
but instead a function of some implicit state object representing the property
list settings for all symbols.
ACL2 provides the functions getprop and putprop which allow one
to mimic the Common Lisp property list facility. However, ACL2's getprop
takes as one of its arguments a list that is a direct encoding of what was
above called the ``state object representing the property list settings for
all symbols.'' Because ACL2 already has a notion of ``state'' that is
quite distinct from that used here, we call this property list object a
``world.'' A world is just a true list of triples. Each triple is of the
form (sym prop . val). This world can be thought of as a slightly
elaborated form of association list and getprop is a slightly elaborated
form of assoc that takes two keys. When getprop is called on a
symbol, s, property p, and world, w, it scans w for the
first triple whose sym is s and prop is p and returns the
corresponding val. Getprop has two additional arguments: one
controls what it returns if no such sym and prop exist in w,
and the other allows an extremely efficient implementation. To set some
property's value for some symbol, ACL2 provides putprop. (putprop sym
prop val w) merely returns a new world, w', in which (sym prop
. val) has been consed onto the front of w, thus
``overwriting'' the prop value of sym in w to val and
leaving all other properties in w unchanged.
One aspect of ACL2's property list arrangement is that it is possible to
have many different property list worlds. For example, 'box-14 can have
'color 'purple in one world and can have 'color 'yes in
another, and these two worlds can exist simultaneously because getprop is
explicitly provided the world from which the property value is to be
extracted.
The efficiency alluded to above stems from the fact that Common Lisp
provides property lists. Using Common Lisp's provisions behind the scenes,
ACL2 can ``install'' the properties of a given world into the Common Lisp
property list state so as to make retrieval via getprop very fast in the
special case that the world provided to getprop has been installed. To
permit more than one installed world, each of which is permitted to be changed
via putprop, ACL2 requires that worlds be named and these names are used
to distinguish installed versions of the various worlds. See extend-world and retract-world for how to install a world.
However, the ACL2 system uses a property list world, named
'current-acl2-world, in which to store the succession of user commands and their effects on the logic. This world is often referred to in
our documentation as ``the world'' though it should be stressed that
the user is permitted to have worlds and ACL2's is in no way distinguished
except that the user is not permitted to modify it except via event commands. The ACL2 world is part of the ACL2 state and may be
obtained via (w state).
Warning: The ACL2 world is very large. Its length as of this
writing (Version 2.5) is over 40,000 and it grows with each release.
Furthermore, some of the values stored in it are pointers to old versions of
itself. Printing (w state) is something you should avoid because you
likely will not have the patience to await its completion. For these
practical reasons, the only thing you should do with (w state) is provide
it to getprop, as in the form
(getprop sym prop default 'current-acl2-world (w state))
or its convenient abbreviation
(getpropc sym prop default)
to inspect properties within it, or to pass it to ACL2 primitives, such as
theory functions, where it is expected.
Some ACL2 command forms, such as theory expressions (see theories) and the values to be stored in tables (see table), are
permitted to use the variable symbol world freely with the understanding
that when these forms are evaluated that variable is bound to (w state).
Theoretically, this gives those forms complete knowledge of the current
logical configuration of ACL2. However, at the moment, few world scanning
functions have been documented for the ACL2 user. Instead, supposedly
convenient macro forms have been created and documented. For example,
(current-theory :here), which is the theory expression which returns the
currently enabled theory, actually macroexpands to
(current-theory-fn :here world). When evaluated with world bound to
(w state), current-theory-fn scans the current ACL2 world and
computes the set of runes currently enabled in it.
Subtopics
- Logical-name
- A name created by a logical event
- Formula
- The formula of a name or rune
- Redefined-names
- To collect the names that have been redefined
- Retract-world
- Install an initial segment (retraction) of a given ACL2 world
- Extend-world
- Install an extension of a given ACL2 world
- Getprop
- Access fast property lists
- Getpropc
- Access fast property lists
- Putprop
- Update fast property lists
- Props
- Print the ACL2 properties on a symbol
