Major Section: ACL2-BUILT-INS
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 soft 'top-level "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 two abort evaluation
after printing an error message (while logically returning nil, though in
ordinary evaluation the return value is never seen); while the third returns
(mv t nil state) after printing an error message. The result in the
third case 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 (er hard ...) or (er hard? ...) 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.
Er is a macro, and the above three examples expand to calls of ACL2
functions, as shown below. See illegal, see hard-error, and see error1.
The first two have guards of (essentially) NIL and T, respectively,
while error1 is in :program mode.
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 soft ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ERROR1 CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
