ACL2-PC::PUT

(macro) substitute for a ``free variable''
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(put x 17)

General Form: (put var expr)

Substitute expr for the ``free variable'' var, as explained below.

A ``free variable'' is, for our purposes, a variable var such that the instruction (free var) has been executed earlier in the state-stack. What (free var) really does is to let var be an abbreviation for the term (hide var) (see documentation for add-abbreviation). What (put var expr) really does is to unwind the state-stack, replacing that free instruction with the instruction (add-abbreviation var expr), so that future references to (? var) become reference to expr rather than to (hide var), and then to replay all the other instructions that were unwound. Because hide was used, the expectation is that in most cases, the instructions will replay successfully and put will ``succeed''. However, if any replayed instruction ``fails'', then the entire replay will abort and ``fail'', and the state-stack will revert to its value before the put instruction was executed.

If (put var expr) ``succeeds'', then (remove-abbreviation var) will be executed at the end.

Note: The restore command will revert the state-stack to its value present before the put instruction was executed.