		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-everything

Generate all the events.

Signature
(defstruct-gen-everything tag tag-ident members flexiblep call) → event
Arguments: tag — Guard (symbolp tag).; tag-ident — Guard (identp tag-ident).; members — Guard (member-type-listp members).; flexiblep — Guard (booleanp flexiblep).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

These are the recognizer, fixer, fixtype, member operations, and the table event. We conclude with a deflabel event that facilitates history manipulation.

Definitions and Theorems

Function: defstruct-gen-everything

(defun defstruct-gen-everything
       (tag tag-ident members flexiblep call)
 (declare (xargs :guard (and (symbolp tag)
                             (identp tag-ident)
                             (member-type-listp members)
                             (booleanp flexiblep)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defstruct-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((struct-tag (packn-pos (list 'struct- tag) tag))
    (struct-tag-p (packn-pos (list struct-tag '-p) tag))
    (struct-tag-fix (packn-pos (list struct-tag '-fix) tag))
    (struct-tag-equiv (packn-pos (list struct-tag '-equiv)
                                 tag))
    ((mv recognizer-event
         not-errorp-when-struct-tag-p
         valuep-when-struct-tag-p
         value-kind-when-struct-tag-p
         type-of-value-when-struct-tag-p
         flexiblep-when-struct-tag-p
         struct-tag-to-quoted
         pointer-struct-tag-to-quoted)
     (defstruct-gen-recognizer struct-tag-p tag members flexiblep))
    ((mv fixer-event fixer-recognizer-thm)
     (defstruct-gen-fixer struct-tag-fix
                          struct-tag-p tag members flexiblep))
    (fixtype-event
         (defstruct-gen-fixtype struct-tag struct-tag-p
                                struct-tag-fix struct-tag-equiv))
    (constructor-event
         (defstruct-gen-constructor tag-ident struct-tag
                                    struct-tag-p members flexiblep))
    ((mv member-op-events member-infos)
     (defstruct-gen-all-member-ops
          struct-tag struct-tag-p struct-tag-fix
          value-kind-when-struct-tag-p
          valuep-when-struct-tag-p members))
    (info
       (make-defstruct-info
            :tag tag-ident
            :members member-infos
            :flexiblep flexiblep
            :fixtype struct-tag
            :recognizer struct-tag-p
            :fixer struct-tag-fix
            :fixer-recognizer-thm fixer-recognizer-thm
            :not-error-thm not-errorp-when-struct-tag-p
            :valuep-thm valuep-when-struct-tag-p
            :value-kind-thm value-kind-when-struct-tag-p
            :type-of-value-thm type-of-value-when-struct-tag-p
            :flexiblep-thm flexiblep-when-struct-tag-p
            :type-to-quoted-thm struct-tag-to-quoted
            :pointer-type-to-quoted-thm pointer-struct-tag-to-quoted
            :call call))
    (table-event (defstruct-table-record-event (symbol-name tag)
                                               info))
    (label-event (cons 'deflabel (cons tag 'nil))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      recognizer-event
      (cons
        fixer-event
        (cons fixtype-event
              (cons constructor-event
                    (append member-op-events
                            (cons table-event
                                  (cons label-event 'nil))))))))))))

Theorem: pseudo-event-formp-of-defstruct-gen-everything

(defthm pseudo-event-formp-of-defstruct-gen-everything
  (b* ((event (defstruct-gen-everything
                   tag tag-ident members flexiblep call)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)