		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)