		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-unparam-newname

Generate a new name for an unparameterized module.

Signature
(vl-unparam-newname origname paramdecls) → 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).
Returns: new-name — New, mangled name, e.g., my_adder$size=5.
Type (stringp new-name).

This is a dumb but probably sufficient way to generate new names. Note that we explicitly check (later on) that no name conflicts are introduced.

Definitions and Theorems

Function: vl-unparam-newname

(defun vl-unparam-newname (origname paramdecls)
  (declare (xargs :guard (and (stringp origname)
                              (vl-paramdecllist-p paramdecls))))
  (let ((__function__ 'vl-unparam-newname))
    (declare (ignorable __function__))
    (hons-copy
         (with-local-ps
              (vl-ps-seq (vl-print-str origname)
                         (vl-unparam-newname-aux paramdecls))))))

Theorem: stringp-of-vl-unparam-newname

(defthm stringp-of-vl-unparam-newname
  (b* ((new-name (vl-unparam-newname origname paramdecls)))
    (stringp new-name))
  :rule-classes :type-prescription)

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

(defthm vl-unparam-newname-of-str-fix-origname
  (equal (vl-unparam-newname (str-fix origname)
                             paramdecls)
         (vl-unparam-newname origname paramdecls)))

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

(defthm vl-unparam-newname-streqv-congruence-on-origname
  (implies (streqv origname origname-equiv)
           (equal (vl-unparam-newname origname paramdecls)
                  (vl-unparam-newname origname-equiv paramdecls)))
  :rule-classes :congruence)

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

(defthm vl-unparam-newname-of-vl-paramdecllist-fix-paramdecls
  (equal (vl-unparam-newname origname
                             (vl-paramdecllist-fix paramdecls))
         (vl-unparam-newname origname paramdecls)))

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

(defthm
 vl-unparam-newname-vl-paramdecllist-equiv-congruence-on-paramdecls
 (implies (vl-paramdecllist-equiv paramdecls paramdecls-equiv)
          (equal (vl-unparam-newname origname paramdecls)
                 (vl-unparam-newname origname paramdecls-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-unparam-newname-aux