• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
          • Tag
            • Prod-cons
            • Defaggrify-defrec
          • Define
          • Defmapping
          • Defenum
          • Add-io-pairs
          • Defalist
          • Defmapappend
          • Defarbrec
          • Returns-specifiers
          • Define-sk
          • Defmax-nat
          • Defines
          • Error-value-tuples
          • Defmin-int
          • Deftutorial
          • Extended-formals
          • Defrule
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Support
          • Defthm-signed-byte-p
          • Defthm-unsigned-byte-p
          • Std/util-extensions
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Defaggregate

    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)