• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
              • Fty-pseudo-term-utilities
              • Atc-term-recognizers
              • Atc-input-processing
              • Atc-shallow-embedding
                • Defstruct
                  • Defstruct-implementation
                    • Defstruct-info
                    • Defstruct-gen-recognizer
                    • Defstruct-gen-integer-member-ops
                    • Defstruct-gen-constructor
                    • Defstruct-gen-array-member-ops
                    • Defstruct-gen-recognizer-conjuncts
                    • Defstruct-member-info
                      • Defstruct-member-info-fix
                      • Make-defstruct-member-info
                        • Defstruct-member-info-equiv
                        • Defstruct-member-infop
                        • Defstruct-member-info->writer-element-return-thm
                        • Defstruct-member-info->reader-element-return-thm
                        • Change-defstruct-member-info
                        • Defstruct-member-info->writer-return-thm
                        • Defstruct-member-info->reader-return-thm
                        • Defstruct-member-info->writer-element
                        • Defstruct-member-info->reader-element
                        • Defstruct-member-info->memtype
                        • Defstruct-member-info->writer
                        • Defstruct-member-info->reader
                        • Defstruct-member-info->length
                        • Defstruct-member-info->checker
                      • Defstruct-member-info-list->memtype-list
                      • Defstruct-process-members
                      • Defstruct-gen-fixer
                      • Defstruct-gen-member-ops
                      • Defstruct-process-inputs
                      • Defstruct-gen-fixing-term
                      • Defstruct-info-option
                      • Defstruct-gen-everything
                      • Defstruct-gen-all-member-ops
                      • Defstruct-gen-recognizer-all-conjuncts
                      • Defstruct-info->writer-element-list
                      • Defstruct-info->reader-element-list
                      • Defstruct-gen-fixtype
                      • Defstruct-info->writer-list
                      • Defstruct-info->reader-list
                      • Defstruct-fn
                      • Defstruct-table-record-event
                      • Defstruct-table-lookup
                      • Irr-defstruct-info
                      • Defstruct-info->writer-element-list-aux
                      • Defstruct-info->reader-element-list-aux
                      • Defstruct-info->writer-list-aux
                      • Defstruct-info->reader-list-aux
                      • Defstruct-member-info-list
                      • Defstruct-table-definition
                      • *defstruct-table*
                      • Defstruct-macro-implementtion
                  • Defobject
                  • Atc-let-designations
                  • Pointer-types
                  • Atc-conditional-expressions
                • Atc-process-inputs-and-gen-everything
                • Atc-table
                • Atc-fn
                • Atc-pretty-printing-options
                • Atc-types
                • Atc-macro-definition
              • Atc-tutorial
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Riscv
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Defstruct-member-info

    Make-defstruct-member-info

    Basic constructor macro for defstruct-member-info structures.

    Syntax
    (make-defstruct-member-info [:memtype <memtype>] 
                                [:reader <reader>] 
                                [:reader-element <reader-element>] 
                                [:writer <writer>] 
                                [:writer-element <writer-element>] 
                                [:checker <checker>] 
                                [:length <length>] 
                                [:reader-return-thm <reader-return-thm>] 
                                [:reader-element-return-thm <reader-element-return-thm>] 
                                [:writer-return-thm <writer-return-thm>] 
                                [:writer-element-return-thm <writer-element-return-thm>]) 
    

    This is the usual way to construct defstruct-member-info structures. It simply conses together a structure with the specified fields.

    This macro generates a new defstruct-member-info structure from scratch. See also change-defstruct-member-info, which can "change" an existing structure, instead.

    Definition

    This is an ordinary make- macro introduced by fty::defprod.

    Macro: make-defstruct-member-info

    (defmacro make-defstruct-member-info (&rest args)
      (std::make-aggregate 'defstruct-member-info
                           args
                           '((:memtype)
                             (:reader)
                             (:reader-element)
                             (:writer)
                             (:writer-element)
                             (:checker)
                             (:length)
                             (:reader-return-thm)
                             (:reader-element-return-thm)
                             (:writer-return-thm)
                             (:writer-element-return-thm))
                           'make-defstruct-member-info
                           nil))

    Function: defstruct-member-info

    (defun defstruct-member-info
           (memtype reader
                    reader-element writer writer-element
                    checker length reader-return-thm
                    reader-element-return-thm
                    writer-return-thm
                    writer-element-return-thm)
     (declare (xargs :guard (and (member-typep memtype)
                                 (symbolp reader)
                                 (symbolp reader-element)
                                 (symbolp writer)
                                 (symbolp writer-element)
                                 (symbolp checker)
                                 (symbolp length)
                                 (symbolp reader-return-thm)
                                 (symbolp reader-element-return-thm)
                                 (symbolp writer-return-thm)
                                 (symbolp writer-element-return-thm))))
     (declare (xargs :guard t))
     (let ((__function__ 'defstruct-member-info))
      (declare (ignorable __function__))
      (b* ((memtype (mbe :logic (member-type-fix memtype)
                         :exec memtype))
           (reader (mbe :logic (symbol-fix reader)
                        :exec reader))
           (reader-element (mbe :logic (symbol-fix reader-element)
                                :exec reader-element))
           (writer (mbe :logic (symbol-fix writer)
                        :exec writer))
           (writer-element (mbe :logic (symbol-fix writer-element)
                                :exec writer-element))
           (checker (mbe :logic (symbol-fix checker)
                         :exec checker))
           (length (mbe :logic (symbol-fix length)
                        :exec length))
           (reader-return-thm (mbe :logic (symbol-fix reader-return-thm)
                                   :exec reader-return-thm))
           (reader-element-return-thm
                (mbe :logic (symbol-fix reader-element-return-thm)
                     :exec reader-element-return-thm))
           (writer-return-thm (mbe :logic (symbol-fix writer-return-thm)
                                   :exec writer-return-thm))
           (writer-element-return-thm
                (mbe :logic (symbol-fix writer-element-return-thm)
                     :exec writer-element-return-thm)))
        (list (cons 'memtype memtype)
              (cons 'reader reader)
              (cons 'reader-element reader-element)
              (cons 'writer writer)
              (cons 'writer-element writer-element)
              (cons 'checker checker)
              (cons 'length length)
              (cons 'reader-return-thm
                    reader-return-thm)
              (cons 'reader-element-return-thm
                    reader-element-return-thm)
              (cons 'writer-return-thm
                    writer-return-thm)
              (cons 'writer-element-return-thm
                    writer-element-return-thm)))))