ORACLE-APPLY

call a function argument on the given list of arguments
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 subtlely 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.