• 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Namemangle

Vl-namemangle-modinsts

Safely rename module instances, preferring names of the form prefix_{current-name}.

Signature

(vl-namemangle-modinsts prefix modinsts nf) 
  → 
(mv new-modinsts new-nf)

Arguments

prefix — Guard (stringp prefix).

modinsts — Guard (vl-modinstlist-p modinsts).

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

Returns

new-modinsts — Type (vl-modinstlist-p new-modinsts).

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

Definitions and Theorems

Function: vl-namemangle-modinsts

(defun vl-namemangle-modinsts (prefix modinsts nf)
  (declare (xargs :guard (and (stringp prefix)
                              (vl-modinstlist-p modinsts)
                              (vl-namefactory-p nf))))
  (let ((__function__ 'vl-namemangle-modinsts))
    (declare (ignorable __function__))
    (b* (((when (atom modinsts))
          (mv nil (vl-namefactory-fix nf)))
         (instname1 (or (vl-modinst->instname (car modinsts))
                        "inst"))
         (want1 (cat prefix "_" instname1))
         ((mv fresh1 nf)
          (vl-namefactory-plain-name want1 nf))
         (inst1 (change-vl-modinst (car modinsts)
                                   :instname fresh1))
         ((mv insts2 nf)
          (vl-namemangle-modinsts prefix (cdr modinsts)
                                  nf)))
      (mv (cons inst1 insts2) nf))))

Theorem: vl-modinstlist-p-of-vl-namemangle-modinsts.new-modinsts

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

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

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

Theorem: vl-namemangle-modinsts-mvtypes-0

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

Theorem: len-of-vl-namemangle-modinsts

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

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

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

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

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

Theorem: vl-namemangle-modinsts-of-vl-modinstlist-fix-modinsts

(defthm vl-namemangle-modinsts-of-vl-modinstlist-fix-modinsts
 (equal (vl-namemangle-modinsts prefix (vl-modinstlist-fix modinsts)
                                nf)
        (vl-namemangle-modinsts prefix modinsts nf)))

Theorem: vl-namemangle-modinsts-vl-modinstlist-equiv-congruence-on-modinsts

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

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

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

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

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