		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-fundef

Disambiguate a function definition.

Signature
(dimb-fundef fundef table gcc) → (mv erp new-fundef new-table)
Arguments: fundef — Guard (fundefp fundef).; table — Guard (dimb-tablep table).; gcc — Guard (booleanp gcc).
Returns: erp — Type (maybe-msgp erp).; 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 fundef-params-p 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 fundef-params-p 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).

As with declarations, the scope of the function name starts just after its declarator; it must be added to the file scope of the disambiguation table. However, recall that the disambiguation of the declarator pushes a new scope for the outermost block of the function definition. Thus, instead of using dimb-add-ident-objfun to add the function, we use dimb-add-ident-objfun-file-scope.

We process any declarations, which add 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]. If the GCC flag is enabled (i.e. GCC extensions are allowed), we further extend the table with the identifiers __FUNCTION__ and __PRETTY_FUNCTION__ (GCC manual, ``Function Names'').

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 gcc)
 (declare (xargs :guard (and (fundefp fundef)
                             (dimb-tablep table)
                             (booleanp gcc))))
 (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))
    (table (dimb-add-ident-objfun-file-scope ident table)
)
    ((erp new-decls table)
     (dimb-decl-list fundef.decls table))
    (table (dimb-add-ident-objfun (ident "__func__")
                                  table)
)
    (table
     (if gcc
       (dimb-add-idents-objfun (list (ident "__FUNCTION__")
                                     (ident "__PRETTY_FUNCTION__"))
                               table)
       table)
)
    ((unless (stmt-case fundef.body :compound))
     (retmsg$
      "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: maybe-msgp-of-dimb-fundef.erp

(defthm maybe-msgp-of-dimb-fundef.erp
  (b* (((mv acl2::?erp ?new-fundef ?new-table)
        (dimb-fundef fundef table gcc)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

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 gcc)))
    (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 gcc)))
    (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 gcc)))
    (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 gcc)
         (dimb-fundef fundef table gcc)))

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 gcc)
                  (dimb-fundef fundef-equiv table gcc)))
  :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)
                      gcc)
         (dimb-fundef fundef table gcc)))

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 gcc)
                  (dimb-fundef fundef table-equiv gcc)))
  :rule-classes :congruence)

Theorem: dimb-fundef-of-bool-fix-gcc

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

Theorem: dimb-fundef-iff-congruence-on-gcc

(defthm dimb-fundef-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dimb-fundef fundef table gcc)
                  (dimb-fundef fundef table gcc-equiv)))
  :rule-classes :congruence)