		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-err->fatal

Signature
(vl-err->fatal err &key type msg args (fn '__function__) (acc 'warnings)) → warnings
Arguments: err — Guard (implies err (vl-msg-p err)).; type — Guard (symbolp type).; msg — Guard (stringp msg).; args — Guard (true-listp args).; fn — Guard (symbolp fn).; acc — Guard (vl-warninglist-p acc).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-err->fatal-fn

(defun vl-err->fatal-fn (err type msg args fn acc)
  (declare (xargs :guard (and (implies err (vl-msg-p err))
                              (symbolp type)
                              (stringp msg)
                              (true-listp args)
                              (symbolp fn)
                              (vl-warninglist-p acc))))
  (let ((__function__ 'vl-err->fatal))
    (declare (ignorable __function__))
    (b* ((warnings acc)
         (msg (string-fix msg))
         (args (mbe :logic (list-fix args)
                    :exec args)))
      (if err (fatal :type type
                     :msg "~@0: ~@1"
                     :args (list (make-vl-msg :msg msg :args args)
                                 err)
                     :fn fn)
        (ok)))))

Theorem: vl-warninglist-p-of-vl-err->fatal

(defthm vl-warninglist-p-of-vl-err->fatal
  (b* ((warnings (vl-err->fatal-fn err type msg args fn acc)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-err->fatal-fn-of-symbol-fix-type

(defthm vl-err->fatal-fn-of-symbol-fix-type
  (equal (vl-err->fatal-fn err (acl2::symbol-fix type)
                           msg args fn acc)
         (vl-err->fatal-fn err type msg args fn acc)))

Theorem: vl-err->fatal-fn-symbol-equiv-congruence-on-type

(defthm vl-err->fatal-fn-symbol-equiv-congruence-on-type
 (implies (acl2::symbol-equiv type type-equiv)
          (equal (vl-err->fatal-fn err type msg args fn acc)
                 (vl-err->fatal-fn err type-equiv msg args fn acc)))
 :rule-classes :congruence)

Theorem: vl-err->fatal-fn-of-str-fix-msg

(defthm vl-err->fatal-fn-of-str-fix-msg
  (equal (vl-err->fatal-fn err type (str-fix msg)
                           args fn acc)
         (vl-err->fatal-fn err type msg args fn acc)))

Theorem: vl-err->fatal-fn-streqv-congruence-on-msg

(defthm vl-err->fatal-fn-streqv-congruence-on-msg
 (implies (streqv msg msg-equiv)
          (equal (vl-err->fatal-fn err type msg args fn acc)
                 (vl-err->fatal-fn err type msg-equiv args fn acc)))
 :rule-classes :congruence)

Theorem: vl-err->fatal-fn-of-list-fix-args

(defthm vl-err->fatal-fn-of-list-fix-args
  (equal (vl-err->fatal-fn err type msg (list-fix args)
                           fn acc)
         (vl-err->fatal-fn err type msg args fn acc)))

Theorem: vl-err->fatal-fn-list-equiv-congruence-on-args

(defthm vl-err->fatal-fn-list-equiv-congruence-on-args
 (implies (list-equiv args args-equiv)
          (equal (vl-err->fatal-fn err type msg args fn acc)
                 (vl-err->fatal-fn err type msg args-equiv fn acc)))
 :rule-classes :congruence)

Theorem: vl-err->fatal-fn-of-symbol-fix-fn

(defthm vl-err->fatal-fn-of-symbol-fix-fn
  (equal (vl-err->fatal-fn err type msg args (acl2::symbol-fix fn)
                           acc)
         (vl-err->fatal-fn err type msg args fn acc)))

Theorem: vl-err->fatal-fn-symbol-equiv-congruence-on-fn

(defthm vl-err->fatal-fn-symbol-equiv-congruence-on-fn
 (implies (acl2::symbol-equiv fn fn-equiv)
          (equal (vl-err->fatal-fn err type msg args fn acc)
                 (vl-err->fatal-fn err type msg args fn-equiv acc)))
 :rule-classes :congruence)

Theorem: vl-err->fatal-fn-of-vl-warninglist-fix-acc

(defthm vl-err->fatal-fn-of-vl-warninglist-fix-acc
  (equal (vl-err->fatal-fn err type
                           msg args fn (vl-warninglist-fix acc))
         (vl-err->fatal-fn err type msg args fn acc)))

Theorem: vl-err->fatal-fn-vl-warninglist-equiv-congruence-on-acc

(defthm vl-err->fatal-fn-vl-warninglist-equiv-congruence-on-acc
 (implies (vl-warninglist-equiv acc acc-equiv)
          (equal (vl-err->fatal-fn err type msg args fn acc)
                 (vl-err->fatal-fn err type msg args fn acc-equiv)))
 :rule-classes :congruence)