		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-fnnative-all-methods

Generate all the overloaded Java methods for an ACL2 function that is natively implemented in AIJ.

Signature
(atj-gen-shallow-fnnative-all-methods fn fns-that-may-throw pkg-class-names fn-method-names guards$ verbose$ wrld) → methods
Arguments: fn — Guard (symbolp fn).; fns-that-may-throw — Guard (symbol-listp fns-that-may-throw).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; guards$ — Guard (booleanp guards$).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: methods — Type (jmethod-listp 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 fn, and generate an overloaded method for each. Note that if guards$ is nil, then the retrieved function types boil down to one that consists of all :value types.

Definitions and Theorems

Function: atj-gen-shallow-fnnative-all-methods

(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: jmethod-listp-of-atj-gen-shallow-fnnative-all-methods

(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)