		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-constructor

Generate the constructor of values of the structure type.

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

See the user documentation for details on the parameters, additional guard (if any), and return type. We use an auxiliary recursive function to go through the members and collect the parameters and their types, the len conjuncts in the extra guard (if any), the consp conjuncts in the extra guard (if any; always one or none), and terms use to make the members of the structure value. The body of the function just calls the structure value constructor from the C language formalization, with suitable inputs. Note that we fix the integer member values, to avoid having the return type theorem require additional hypotheses. However, we have the hypotheses about the length of the array members; it seems a bit awkward, or at least less natural, to fix the inputs of the constructor to make those unnecessary; nonetheless, we may consider doing that in the future.

Definitions and Theorems

Function: defstruct-gen-constructor-aux

(defun defstruct-gen-constructor-aux (struct-tag members)
 (declare (xargs :guard (and (symbolp struct-tag)
                             (member-type-listp members))))
 (let ((__function__ 'defstruct-gen-constructor-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp members))
     (mv nil nil nil nil))
    (member (car members))
    (name (member-type->name member))
    (type (member-type->type member))
    (param-name (intern-in-package-of-symbol (ident->name name)
                                             struct-tag))
    ((mv parameter
         len-conjunct consp-conjunct make-member)
     (cond
      ((type-nonchar-integerp type)
       (b*
        ((fixtype (integer-type-to-fixtype type))
         (pred (pack fixtype 'p))
         (fixer (pack fixtype '-fix))
         (parameter (cons param-name (cons pred 'nil)))
         (len-conjunct nil)
         (consp-conjunct nil)
         (make-member
          (cons
           'make-member-value
           (cons
               ':name
               (cons (cons 'ident
                           (cons (ident->name name) 'nil))
                     (cons ':value
                           (cons (cons fixer (cons param-name 'nil))
                                 'nil)))))))
        (mv parameter len-conjunct
            consp-conjunct make-member)))
      ((and (type-case type :array)
            (type-nonchar-integerp (type-array->of type)))
       (b*
        ((fixtype (integer-type-to-fixtype (type-array->of type)))
         (pred (pack fixtype '-listp))
         (parameter (cons param-name (cons pred 'nil)))
         (size (type-array->size type))
         ((mv len-conjunct consp-conjunct)
          (if size
              (mv (cons 'equal
                        (cons (cons 'len (cons param-name 'nil))
                              (cons size 'nil)))
                  nil)
            (mv nil
                (cons 'consp (cons param-name 'nil)))))
         (array-of (pack fixtype '-array-of))
         (make-member
          (cons
           'make-member-value
           (cons
            ':name
            (cons (cons 'ident
                        (cons (ident->name name) 'nil))
                  (cons ':value
                        (cons (cons array-of (cons param-name 'nil))
                              'nil)))))))
        (mv parameter len-conjunct
            consp-conjunct make-member)))
      (t (prog2$ (raise "Internal error: member type ~x0." type)
                 (mv nil nil nil nil)))))
    ((mv parameters len-conjuncts
         consp-conjuncts make-members)
     (defstruct-gen-constructor-aux struct-tag (cdr members))))
   (mv (cons parameter parameters)
       (if len-conjunct (cons len-conjunct len-conjuncts)
         len-conjuncts)
       (if consp-conjunct (cons consp-conjunct consp-conjuncts)
         consp-conjuncts)
       (cons make-member make-members)))))

Theorem: true-listp-of-defstruct-gen-constructor-aux.parameters

(defthm true-listp-of-defstruct-gen-constructor-aux.parameters
  (b* (((mv ?parameters ?len-conjuncts
            ?consp-conjuncts ?make-members)
        (defstruct-gen-constructor-aux struct-tag members)))
    (true-listp parameters))
  :rule-classes :rewrite)

Theorem: true-listp-of-defstruct-gen-constructor-aux.len-conjuncts

(defthm true-listp-of-defstruct-gen-constructor-aux.len-conjuncts
  (b* (((mv ?parameters ?len-conjuncts
            ?consp-conjuncts ?make-members)
        (defstruct-gen-constructor-aux struct-tag members)))
    (true-listp len-conjuncts))
  :rule-classes :rewrite)

Theorem: true-listp-of-defstruct-gen-constructor-aux.consp-conjuncts

(defthm true-listp-of-defstruct-gen-constructor-aux.consp-conjuncts
  (b* (((mv ?parameters ?len-conjuncts
            ?consp-conjuncts ?make-members)
        (defstruct-gen-constructor-aux struct-tag members)))
    (true-listp consp-conjuncts))
  :rule-classes :rewrite)

Theorem: true-listp-of-defstruct-gen-constructor-aux.make-members

(defthm true-listp-of-defstruct-gen-constructor-aux.make-members
  (b* (((mv ?parameters ?len-conjuncts
            ?consp-conjuncts ?make-members)
        (defstruct-gen-constructor-aux struct-tag members)))
    (true-listp make-members))
  :rule-classes :rewrite)

Function: defstruct-gen-constructor

(defun defstruct-gen-constructor
       (tag-ident struct-tag
                  struct-tag-p members flexiblep)
 (declare (xargs :guard (and (identp tag-ident)
                             (symbolp struct-tag)
                             (symbolp struct-tag-p)
                             (member-type-listp members)
                             (booleanp flexiblep))))
 (let ((__function__ 'defstruct-gen-constructor))
  (declare (ignorable __function__))
  (b*
   (((mv parameters len-conjuncts
         consp-conjuncts make-members)
     (defstruct-gen-constructor-aux struct-tag members))
    (guard-theory
         '(defstruct-consp-len-lemma
               (:e posp)
               (:e member-value-listp)
               (:e len)
               true-listp-when-uchar-listp-compound-recognizer
               member-value-listp-of-cons
               member-valuep-of-member-value
               schar-fix-when-scharp
               uchar-fix-when-ucharp
               sshort-fix-when-sshortp
               ushort-fix-when-ushortp
               sint-fix-when-sintp uint-fix-when-uintp
               slong-fix-when-slongp
               ulong-fix-when-ulongp
               sllong-fix-when-sllongp
               ullong-fix-when-ullongp
               valuep-when-scharp valuep-when-ucharp
               valuep-when-sshortp valuep-when-ushortp
               valuep-when-sintp valuep-when-uintp
               valuep-when-slongp valuep-when-ulongp
               valuep-when-sllongp valuep-when-ullongp
               valuep-when-schar-arrayp
               valuep-when-uchar-arrayp
               valuep-when-sshort-arrayp
               valuep-when-ushort-arrayp
               valuep-when-sint-arrayp
               valuep-when-uint-arrayp
               valuep-when-slong-arrayp
               valuep-when-ulong-arrayp
               valuep-when-sllong-arrayp
               valuep-when-ullong-arrayp
               schar-arrayp-of-schar-array-of
               uchar-arrayp-of-uchar-array-of
               sshort-arrayp-of-sshort-array-of
               ushort-arrayp-of-ushort-array-of
               sint-arrayp-of-sint-array-of
               uint-arrayp-of-uint-array-of
               slong-arrayp-of-slong-array-of
               ulong-arrayp-of-ulong-array-of
               sllong-arrayp-of-sllong-array-of
               ullong-arrayp-of-ullong-array-of
               identp-of-ident
               booleanp-compound-recognizer))
    (returns-theory
     (cons
      'defstruct-consp-len-lemma
      (cons
       '(:e posp)
       (cons
        '(:e acl2::bool-fix)
        (cons
         '(:e ident)
         (cons
          '(:e ident-fix)
          (cons
           '(:e member-value-list->name-list)
           (cons
            '(:e member-value-list-fix)
            (cons
                struct-tag
                (cons struct-tag-p
                      '(scharp-of-schar-fix
                            ucharp-of-uchar-fix
                            sshortp-of-sshort-fix
                            ushortp-of-ushort-fix
                            sintp-of-sint-fix uintp-of-uint-fix
                            slongp-of-slong-fix ulongp-of-ulong-fix
                            sllongp-of-sllong-fix
                            ullongp-of-ullong-fix
                            schar-fix-when-scharp
                            uchar-fix-when-ucharp
                            sshort-fix-when-sshortp
                            ushort-fix-when-ushortp
                            sint-fix-when-sintp uint-fix-when-uintp
                            slong-fix-when-slongp
                            ulong-fix-when-ulongp
                            sllong-fix-when-sllongp
                            ullong-fix-when-ullongp
                            valuep-when-scharp valuep-when-ucharp
                            valuep-when-sshortp valuep-when-ushortp
                            valuep-when-sintp valuep-when-uintp
                            valuep-when-slongp valuep-when-ulongp
                            valuep-when-sllongp valuep-when-ullongp
                            valuep-when-schar-arrayp
                            valuep-when-uchar-arrayp
                            valuep-when-sshort-arrayp
                            valuep-when-ushort-arrayp
                            valuep-when-sint-arrayp
                            valuep-when-uint-arrayp
                            valuep-when-slong-arrayp
                            valuep-when-ulong-arrayp
                            valuep-when-sllong-arrayp
                            valuep-when-ullong-arrayp
                            schar-array-length uchar-array-length
                            sshort-array-length ushort-array-length
                            sint-array-length uint-array-length
                            slong-array-length ulong-array-length
                            sllong-array-length ullong-array-length
                            schar-array-of uchar-array-of
                            sshort-array-of ushort-array-of
                            sint-array-of uint-array-of
                            slong-array-of ulong-array-of
                            sllong-array-of ullong-array-of
                            schar-arrayp-of-schar-array
                            uchar-arrayp-of-uchar-array
                            sshort-arrayp-of-sshort-array
                            ushort-arrayp-of-ushort-array
                            sint-arrayp-of-sint-array
                            uint-arrayp-of-uint-array
                            slong-arrayp-of-slong-array
                            ulong-arrayp-of-ulong-array
                            sllong-arrayp-of-sllong-array
                            ullong-arrayp-of-ullong-array
                            consp-of-schar-list-fix
                            consp-of-uchar-list-fix
                            consp-of-sshort-list-fix
                            consp-of-ushort-list-fix
                            consp-of-sint-list-fix
                            consp-of-uint-list-fix
                            consp-of-slong-list-fix
                            consp-of-ulong-list-fix
                            consp-of-sllong-list-fix
                            consp-of-ullong-list-fix
                            len-of-schar-list-fix
                            len-of-uchar-list-fix
                            len-of-sshort-list-fix
                            len-of-ushort-list-fix
                            len-of-sint-list-fix
                            len-of-uint-list-fix
                            len-of-slong-list-fix
                            len-of-ulong-list-fix
                            len-of-sllong-list-fix
                            len-of-ullong-list-fix
                            schar-array->elements-of-schar-array
                            uchar-array->elements-of-uchar-array
                            sshort-array->elements-of-sshort-array
                            ushort-array->elements-of-ushort-array
                            sint-array->elements-of-sint-array
                            uint-array->elements-of-uint-array
                            slong-array->elements-of-slong-array
                            ulong-array->elements-of-ulong-array
                            sllong-array->elements-of-sllong-array
                            ullong-array->elements-of-ullong-array
                            car-cons cdr-cons value-struct-read-aux
                            value-fix-when-valuep
                            member-value->name-of-member-value
                            member-value->value-of-member-value
                            value-struct->members-of-value-struct
                            value-struct->tag-of-value-struct
                            value-struct->flexiblep-of-value-struct
                            return-type-of-value-struct
                            member-value-fix-when-member-valuep
                            member-value-list->name-list-of-cons
                            member-value-list-fix-of-cons
                            member-valuep-of-member-value)))))))))))
    (guard-conjuncts (append len-conjuncts consp-conjuncts)))
   (cons
    'define
    (cons
     struct-tag
     (cons
      parameters
      (append
       (and guard-conjuncts
            (cons ':guard
                  (cons (cons 'and guard-conjuncts)
                        'nil)))
       (cons
        ':returns
        (cons
         (cons
          'struct
          (cons
           struct-tag-p
           (append
            (and guard-conjuncts
                 (cons ':hyp
                       (cons (cons 'and len-conjuncts) 'nil)))
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons ':in-theory
                      (cons (cons 'quote (cons returns-theory 'nil))
                            'nil)))
               'nil)
              'nil)))))
         (cons
          (cons
           'make-value-struct
           (cons ':tag
                 (cons (cons 'ident
                             (cons (ident->name tag-ident) 'nil))
                       (cons ':members
                             (cons (cons 'list make-members)
                                   (cons ':flexiblep
                                         (cons flexiblep 'nil)))))))
          (cons
           ':guard-simplify
           (cons
            ':limited
            (cons
             ':guard-hints
             (cons
              (cons
               (cons
                  '"Goal"
                  (cons ':in-theory
                        (cons (cons 'quote (cons guard-theory 'nil))
                              'nil)))
               'nil)
              'nil))))))))))))))

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

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

Theorem: defstruct-consp-len-lemma

(defthm defstruct-consp-len-lemma
  (implies (and (equal (len x) c) (posp c))
           (consp x)))