		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-namedb-plain-name

Safely try to generate a particular name.

Signature
(vl-namedb-plain-name name db) → (mv fresh-name new-db)
Arguments: name — The desired name to use, if available.
Guard (stringp name).; db — The name database.
Guard (vl-namedb-p db).
Returns: fresh-name — When possible this is just name. When name is already in use, we instead produce, e.g., name_1, name_2, or similar.
Type (stringp fresh-name).; new-db — Extended name database with fresh-name being marked as used.
Type (vl-namedb-p new-db), given (vl-namedb-p db).

Definitions and Theorems

Function: vl-namedb-plain-name

(defun vl-namedb-plain-name (name db)
 (declare (xargs :guard (and (stringp name) (vl-namedb-p db))))
 (let ((__function__ 'vl-namedb-plain-name))
  (declare (ignorable __function__))
  (b*
   ((name (string-fix name))
    (names (vl-namedb->names db))
    (pset (vl-namedb->pset db))
    ((when (hons-get name names))
     (mv-let (fresh-name db)
             (vl-namedb-indexed-name name db)
      (prog2$
       (cw
         "; Name db note: ~x0 is not available; made ~x1 instead.~%"
         name fresh-name)
       (mv fresh-name db))))
    ((unless (vl-unlike-any-prefix-p-of-alist-keys name pset))
     (mv-let (fresh-name db)
             (vl-namedb-indexed-name name db)
      (prog2$
       (cw
        "; Name db note: ~x0 is like an existing prefix; made ~x1 instead.~%"
        name fresh-name)
       (mv fresh-name db))))
    (names (hons-acons name t names))
    (db (change-vl-namedb db :names names)))
   (mv name db))))

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

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

Theorem: vl-namedb-p-of-vl-namedb-plain-name.new-db

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

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

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

Theorem: vl-namedb->names-of-vl-namedb-plain-name

(defthm vl-namedb->names-of-vl-namedb-plain-name
  (vl-namedb->names (mv-nth 1 (vl-namedb-plain-name name db))))

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

(defthm vl-namedb-plain-name-is-fresh
  (not (member-equal (mv-nth 0 (vl-namedb-plain-name name db))
                     (vl-namedb-allnames db))))

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

(defthm vl-namedb-plain-name-of-str-fix-name
  (equal (vl-namedb-plain-name (str-fix name) db)
         (vl-namedb-plain-name name db)))

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

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

Theorem: vl-namedb-plain-name-of-vl-namedb-fix-db

(defthm vl-namedb-plain-name-of-vl-namedb-fix-db
  (equal (vl-namedb-plain-name name (vl-namedb-fix db))
         (vl-namedb-plain-name name db)))

Theorem: vl-namedb-plain-name-vl-namedb-equiv-congruence-on-db

(defthm vl-namedb-plain-name-vl-namedb-equiv-congruence-on-db
  (implies (vl-namedb-equiv db db-equiv)
           (equal (vl-namedb-plain-name name db)
                  (vl-namedb-plain-name name db-equiv)))
  :rule-classes :congruence)