Check a list of external declarations.
(check-ext-declon-list exts funtab vartab tagenv) → new-funtab+vartab+tagenv
We thread through the function table, variable table, and tag environment.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)