		Search-engine friendly clone of the ACL2 documentation.

Vl-namefactory

Vl-namefactory-p

Recognizer for vl-namefactory structures.

Signature
(vl-namefactory-p x) → *

Definitions and Theorems

Function: vl-namefactory-p

(defun vl-namefactory-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-namefactory-p))
    (declare (ignorable __function__))
    (and (consp x)
         (eq (car x) :vl-namefactory)
         (std::prod-consp (cdr x))
         (b* ((mod (std::prod-car (cdr x)))
              (namedb (std::prod-cdr (cdr x))))
           (and (vl-maybe-module-p mod)
                (vl-namedb-p namedb)
                (vl-namefactory-namedb-okp mod namedb))))))

Theorem: consp-when-vl-namefactory-p

(defthm consp-when-vl-namefactory-p
  (implies (vl-namefactory-p x) (consp x))
  :rule-classes :compound-recognizer)

Subtopics

Vl-namefactory-plain-names: Generate a list of fresh names, using particular, preferred names if possible.
Vl-namefactory-indexed-name: (vl-namefactory-indexed-name prefix factory) constructs a fresh name that looks like prefix_n for some natural number n, and returns (mv fresh-name factory-prime).
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.
Vl-namefactory-maybe-initialize: Make sure that the modnamespace is computed, or generate it if it isn't available already.
Vl-namefactory-namedb-fix
Vl-namefactory-allnames: (vl-namefactory-p x) returns a list of all names that are considered to be used by the name factory.
Vl-starting-namefactory: (vl-starting-namefactory mod) creates a name factory for a module.
Vl-namefactory-namedb-okp
Vl-empty-namefactory: (vl-empty-namefactory) creates an empty name factory without a module.
Vl-free-namefactory: (vl-free-namefactory factory) frees the fast alists associated with a name factory and returns nil.