		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-member-ops

Generate the operations for a member of the structures defined by the defstruct.

Signature
(defstruct-gen-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p member) → (mv event info)
Arguments: struct-tag — Guard (symbolp struct-tag).; struct-tag-p — Guard (symbolp struct-tag-p).; struct-tag-fix — Guard (symbolp struct-tag-fix).; value-kind-when-struct-tag-p — Guard (symbolp value-kind-when-struct-tag-p).; valuep-when-struct-tag-p — Guard (symbolp valuep-when-struct-tag-p).; member — Guard (member-typep member).
Returns: event — Type (pseudo-event-formp event).; info — Type (defstruct-member-infop info).

Definitions and Theorems

Function: defstruct-gen-member-ops

(defun defstruct-gen-member-ops
       (struct-tag struct-tag-p struct-tag-fix
                   value-kind-when-struct-tag-p
                   valuep-when-struct-tag-p member)
 (declare (xargs :guard (and (symbolp struct-tag)
                             (symbolp struct-tag-p)
                             (symbolp struct-tag-fix)
                             (symbolp value-kind-when-struct-tag-p)
                             (symbolp valuep-when-struct-tag-p)
                             (member-typep member))))
 (let ((__function__ 'defstruct-gen-member-ops))
  (declare (ignorable __function__))
  (b*
   ((name (member-type->name member))
    (type (member-type->type member))
    ((when (type-nonchar-integerp type))
     (b* (((mv event reader writer
               reader-return-thm writer-return-thm)
           (defstruct-gen-integer-member-ops
                struct-tag struct-tag-p struct-tag-fix
                value-kind-when-struct-tag-p
                valuep-when-struct-tag-p name type))
          (info (make-defstruct-member-info
                     :memtype member
                     :reader reader
                     :reader-element nil
                     :writer writer
                     :writer-element nil
                     :checker nil
                     :length nil
                     :reader-return-thm reader-return-thm
                     :reader-element-return-thm nil
                     :writer-return-thm writer-return-thm
                     :writer-element-return-thm nil)))
       (mv event info)))
    ((unless (type-case type :array))
     (raise "Internal error: member type ~x0." type)
     (mv '(_)
         (make-defstruct-member-info :memtype member)))
    (elem-type (type-array->of type))
    ((unless (type-nonchar-integerp elem-type))
     (raise "Internal error: member type ~x0." type)
     (mv '(_)
         (make-defstruct-member-info :memtype member)))
    (size? (type-array->size type))
    ((mv event
         length checker reader reader-element
         writer writer-element reader-return-thm
         reader-element-return-thm
         writer-return-thm
         writer-element-return-thm)
     (defstruct-gen-array-member-ops
          struct-tag struct-tag-p
          struct-tag-fix name elem-type size?))
    (info
        (make-defstruct-member-info
             :memtype member
             :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)))
   (mv event info))))

Theorem: pseudo-event-formp-of-defstruct-gen-member-ops.event

(defthm pseudo-event-formp-of-defstruct-gen-member-ops.event
 (b*
  (((mv acl2::?event ?info)
    (defstruct-gen-member-ops struct-tag struct-tag-p struct-tag-fix
                              value-kind-when-struct-tag-p
                              valuep-when-struct-tag-p member)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)

Theorem: defstruct-member-infop-of-defstruct-gen-member-ops.info

(defthm defstruct-member-infop-of-defstruct-gen-member-ops.info
 (b*
  (((mv acl2::?event ?info)
    (defstruct-gen-member-ops struct-tag struct-tag-p struct-tag-fix
                              value-kind-when-struct-tag-p
                              valuep-when-struct-tag-p member)))
  (defstruct-member-infop info))
 :rule-classes :rewrite)