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 a and b are illegal inputs. However, the first three 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 return (mv t nil state) after printing an error message.
The result in each of the last two 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 use a call other than the last to cause
an 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 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.
