Map a function definition to the language definition.
(ldm-fundef fundef) → (mv erp fundef1)
The declaration specifiers must be all type specifiers, and their list must form a supported sequence.
The declarator must be a supported function declarator.
There must be no declarations (between declarator and body).
Function:
(defun ldm-fundef (fundef) (declare (xargs :guard (fundefp fundef))) (declare (xargs :guard (fundef-unambp fundef))) (let ((__function__ 'ldm-fundef)) (declare (ignorable __function__)) (b* (((reterr) (c::fundef (c::tyspecseq-void) (c::fun-declor-base (c::ident "irrelevant") nil) nil)) ((fundef fundef) fundef) ((mv okp tyspecs) (check-declspec-list-all-tyspec fundef.spec)) ((when (not okp)) (reterr (msg "Unsupported declaration specifiers ~ in function definition ~x0." (fundef-fix fundef)))) ((erp tyspecseq) (ldm-type-spec-list tyspecs)) ((erp fundeclor) (ldm-declor-fun fundef.declor)) ((when fundef.asm?) (reterr (msg "Unsupported assembler name specifier ~ in function definition ~x0." (fundef-fix fundef)))) ((when fundef.decls) (reterr (msg "Unsupported declarations ~ in function definition ~x0." (fundef-fix fundef)))) ((erp body) (ldm-stmt fundef.body)) ((unless (c::stmt-case body :compound)) (reterr (msg "Unsupported non-compound statement body ~ in function definition ~x0." (fundef-fix fundef))))) (retok (c::make-fundef :tyspec tyspecseq :declor fundeclor :body (c::stmt-compound->items body))))))
Theorem:
(defthm fundefp-of-ldm-fundef.fundef1 (b* (((mv acl2::?erp ?fundef1) (ldm-fundef fundef))) (c::fundefp fundef1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-fundef-of-fundef-fix-fundef (equal (ldm-fundef (fundef-fix fundef)) (ldm-fundef fundef)))
Theorem:
(defthm ldm-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (ldm-fundef fundef) (ldm-fundef fundef-equiv))) :rule-classes :congruence)