		Search-engine friendly clone of the ACL2 documentation.

Genblob

Vl-package->genblob

Convert most of a package into a vl-genblob.

Signature
(vl-package->genblob x) → genblob
Arguments: x — Guard (vl-package-p x).
Returns: genblob — Type (vl-genblob-p genblob).

Certain fields of a vl-package aren't also fields of a vl-genblob, for instance, a genblob doesn't have warnings, a name, location information, etc.

But aside from these fields, most of a package can be extracted and turned into a genblob for easy processing. After processing the blob, the updated fields can be reinstalled into the package using vl-genblob->package.

Definitions and Theorems

Function: vl-package->genblob

(defun vl-package->genblob (x)
  (declare (xargs :guard (vl-package-p x)))
  (let ((__function__ 'vl-package->genblob))
    (declare (ignorable __function__))
    (b* (((vl-package x)))
      (make-vl-genblob :id x.name
                       :scopetype :vl-package
                       :fundecls x.fundecls
                       :taskdecls x.taskdecls
                       :typedefs x.typedefs
                       :paramdecls x.paramdecls
                       :vardecls x.vardecls
                       :imports x.imports))))

Theorem: vl-genblob-p-of-vl-package->genblob

(defthm vl-genblob-p-of-vl-package->genblob
  (b* ((genblob (vl-package->genblob x)))
    (vl-genblob-p genblob))
  :rule-classes :rewrite)

Theorem: vl-package->genblob-of-vl-package-fix-x

(defthm vl-package->genblob-of-vl-package-fix-x
  (equal (vl-package->genblob (vl-package-fix x))
         (vl-package->genblob x)))

Theorem: vl-package->genblob-vl-package-equiv-congruence-on-x

(defthm vl-package->genblob-vl-package-equiv-congruence-on-x
  (implies (vl-package-equiv x x-equiv)
           (equal (vl-package->genblob x)
                  (vl-package->genblob x-equiv)))
  :rule-classes :congruence)