		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-recognizer

Generate the recognizer of the structures defined by the defstruct.

Signature
(defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep) → (mv event not-error-thm valuep-thm value-kind-thm type-of-value-thm flexiblep-thm type-to-quoted-thm pointer-type-to-quoted-thm)
Arguments: 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).; not-error-thm — Type (symbolp not-error-thm).; valuep-thm — Type (symbolp valuep-thm).; value-kind-thm — Type (symbolp value-kind-thm).; type-of-value-thm — Type (symbolp type-of-value-thm).; flexiblep-thm — Type (symbolp flexiblep-thm).; type-to-quoted-thm — Type (symbolp type-to-quoted-thm).; pointer-type-to-quoted-thm — Type (symbolp pointer-type-to-quoted-thm).

This recognizes structures with the appropriate types, member names, and member types. For now the flexible array member flag (see value) is unset, because defstruct does not support that.

We also generate several theorems; see defstruct-info.

Definitions and Theorems

Function: defstruct-gen-recognizer

(defun defstruct-gen-recognizer
       (struct-tag-p tag memtypes flexiblep)
 (declare (xargs :guard (and (symbolp struct-tag-p)
                             (symbolp tag)
                             (member-type-listp memtypes)
                             (booleanp flexiblep))))
 (let ((__function__ 'defstruct-gen-recognizer))
  (declare (ignorable __function__))
  (b*
   ((not-errorp-when-struct-tag-p
         (packn-pos (list 'not-errorp-when- struct-tag-p)
                    struct-tag-p))
    (valuep-when-struct-tag-p
         (packn-pos (list 'valuep-when- struct-tag-p)
                    struct-tag-p))
    (value-kind-when-struct-tag-p
         (packn-pos (list 'value-kind-when- struct-tag-p)
                    struct-tag-p))
    (type-of-value-when-struct-tag-p
         (packn-pos (list 'type-of-value-when- struct-tag-p)
                    struct-tag-p))
    (flexiblep-when-struct-tag-p
         (packn-pos (list 'flexiblep-when- struct-tag-p)
                    struct-tag-p))
    (struct-tag-to-quoted (packn-pos (list 'struct- tag '-to-quoted)
                                     struct-tag-p))
    (pointer-struct-tag-to-quoted
         (packn-pos (list 'pointer-struct- tag '-to-quoted)
                    struct-tag-p))
    (event
     (cons
      'define
      (cons
       struct-tag-p
       (cons
        '(x)
        (cons
         ':returns
         (cons
          (cons
           'yes/no
           (cons
            'booleanp
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons 'quote
                        (cons (cons struct-tag-p
                                    '(booleanp-compound-recognizer))
                              'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           (cons
            'and
            (cons
             '(valuep x)
             (cons
              '(value-case x :struct)
              (cons
               (cons
                    'equal
                    (cons '(value-struct->tag x)
                          (cons (cons 'ident
                                      (cons (symbol-name tag) 'nil))
                                'nil)))
               (cons
                (cons
                 'equal
                 (cons
                  '(member-value-list->name-list
                        (value-struct->members x))
                  (cons
                   (cons
                        'quote
                        (cons (member-type-list->name-list memtypes)
                              'nil))
                   'nil)))
                (append
                   (defstruct-gen-recognizer-all-conjuncts memtypes)
                   (cons (cons 'equal
                               (cons '(value-struct->flexiblep x)
                                     (cons flexiblep 'nil)))
                         'nil)))))))
           (cons
            ':guard-simplify
            (cons
             ':limited
             (cons
              ':guard-hints
              (cons
               '(("Goal" :in-theory '(member-value-listp-of-value-struct->members
                                          (:e identp))))
               (cons
                '///
                (cons
                 (cons 'fty::deffixequiv
                       (cons struct-tag-p
                             '(:hints (("Goal" :in-theory nil)))))
                 (cons
                  (cons
                   'defruled
                   (cons
                    not-errorp-when-struct-tag-p
                    (cons
                     (cons 'implies
                           (cons (cons struct-tag-p '(x))
                                 '((not (errorp x)))))
                     (cons
                      ':in-theory
                      (cons
                       (cons
                          'quote
                          (cons (cons 'errorp
                                      (cons struct-tag-p '(valuep)))
                                'nil))
                       'nil)))))
                  (cons
                   (cons
                    'defruled
                    (cons
                     valuep-when-struct-tag-p
                     (cons
                      (cons 'implies
                            (cons (cons struct-tag-p '(x))
                                  '((valuep x))))
                      (cons
                       ':in-theory
                       (cons
                         (cons 'quote
                               (cons (cons struct-tag-p 'nil) 'nil))
                         'nil)))))
                   (cons
                    (cons
                     'defruled
                     (cons
                      value-kind-when-struct-tag-p
                      (cons
                       (cons
                           'implies
                           (cons (cons struct-tag-p '(x))
                                 '((equal (value-kind x) :struct))))
                       (cons
                        ':in-theory
                        (cons
                         (cons 'quote
                               (cons (cons struct-tag-p 'nil) 'nil))
                         'nil)))))
                    (cons
                     (cons
                      'defruled
                      (cons
                       type-of-value-when-struct-tag-p
                       (cons
                        (cons
                         'implies
                         (cons
                          (cons struct-tag-p '(x))
                          (cons
                           (cons
                            'equal
                            (cons
                             '(type-of-value x)
                             (cons
                              (cons
                               'type-struct
                               (cons
                                (cons 'ident
                                      (cons (symbol-name tag) 'nil))
                                'nil))
                              'nil)))
                           'nil)))
                        (cons
                         ':in-theory
                         (cons
                          (cons
                           'quote
                           (cons
                                (cons struct-tag-p '(type-of-value))
                                'nil))
                          'nil)))))
                     (cons
                      (cons
                       'defruled
                       (cons
                        flexiblep-when-struct-tag-p
                        (cons
                         (cons
                          'implies
                          (cons
                           (cons struct-tag-p '(x))
                           (cons
                            (cons 'equal
                                  (cons '(value-struct->flexiblep x)
                                        (cons flexiblep 'nil)))
                            'nil)))
                         (cons
                          ':in-theory
                          (cons
                           (cons
                               'quote
                               (cons (cons struct-tag-p 'nil) 'nil))
                           'nil)))))
                      (cons
                       (cons
                        'defruled
                        (cons
                         struct-tag-to-quoted
                         (cons
                          (cons
                           'equal
                           (cons
                            (cons
                             'type-struct
                             (cons
                                (cons 'ident
                                      (cons (symbol-name tag) 'nil))
                                'nil))
                            (cons
                             (cons
                               'quote
                               (cons (type-struct
                                          (ident (symbol-name tag)))
                                     'nil))
                             'nil)))
                          '(:in-theory
                                '((:e ident) (:e type-struct))))))
                       (cons
                        (cons
                         'defruled
                         (cons
                          pointer-struct-tag-to-quoted
                          (cons
                           (cons
                            'equal
                            (cons
                             (cons
                              'type-pointer
                              (cons
                               (cons
                                'type-struct
                                (cons
                                 (cons
                                      'ident
                                      (cons (symbol-name tag) 'nil))
                                 'nil))
                               'nil))
                             (cons
                              (cons
                               'quote
                               (cons
                                (type-pointer
                                    (type-struct
                                         (ident (symbol-name tag))))
                                'nil))
                              'nil)))
                           '(:in-theory '((:e ident)
                                          (:e type-struct)
                                          (:e type-pointer))))))
                        'nil)))))))))))))))))))))
   (mv 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))))

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

(defthm pseudo-event-formp-of-defstruct-gen-recognizer.event
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-recognizer.not-error-thm

(defthm symbolp-of-defstruct-gen-recognizer.not-error-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp not-error-thm))
 :rule-classes :rewrite)

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

(defthm symbolp-of-defstruct-gen-recognizer.valuep-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp valuep-thm))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-recognizer.value-kind-thm

(defthm symbolp-of-defstruct-gen-recognizer.value-kind-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp value-kind-thm))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-recognizer.type-of-value-thm

(defthm symbolp-of-defstruct-gen-recognizer.type-of-value-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp type-of-value-thm))
 :rule-classes :rewrite)

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

(defthm symbolp-of-defstruct-gen-recognizer.flexiblep-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp flexiblep-thm))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-recognizer.type-to-quoted-thm

(defthm symbolp-of-defstruct-gen-recognizer.type-to-quoted-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp type-to-quoted-thm))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-recognizer.pointer-type-to-quoted-thm

(defthm
     symbolp-of-defstruct-gen-recognizer.pointer-type-to-quoted-thm
 (b*
  (((mv acl2::?event ?not-error-thm ?valuep-thm
        ?value-kind-thm ?type-of-value-thm
        ?flexiblep-thm ?type-to-quoted-thm
        ?pointer-type-to-quoted-thm)
    (defstruct-gen-recognizer struct-tag-p tag memtypes flexiblep)))
  (symbolp pointer-type-to-quoted-thm))
 :rule-classes :rewrite)