		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-ext-declon-list

Check a list of external declarations.

Signature
(check-ext-declon-list exts funtab vartab tagenv) → new-funtab+vartab+tagenv
Arguments: exts — Guard (ext-declon-listp exts).; 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).

We thread through the function table, variable table, and tag environment.

Definitions and Theorems

Function: check-ext-declon-list

(defun check-ext-declon-list (exts funtab vartab tagenv)
  (declare (xargs :guard (and (ext-declon-listp exts)
                              (fun-tablep funtab)
                              (var-tablep vartab)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-ext-declon-list))
    (declare (ignorable __function__))
    (b* (((when (endp exts))
          (make-funtab+vartab+tagenv :funs (fun-table-fix funtab)
                                     :vars (var-table-fix vartab)
                                     :tags (tag-env-fix tagenv)))
         ((okf funtab+vartab+tagenv)
          (check-ext-declon (car exts)
                            funtab vartab tagenv)))
      (check-ext-declon-list
           (cdr exts)
           (funtab+vartab+tagenv->funs funtab+vartab+tagenv)
           (funtab+vartab+tagenv->vars funtab+vartab+tagenv)
           (funtab+vartab+tagenv->tags funtab+vartab+tagenv)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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