		Search-engine friendly clone of the ACL2 documentation.

World

Extend-world

Install an extension of a given ACL2 world

See world for relevant background on ACL2 property list worlds. Here we discuss how to install an extension 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 retract-world for a similar utility that instead installs an initial segment of a named world.

General Form:

(extend-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)))
         (assign my-w (extend-world 'my-world wrld3)))
 ((MY-SYM1 MY-KEY1 . MY-VAL1)
  (MY-SYM2 MY-KEY2 . MY-VAL2)
  (MY-SYM1 MY-KEY1 . MY-VAL1-OLD))
ACL2 !>(getprop 'my-sym1 'my-key1 nil 'my-world (@ my-w))
MY-VAL1
ACL2 !>

The first top-level form sets the value of state global my-w to the world obtained by extending the empty world three times, as shown. The second top-level form returns the most recent 'my-key1 property of the symbol 'my-sym1. This second computation is efficient, because extend-world has installed the value of my-w as the world that is current for the name 'my-world. See world.