orelse

(in-package "ACL2")

(defxdoc orelse
  :parents (system-utilities-non-built-in)
  :short "Evaluate an event and, if it fails, then evaluate a second event"
  :long "<p>NOTE: Also see @(see orelse*) for a similar utility that allows any
 number of @(see events).</p>

 @({
 General Form:

 (orelse form1 form2
         :quiet       q ; default nil
         :no-error    n ; default nil
         :expansion?p e ; default t
 })

 <p>where @('form1') and @('form2') are @(see events) (see @(see
 embedded-event-form)) and the keywords have the indicated defaults.  The
 behavior is as follows: @('form1') is submitted and if that succeeds &mdash;
 that is, if the result is an @(see error-triple) @('(mv nil val state)')
 &mdash; then the @('orelse') call returns that error-triple.  Otherwise, it
 return the result of evaluating @('form2'), except that if that evaluation
 also fails and if @(':no-error') is non-@('nil'), then evaluation concludes by
 submitting the event @('(value-triple :failed)').</p>

 <p>If @(':quiet') has a non-@('nil') value, then output is suppressed using
 @(tsee with-output) with argument @(':stack :push'), so that @('form1') and
 @('form2') may recover the original output environment using @('with-output')
 with argument @(':stack :pop').</p>

 <p>The sizes of @(see certificate) files may be reduced with @(':expansion?p
 t') (the default).  That argument avoids storing a @(tsee make-event)
 expansion for @('(orelse form1 form2 ...)') when evaluation of the first event
 form succeeds.</p>

 <p>See community book @('kestrel/utilities/orelse.lisp') for a utility, @(tsee
 encapsulate-report-errors), that employs @('orelse').</p>")

(defxdoc orelse*
  :parents (system-utilities-non-built-in)
  :short "Evaluate a sequence of @(see events), until one succeeds"
  :long "<p>@('Orelse*') behaves as described in the documentation for @(see
 orelse), except that @('orelse*') takes a list of forms.</p>

 @({
 General Form:

 (orelse* (form1 form2 ...)
          :quiet       q ; default nil
          :no-error    n ; default nil
          :expansion?p e ; default t
 })")

(defxdoc on-failure
  :parents (system-utilities-non-built-in)
  :short "Run an event, printing a custom error message if it fails."
  :long "
 @({
 General Form:

 (on-failure event
             :ctx ctx ; default "event processing"
             :erp erp ; default t
             :val val ; default nil
             :msg msg ; default nil
             )
 })

 <p>where @('event') is an @(see embedded-event-form), and the other arguments
 are passed to @(tsee fail-event) as explained below.  Thus, none of the
 arguments is evaluated.  The General Form above expands to the following.</p>

 @({
 (ORELSE EVENT
         (FAIL-EVENT CTX ERP VAL MSG))
 })

 <p>Thus, first @('event') is evaluated &mdash; see @(see orelse) &mdash; and
 either it succeeds or else the indicated error occurs &mdash; see @(see
 fail-event).</p>

 <p>Consider the following example.</p>

 @({
 (on-failure (defund f (x) x)
             :ctx (defund . f) ; see :doc ctx
             :erp t   ; see :doc er-soft+
             :val nil ; see :doc er-soft+
             :msg ("Failed:~|~%~x0" (#\0 . (defun f (x) x))))
 })

 <p>If @('f') is not already defined, then this is essentially equivalent to
 @('(defund f (x) x)').  But if @('f') currently has a conflicting definition,
 then the event will fail and the final error message, unless error output is
 inhibited (see @(see set-inhibit-output-lst)), will be the following.</p>

 @({
 ACL2 Error in (DEFUND F ...):  Failed:

 (DEFUN F (X) X)
 })

 <p>For another example of the use of @('on-failure'), which uses the macro
 @(tsee msg) to construct a @(see msgp), see the definition of function
 @('report-event-when-error-fn') in @(see community-book)
 @('books/kestrel/utilities/orelse.lisp').</p>")

(defxdoc encapsulate-report-errors
  :parents (system-utilities-non-built-in)
  :short "Run @(tsee encapsulate), but with a helpful error at the first
 failure of one of its top-level events (if any)."
  :long "<p>This macro is equivalent to @(see encapsulate) except that it takes
 an extra argument, which is a @(see context), that goes in the first
 position.  Unlike @('encapsulate'), it provides a helpful error if any of its
 given @(see 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.)</p>

 @({
 General Form:

 (encapsulate-report-errors ctx signature-list event1 event2 ... eventk)
 })

 <p>where @('ctx') is a context, @('signature-list') is a list of @(see
 signature)s, and each @('eventi') is an @(see embedded-event-form).  Note that
 none of these arguments is evaluated.  Thus, a typical call might be laid down
 as follows.</p>

 @({
 `(encapsulate-report-errors ,ctx () ,@events)
 })

 <p>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.</p>

 @({
 ACL2 Error in <CTX>:  The following event has caused an
 unexpected error:

 <EV>

 Please contact the implementor of the tool that you are using.
 })

 <p>However, if the event is of the form @('(on-failure ...)'), then the
 specified failure message is printed instead of this generic one.  See @(see
 on-failure).</p>")

(defxdoc identity-macro
  :parents (system-utilities-non-built-in)
  :short "The most trivial macro imaginable"
  :long "<p>@('(Identity-macro x)') macroexpands to @('x').</p>")