• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
          • Scopestack
          • Hid-tools
            • Vl-follow-hidexpr
            • Vl-index-expr-typetrace
            • Vl-follow-scopeexpr
            • Vl-follow-hidexpr-dimscheck
            • Vl-datatype-resolve-selects
            • Vl-datatype-remove-dim
            • Vl-operandinfo
            • Vl-follow-hidexpr-dimcheck
            • Vl-follow-data-selects
            • Vl-follow-hidexpr-error
            • Vl-hidstep
            • Vl-scopestack-find-item/ss/path
            • Vl-follow-array-indices
            • Vl-scopecontext
            • Vl-datatype-set-unsigned
            • Vl-selstep
            • Vl-scopestack-find-elabpath
            • Vl-hid-prefix-for-subhid
            • Vl-find-structmember
            • Vl-select
              • Vl-select-fix
              • Vl-select-case
                • Vl-select-equiv
                • Vl-select-field
                • Vl-select-index
                • Vl-select-p
                • Vl-select-kind
              • Vl-scopeexpr-replace-hid
              • Vl-genblocklist-find-block
              • Vl-partselect-width
              • Vl-seltrace->indices
              • Vl-datatype->structmembers
              • Vl-hidexpr-resolved-p
              • Vl-operandinfo->indices
              • Vl-flatten-hidindex
              • Vl-subhid-p
              • Vl-seltrace-usertypes-ok
              • Vl-flatten-hidexpr
              • Vl-scopeexpr->hid
              • Vl-seltrace-index-count
              • Vl-operandinfo-usertypes-ok
              • Vl-operandinfo-index-count
              • Vl-datatype-dims-count
              • Vl-scopeexpr-index-count
              • Vl-hidexpr-index-count
              • Vl-usertype-lookup
              • Vl-hidindex-resolved-p
              • Vl-scopeexpr-resolved-p
              • Vl-selstep-usertypes-ok
              • Vl-hidtrace
              • Vl-seltrace
              • Vl-scopedef-interface-p
            • Filtering-by-name
            • Vl-interface-mocktype
            • Stripping-functions
            • Genblob
            • Expr-tools
            • Extract-vl-types
            • Hierarchy
            • Range-tools
            • Finding-by-name
            • Stmt-tools
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-select

    Vl-select-case

    Case macro for the different kinds of vl-select structures.

    This is an fty sum-type case macro, typically introduced by defflexsum or deftagsum. It allows you to safely check the type of a vl-select structure, or to split into cases based on its type.

    Short Form

    In its short form, vl-select-case allows you to safely check the type of a vl-select structure. For example:

    (vl-select-case x :field)

    is essentially just a safer alternative to writing:

    (equal (vl-select-kind x) :field)

    Why is using vl-select-case safer? When we directly inspect the kind with equal, there is no static checking being done to ensure that, e.g., :field is a valid kind of vl-select structure. That means there is nothing to save you if, later, you change the kind keyword for this type from :field to something else. It also means you get no help if you just make a typo when writing the :field symbol. Over the course of developing VL, we found that such issues were very frequent sources of errors!

    Long Form

    In its longer form, vl-select-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

    (vl-select-case x
      :field ...
      :index ...)

    It is also possible to consolidate ``uninteresting'' cases using :otherwise.

    For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :field case, you can use defprod-style foo.bar style accessors for x without having to explicitly add a field b* binder.