ACL2-pc::put
(macro)
substitute for a ``free variable''
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 ACL2-pc::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.
Remark: The restore command will revert the state-stack to its
value present before the put instruction was executed.
