Er
Print an error message and ``cause an error''
See fmt for a general discussion of formatted printing in
ACL2. All calls of er print formatted strings, just as is done by fmt.
Example Forms:
(er hard 'top-level "Illegal inputs, ~x0 and ~x1." a b)
(er hard? 'top-level "Illegal inputs, ~x0 and ~x1." a b)
(er hard! 'top-level "Illegal inputs, ~x0 and ~x1." a b)
(er soft 'top-level "Illegal inputs, ~x0 and ~x1." a b)
(er-soft 'top-level "Illegal-inputs" "Illegal inputs, ~x0 and ~x1." a b)
The examples above all print an error message to standard output saying
that (the values of) a and b are illegal inputs. However, the first
three — which we call hard errors — abort evaluation after
printing an error message (while logically returning nil, though in
ordinary evaluation the return value is never seen); while the last two
— so-called soft errors — return an error-triple,
(mv t nil state), after printing an error message. The result in each of
the two soft error cases can be interpreted as an ``error'' when programming
with the ACL2 state, something most ACL2 users will probably not want
to do unless they are building systems of some sort; see programming-with-state. If state is not available in the current context
then you will probably want to cause a hard error; for example, if you are
returning two values, you may write (mv (er hard ...) nil).
The difference between the hard and hard? forms is one of guards.
Use hard if you want the call to generate a (clearly impossible) guard
proof obligation of (essentially) NIL. But use hard? if you want to
be able to call this function in guard-verified code, since the call generates
a (trivially satisfied) guard proof obligation of T.
The difference between the hard and hard! forms is that there are
situations in which (er hard ...) returns nil rather than causing an
error, while (er hard! ...) will always cause an error (though such
errors are sometimes ``caught'', for example during proofs). You will
probably be happy using hard rather than considering the use of
hard!, which is really provided mostly for system implementors; but you
can try hard! if you are not getting the errors you expect. There is
even an additional option, hard?!, which avoids guard proof obligations
like hard? but ensures errors like hard!.
Er is a macro, and the examples above expand to calls of ACL2
functions; see below. Also see illegal, hard-error, and error1. The hard?/hard?! forms have expansions that call the
function hard-error, which has a guard of T, while the
hard/hard! forms have expansions that call the function illegal, which has a guard that is logically NIL. Those generate code
that is in :logic mode, as do variants of (er soft ...).
The soft error forms expand to calls of the function error1, which
necessarily takes state as an explicit argument since it returns an
error-triple. The guard for the soft error forms is that of error1. Note in particular that soft errors require the state to satisfy
certain restrictions beyond just the usual state-p predicate.
The general forms of the macros are as follows. Their macroexpansions
include code that avoids the printing of error messages when error output is
inhibited — see set-inhibit-output-lst — but here we show
only the essential function calls. Note that all arguments are evaluated even
when error output is inhibited.
General Forms:
(er hard ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ILLEGAL CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
(er hard? ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(HARD-ERROR CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
(er hard! ctx fmt-string arg1 arg2 ... argk)
; logically is same as (er hard ...), but always produces an error
(er soft ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ERROR1 CTX NIL FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
(er-soft ctx summary fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ERROR1 CTX SUMMARY FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
See ctx for the possible forms of the ctx argument.
Technical note for raw Lisp programmers only: It is possible to cause hard
errors to signal actual raw Lisp errors. See hard-error.
Subtopics
- Raise
- Shorthand for causing hard errors.
