		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-fun-declon

Check a function declaration.

Signature
(check-fun-declon declon funtab vartab tagenv) → new-funtab
Arguments: declon — Guard (fun-declonp declon).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: new-funtab — Type (fun-table-resultp new-funtab).

We check the type specifier sequence and the declarator. We extend the function table with information about the new function.

We adjust the parameter types [C:6.7.6.3/7].

Definitions and Theorems

Function: check-fun-declon

(defun check-fun-declon (declon funtab vartab tagenv)
  (declare (xargs :guard (and (fun-declonp declon)
                              (fun-tablep funtab)
                              (var-tablep vartab)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-fun-declon))
    (declare (ignorable __function__))
    (b* (((fun-declon declon) declon)
         ((mv name params out-tyname)
          (tyspec+declor-to-ident+params+tyname
               declon.tyspec declon.declor))
         ((okf out-type)
          (check-tyname out-tyname tagenv))
         ((okf &)
          (check-fun-declor declon.declor vartab tagenv))
         ((mv & in-tynames)
          (param-declon-list-to-ident+tyname-lists params))
         (in-types (type-name-list-to-type-list in-tynames))
         (in-types (adjust-type-list in-types)))
      (fun-table-add-fun name in-types out-type nil funtab))))

Theorem: fun-table-resultp-of-check-fun-declon

(defthm fun-table-resultp-of-check-fun-declon
  (b* ((new-funtab (check-fun-declon declon funtab vartab tagenv)))
    (fun-table-resultp new-funtab))
  :rule-classes :rewrite)

Theorem: check-fun-declon-of-fun-declon-fix-declon

(defthm check-fun-declon-of-fun-declon-fix-declon
  (equal (check-fun-declon (fun-declon-fix declon)
                           funtab vartab tagenv)
         (check-fun-declon declon funtab vartab tagenv)))

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

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

Theorem: check-fun-declon-of-fun-table-fix-funtab

(defthm check-fun-declon-of-fun-table-fix-funtab
  (equal (check-fun-declon declon (fun-table-fix funtab)
                           vartab tagenv)
         (check-fun-declon declon funtab vartab tagenv)))

Theorem: check-fun-declon-fun-table-equiv-congruence-on-funtab

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

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

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

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

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

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

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

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

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