		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-fixer

Generate the fixer of the structures defined by the defstruct.

Signature
(defstruct-gen-fixer struct-tag-fix struct-tag-p tag memtypes flexiblep) → (mv event fixer-recognizer-thm)
Arguments: struct-tag-fix — Guard (symbolp struct-tag-fix).; struct-tag-p — Guard (symbolp struct-tag-p).; tag — Guard (symbolp tag).; memtypes — Guard (member-type-listp memtypes).; flexiblep — Guard (booleanp flexiblep).
Returns: event — Type (pseudo-event-formp event).; fixer-recognizer-thm — Type (symbolp fixer-recognizer-thm).

As the fixing value, we pick a structure with the right tag, the right member names, zero integer values of appropriate types for the integer members, and arrays of zeros of appropriate types and appropriate lengths for the integer array mmbers.

We also return the name of the theorem that rewrites the fixer away when the recognizer holds.

Definitions and Theorems

Function: defstruct-gen-fixer-aux

(defun defstruct-gen-fixer-aux (memtypes)
 (declare (xargs :guard (member-type-listp memtypes)))
 (let ((__function__ 'defstruct-gen-fixer-aux))
  (declare (ignorable __function__))
  (b* (((when (endp memtypes)) nil)
       ((member-type member) (car memtypes))
       (val (defstruct-gen-fixing-term member.type))
       (term (cons 'make-member-value
                   (cons ':name
                         (cons (cons 'quote (cons member.name 'nil))
                               (cons ':value (cons val 'nil))))))
       (terms (defstruct-gen-fixer-aux (cdr memtypes))))
    (cons term terms))))

Theorem: true-listp-of-defstruct-gen-fixer-aux

(defthm true-listp-of-defstruct-gen-fixer-aux
  (b* ((terms (defstruct-gen-fixer-aux memtypes)))
    (true-listp terms))
  :rule-classes :rewrite)

Function: defstruct-gen-fixer

(defun defstruct-gen-fixer
       (struct-tag-fix struct-tag-p tag memtypes flexiblep)
 (declare (xargs :guard (and (symbolp struct-tag-fix)
                             (symbolp struct-tag-p)
                             (symbolp tag)
                             (member-type-listp memtypes)
                             (booleanp flexiblep))))
 (let ((__function__ 'defstruct-gen-fixer))
  (declare (ignorable __function__))
  (b*
   ((event-theory
     (cons
      '(:e cons)
      (cons
       '(:e ident)
       (cons
        '(:e repeat)
        (cons
         '(:e member-value)
         (cons
          '(:e value-array)
          (cons
           '(:e value-struct)
           (cons
            (cons ':e (cons struct-tag-p 'nil))
            (cons
             '(:e type-uchar)
             (cons
              '(:e type-ushort)
              (cons
               '(:e type-uint)
               (cons
                '(:e type-ulong)
                (cons
                 '(:e type-ullong)
                 (cons
                  '(:e type-schar)
                  (cons
                   '(:e type-sshort)
                   (cons
                    '(:e type-sint)
                    (cons
                     '(:e type-slong)
                     (cons
                      '(:e type-sllong)
                      (cons
                       '(:e uchar-from-integer)
                       (cons
                        '(:e ushort-from-integer)
                        (cons
                         '(:e uint-from-integer)
                         (cons
                          '(:e ulong-from-integer)
                          (cons
                           '(:e ullong-from-integer)
                           (cons
                            '(:e schar-from-integer)
                            (cons
                             '(:e sshort-from-integer)
                             (cons
                              '(:e sint-from-integer)
                              (cons
                               '(:e slong-from-integer)
                               (cons
                                '(:e sllong-from-integer)
                                (cons
                                 '(:t value-struct)
                                 (cons
                                  (cons ':t
                                        (cons struct-tag-p 'nil))
                                  'nil))))))))))))))))))))))))))))))
    (event
     (cons
      'encapsulate
      (cons
       'nil
       (cons
        (cons
            'local
            (cons (cons 'in-theory
                        (cons (cons 'quote (cons event-theory 'nil))
                              'nil))
                  'nil))
        (cons
         (cons
          'std::deffixer
          (cons
           struct-tag-fix
           (cons
            ':pred
            (cons
             struct-tag-p
             (cons
              ':param
              (cons
               'x
               (cons
                ':body-fix
                (cons
                 (cons
                  'make-value-struct
                  (cons
                   ':tag
                   (cons
                    (cons 'ident
                          (cons (symbol-name tag) 'nil))
                    (cons
                     ':members
                     (cons (cons 'list
                                 (defstruct-gen-fixer-aux memtypes))
                           (cons ':flexiblep
                                 (cons flexiblep 'nil)))))))
                 'nil))))))))
         'nil)))))
    (thm (packn-pos (list struct-tag-fix '-when-
                          struct-tag-p)
                    struct-tag-fix)))
   (mv event thm))))

Theorem: pseudo-event-formp-of-defstruct-gen-fixer.event

(defthm pseudo-event-formp-of-defstruct-gen-fixer.event
  (b* (((mv acl2::?event ?fixer-recognizer-thm)
        (defstruct-gen-fixer struct-tag-fix
                             struct-tag-p tag memtypes flexiblep)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-fixer.fixer-recognizer-thm

(defthm symbolp-of-defstruct-gen-fixer.fixer-recognizer-thm
  (b* (((mv acl2::?event ?fixer-recognizer-thm)
        (defstruct-gen-fixer struct-tag-fix
                             struct-tag-p tag memtypes flexiblep)))
    (symbolp fixer-recognizer-thm))
  :rule-classes :rewrite)