Value-triple
Compute a value, optionally checking that it is not nil
Simple Example
; Return the value 7 as an error triple, i.e., (mv nil 7 state)).
(value-triple (+ 3 4))
Examples Involving Keyword Arguments
; Print "hi" even when skipping proofs.
(value-triple (cw "hi") :on-skip-proofs t)
; Return an error triple containing the value of a state global.
; (This shows that it's OK to reference state.)
(value-triple (@ ld-pre-eval-print))
; Check that the given form returns a non-nil value.
(value-triple (equal (+ 3 4) 7) :check t)
; Check that the given defun is admissible, then revert the world.
(value-triple (er-progn (defun foo (x) (cons x x))
(value :success))
:stobjs-out :auto)
General Form
(value-triple form
:check chk ; default nil
:ctx ; default 'value-triple
:on-skip-proofs sp ; default nil
:safe-mode safe-mode ; default :same
:stobjs-out stobjs-out ; default nil
)
where all keyword arguments are evaluated and optional, and the defaults
shown above represent values after evaluation.
The following example illustrates all of the keyword arguments, which are
documented below.
(value-triple (mv nil (equal (+ 3 4) 7) state)
:check (msg "Oops, I forgot what ~x0+~x1 is!" 3 4)
:ctx '(value-triple . <some-mv>)
:on-skip-proofs t
:safe-mode nil ; legacy behavior (rarely used)
:stobjs-out '(nil nil state))
Description
Value-triple provides a convenient way to evaluate a form in a context
where an event is expected; thus, a call of value-triple may occur
in progn and encapsulate forms and in books. By
default, the form should evaluate to a single, non-stobj value (but see
the discussion below about the :STOBJS-OUT keyword argument). Calls of
value-triple are skipped by default when proofs are being skipped (but
see the discussion below about the :ON-SKIP-PROOFS keyword argument). By
default, a value-triple call has no effect other than to evaluate its
form, but see the discussion of the :CHECK keyword below for how to check
the result.
A call of value-triple returns an error-triple, (mv erp val
state). By default or when :CHECK nil is supplied: erp is
nil when evaluation completes without error and val is the value
returned by evaluating the given form. However, when the keyword argument
:CHECK has a non-nil value, there is a check that val is
non-nil. Note that the value of keyword argument :STOBJS-OUT can
affect this notion of ``the value returned'' (by evaluation), as discussed
below.
Keyword Arguments
Here is documentation for the keyword arguments, arranged alphabetically
and followed by relevant remarks.
:CHECK chk (default: nil)
When chk is supplied and non-nil, the value returned by
evaluating the given form must be non-nil, or else an error occurs: The
error message is generic if chk is t. (By default a single value is
returned, so the notion of ``the value returned'' is clear; but see the
discussion of :STOBJS-OUT below for the notion of ``the value returned''
in the general case.) If chk is supplied and is neither t nor
nil, then it should be a ``message'' (see msg) that is used when
printing the error message.
:CTX ctx (default: 'value-triple)
Error messages from value-triple start, by default, with ``ACL2 Error
in VALUE-TRIPLE''. To replace VALUE-TRIPLE with a different context (see
ctx), ctx, supply keyword argument :CTX ctx.
:ON-SKIP-PROOFS sp (default: nil)
By default or when :ON-SKIP-PROOFS has value nil, the form is not
evaluated when proofs are being skipped. The form is, however, evaluated when
:ON-SKIP-PROOFS t is supplied. The other legal value for
:ON-SKIP-PROOFS is :interactive, which is more restrictive than
t. :Interactive directs the value-triple call to be skipped
when executing an include-book or making a second pass through an
encapsulate, but not merely because (set-ld-skip-proofsp t state)
has been executed.
:SAFE-MODE safe-mode (default: :same)
It is usually safe to ignore this option, which is available for backward
compatibility: :SAFE-MODE t gives the behavior of assert-event from
before April, 2021. Normally ACL2 operates without so-called ``safe-mode'';
see safe-mode. The value :same prevents any change in whether
safe-mode is on or off; otherwise the value is t to evaluate the form
with safe-mode on and nil for safe-mode off.
:STOBJS-OUT stobjs-out (default: nil)
When stobjs-out has its default value of nil, which abbreviates
the value (nil), the form supplied to value-triple is expected to
evaluate to a single value that is neither a stobj nor a df.
However, multiple-value return is also allowed, including
stobjs (user-defined stobjs as well as state). The return shape is
specified by supplying stobjs-out as a true list corresponding to the
values returned, with stobj names in stobj positions and, :DF in df
positions, and nil elsewhere. (The list has length one if a single value
is returned.) For example, if stobjs-out is (nil st1 nil st2) then
the form should evaluate to a multiple-value return, with ordinary
values in (zero-based) positions 0 and 2, stobj st1 in position 1, and
stobj st2 in position 3.
Stobjs-out may also be :auto, which allows arbitrary returns.
We speak of ``the value returned''. When the evaluation results in a
single value, that is of course the value returned. When multiple values are
returned, the first of those values is normally what we mean by ``the value
returned'', with the following exception. When an error-triple is
returned — say (mv erp val state) where erp is an ordinary
value, val is a non-stobj value, and state is the ACL2 state — then val is considered to be the value returned if
erp is nil; but if erp is not nil, then there is no value
returned, and value-triple results in an error.
If :CHECK has a non-nil value then the value returned must not be
a stobj. Otherwise, when the value returned is a stobj it is replaced by the
stobj's name, as discussed below.
Remarks
We conclude by remarking on some details. These remarks also apply to
assert-event, since it expands to make corresponding calls of
value-triple.
- Since value-triple is an event macro, it returns an error-triple, that is, the multiple values (mv erp val state), where
erp is nil exactly when the event completes without error. If the
value of keyword argument :CHECK is non-nil and erp is
nil, then val is :passed. Otherwise val is the value
returned as discussed above. To be precise: val is the result of
evaluating the given form in the default case, when :STOBJS-OUT is not
provided (or is nil or (nil)), but in general there several cases
possible, as follows.
- If the evaluation of the given form results in a single ordinary value,
then val is that value.
- If the evaluation of the given form results in a single stobj value, then
val is that stobj's name (a symbol). In particular, if the value is
state, then val is the symbol STATE (in the "ACL2"
package).
- If the evaluation of the given form results in a single df value,
then val is the corresponding rational number.
- If the evaluation of the given form results in multiple values (mv x1
...), then val is x1 if x1 is not a stobj (but converted to a
rational if x1 is a df), else val is the name of that
stobj.
- When :STOBJS-OUT is :auto and at least one user-defined stobj is returned, you will see a "User-stobjs-modified" warning
unless warnings have been suppressed. Although warnings are typically
suppressed by general utilities such as set-inhibit-output-lst, set-inhibit-warnings, and with-output, a more direct way to avoid
this warning is to specify :STOBJS-OUT as a list (as discussed
above).
- As noted above, the ACL2 state may change when keyword option
:STOBJS-OUT has a value other than nil or (nil). Nevertheless,
ACL2 ensures that certain parts of the state, including the logical world, are the same after the value-triple call completes as they were
before (as with make-event expansion; see make-event). Also,
trust tags (see defttag) must not be introduced during such
evaluation.
- (Ignore this remark unless you make many, many calls of
value-triple.) Evaluation may be much faster when :STOBJS-OUT is
omitted or is specified as nil (the default) or (nil). That is
because otherwise, since the return shape is checked only after evaluation
completes, therefore a somewhat complex environment set-up is performed prior
to evaluation, in which certain parts of the ACL2 state are protected
as for make-event (using revert-world, and also as discussed
in the documentation for make-event about
*protected-system-state-globals*). Moreover, evaluation is faster still
if in addition, the given form is t, nil, a keyword, or of
the form (QUOTE x).
