er-soft-logic - ACL2 Book

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

other

(defxdoc er-soft-logic
  :parents (errors)
  :short "Print an error message and ``cause an error''"
  :long "<p>See @(see er) for relevant background.</p>

 @({
 General Form:
 (er-soft-logic ctx fmt-string arg1 arg2 ... argk)
 })

 <p>The form above has essentially the same effect as the following.</p>

 @({
 (er soft ctx fmt-string arg1 arg2 ... argk)
 })

 <p>Both expressions generate @(see logic)-mode code, though the latter
 generates a stronger @(see guard) proof obligation.  (At one time, the latter
 generated @(see program)-mode code, which is why @('er-soft-logic') was
 introduced.)  @('Er-soft-logic') works by invoking the function call
 @('(error-fms-soft-logic ctx fmt-string alist state)'), where @('alist') is as
 in the @('alist') argument of @(tsee fmt).</p>

 <p>For a similar utility that returns a specified error and value component of
 the returned @(see error-triple), see @(see er-soft+).</p>")

error-fms-soft-logicfunction

(defun error-fms-soft-logic
  (ctx str alist state)
  (declare (xargs :stobjs state))
  (and (f-boundp-global 'abbrev-evisc-tuple state)
    (f-boundp-global 'inhibit-output-lst state)
    (true-listp (f-get-global 'inhibit-output-lst state))
    (not (member-eq 'error (f-get-global 'inhibit-output-lst state)))
    (fmt-to-comment-window+ "~%~%ACL2 Error in ~@0:  ~@1~%~%"
      (list (cons #\0
          (cond ((null ctx) "")
            ((symbolp ctx) (msg "~x0" ctx))
            ((and (consp ctx) (symbolp (car ctx))) (msg "(~@0~x1 ~x2 ...)"
                (if (member-eq (car ctx) *fmt-ctx-spacers*)
                  " "
                  "")
                (car ctx)
                (cdr ctx)))
            (t ctx)))
        (cons #\1 (cons str alist)))
      0
      (abbrev-evisc-tuple state)
      nil)))

error1-logicfunction

(defun error1-logic
  (ctx str alist state)
  (declare (xargs :stobjs state))
  (prog2$ (error-fms-soft-logic ctx str alist state)
    (mv t nil state)))

er-soft-logicmacro

(defmacro er-soft-logic
  (ctx str &rest str-args)
  (let ((alist (make-fmt-bindings '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
         str-args)))
    (list 'error1-logic ctx str alist 'state)))