Major Section: MISCELLANEOUS
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 the database of rules.
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 of which that controls what it returns if
no such sym and prop exist in w, and other other of which
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 arrangment 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 distinquish
installed versions of the various worlds. At the moment we do not
further document getprop and putprop.
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))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.
