• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
            • Vl-namefactory-p
              • Vl-namefactory-plain-names
              • Vl-namefactory-indexed-name
              • Vl-namefactory-plain-name
                • Vl-namefactory-maybe-initialize
                • Vl-namefactory-namedb-fix
                • Vl-namefactory-allnames
                • Vl-starting-namefactory
                • Vl-namefactory-namedb-okp
                • Vl-empty-namefactory
                • Vl-free-namefactory
              • Vl-namefactory-fix
              • Vl-namefactory-equiv
              • Make-vl-namefactory
              • Vl-namefactory->namedb
              • Vl-namefactory->mod
              • Change-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
            • Caremask
            • Port-tools
            • Lvalues
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-namefactory-p

    Vl-namefactory-plain-name

    (vl-namefactory-plain-name name factory) returns (mv fresh-name factory-prime). When possible, fresh-name is just name. When this is not possible, a note is printed and fresh-name looks like name_n instead.

    Signature
    (vl-namefactory-plain-name name factory) 
      → 
    (mv fresh-name new-factory)
    Arguments
    name — Guard (stringp name).
    factory — Guard (vl-namefactory-p factory).
    Returns
    fresh-name — Type (stringp fresh-name).
    new-factory — Type (vl-namefactory-p new-factory).

    Definitions and Theorems

    Function: vl-namefactory-plain-name

    (defun vl-namefactory-plain-name (name factory)
     (declare (xargs :guard (and (stringp name)
                                 (vl-namefactory-p factory))))
     (let ((__function__ 'vl-namefactory-plain-name))
       (declare (ignorable __function__))
       (b*
         ((factory (vl-namefactory-maybe-initialize factory))
          ((mv newname db-prime)
           (vl-namedb-plain-name name (vl-namefactory->namedb factory)))
          (factory (change-vl-namefactory factory
                                          :namedb db-prime)))
         (mv newname factory))))

    Theorem: stringp-of-vl-namefactory-plain-name.fresh-name

    (defthm stringp-of-vl-namefactory-plain-name.fresh-name
      (b* (((mv ?fresh-name ?new-factory)
            (vl-namefactory-plain-name name factory)))
        (stringp fresh-name))
      :rule-classes :type-prescription)

    Theorem: vl-namefactory-p-of-vl-namefactory-plain-name.new-factory

    (defthm vl-namefactory-p-of-vl-namefactory-plain-name.new-factory
      (b* (((mv ?fresh-name ?new-factory)
            (vl-namefactory-plain-name name factory)))
        (vl-namefactory-p new-factory))
      :rule-classes :rewrite)

    Theorem: vl-namefactory-allnames-of-vl-namefactory-plain-name

    (defthm vl-namefactory-allnames-of-vl-namefactory-plain-name
      (b* (((mv fresh-name new-factory)
            (vl-namefactory-plain-name name factory)))
        (equal (vl-namefactory-allnames new-factory)
               (cons fresh-name
                     (vl-namefactory-allnames factory)))))

    Theorem: vl-namefactory-plain-name-is-fresh

    (defthm vl-namefactory-plain-name-is-fresh
      (b* (((mv fresh-name ?new-factory)
            (vl-namefactory-plain-name name factory)))
        (not (member-equal fresh-name
                           (vl-namefactory-allnames factory)))))

    Theorem: vl-namefactory-plain-name-of-str-fix-name

    (defthm vl-namefactory-plain-name-of-str-fix-name
      (equal (vl-namefactory-plain-name (str-fix name)
                                        factory)
             (vl-namefactory-plain-name name factory)))

    Theorem: vl-namefactory-plain-name-streqv-congruence-on-name

    (defthm vl-namefactory-plain-name-streqv-congruence-on-name
      (implies (streqv name name-equiv)
               (equal (vl-namefactory-plain-name name factory)
                      (vl-namefactory-plain-name name-equiv factory)))
      :rule-classes :congruence)

    Theorem: vl-namefactory-plain-name-of-vl-namefactory-fix-factory

    (defthm vl-namefactory-plain-name-of-vl-namefactory-fix-factory
      (equal
           (vl-namefactory-plain-name name (vl-namefactory-fix factory))
           (vl-namefactory-plain-name name factory)))

    Theorem: vl-namefactory-plain-name-vl-namefactory-equiv-congruence-on-factory

    (defthm
     vl-namefactory-plain-name-vl-namefactory-equiv-congruence-on-factory
     (implies (vl-namefactory-equiv factory factory-equiv)
              (equal (vl-namefactory-plain-name name factory)
                     (vl-namefactory-plain-name name factory-equiv)))
     :rule-classes :congruence)