Generate all the methods of the classes for all the ACL2 packages.
(atj-gen-shallow-all-pkg-methods pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld) → (mv methods-by-pkg new-qconsts new-mv-typess)
We go through all the packages in
Function:
(defun atj-gen-shallow-all-pkg-methods (pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld) (declare (xargs :guard (and (string-listp pkgs) (string-symbollist-alistp fns-by-pkg) (symbol-listp fns) (symbol-listp fns-that-may-throw) (atj-qconstants-p qconsts) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (atj-type-list-listp mv-typess) (booleanp guards$) (booleanp no-aij-types$) (booleanp verbose$) (plist-worldp wrld)))) (declare (xargs :guard (cons-listp mv-typess))) (let ((__function__ 'atj-gen-shallow-all-pkg-methods)) (declare (ignorable __function__)) (b* (((when (endp pkgs)) (mv nil qconsts mv-typess)) (pkg (car pkgs)) ((mv first-methods qconsts mv-typess) (atj-gen-shallow-pkg-methods pkg fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld)) ((mv rest-methods qconsts mv-typess) (atj-gen-shallow-all-pkg-methods (cdr pkgs) fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld))) (if (null first-methods) (mv rest-methods qconsts mv-typess) (mv (acons pkg first-methods rest-methods) qconsts mv-typess)))))
Theorem:
(defthm string-jmethodlist-alistp-of-atj-gen-shallow-all-pkg-methods.methods-by-pkg (implies (string-listp pkgs) (b* (((mv ?methods-by-pkg ?new-qconsts ?new-mv-typess) (atj-gen-shallow-all-pkg-methods pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld))) (string-jmethodlist-alistp methods-by-pkg))) :rule-classes :rewrite)
Theorem:
(defthm atj-qconstants-p-of-atj-gen-shallow-all-pkg-methods.new-qconsts (implies (atj-qconstants-p qconsts) (b* (((mv ?methods-by-pkg ?new-qconsts ?new-mv-typess) (atj-gen-shallow-all-pkg-methods pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld))) (atj-qconstants-p new-qconsts))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-all-pkg-methods.new-mv-typess (implies (and (atj-type-list-listp mv-typess) (cons-listp mv-typess)) (b* (((mv ?methods-by-pkg ?new-qconsts ?new-mv-typess) (atj-gen-shallow-all-pkg-methods pkgs fns-by-pkg fns fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld))) (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)))) :rule-classes :rewrite)