• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
          • Vl-namemangle-vardecls
          • Vl-namemangle-gateinsts
          • Vl-namemangle-modinsts
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Namemangle

Vl-namemangle-vardecls

Safely try to give these vardecls new names of the form prefix_{current-name}.

Signature

(vl-namemangle-vardecls prefix vardecls nf) 
  → 
(mv new-vars new-nf)

Arguments

prefix — Guard (stringp prefix).

vardecls — Guard (vl-vardecllist-p vardecls).

nf — Guard (vl-namefactory-p nf).

Returns

new-vars — Type (vl-vardecllist-p new-vars).

new-nf — Type (vl-namefactory-p new-nf).

You'll generally want to do something like:

(pairlis$ (vl-vardecllist->names old-vardecls)
          (vl-vardecllist->names renamed-vardecls))

And then use this as a substitution.

Definitions and Theorems

Function: vl-namemangle-vardecls

(defun vl-namemangle-vardecls (prefix vardecls nf)
  (declare (xargs :guard (and (stringp prefix)
                              (vl-vardecllist-p vardecls)
                              (vl-namefactory-p nf))))
  (let ((__function__ 'vl-namemangle-vardecls))
    (declare (ignorable __function__))
    (b* (((when (atom vardecls))
          (mv nil (vl-namefactory-fix nf)))
         (name1 (vl-vardecl->name (car vardecls)))
         (want1 (cat prefix "_" name1))
         ((mv fresh1 nf)
          (vl-namefactory-plain-name want1 nf))
         (inst1 (change-vl-vardecl (car vardecls)
                                   :name fresh1))
         ((mv insts2 nf)
          (vl-namemangle-vardecls prefix (cdr vardecls)
                                  nf)))
      (mv (cons inst1 insts2) nf))))

Theorem: vl-vardecllist-p-of-vl-namemangle-vardecls.new-vars

(defthm vl-vardecllist-p-of-vl-namemangle-vardecls.new-vars
  (b* (((mv ?new-vars ?new-nf)
        (vl-namemangle-vardecls prefix vardecls nf)))
    (vl-vardecllist-p new-vars))
  :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-namemangle-vardecls.new-nf

(defthm vl-namefactory-p-of-vl-namemangle-vardecls.new-nf
  (b* (((mv ?new-vars ?new-nf)
        (vl-namemangle-vardecls prefix vardecls nf)))
    (vl-namefactory-p new-nf))
  :rule-classes :rewrite)

Theorem: vl-namemangle-vardecls-mvtypes-0

(defthm vl-namemangle-vardecls-mvtypes-0
  (true-listp (mv-nth 0
                      (vl-namemangle-vardecls prefix vardecls nf)))
  :rule-classes :type-prescription)

Theorem: len-of-vl-namemangle-vardecls

(defthm len-of-vl-namemangle-vardecls
  (b* (((mv new-vardecls ?new-nf)
        (vl-namemangle-vardecls loc vardecls nf)))
    (equal (len new-vardecls)
           (len vardecls))))

Theorem: vl-namemangle-vardecls-of-str-fix-prefix

(defthm vl-namemangle-vardecls-of-str-fix-prefix
  (equal (vl-namemangle-vardecls (str-fix prefix)
                                 vardecls nf)
         (vl-namemangle-vardecls prefix vardecls nf)))

Theorem: vl-namemangle-vardecls-streqv-congruence-on-prefix

(defthm vl-namemangle-vardecls-streqv-congruence-on-prefix
 (implies (streqv prefix prefix-equiv)
          (equal (vl-namemangle-vardecls prefix vardecls nf)
                 (vl-namemangle-vardecls prefix-equiv vardecls nf)))
 :rule-classes :congruence)

Theorem: vl-namemangle-vardecls-of-vl-vardecllist-fix-vardecls

(defthm vl-namemangle-vardecls-of-vl-vardecllist-fix-vardecls
 (equal (vl-namemangle-vardecls prefix (vl-vardecllist-fix vardecls)
                                nf)
        (vl-namemangle-vardecls prefix vardecls nf)))

Theorem: vl-namemangle-vardecls-vl-vardecllist-equiv-congruence-on-vardecls

(defthm
 vl-namemangle-vardecls-vl-vardecllist-equiv-congruence-on-vardecls
 (implies (vl-vardecllist-equiv vardecls vardecls-equiv)
          (equal (vl-namemangle-vardecls prefix vardecls nf)
                 (vl-namemangle-vardecls prefix vardecls-equiv nf)))
 :rule-classes :congruence)

Theorem: vl-namemangle-vardecls-of-vl-namefactory-fix-nf

(defthm vl-namemangle-vardecls-of-vl-namefactory-fix-nf
 (equal
    (vl-namemangle-vardecls prefix vardecls (vl-namefactory-fix nf))
    (vl-namemangle-vardecls prefix vardecls nf)))

Theorem: vl-namemangle-vardecls-vl-namefactory-equiv-congruence-on-nf

(defthm vl-namemangle-vardecls-vl-namefactory-equiv-congruence-on-nf
 (implies (vl-namefactory-equiv nf nf-equiv)
          (equal (vl-namemangle-vardecls prefix vardecls nf)
                 (vl-namemangle-vardecls prefix vardecls nf-equiv)))
 :rule-classes :congruence)