Encapsulate-report-errors
Run encapsulate, but with a helpful error at the first
failure of one of its top-level events (if any).
This macro is equivalent to encapsulate except that it takes
an extra argument, which is a context, that goes in the first
position. Unlike encapsulate, it provides a helpful error if any of its
given events fails. It uses that extra `context' argument in reporting
that error. (But the error itself is reported by the event, with the usual
context constructed for that event.)
General Form:
(encapsulate-report-errors ctx signature-list event1 event2 ... eventk)
where ctx is a context, signature-list is a list of signatures, and each eventi is an embedded-event-form. Note that
none of these arguments is evaluated. Thus, a typical call might be laid down
as follows.
`(encapsulate-report-errors ,ctx () ,@events)
Normally, if if any of the given events (shown above as ``event1 event2
... eventk'') fails, then the output will conclude as follows, where here we
write <CTX> to denote the formatted context and <EV> to denote the
failed event printed in abbreviated form.
ACL2 Error in <CTX>: The following event has caused an
unexpected error:
<EV>
Please contact the implementor of the tool that you are using.
However, if the event is of the form (on-failure ...), then the
specified failure message is printed instead of this generic one. See on-failure.
