		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-process-inputs

Process the inputs of a defstruct call.

Signature
(defstruct-process-inputs args call ctx state) → (mv erp val state)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).; ctx — Guard (ctxp ctx).
Returns: val — Type (tuple (tag symbolp) (tag-ident identp) (memtypes member-type-listp) (flexiblep booleanp) (redundant booleanp) val) .

We process the tag and the members. If the table already contains an entry for this tag, the call must be identical, in which case the call is redundant; if the call is not identical, it is an error.

Definitions and Theorems

Function: defstruct-process-inputs

(defun defstruct-process-inputs (args call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call)
                             (ctxp ctx))))
 (let ((__function__ 'defstruct-process-inputs))
  (declare (ignorable __function__))
  (b*
   ((irrelevant (list nil (irr-ident) nil nil nil))
    ((unless (consp args))
     (er-soft+
      ctx t irrelevant
      "There must be at least one input, ~
                   but no inputs were supplied."))
    (tag (car args))
    ((unless (symbolp tag))
     (er-soft+
      ctx t irrelevant
      "The first input must be a symbol, ~
                   but ~x0 is not."
      tag))
    (tag-name (symbol-name tag))
    ((unless (paident-stringp tag-name))
     (er-soft+
      ctx t irrelevant
      "The name ~x0 of the symbol ~x1 passed as first input, ~
                   which defines the name of the structure, ~
                   must be a portable ASCII C identifier."
      tag-name tag))
    (tag-ident (ident tag-name))
    (info (defstruct-table-lookup tag-name (w state)))
    ((when info)
     (if (equal (defstruct-info->call info) call)
         (acl2::value (list tag (irr-ident) nil nil t))
      (er-soft+
       ctx t irrelevant
       "There is already a structure with tag ~x0 ~
                     recorded in the table of shallowly embedded C structures, ~
                     but its call ~x1 differs from the current ~x2, ~
                     so the call is not redundant."
       tag-name (defstruct-info->call info)
       call)))
    (members (cdr args))
    ((unless (consp members))
     (er-soft+ ctx t irrelevant
               "There must be at least one member."))
    ((er memtypes :iferr irrelevant)
     (defstruct-process-members members ctx state))
    (flexiblep (and (consp memtypes)
                    (b* ((memtype (car (last memtypes)))
                         (type (member-type->type memtype)))
                      (and (type-case type :array)
                           (not (type-array->size type))))))
    ((when (and flexiblep (not (consp (cdr members)))))
     (er-soft+
      ctx t irrelevant
      "Since there is a flexible array member, ~
                   there must be at least another member.")))
   (acl2::value (list tag
                      tag-ident memtypes flexiblep nil)))))

Theorem: return-type-of-defstruct-process-inputs.val

(defthm return-type-of-defstruct-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defstruct-process-inputs args call ctx state)))
    (tuple (tag symbolp)
           (tag-ident identp)
           (memtypes member-type-listp)
           (flexiblep booleanp)
           (redundant booleanp)
           val))
  :rule-classes :rewrite)

Theorem: true-listp-of-defstruct-process-inputs.val

(defthm true-listp-of-defstruct-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defstruct-process-inputs args call ctx state)))
    (true-listp val))
  :rule-classes :type-prescription)