Disambiguate a function definition.
(dimb-fundef fundef table) → (mv erp new-fundef new-table)
We process the declaration specifiers,
obtaining the kind of the identifier declared by the declarator,
which in valid code must be
Then we process the declarator, passing
We process those declarations, which will add the function parameters to the scope that was added when processing the declarator.
Then we add the declared function to the disambiguation table, so that it can be referenced from the body, in a recursive call.
After all of that, we disambiguate the body of the function definition, which is a block (i.e. compound statement) in valid code. But we do not push a new scope for the block, because the scope pushed by dimb-declor is already the one for the function body.
At the end, we pop the scope for the function definition, and we add the function to the table, so that it is available in the rest of the translation unit.
Function:
(defun dimb-fundef (fundef table) (declare (xargs :guard (and (fundefp fundef) (dimb-tablep table)))) (let ((__function__ 'dimb-fundef)) (declare (ignorable __function__)) (b* (((reterr) (irr-fundef) (irr-dimb-table)) ((fundef fundef) fundef) ((erp new-spec & table) (dimb-declspec-list fundef.spec (dimb-kind-objfun) table)) ((erp new-declor ident table) (dimb-declor fundef.declor t table)) ((erp new-decls table) (dimb-decl-list fundef.decls table)) (table (dimb-add-ident ident (dimb-kind-objfun) table) ) ((unless (stmt-case fundef.body :compound)) (reterr (msg "The body of the function definition ~x0 ~ is not a compound statement; ~ the code is invalid." (fundef-fix fundef)))) ((erp new-items table) (dimb-block-item-list (stmt-compound->items fundef.body) table)) (table (dimb-pop-scope table)) (table (dimb-add-ident ident (dimb-kind-objfun) table) )) (retok (make-fundef :extension fundef.extension :spec new-spec :declor new-declor :decls new-decls :body (stmt-compound new-items)) table))))
Theorem:
(defthm fundefp-of-dimb-fundef.new-fundef (b* (((mv acl2::?erp ?new-fundef ?new-table) (dimb-fundef fundef table))) (fundefp new-fundef)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-fundef.new-table (b* (((mv acl2::?erp ?new-fundef ?new-table) (dimb-fundef fundef table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm fundef-unambp-of-dimb-fundef (b* (((mv acl2::?erp ?new-fundef ?new-table) (dimb-fundef fundef table))) (implies (not erp) (fundef-unambp new-fundef))))
Theorem:
(defthm dimb-fundef-of-fundef-fix-fundef (equal (dimb-fundef (fundef-fix fundef) table) (dimb-fundef fundef table)))
Theorem:
(defthm dimb-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (dimb-fundef fundef table) (dimb-fundef fundef-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-fundef-of-dimb-table-fix-table (equal (dimb-fundef fundef (dimb-table-fix table)) (dimb-fundef fundef table)))
Theorem:
(defthm dimb-fundef-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-fundef fundef table) (dimb-fundef fundef table-equiv))) :rule-classes :congruence)