		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-idexpr

Signature
(vl-idexpr name) → expr
Arguments: name — Guard (stringp name).
Returns: expr — Type (vl-expr-p expr).

(vl-idexpr name) constructs a simple identifier expression with the given name, width, and type.

I didn't always hons these, but now it seems like a good idea since the same identifier may be needed in several contexts, and since we often want to construct fast alists binding identifiers to things, etc.

Definitions and Theorems

Function: vl-idexpr$inline

(defun vl-idexpr$inline (name)
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'vl-idexpr))
    (declare (ignorable __function__))
    (hons-copy (make-vl-index :scope (vl-idscope name)
                              :indices nil
                              :part (make-vl-partselect-none)))))

Theorem: vl-expr-p-of-vl-idexpr

(defthm vl-expr-p-of-vl-idexpr
  (b* ((expr (vl-idexpr$inline name)))
    (vl-expr-p expr))
  :rule-classes :rewrite)

Theorem: vl-idexpr-p-of-vl-idexpr

(defthm vl-idexpr-p-of-vl-idexpr
  (vl-idexpr-p (vl-idexpr name)))

Theorem: vl-idexpr->name-of-vl-idexpr

(defthm vl-idexpr->name-of-vl-idexpr
  (equal (vl-idexpr->name (vl-idexpr name))
         (str-fix name)))

Theorem: vl-expr-kind-of-vl-idexpr

(defthm vl-expr-kind-of-vl-idexpr
  (equal (vl-expr-kind (vl-idexpr name))
         :vl-index))

Theorem: vl-idexpr$inline-of-str-fix-name

(defthm vl-idexpr$inline-of-str-fix-name
  (equal (vl-idexpr$inline (str-fix name))
         (vl-idexpr$inline name)))

Theorem: vl-idexpr$inline-streqv-congruence-on-name

(defthm vl-idexpr$inline-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-idexpr$inline name)
                  (vl-idexpr$inline name-equiv)))
  :rule-classes :congruence)