(vl-unlike-any-prefix-p name prefixes) determines whether for all
We use this function in the implementation of vl-namedb-plain-name. When requesting a plain name, one might ask for a name
like
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.
Function:
(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:
(defthm vl-unlike-any-prefix-p-when-atom (implies (atom prefixes) (vl-unlike-any-prefix-p name prefixes)))
Theorem:
(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:
(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:
(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:
(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:
(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))))