		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-ext-declon

Check an external declaration.

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

For object declarations, we require the initializer to be constant if present [C:6.7.9/4], without requiring it to be present.

If successful, we return updated function table, variable table, and tag environment.

For now we reject function declarations. We plan to add support soon.

Definitions and Theorems

Function: check-ext-declon

(defun check-ext-declon (ext funtab vartab tagenv)
 (declare (xargs :guard (and (ext-declonp ext)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-ext-declon))
  (declare (ignorable __function__))
  (ext-declon-case
       ext :fundef
       (b* (((okf funtab)
             (check-fundef ext.get funtab vartab tagenv)))
         (make-funtab+vartab+tagenv :funs funtab
                                    :vars (var-table-fix vartab)
                                    :tags (tag-env-fix tagenv)))
       :fun-declon
       (b* (((okf funtab)
             (check-fun-declon ext.get funtab vartab tagenv)))
         (make-funtab+vartab+tagenv :funs funtab
                                    :vars (var-table-fix vartab)
                                    :tags (tag-env-fix tagenv)))
       :obj-declon
       (b* (((okf vartab)
             (check-obj-declon ext.get funtab vartab tagenv t nil)))
         (make-funtab+vartab+tagenv :funs (fun-table-fix funtab)
                                    :vars vartab
                                    :tags (tag-env-fix tagenv)))
       :tag-declon
       (b* (((okf tagenv)
             (check-tag-declon ext.get tagenv)))
         (make-funtab+vartab+tagenv :funs (fun-table-fix funtab)
                                    :vars (var-table-fix vartab)
                                    :tags tagenv)))))

Theorem: funtab+vartab+tagenv-resultp-of-check-ext-declon

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

Theorem: check-ext-declon-of-ext-declon-fix-ext

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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