Map a declaration to a function declaration in the language definition.
(ldm-decl-fun decl) → (mv erp fundeclon)
The declaration must not be a static assertion declaration.
The declaration specifiers must be all type specifiers, and form a supported sequence.
The initialization declarator must be a declarator, without initializer, and it must be a supported declarator for a function.
Function:
(defun ldm-decl-fun (decl) (declare (xargs :guard (declp decl))) (declare (xargs :guard (decl-unambp decl))) (let ((__function__ 'ldm-decl-fun)) (declare (ignorable __function__)) (b* (((reterr) (c::fun-declon (c::tyspecseq-void) (c::fun-declor-base (c::ident "irrelevant") nil))) ((when (decl-case decl :statassert)) (reterr (msg "Unsupported static assertion declaration ~x0." (decl-fix decl)))) (declspecs (decl-decl->specs decl)) (initdeclors (decl-decl->init decl)) ((when initdeclors) (reterr (msg "Unsupported initialization declarators ~x0 ~ for function declaration." initdeclors))) ((mv okp tyspecs) (check-declspec-list-all-tyspec declspecs)) ((when (not okp)) (reterr (msg "Unsupported declaration specifier list ~ in declaration ~x0 for function." (decl-fix decl)))) ((erp tyspecseq) (ldm-type-spec-list tyspecs)) ((unless (and (consp initdeclors) (endp (cdr initdeclors)))) (reterr (msg "Unsupported number of declarators ~x0 ~ for function declaration." initdeclors))) ((initdeclor initdeclor) (car initdeclors)) ((when initdeclor.init?) (reterr (msg "Unsupported initializer ~x0 ~ for function declaration." initdeclor.init?))) ((erp fundeclor) (ldm-declor-fun initdeclor.declor))) (retok (c::make-fun-declon :tyspec tyspecseq :declor fundeclor)))))
Theorem:
(defthm fun-declonp-of-ldm-decl-fun.fundeclon (b* (((mv acl2::?erp ?fundeclon) (ldm-decl-fun decl))) (c::fun-declonp fundeclon)) :rule-classes :rewrite)
Theorem:
(defthm ldm-decl-fun-of-decl-fix-decl (equal (ldm-decl-fun (decl-fix decl)) (ldm-decl-fun decl)))
Theorem:
(defthm ldm-decl-fun-decl-equiv-congruence-on-decl (implies (decl-equiv decl decl-equiv) (equal (ldm-decl-fun decl) (ldm-decl-fun decl-equiv))) :rule-classes :congruence)