Major Section: PROGRAMMING
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 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;
see ld-error-triples and see er-progn.
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)))
