		Search-engine friendly clone of the ACL2 documentation.

Vl-namefactory-p

Vl-namefactory-plain-names

Generate a list of fresh names, using particular, preferred names if possible.

Signature
(vl-namefactory-plain-names names factory) → (mv fresh-names new-factory)
Arguments: names — The names you would ideally like to use.
Guard (string-listp names).; factory — Guard (vl-namefactory-p factory).
Returns: fresh-names — Fresh names that you may use. When possible, these are just names. If this is not possible due to name collisions, then some of the fresh_names may have additional indexes as in vl-namefactory-indexed-name and some notes may be printed.
Type (string-listp fresh-names).; new-factory — Updated name factory where the fresh-names are marked as used.
Type (vl-namefactory-p new-factory).

Definitions and Theorems

Function: vl-namefactory-plain-names

(defun vl-namefactory-plain-names (names factory)
  (declare (xargs :guard (and (string-listp names)
                              (vl-namefactory-p factory))))
  (let ((__function__ 'vl-namefactory-plain-names))
    (declare (ignorable __function__))
    (b* (((when (atom names))
          (mv nil (vl-namefactory-fix factory)))
         ((mv name factory)
          (vl-namefactory-plain-name (car names)
                                     factory))
         ((mv rest factory)
          (vl-namefactory-plain-names (cdr names)
                                      factory)))
      (mv (cons name rest) factory))))

Theorem: string-listp-of-vl-namefactory-plain-names.fresh-names

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

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

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

Theorem: len-vl-namefactory-plain-names

(defthm len-vl-namefactory-plain-names
  (equal (len (mv-nth 0
                      (vl-namefactory-plain-names names factory)))
         (len names)))

Theorem: true-listp-vl-namefactory-plain-names

(defthm true-listp-vl-namefactory-plain-names
  (true-listp (mv-nth 0
                      (vl-namefactory-plain-names names factory)))
  :rule-classes :type-prescription)

Theorem: vl-namefactory-plain-names-are-fresh

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

Theorem: vl-namefactory-plain-names-of-string-list-fix-names

(defthm vl-namefactory-plain-names-of-string-list-fix-names
  (equal (vl-namefactory-plain-names (string-list-fix names)
                                     factory)
         (vl-namefactory-plain-names names factory)))

Theorem: vl-namefactory-plain-names-string-list-equiv-congruence-on-names

(defthm
   vl-namefactory-plain-names-string-list-equiv-congruence-on-names
  (implies (str::string-list-equiv names names-equiv)
           (equal (vl-namefactory-plain-names names factory)
                  (vl-namefactory-plain-names names-equiv factory)))
  :rule-classes :congruence)

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

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

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

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