Sneaky-mutate
Low-level way to modify the sneaky store.
- Signature
(sneaky-mutate fnname get-keys user-arg) → *
- Arguments
- fnname — The true mutator function to invoke.
Guard (symbolp fnname).
- get-keys — The keys whose values will be retrieved and passed
to fnname as its first argument.
Guard (true-listp get-keys).
- user-arg — Arbitrary additional information to pass to the
fnname as its second argument.
Warning: this is a very low-level function. Most of the
time you will want to use higher-level functions like sneaky-save, sneaky-push, and sneaky-incf instead.
In the ACL2 logic, this function simply returns nil. Under the hood,
it can cause (logically invisible) side-effects, typically modifying the hidden
"sneaky store."
The particular details of these side-effects depend upon the fnname
argument passed in. As an example, the definition of sneaky-push is the
following:
(defun sneaky-push (name new-elem)
(sneaky-mutate 'sneaky-push-mutator (list name) (cons name new-elem)))
The symbol sneaky-push-mutator refers to the following function:
(defun sneaky-push-mutator (stored-vals name-elem-pair)
(list (cons (car name-elem-pair)
(cons (cdr name-elem-pair) (car stored-vals)))))
What is going on here? Sneaky-push accesses a value stored under the
name name, and re-stores it with new-elem consed onto it. How does
this occur? A call of
(sneaky-mutate fnname get-keys user-arg)
calls the function f named by fnname, in this case
sneaky-push-mutator. f must always have two arguments:
- The list of values currently associated with get-keys. That is,
sneaky-mutate will look up each key in get-keys and will
send the resulting values to fnname.
- An arbitrary additional argument, provided by user-arg.
So in the case of sneaky-push, the two arguments passed to
sneaky-push-mutator are:
- A list containing the stored value that was previously associated with
name, and
- The cons of name itself onto new-elem.
f must return a single value, which should be an association list.
This alist will be used to update the hidden "sneaky store." In particular,
the store will be modified by assigning each key in the alist to its
corresponding value.
In the case of sneaky-push, the stored value associated with name
is changed to be the cons of new-elem onto the previous stored value; that
is, name gets new-elem pushed onto it.
Definitions and Theorems
Function: sneaky-mutate
(defun sneaky-mutate (fnname get-keys user-arg)
(declare (xargs :guard (and (symbolp fnname)
(true-listp get-keys))))
(declare (ignorable fnname get-keys user-arg))
(let ((__function__ 'sneaky-mutate))
(declare (ignorable __function__))
(progn$ (raise "Under-the-hood definition not yet installed")
nil)))
