		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-struct-declon-list

Check a list of structure declarations.

Signature
(check-struct-declon-list declons tagenv) → members
Arguments: declons — Guard (struct-declon-listp declons).; tagenv — Guard (tag-envp tagenv).
Returns: members — Type (member-type-list-resultp members).

These specify the members of a structure or union type (see struct-declon); for now we only use this for the members of a structure type, since we do not model union types.

We go through the declarations and turn each of them into member types (see member-type). We ensure that each member name is well-formed. We check that each type is well-formed. We also check that each type either is complete [C17:6.7.2.1/9], or is an array type of unspecified size in the last member; the latter is a flexible array member [C17:6.7.2.1/18]. By using member-type-add-first, we ensure that there are no duplicate member names.

Definitions and Theorems

Function: check-struct-declon-list

(defun check-struct-declon-list (declons tagenv)
  (declare (xargs :guard (and (struct-declon-listp declons)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-struct-declon-list))
    (declare (ignorable __function__))
    (b* (((when (endp declons)) nil)
         (lastp (endp (cdr declons)))
         ((okf members)
          (check-struct-declon-list (cdr declons)
                                    tagenv))
         ((mv name tyname)
          (struct-declon-to-ident+tyname (car declons)))
         ((okf type)
          (check-tyname tyname tagenv))
         (completep (type-completep type))
         (flexiblep (and lastp (type-case type :array)
                         (not (type-array->size type))))
         ((unless (or completep flexiblep))
          (reserrf (list :incomplete-member-type type)))
         ((okf &) (check-ident name))
         (members-opt (member-type-add-first name type members)))
      (member-type-list-option-case
           members-opt
           :some members-opt.val
           :none (reserrf (list :duplicate-member name))))))

Theorem: member-type-list-resultp-of-check-struct-declon-list

(defthm member-type-list-resultp-of-check-struct-declon-list
  (b* ((members (check-struct-declon-list declons tagenv)))
    (member-type-list-resultp members))
  :rule-classes :rewrite)

Theorem: check-struct-declon-list-of-struct-declon-list-fix-declons

(defthm check-struct-declon-list-of-struct-declon-list-fix-declons
  (equal (check-struct-declon-list (struct-declon-list-fix declons)
                                   tagenv)
         (check-struct-declon-list declons tagenv)))

Theorem: check-struct-declon-list-struct-declon-list-equiv-congruence-on-declons

(defthm
 check-struct-declon-list-struct-declon-list-equiv-congruence-on-declons
 (implies (struct-declon-list-equiv declons declons-equiv)
          (equal (check-struct-declon-list declons tagenv)
                 (check-struct-declon-list declons-equiv tagenv)))
 :rule-classes :congruence)

Theorem: check-struct-declon-list-of-tag-env-fix-tagenv

(defthm check-struct-declon-list-of-tag-env-fix-tagenv
  (equal (check-struct-declon-list declons (tag-env-fix tagenv))
         (check-struct-declon-list declons tagenv)))

Theorem: check-struct-declon-list-tag-env-equiv-congruence-on-tagenv

(defthm check-struct-declon-list-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-struct-declon-list declons tagenv)
                  (check-struct-declon-list declons tagenv-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-check-struct-declon-list

(defthm consp-of-check-struct-declon-list
  (b* nil
    (equal (consp (check-struct-declon-list declons tagenv))
           (consp declons))))