		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-unlike-any-prefix-p

(vl-unlike-any-prefix-p name prefixes) determines whether for all p in prefixes, (vl-pgenstr-p p name) is false.

We use this function in the implementation of vl-namedb-plain-name. When requesting a plain name, one might ask for a name like foo_3, which could screw up the prefix map if we are using foo as a prefix.

One solution would be to fix up the prefix map when this occurs. But we take the easier approach of just not allowing you to request any name that matches a current prefix.

Definitions and Theorems

Function: vl-unlike-any-prefix-p

(defun vl-unlike-any-prefix-p (name prefixes)
  (declare (xargs :guard (and (stringp name)
                              (string-listp prefixes))))
  (or (atom prefixes)
      (and (not (vl-pgenstr-p (car prefixes) name))
           (vl-unlike-any-prefix-p name (cdr prefixes)))))

Theorem: vl-unlike-any-prefix-p-when-atom

(defthm vl-unlike-any-prefix-p-when-atom
  (implies (atom prefixes)
           (vl-unlike-any-prefix-p name prefixes)))

Theorem: vl-unlike-any-prefix-p-of-cons

(defthm vl-unlike-any-prefix-p-of-cons
  (equal (vl-unlike-any-prefix-p name (cons a x))
         (and (not (vl-pgenstr-p a name))
              (vl-unlike-any-prefix-p name x))))

Theorem: vl-pgenstr-p-when-vl-unlike-any-prefix-p

(defthm vl-pgenstr-p-when-vl-unlike-any-prefix-p
  (implies (and (member-equal key prefixes)
                (vl-unlike-any-prefix-p name prefixes))
           (not (vl-pgenstr-p key name))))

Theorem: vl-unlike-any-prefix-p-preserves-set-equiv-prefixes

(defthm vl-unlike-any-prefix-p-preserves-set-equiv-prefixes
  (implies (set-equiv prefixes prefixes-equiv)
           (equal (vl-unlike-any-prefix-p name prefixes)
                  (vl-unlike-any-prefix-p name prefixes-equiv)))
  :rule-classes (:congruence))

Theorem: vl-prefix-map-correct-p-aux-when-vl-unlike-any-prefix-p

(defthm vl-prefix-map-correct-p-aux-when-vl-unlike-any-prefix-p
  (implies
       (and (vl-prefix-map-correct-p-aux domain pmap names)
            (vl-unlike-any-prefix-p name (alist-keys pmap)))
       (vl-prefix-map-correct-p-aux domain pmap (cons name names))))

Theorem: vl-prefix-map-correct-p-when-vl-unlike-any-prefix-p

(defthm vl-prefix-map-correct-p-when-vl-unlike-any-prefix-p
  (implies (and (vl-prefix-map-correct-p pset names)
                (vl-unlike-any-prefix-p name (alist-keys pset)))
           (vl-prefix-map-correct-p pset (cons name names))))