Trans-eval
Evaluate a form
This relatively advanced system utility translates and evaluates a
form. The following examples illustrate that an error-triple is
returned whose value component is (stobjs-out . values).
ACL2 !>(trans-eval '(+ 3 4) 'my-ctx state nil)
((NIL) . 7)
ACL2 !>(trans-eval '(mv (+ 3 4) (car '(5))) 'my-ctx state nil)
((NIL NIL) 7 5)
ACL2 !>
General Form:
(trans-eval form ; an untranslated form
ctx ; a context
state
aokp) ; allow attachments
The result is an error-triple, (mv erp val state). The value
of erp is non-nil if there is an error when translating form.
Otherwise erp is typically nil, in which case val is a
cons pair whose car is the stobjs-out — a list whose
length is the number of values returned, with nil in each position except
when occupied by a returned stobj for that position — and whose
cdr is the returned value or list of values in the multiple-value
case.
Also see simple-translate-and-eval-cmp in the ACL2 sources, and see
trans-eval-error-triple (and, which is perhaps less useful, trans-eval-state).
If you use trans-eval then you may see a warning, for example as
follows.
ACL2 !>(foo st state)
ACL2 Warning [User-stobjs-modified] in FOO: A call of the ACL2 evaluator
on the term (UPDATE-FLD '4 ST) may have modified the user stobj ST. See
:DOC user-stobjs-modified-warning.
(4 <state> <st>)
ACL2 !>
These warnings indicate a potentially serious violation of applicative
semantics when one is also updating user-defined stobjs outside calls of
trans-eval! To understand and perhaps avoid such warnings, see user-stobjs-modified-warnings. Also see trans-eval-and-locally-bound-stobjs for discussion of how trans-eval
modifies global stobj values, not locally-bound stobjs.
Subtopics
- User-stobjs-modified-warnings
- Interactions of trans-eval with stobjs that violate
applicative semantics
- Trans-eval-and-stobjs
- How user-defined stobjs are handled by trans-eval
- Trans-eval-and-locally-bound-stobjs
- Trans-eval deals in global stobjs.
