Tag
Get the tag from a tagged object.
The tag function is simply an alias for car that is
especially meant to be used for accessing the tag of a tagged
object.
When new types are introduced by macros such as defaggregate, fty::defprod, fty::deftagsum, etc., they may be tagged. When a type is
tagged, its objects have the form (tag . data), where the tag says
what kind of object is being represented (e.g., ``employee'', ``student'',
etc.) and data contains the actual information for this kind of
structure (e.g., name, age, ...). Tagging objects has some runtime/memory
cost (an extra cons for each object), but makes it easy to tell different kinds
of objects apart by inspecting their tags.
We could (of course) just get the tag with car, but car is a
widely used function and we do not want to slow down reasoning about it.
Instead, we introduce tag as an alias for car and keep it disabled so
that reasoning about the tags of objects does not slow down reasoning about
car in general.
Even so, tag reasoning can occasionally get expensive. Macros like
defaggregate, fty::defprod, etc., generally add their tag-related
rules to the tag-reasoning ruleset; see ACL2::rulesets. You may
generally want to keep this ruleset disabled, and only enable it when you
really want to use tags to distinguish between objects.
Note: if you are using the ACL2::fty framework, it is generally best
to avoid using tag to distinguish between members of the same sum of
products type. Instead, consider using the custom -kind macros that are
introduced by macros such as fty::deftagsum and fty::deftranssum.
Definitions and Theorems
Function: tag$inline
(defun acl2::tag$inline (x)
(declare (xargs :guard t))
(mbe :logic (car x)
:exec (if (consp x) (car x) nil)))
Theorem: tag-forward-to-consp
(defthm tag-forward-to-consp
(implies (tag x) (consp x))
:rule-classes :forward-chaining)
