Generate all the overloaded Java methods for an ACL2 function definition.
(atj-gen-shallow-fndef-all-methods fn 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)
See atj-gen-shallow-fndef-method first. Here we calculate, once, the data to pass to that function (via atj-gen-shallow-fndef-methods).
We retrieve all the primary and secondary function types of
Function:
(defun atj-gen-shallow-fndef-all-methods (fn fns-that-may-throw qconsts pkg-class-names fn-method-names mv-typess guards$ no-aij-types$ verbose$ wrld) (declare (xargs :guard (and (symbolp fn) (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 (and (not (aij-nativep fn)) (cons-listp mv-typess)))) (let ((__function__ 'atj-gen-shallow-fndef-all-methods)) (declare (ignorable __function__)) (b* ((curr-pkg (symbol-package-name fn)) (formals (formals+ fn wrld)) (body (atj-fn-body fn wrld)) ((run-when (null body)) (raise "Internal error: ~ the function ~x0 has no unnormalized body." fn)) (fn-info (atj-get-function-type-info fn guards$ wrld)) (main-fn-type (atj-function-type-info->main fn-info)) (other-fn-types (atj-function-type-info->others fn-info)) (all-fn-types (cons main-fn-type other-fn-types)) (method-name (atj-gen-shallow-fnname fn pkg-class-names fn-method-names curr-pkg)) ((run-when verbose$) (cw " ~s0 for ~x1~%" method-name fn))) (atj-gen-shallow-fndef-methods fn fns-that-may-throw all-fn-types formals body method-name qconsts pkg-class-names fn-method-names curr-pkg mv-typess guards$ no-aij-types$ wrld))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-fndef-all-methods.methods (b* (((mv ?methods ?new-qconsts ?new-mv-typess) (atj-gen-shallow-fndef-all-methods fn 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-fndef-all-methods.new-qconsts (implies (atj-qconstants-p qconsts) (b* (((mv ?methods ?new-qconsts ?new-mv-typess) (atj-gen-shallow-fndef-all-methods fn 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-fndef-all-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-fndef-all-methods fn 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)