		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-fundef

Disambiguate a function definition.

Signature
(dimb-fundef fundef table) → (mv erp new-fundef new-table)
Arguments: fundef — Guard (fundefp fundef).; table — Guard (dimb-tablep table).
Returns: new-fundef — Type (fundefp new-fundef).; new-table — Type (dimb-tablep new-table).

We process the declaration specifiers, obtaining the kind of the identifier declared by the declarator, which in valid code must be :objfun, but we do not check this explicitly.

Then we process the declarator, passing t as the fundefp flag, because we are processing the declarator of a defined function. In valid code, this declarator will include a function declarator with either parameter declarations or identifiers, after it has been processed. Because of the fundefp flag set to t, the disambiguation table returned from dimb-declor will contain a newly pushed scope for the function definition. If the (disambiguated) declarator has parameter declarations, those will have added the formal parameters of the function to that scope. If instead the (disambiguated) declarator has just identifiers, the new scope will be empty, but the declarator will be followed, in the function definition, by declarations for the identifiers (again, assuming the code is valid).

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.

We extend the disambiguation table with the identifier __func__ [C17:6.4.2.2].

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.

Definitions and Theorems

Function: dimb-fundef

(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-decl-spec-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-objfun ident table)
)
    (table (dimb-add-ident-objfun (ident "__func__")
                                  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: fundefp-of-dimb-fundef.new-fundef

(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: dimb-tablep-of-dimb-fundef.new-table

(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: fundef-unambp-of-dimb-fundef

(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: dimb-fundef-of-fundef-fix-fundef

(defthm dimb-fundef-of-fundef-fix-fundef
  (equal (dimb-fundef (fundef-fix fundef) table)
         (dimb-fundef fundef table)))

Theorem: dimb-fundef-fundef-equiv-congruence-on-fundef

(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: dimb-fundef-of-dimb-table-fix-table

(defthm dimb-fundef-of-dimb-table-fix-table
  (equal (dimb-fundef fundef (dimb-table-fix table))
         (dimb-fundef fundef table)))

Theorem: dimb-fundef-dimb-table-equiv-congruence-on-table

(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)