Major Section: ACL2-BUILT-INS
See oracle-apply, as we assume familiarity with that function.
Oracle-apply-raw is a variant of oracle-apply that is untouchable,
and hence requires a trust tag to remove the untouchability (see defttag and
see remove-untouchable). Unlike oracle-apply, oracle-apply-raw
simply calls the raw Lisp function funcall to compute the result, without
restriction: the specified :guard is t, the function itself is
applied (not its executable counterpart), there is no restriction for
untouchable functions or return-last, and safe mode is not used. Thus,
in general, oracle-apply-raw can be dangerous to use: any manner of error
can occur!
As is the case for oracle-apply, the function symbol
oracle-apply-raw is defined in :logic mode and is
guard-verified. Oracle-apply-raw is logically defined to be
oracle-apply; more precisely:
(oracle-apply-raw fn args state)
= {logical definition}
(ec-call (oracle-apply fn args state))
