Major Section: ACL2-BUILT-INS
Oracle-apply evaluates its first argument to produce an ACL2 function
symbol, FN, and then applies FN to the value of the second argument,
which should be a true list whose length is the number of inputs for FN.
The return value is of the form (mv call-result state).
Examples: (oracle-apply 'cons '(3 4) state) = (mv '(3 . 4) <state>) (oracle-apply (car '(floor foo)) (list (+ 6 7) 5) state) = (mv 2 <state>)
Also see oracle-funcall for a related utility.
Note that calls of oracle-funcall and oracle-apply return two values:
the result of the function application, and a modified state.
Oracle-apply is defined in :logic mode, and in fact is
guard-verified. However, you will not be able to prove much about this
function, because it is defined in the logic using the acl2-oracle field
of the ACL2 state. The behavior described above -- i.e., making a
function call -- takes place when the third argument is the ACL2
state, so during proofs (when that can never happen), a term
(oracle-apply 'fn '...) will not simplify using a call of fn.
The guard for (oracle-apply fn args state) is the term
(oracle-apply-guard fn args state), which says the following: fn and
args must satisfy symbolp and true-listp, respectively;
fn must be a known function symbol other than return-last that is
not untouchable (see push-untouchable) and has no stobj arguments (not
even state); and the length of args must equal the arity of
fn (see signature). The requirement that fn be a known function
symbol may be a bit onerous for guard verification, but this is easily
overcome by using ec-call, for example as follows.
(defun f (x state) (declare (xargs :stobjs state)) (ec-call (oracle-apply 'car (list x) state)))This use of
ec-call will, however, cause the guard of
oracle-apply to be checked at runtime.If the guard for oracle-apply fails to hold but there is no guard
violation because guard-checking is suppressed (see set-guard-checking),
then the value returned is computed using its logical definition -- which,
as mentioned above, uses the ACL2 oracle -- and hence the value computed is
unpredictable (indeed, the function argument will not actually be called).
The value returned by oracle-apply is always a single value obtained by
calling the executable counterpart of its function argument, as we now
explain. Consider a form (oracle-apply fn args state) that evaluates to
(mv VAL state'), where fn evaluates to the function symbol F. If
F returns multiple values, then VAL is the first value computed by
the call of F on the value of args. More precisely, oracle-apply
actually invokes the executable counterpart of F; thus, if args is
the expression (list x1 ... xk), then VAL is the same as (first)
value returned by evaluating (ec-call (F x1 x2 ... xk)). See ec-call.
(Remark. If you identify a need for a version of oracle-apply to return
multiple values, we can perhaps provide such a utility; feel free to contact
the ACL2 implementors to request it.)
A subtlety is that the evaluation takes place in so-called ``safe mode'',
which avoids raw Lisp errors due to calls of :program mode
functions. The use of safe mode is unlikely to be noticed if the value of
the first argument of oracle-apply is a :logic mode function
symbol. However, for :program mode functions with side effects due to
special raw Lisp code, as may be the case for built-in functions or for
custom functions defined with active trust tags (see defttag), use of the
following function may be preferable:
See oracle-apply-raw for a much less restrictive version of oracle-apply,
which avoids safe mode and (for example) can apply a function that has a
definition in the host Lisp but not in the ACL2 world.
