Check a list of structure declarations.
(check-struct-declon-list declons tagenv) → 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 [C:6.7.2.1/9], or is an array type of unspecified size in the last member; the latter is a flexible array member [C:6.7.2.1/18]. By using member-type-add-first, we ensure that there are no duplicate member names.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm consp-of-check-struct-declon-list (b* nil (equal (consp (check-struct-declon-list declons tagenv)) (consp declons))))