Error1
Print an error message and cause a ``soft error''
(Error1 ctx summary str alist state) returns (mv t nil
state). An error message is first printed using the ``context'' ctx,
as well as the string str and alist alist that are of the same kind
as expected by fmt — unless error output is inhibited
(see set-inhibit-output-lst and with-output) or summary is
non-nil, in which case it is a string, and error output of that type is
inhibited (see set-inhibit-er). See fmt.
Error1 can be interpreted as causing 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. However, error1
is a guard verified logic mode function whose guard is
(AND (STATE-P STATE)
(STRINGP STR)
(ERROR1-STATE-P STATE)
(CHARACTER-ALISTP ALIST)
(OR (NULL SUMMARY) (STRINGP SUMMARY)))
Note in particular that the state must not only satisfy the basic
recognizer, state-p, for ACL2 states but must also satisfy
error1-state-p, which includes additional restrictions ensuring that
error1 can print formatted output to the standard character output
channel, standard-co, interpret the table maintained by set-inhibit-er, etc. If the complexity of error1's guard discourages
you from using it in guard-verified logic mode systems you may wish to cause a
hard-error with illegal or the more unified way of signaling
errors with the macro er.
As mentioned above, error1 always returns (mv t nil state). But
if a call (error1 ctx summary str alist) is encountered during
evaluation, then unless output is inhibited as described above, the string
str is first printed using the association list alist (as in fmt). Here is a trivial, contrived example.
ACL2 !>(error1 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))
state)
ACL2 Error in MY-CONTEXT: Printing 4: four
ACL2 !>
