		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-fun-declor

Check a function declarator.

Signature
(check-fun-declor declor vartab tagenv) → vartab
Arguments: declor — Guard (fun-declorp declor).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: vartab — Type (var-table-resultp vartab).

We go through all the pointers, if any. We check the identifier and the list of parameter declarations. We add a new block scope to the variable table, for the block associated to the function definition of which this declarator is part; in fact, this is also adequate for checking a function declarator that is part of a function declaration that is not a function definition, as in that case we just need to ensure that the parameters are distinct. We check the parameters starting with this variable table, which (if successful) produces a variable table that includes the parameters; this table is used when checking the function definition.

Definitions and Theorems

Function: check-fun-declor

(defun check-fun-declor (declor vartab tagenv)
  (declare (xargs :guard (and (fun-declorp declor)
                              (var-tablep vartab)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-fun-declor))
    (declare (ignorable __function__))
    (fun-declor-case
         declor :base
         (b* (((okf &) (check-ident declor.name))
              (vartab (var-table-add-block vartab)))
           (check-param-declon-list declor.params vartab tagenv))
         :pointer (check-fun-declor declor.decl vartab tagenv))))

Theorem: var-table-resultp-of-check-fun-declor

(defthm var-table-resultp-of-check-fun-declor
  (b* ((vartab (check-fun-declor declor vartab tagenv)))
    (var-table-resultp vartab))
  :rule-classes :rewrite)

Theorem: check-fun-declor-of-fun-declor-fix-declor

(defthm check-fun-declor-of-fun-declor-fix-declor
  (equal (check-fun-declor (fun-declor-fix declor)
                           vartab tagenv)
         (check-fun-declor declor vartab tagenv)))

Theorem: check-fun-declor-fun-declor-equiv-congruence-on-declor

(defthm check-fun-declor-fun-declor-equiv-congruence-on-declor
  (implies (fun-declor-equiv declor declor-equiv)
           (equal (check-fun-declor declor vartab tagenv)
                  (check-fun-declor declor-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-fun-declor-of-var-table-fix-vartab

(defthm check-fun-declor-of-var-table-fix-vartab
  (equal (check-fun-declor declor (var-table-fix vartab)
                           tagenv)
         (check-fun-declor declor vartab tagenv)))

Theorem: check-fun-declor-var-table-equiv-congruence-on-vartab

(defthm check-fun-declor-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-fun-declor declor vartab tagenv)
                  (check-fun-declor declor vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-fun-declor-of-tag-env-fix-tagenv

(defthm check-fun-declor-of-tag-env-fix-tagenv
  (equal (check-fun-declor declor vartab (tag-env-fix tagenv))
         (check-fun-declor declor vartab tagenv)))

Theorem: check-fun-declor-tag-env-equiv-congruence-on-tagenv

(defthm check-fun-declor-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-fun-declor declor vartab tagenv)
                  (check-fun-declor declor vartab tagenv-equiv)))
  :rule-classes :congruence)