		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-pkg-methods

Generate all the methods of the class for an ACL2 package.

Signature
(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)
Arguments: pkg — Guard (stringp pkg).; fns-by-pkg — Guard (string-symbollist-alistp fns-by-pkg).; fns — Guard (symbol-listp fns).; fns-that-may-throw — Guard (symbol-listp fns-that-may-throw).; qconsts — Guard (atj-qconstants-p qconsts).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; mv-typess — Guard (atj-type-list-listp mv-typess).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: methods — Type (jmethod-listp methods).; new-qconsts — Type (atj-qconstants-p new-qconsts), given (atj-qconstants-p qconsts).; new-mv-typess — Type (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess)), given (and (atj-type-list-listp mv-typess) (cons-listp mv-typess)).

We generate methods for the functions in fns-by-pkg (i.e. the functions to translate to Java, organized by package) that are associated to pkg.

We also generate synonym methods for all the functions in fns (i.e. the functions to translate to Java) that are in other ACL2 packages but that are imported by pkg; see atj-gen-shallow-synonym-method for motivation. However, if fns-by-pkg has no functions associated to pkg, then we skip these synonym methods, because they are not needed by any other code in the class for pkg; in fact, unless the class has fields for symbols, we do not generate the class (see atj-gen-shallow-pkg-classes).

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 pkg that are translated to Java.

Definitions and Theorems

Function: atj-gen-shallow-pkg-methods

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

(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: atj-qconstants-p-of-atj-gen-shallow-pkg-methods.new-qconsts

(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: return-type-of-atj-gen-shallow-pkg-methods.new-mv-typess

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