		Search-engine friendly clone of the ACL2 documentation.

Expressions

Vl-hidpiece

Represents one piece of a hierarchical identifier.

This is a product type introduced by defprod.

Fields

name — stringp

We represent hierarchical identifiers like top.processor[2][3].reset as non-atomic expressions. To represent this particular expression, we build a vl-expr-p that is something like this:

(:vl-hid-dot top
             (vl-hid-dot
                 (:vl-index (:vl-index processor 2)
                            3)
                 reset))

In other words, the :vl-hid-dot operator is used to join pieces of a hierarchical identifier, and :vl-index operators are used when arrays or instance arrays are being accessed.

To add slightly more precision, our representation is really more like the following:

(:vl-hid-dot (hidpiece "top")
             (vl-hid-dot
                (:vl-index (:vl-index (hidpiece "processor") (constint 2))
                           (constint 3))
                (hidpiece "reset")))

In other words, the individual identifiers used throughout a hierarchical identifier are actually vl-hidpiece-p objects instead of vl-id-p objects.

We make this distinction so that in the ordinary course of working with the parse tree, you can freely assume that any vl-id-p you come across really refers to some module item, and not to some part of a hierarchical identifier.

Subtopics

Vl-hidpiece-fix: Fixing function for vl-hidpiece structures.
Vl-hidpiece-equiv: Basic equivalence relation for vl-hidpiece structures.
Make-vl-hidpiece: Basic constructor macro for vl-hidpiece structures.
Vl-hidpiece-p: Recognizer for vl-hidpiece structures.
Vl-hidpiece->name: Get the name field from a vl-hidpiece.
Change-vl-hidpiece: Modifying constructor for vl-hidpiece structures.