		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-unparam-basename

Generate a new name for an unparameterized module.

Signature
(vl-unparam-basename origname paramdecls ifportalist include-default) → new-name
Arguments: origname — Original name of the module, e.g., my_adder.
Guard (stringp origname).; paramdecls — Final, overridden paramdecls for the module.
Guard (vl-paramdecllist-p paramdecls).; ifportalist — Interface port alist.
Guard (vl-ifport-alist-p ifportalist).; include-default — Include non-overridden parameters in the generated names.
Guard (booleanp include-default).
Returns: new-name — New, mangled name, e.g., my_adder$size=5.
Type (stringp new-name).

Definitions and Theorems

Function: vl-unparam-basename

(defun vl-unparam-basename
       (origname paramdecls ifportalist include-default)
 (declare (xargs :guard (and (stringp origname)
                             (vl-paramdecllist-p paramdecls)
                             (vl-ifport-alist-p ifportalist)
                             (booleanp include-default))))
 (let ((__function__ 'vl-unparam-basename))
  (declare (ignorable __function__))
  (with-local-ps
    (vl-ps-seq
         (vl-print-str origname)
         (vl-unparam-basename-paramdecls paramdecls include-default)
         (vl-unparam-basename-ifports ifportalist)))))

Theorem: stringp-of-vl-unparam-basename

(defthm stringp-of-vl-unparam-basename
  (b* ((new-name (vl-unparam-basename origname paramdecls
                                      ifportalist include-default)))
    (stringp new-name))
  :rule-classes :type-prescription)

Theorem: vl-unparam-basename-of-str-fix-origname

(defthm vl-unparam-basename-of-str-fix-origname
 (equal (vl-unparam-basename (str-fix origname)
                             paramdecls ifportalist include-default)
        (vl-unparam-basename origname paramdecls
                             ifportalist include-default)))

Theorem: vl-unparam-basename-streqv-congruence-on-origname

(defthm vl-unparam-basename-streqv-congruence-on-origname
 (implies
   (streqv origname origname-equiv)
   (equal
        (vl-unparam-basename origname
                             paramdecls ifportalist include-default)
        (vl-unparam-basename origname-equiv paramdecls
                             ifportalist include-default)))
 :rule-classes :congruence)

Theorem: vl-unparam-basename-of-vl-paramdecllist-fix-paramdecls

(defthm vl-unparam-basename-of-vl-paramdecllist-fix-paramdecls
  (equal (vl-unparam-basename origname
                              (vl-paramdecllist-fix paramdecls)
                              ifportalist include-default)
         (vl-unparam-basename origname paramdecls
                              ifportalist include-default)))

Theorem: vl-unparam-basename-vl-paramdecllist-equiv-congruence-on-paramdecls

(defthm
 vl-unparam-basename-vl-paramdecllist-equiv-congruence-on-paramdecls
 (implies
   (vl-paramdecllist-equiv paramdecls paramdecls-equiv)
   (equal
        (vl-unparam-basename origname
                             paramdecls ifportalist include-default)
        (vl-unparam-basename origname paramdecls-equiv
                             ifportalist include-default)))
 :rule-classes :congruence)

Theorem: vl-unparam-basename-of-vl-ifport-alist-fix-ifportalist

(defthm vl-unparam-basename-of-vl-ifport-alist-fix-ifportalist
  (equal (vl-unparam-basename origname paramdecls
                              (vl-ifport-alist-fix ifportalist)
                              include-default)
         (vl-unparam-basename origname paramdecls
                              ifportalist include-default)))

Theorem: vl-unparam-basename-vl-ifport-alist-equiv-congruence-on-ifportalist

(defthm
 vl-unparam-basename-vl-ifport-alist-equiv-congruence-on-ifportalist
 (implies
   (vl-ifport-alist-equiv ifportalist ifportalist-equiv)
   (equal
        (vl-unparam-basename origname
                             paramdecls ifportalist include-default)
        (vl-unparam-basename origname paramdecls
                             ifportalist-equiv include-default)))
 :rule-classes :congruence)

Theorem: vl-unparam-basename-of-bool-fix-include-default

(defthm vl-unparam-basename-of-bool-fix-include-default
  (equal (vl-unparam-basename origname paramdecls ifportalist
                              (acl2::bool-fix include-default))
         (vl-unparam-basename origname paramdecls
                              ifportalist include-default)))

Theorem: vl-unparam-basename-iff-congruence-on-include-default

(defthm vl-unparam-basename-iff-congruence-on-include-default
 (implies
   (iff include-default include-default-equiv)
   (equal
        (vl-unparam-basename origname
                             paramdecls ifportalist include-default)
        (vl-unparam-basename origname paramdecls
                             ifportalist include-default-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-unparam-basename-paramdecls
Vl-unparam-basename-ifports