Magic-ev-fncall
Call the named function on the given arguments and return the value.
Introduction. Magic-ev-fncall is a logic-mode function
that can apply a given function (which need not be in logic mode) to an
argument list. Although the result can be computed, magic-ev-fncall is
technically a constrained function (with unknown constraints), which can be
assumed in metafunctions and clause processors to produce correct
results, via meta-extract.
Examples:
(magic-ev-fncall 'cons '(3 4) state t nil)
= (mv nil '(3 . 4))
(magic-ev-fncall (car '(floor foo)) (list (+ 6 7) 5) state t nil)
= (mv nil 2)
General Form:
(magic-ev-fncall fn arglist state hard-error-returns-nilp aokp)
where fn is a function symbol, arglist is a suitable argument
list for fn, and the last two formals are described below. When
successful, the result is (mv nil value) where value is the
application of fn to arglist. Although this fact cannot be proven,
it may be assumed correct in metafunctions and clause processors via meta-extract, assuming of course that fn is a logic-mode
function.
In general, the result is either (mv t error-msg) (if, e.g., the
function was not defined, the arity was wrong, or the guards were violated) or
(mv nil value) on success. In the case of a multiple-valued
function the second return value is the list of values. A non-nil error
message, error-msg, is a message suitable for printing with fmt;
see msg.
If a hard error is encountered during execution and
hard-error-returns-nilp is non-nil, then the error is ignored and
the value returned is (mv nil nil) (note that the logical value of a call
of HARD-ERROR is nil). If hard-error-returns-nilp is nil
then the return value is of the form (mv T error-msg).
The aokp argument controls whether attachments to constrained
functions may be executed (see defattach). If nil, then an error
message is returned when an attachment would otherwise be executed.
When used in a clause-processor or metafunction, it can be assumed via a
meta-extract hypothesis that magic-ev-fncall works correctly with
respect to the evaluator, but only if hard-error-returns-nilp is t
and aokp is nil.
The guard for (magic-ev-fncall fn arglist state h aokp) is
t, but evaluation of this call enforces the following requirements.
- Fn must be a function symbol of the current ACL2 world other
than if, whose arity is equal to the length of the true-list,
arglist.
- Fn must not have any stobj inputs or be a stobj creator.
- Calls of fn must not require a trust tag (see defttag).
- Fn must not be untouchable (see push-untouchable).
The implementation of these checks incorporates a bit of trickery so that
they are reasonably efficient.
Note that set-guard-checking affects evaluation of calls of
(magic-ev-fncall fn ...) just as it affects calls of fn, for example
as follows.
ACL2 !>(magic-ev-fncall 'car '((a b c)) state t nil)
(NIL A)
ACL2 !>(magic-ev-fncall 'car '(3) state t nil)
(T <... message elided here ...>)
ACL2 !>(set-guard-checking nil)
Masking guard violations but still checking guards except for self-
recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE. See :DOC set-guard-checking.
ACL2 >(magic-ev-fncall 'car '(3) state t nil)
(NIL NIL)
ACL2 >
Additional Notes.
- If fn is a program-mode function, then the call will be
evaluated under safe-mode, which avoids raw Lisp errors due to calls of
ill-guarded program-mode functions.
- If the application of fn returns multiple values (mv v1 v2 ...),
then the resulting value will be the corresponding list (v1 v2 ...).
- A reasonable model for (magic-ev-fncall 'fn (list a1 a2 ...) state h
aokp) is (ec-call (fn a1 a2 ...)).
