|
|
|---|
|
|
|
|---|
A macro to assist in signalling runtime errors
The coi-debug::fail macro allows the user to signal runtime errors in ACL2 code. The return value of coi-debug::fail can be set by specifying a :value parameter. The failure message can be configured via the :message keyword. Additional parameters can be passed in as a list via :parameters.
Typical usage pattern:
(if (consp x) (car x) (coi-debug::fail :value nil :message "~x0 is not a consp" :parameters (x)))
It is sometimes convenient when debugging to induce a common-lisp break on a failure. The following code will do just that.
FOO !> (acl2::progn (acl2::defttag t) (acl2::progn! (acl2::set-raw-mode t) (defun coi-debug::fail-fn (value message parameters) (acl2::prog2$ (acl2::fmt-to-comment-window message parameters 0 nil nil) (acl2::break)))))