Map a structure declaration to a structure declaration in the language definition.
(ldm-structdecl structdecl) → (mv erp structdecl1)
The specifiers and qualifiers must be all type specifiers, and must form a supported type specifier sequence.
There must be a single structure declarator, which must have a declarator and no constant expression.
Function:
(defun ldm-structdecl (structdecl) (declare (xargs :guard (structdeclp structdecl))) (declare (xargs :guard (structdecl-unambp structdecl))) (let ((__function__ 'ldm-structdecl)) (declare (ignorable __function__)) (b* (((reterr) (c::struct-declon (c::tyspecseq-void) (c::obj-declor-ident (c::ident "irrelevant")))) ((when (structdecl-case structdecl :statassert)) (reterr (msg "Unsupported structure declaration ~x0." (structdecl-fix structdecl)))) (specquals (structdecl-member->specqual structdecl)) (declors (structdecl-member->declor structdecl)) ((mv okp tyspecs) (check-spec/qual-list-all-tyspec specquals)) ((unless okp) (reterr (msg "Unsupported specifier and qualifier list ~ in structure declaration ~x0." (structdecl-fix structdecl)))) ((erp tyspecseq) (ldm-type-spec-list tyspecs)) ((unless (and (consp declors) (endp (cdr declors)))) (reterr (msg "Unsupported number of declarators ~ in structure declaration ~x0." (structdecl-fix structdecl)))) ((structdeclor declor) (car declors)) ((unless declor.declor?) (reterr (msg "Unsupported structure declarator ~ in structure declaration ~x0." (structdecl-fix structdecl)))) ((when declor.expr?) (reterr (msg "Unsupported structure declarator ~ in structure declaration ~x0." (structdecl-fix structdecl)))) ((erp objdeclor) (ldm-declor-obj declor.declor?))) (retok (c::make-struct-declon :tyspec tyspecseq :declor objdeclor)))))
Theorem:
(defthm struct-declonp-of-ldm-structdecl.structdecl1 (b* (((mv acl2::?erp ?structdecl1) (ldm-structdecl structdecl))) (c::struct-declonp structdecl1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-structdecl-of-structdecl-fix-structdecl (equal (ldm-structdecl (structdecl-fix structdecl)) (ldm-structdecl structdecl)))
Theorem:
(defthm ldm-structdecl-structdecl-equiv-congruence-on-structdecl (implies (structdecl-equiv structdecl structdecl-equiv) (equal (ldm-structdecl structdecl) (ldm-structdecl structdecl-equiv))) :rule-classes :congruence)