Map a declaration to a tag declaration in the language definition.
(ldm-decl-tag decl) → (mv erp tagdeclon)
The declaration must not be a static assertion declaration, and must consists of a single type specifier without declarators. The type specifier must be a structure, union, or enumeration specifier with members/elements.
Function:
(defun ldm-decl-tag (decl) (declare (xargs :guard (declp decl))) (declare (xargs :guard (decl-unambp decl))) (let ((__function__ 'ldm-decl-tag)) (declare (ignorable __function__)) (b* (((reterr) (c::tag-declon-enum (c::ident "irrelevant") nil)) ((when (decl-case decl :statassert)) (reterr (msg "Unsupported static assertion declaration ~x0." (decl-fix decl)))) (extension (decl-decl->extension decl)) (declspecs (decl-decl->specs decl)) (initdeclors (decl-decl->init decl)) (attrib (decl-decl->attrib decl)) ((when extension) (reterr (msg "Unsupported GCC extension keyword ~ for tag (i.e. structure/union/enumeration) ~ declaration."))) ((when attrib) (reterr (msg "Unsupported GCC attributes ~x0 ~ for tag (i.e. structure/union/enumeration) declaration." attrib))) ((when initdeclors) (reterr (msg "Unsupported initialization declarators ~x0 ~ for tag (i.e. structure/union/enumeration) declaration." initdeclors))) ((unless (and (consp declspecs) (endp (cdr declspecs)))) (reterr (msg "Unsupported number of declaration specifiers ~x0 ~ for tag (i.e. structure/union/enumeration) declaration." declspecs))) (declspec (car declspecs)) ((unless (declspec-case declspec :tyspec)) (reterr (msg "Unsupported declaration specifier ~x0 ~ for tag (i.e. structure/union/enumeration) declaration." declspec))) (tyspec (declspec-tyspec->unwrap declspec)) ((when (type-spec-case tyspec :struct)) (b* (((strunispec strunispec) (type-spec-struct->unwrap tyspec)) ((unless strunispec.name) (reterr (msg "Unsupported structure declaration without name."))) ((erp name1) (ldm-ident strunispec.name)) ((erp members1) (ldm-structdecl-list strunispec.members))) (retok (c::make-tag-declon-struct :tag name1 :members members1)))) ((when (type-spec-case tyspec :union)) (b* (((strunispec strunispec) (type-spec-union->unwrap tyspec)) ((unless strunispec.name) (reterr (msg "Unsupported union declaration without name."))) ((erp name1) (ldm-ident strunispec.name)) ((erp members1) (ldm-structdecl-list strunispec.members))) (retok (c::make-tag-declon-union :tag name1 :members members1)))) ((when (type-spec-case tyspec :enum)) (b* (((enumspec enumspec) (type-spec-enum->unwrap tyspec)) ((unless enumspec.name) (reterr (msg "Unsupported enumeration declaration without name."))) ((erp name1) (ldm-ident enumspec.name)) ((erp idents1) (ldm-enumer-list enumspec.list))) (retok (c::make-tag-declon-enum :tag name1 :enumerators idents1))))) (reterr (msg "Unsupported type specifier ~x0 ~ for tag (i.e. structure/union/enumeration) declaration." tyspec)))))
Theorem:
(defthm tag-declonp-of-ldm-decl-tag.tagdeclon (b* (((mv acl2::?erp ?tagdeclon) (ldm-decl-tag decl))) (c::tag-declonp tagdeclon)) :rule-classes :rewrite)
Theorem:
(defthm ldm-decl-tag-of-decl-fix-decl (equal (ldm-decl-tag (decl-fix decl)) (ldm-decl-tag decl)))
Theorem:
(defthm ldm-decl-tag-decl-equiv-congruence-on-decl (implies (decl-equiv decl decl-equiv) (equal (ldm-decl-tag decl) (ldm-decl-tag decl-equiv))) :rule-classes :congruence)