		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-err->vfatal

Signature
(vl-err->vfatal err &key type msg args (fn '__function__) (vttree 'vttree)) → new-vttree
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).; vttree — Guard (vttree-p vttree).
Returns: new-vttree — Type (vttree-p new-vttree).

Definitions and Theorems

Function: vl-err->vfatal-fn

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

Theorem: vttree-p-of-vl-err->vfatal

(defthm vttree-p-of-vl-err->vfatal
  (b* ((new-vttree (vl-err->vfatal-fn err type msg args fn vttree)))
    (vttree-p new-vttree))
  :rule-classes :rewrite)

Theorem: constraints-of-vl-err->vfatal

(defthm constraints-of-vl-err->vfatal
 (b* ((?new-vttree (vl-err->vfatal-fn err type msg args fn vttree)))
   (equal (vttree->constraints new-vttree)
          (vttree->constraints vttree))))

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

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

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

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

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

(defthm vl-err->vfatal-fn-of-str-fix-msg
  (equal (vl-err->vfatal-fn err type (str-fix msg)
                            args fn vttree)
         (vl-err->vfatal-fn err type msg args fn vttree)))

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

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

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

(defthm vl-err->vfatal-fn-of-list-fix-args
  (equal (vl-err->vfatal-fn err type msg (list-fix args)
                            fn vttree)
         (vl-err->vfatal-fn err type msg args fn vttree)))

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

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

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

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

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

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

Theorem: vl-err->vfatal-fn-of-vttree-fix-vttree

(defthm vl-err->vfatal-fn-of-vttree-fix-vttree
  (equal (vl-err->vfatal-fn err
                            type msg args fn (vttree-fix vttree))
         (vl-err->vfatal-fn err type msg args fn vttree)))

Theorem: vl-err->vfatal-fn-vttree-equiv-congruence-on-vttree

(defthm vl-err->vfatal-fn-vttree-equiv-congruence-on-vttree
 (implies
      (vttree-equiv vttree vttree-equiv)
      (equal (vl-err->vfatal-fn err type msg args fn vttree)
             (vl-err->vfatal-fn err type msg args fn vttree-equiv)))
 :rule-classes :congruence)