		Search-engine friendly clone of the ACL2 documentation.

World

Retract-world

Install an initial segment (retraction) of a given ACL2 world

See world for relevant background on ACL2 property list worlds. Here we discuss how to install an initial segment (retraction) of a user-defined world, that is, a world other than the one named 'current-acl2-world, which is maintained by the ACL2 system. Also see extend-world for a similar utility that instead extends a named world.

General Form:

(retract-world name wrld)

where name is a symbol intended to name the given ACL2 property list world, world. Consider the following example.

ACL2 !>(let* ((wrld0 nil)
              (wrld1 (putprop 'my-sym1 'my-key1 'my-val1-old wrld0))
              (wrld2 (putprop 'my-sym2 'my-key2 'my-val2 wrld1))
              (wrld3 (putprop 'my-sym1 'my-key1 'my-val1 wrld2)))
         (pprogn (f-put-global 'my-w1 wrld1 state)
                 (f-put-global 'my-w3 (extend-world 'my-world wrld3) state)))
<state>
ACL2 !>(retract-world 'my-world (@ my-w1))
((MY-SYM1 MY-KEY1 . MY-VAL1-OLD))
ACL2 !>(getprop 'my-sym1 'my-key1 nil 'my-world (@ my-w1))
MY-VAL1-OLD
ACL2 !>

The first top-level form sets the values of state globals my-w1 and my-w3 to to the worlds obtained by extending the empty world one or three times, respectively, as shown. The second top-level form installs the value of my-w1 as the world that is current for the name 'my-world. The third top-level form returns the 'my-key1 property for the symbol 'my-sym1 in the installed world (@ my-w1), and it does so efficiently because that world is installed. See world.