Generate all the methods of the class for an ACL2 package.
(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 methods new-qconsts new-mv-typess)
We generate methods for the functions in
We also generate synonym methods for all the functions in
Recall that, for each ACL2 function or function synonym, we generate one overloaded method for each primary or secondary type of the function.
We sort all the methods.
We also collect all the quoted constants
that occur in the functions in
Function:
(defun 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) (declare (xargs :guard (and (stringp pkg) (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-pkg-methods)) (declare (ignorable __function__)) (b* ((fns-in-pkg (cdr (assoc-equal pkg fns-by-pkg))) ((run-when (and verbose$ (consp fns-in-pkg))) (cw "~%Generate the Java methods ~ for the ACL2 functions in package ~s0:~%" pkg)) ((mv fn-methods qconsts mv-typess) (atj-gen-shallow-all-fn-methods fns-in-pkg fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld)) (synonym-methods (and (consp fns-in-pkg) (b* ((imported-fns (intersection-eq fns (pkg-imports pkg))) (imported-fns (sort-symbol-listp imported-fns))) (atj-gen-shallow-all-synonym-methods imported-fns fns-that-may-throw pkg-class-names fn-method-names guards$ wrld)))) (all-methods (append synonym-methods fn-methods))) (mv (mergesort-jmethods all-methods) qconsts mv-typess))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-pkg-methods.methods (b* (((mv ?methods ?new-qconsts ?new-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))) (jmethod-listp methods)) :rule-classes :rewrite)
Theorem:
(defthm atj-qconstants-p-of-atj-gen-shallow-pkg-methods.new-qconsts (implies (atj-qconstants-p qconsts) (b* (((mv ?methods ?new-qconsts ?new-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))) (atj-qconstants-p new-qconsts))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-gen-shallow-pkg-methods.new-mv-typess (implies (and (atj-type-list-listp mv-typess) (cons-listp mv-typess)) (b* (((mv ?methods ?new-qconsts ?new-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))) (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)))) :rule-classes :rewrite)