Generate all the overloaded Java methods for an ACL2 function that is natively implemented in AIJ.
(atj-gen-shallow-fnnative-all-methods fn fns-that-may-throw pkg-class-names fn-method-names guards$ verbose$ wrld) → methods
See atj-gen-shallow-fnnative-method first. Here we calculate, once, the data to pass to that function (via atj-gen-shallow-fnnative-methods).
We retrieve all the primary and secondary function types of
Function:
(defun atj-gen-shallow-fnnative-all-methods (fn fns-that-may-throw pkg-class-names fn-method-names guards$ verbose$ wrld) (declare (xargs :guard (and (symbolp fn) (symbol-listp fns-that-may-throw) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (booleanp guards$) (booleanp verbose$) (plist-worldp wrld)))) (declare (xargs :guard (aij-nativep fn))) (let ((__function__ 'atj-gen-shallow-fnnative-all-methods)) (declare (ignorable __function__)) (b* ((curr-pkg (symbol-package-name fn)) (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)) (method-param-names (case fn (hard-error (list "ctx" "str" "alist")) (intern-in-package-of-symbol (list "str" "sym")) (char (list "s" "n")) (if (list "x" "y" "z")) ((pkg-imports pkg-witness) (list "pkg")) ((coerce binary-+ binary-* < complex cons equal bad-atom<=) (list "x" "y")) (nonnegative-integer-quotient (list "i" "j")) (string-append (list "str1" "str2")) (t (list "x")))) (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)) (jcall-method-name (atj-fnnative-method-name fn guards$)) (jcall-arg-exprs (jexpr-name-list method-param-names)) (jcall (jexpr-smethod *aij-type-native-fn* jcall-method-name jcall-arg-exprs)) (method-body (jblock-return jcall))) (atj-gen-shallow-fnnative-methods fn fns-that-may-throw all-fn-types method-name method-param-names method-body))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-fnnative-all-methods (b* ((methods (atj-gen-shallow-fnnative-all-methods fn fns-that-may-throw pkg-class-names fn-method-names guards$ verbose$ wrld))) (jmethod-listp methods)) :rule-classes :rewrite)