		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-process-members

Process the member inputs of a defstruct call.

Signature
(defstruct-process-members members ctx state) → (mv erp memtypes state)
Arguments: members — Guard (true-listp members).; ctx — Guard (ctxp ctx).
Returns: memtypes — Type (member-type-listp memtypes).

These are the inputs of defstruct after the first one, which specifies the structure tag. Each such input must be a doublet.

The first component of the doublet represents the member name. It must be a symbol whose name is a portable ASCII C identifier that is distinct from the other member names.

The second component of the doublet represents the member type. It must be either one of the fixtype names of the C integer types, or a doublet (<type> <size>) consisting of one of the fixtype names of the C integer types followed by a positive integer, or a singleton (<type>) consisting of one of the fixtype names of the C integer types. The latter is for flexible array members, and can only occur in the last member.

Definitions and Theorems

Function: defstruct-process-members

(defun defstruct-process-members (members ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp members) (ctxp ctx))))
 (let ((__function__ 'defstruct-process-members))
  (declare (ignorable __function__))
  (b*
   ((typelist '(schar uchar sshort ushort
                      sint uint slong ulong sllong ullong))
    ((when (endp members))
     (acl2::value nil))
    (lastp (endp (cdr members)))
    (member (car members))
    ((unless (std::tuplep 2 member))
     (er-soft+
      ctx t nil
      "Each input after the first one ~
                   must be a doublet (NAME TYPE), ~
                   but the input ~x0 does not have this form."
      member))
    (name (first member))
    (type (second member))
    ((unless (symbolp name))
     (er-soft+
      ctx t nil
      "Each input after the first one ~
                   must be a doublet (NAME TYPE) of symbols, ~
                   but the first component of ~x0 is not a symbol."
      member))
    (name (symbol-name name))
    ((unless (paident-stringp name))
     (er-soft+
      ctx t nil
      "Each input after the first one ~
                   must be a doublet (NAME TYPE) of symbols ~
                   where the SYMBOL-NAME of NAME is ~
                   a portable ASCII C identifier (see ATC user documentation), ~
                   but the SYMBOL-NAME of the first component of ~x0 ~
                   is not a portable ASCII C identifier."
      member))
    (members-msg
     (msg
      "Each input after the first one ~
                          must be a doublet (NAME TYPE) ~
                          where TYPE is ~
                          either one of the symbols in ~&0, ~
                          or a doublet (ELEM SIZE) ~
                          where ELEM is one of the aforementioned symbols ~
                          and SIZE is a positive integer,
                          or a singleton (ELEM) ~
                          where ELEM is one of the aforementioned symbols."
      typelist))
    ((er type)
     (cond
      ((atom type)
       (b*
        (((unless (symbolp type))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is an atom, ~
                           but not a symbol."
           members-msg member))
         (type (fixtype-to-integer-type type))
         ((when (not type))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a symbol, ~
                           but not among ~&2."
           members-msg member typelist)))
        (acl2::value type)))
      ((std::tuplep 2 type)
       (b*
        ((elem (first type))
         (size (second type))
         ((unless (symbolp elem))
          (er-soft+
           ctx t nil
           "~@0. ~
                           The second component of ~x1 is a doublet, ~
                           but its first component ~x2 is not a symbol."
           members-msg member elem))
         (elem (fixtype-to-integer-type elem))
         ((when (not elem))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a doublet, ~
                           and its first component ~x2 is a symbol, ~
                           but not among ~&3."
           members-msg member elem typelist))
         ((unless (posp size))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a doublet, ~
                           but its second component ~x2 ~
                           is not a positive integer."
           members-msg member size))
         ((unless (<= size (ullong-max)))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a doublet, ~
                           its second component ~x2 is a positive integer, ~
                           but it exceeds ~x3, ~
                           which is the maximum integer ~
                           representable in an unsigned long long int."
           members-msg member size (ullong-max))))
        (acl2::value (make-type-array :of elem :size size))))
      ((std::tuplep 1 type)
       (b*
        ((elem (first type))
         ((unless (symbolp elem))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a singleton, ~
                           but its (only) component ~x2 is not a symbol."
           members-msg member elem))
         (elem (fixtype-to-integer-type elem))
         ((when (not elem))
          (er-soft+
           ctx t nil
           "~@0 ~
                           The second component of ~x1 is a singleton, ~
                           and its (only) component ~x2 is a symbol, ~
                           but not among ~&3."
           members-msg member elem typelist))
         ((unless lastp)
          (er-soft+
           ctx t nil
           "The member ~x0 has ~
                           an array type of unspecified size, ~
                           but it is not the last member. ~
                           A flexible array members can only be ~
                           the last one in a structure."
           member)))
        (acl2::value (make-type-array :of elem :size nil))))
      (t
       (er-soft+
        ctx t nil
        "~@0 ~
                     The member ~x1 is ~
                     neither an atom ~
                     nor a doublet ~
                     nor a singleton."
        members-msg member))))
    (memtype (make-member-type :name (ident name)
                               :type type))
    ((er memtypes)
     (defstruct-process-members (cdr members)
                                ctx state))
    ((when (member-equal (ident name)
                         (member-type-list->name-list memtypes)))
     (er-soft+ ctx t nil
               "There are distinct members with the same name ~x0."
               name)))
   (acl2::value (cons memtype memtypes)))))

Theorem: member-type-listp-of-defstruct-process-members.memtypes

(defthm member-type-listp-of-defstruct-process-members.memtypes
  (b* (((mv acl2::?erp ?memtypes acl2::?state)
        (defstruct-process-members members ctx state)))
    (member-type-listp memtypes))
  :rule-classes :rewrite)