• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
              • Abstract-syntax
                • Expression
                • Syntax-abstraction
                • Statement
                • Files
                  • Funparam-list->name-list
                  • Fundecl
                  • Var/const-sort
                  • Structdecl
                  • File
                  • Finalizer-option
                  • Topdecl
                    • Topdecl-case
                      • Topdecl-fix
                      • Topdeclp
                      • Topdecl-equiv
                      • Topdecl-struct
                      • Topdecl-mapping
                      • Topdecl-function
                      • Topdecl-kind
                    • Mappingdecl
                    • Fundecl-option
                    • Finalizer
                    • Funparam
                    • Fun-sort
                    • Programdecl
                    • Compdecl
                    • Var/const-sort-result
                    • Topdecl-list-result
                    • Programdecl-list-result
                    • Importdecl-list-result
                    • Funparam-list-result
                    • Finalizer-option-result
                    • Compdecl-list-result
                    • Topdecl-result
                    • Structdecl-result
                    • Programdecl-result
                    • Mappingdecl-result
                    • Importdecl-result
                    • Importdecl
                    • Funparam-result
                    • Fundecl-result
                    • Fun-sort-result
                    • Finalizer-result
                    • Compdecl-result
                    • File-result
                    • Funparam-list
                    • Programdecl-list
                    • Importdecl-list
                    • Compdecl-list
                    • Var/const-sort-list
                    • Topdecl-list
                    • Fundecl-list
                  • Input-files
                  • Identifiers
                  • Types
                  • Struct-init
                  • Branch
                  • Statements
                  • Format-strings
                  • Input-syntax-abstraction
                  • Expressions
                  • Output-files
                  • Addresses
                  • Literals
                  • Characters
                  • Expression-list
                  • Statement-list
                  • Output-syntax-abstraction
                  • Struct-init-list
                  • Branch-list
                  • Annotations
                  • Abstract-syntax-trees
                  • Symbols
                  • Keywords
                  • Programs
                  • Packages
                  • Bit-sizes
                • Dynamic-semantics
                • Compilation
                • Static-semantics
                • Concrete-syntax
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Topdecl

    Topdecl-case

    Case macro for the different kinds of topdecl structures.

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

    Short Form

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

    (topdecl-case x :function)

    is essentially just a safer alternative to writing:

    (equal (topdecl-kind x) :function)

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

    Long Form

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

    (topdecl-case x
      :function ...
      :struct ...
      :mapping ...)

    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 :function case, you can use fty::defprod-style foo.bar style accessors for x without having to explicitly add a function b* binder.