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 above examples expand to calls of ACL2
functions, as shown below. See illegal, see hard-error, and see
error1. The hard?/hard?! forms have guards of (essentially)
NIL while the hard/hard! forms have guards of (essentially)
T. Error1, on the other hand, is in :program
mode; for variants of (er soft ...) that generate :logic
mode code, see er-soft-logic and er-soft+.
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.
