		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-pkg-method

Generate a Java method that adds an ACL2 package definition.

Signature
(atj-gen-pkg-method pkg verbose$) → method
Arguments: pkg — Guard (stringp pkg).; verbose$ — Guard (booleanp verbose$).
Returns: method — Type (jmethodp method).

This is a private static method that contains a sequence of statements to incrementally construct the Java list of symbols imported by the package. The sequence starts with a declaration of a local variable initialized with an empty Java list whose capacity is the length of the import list. After all the assignments, we generate a method call to add the ACL2 package definition with the calculated import list.

We set the deep$ and guards$ flag to t and nil when we call atj-gen-symbol, so that we generate Acl2Symbols for ACL2 booleans.

Definitions and Theorems

Function: atj-gen-pkg-method-aux

(defun atj-gen-pkg-method-aux (imports jvar-imports)
 (declare (xargs :guard (and (symbol-listp imports)
                             (stringp jvar-imports))))
 (let ((__function__ 'atj-gen-pkg-method-aux))
  (declare (ignorable __function__))
  (cond
   ((endp imports) nil)
   (t
     (b* ((import-expr (atj-gen-symbol (car imports) t nil))
          (first-block (jblock-method (str::cat jvar-imports ".add")
                                      (list import-expr)))
          (rest-block (atj-gen-pkg-method-aux (cdr imports)
                                              jvar-imports)))
       (append first-block rest-block))))))

Theorem: jblockp-of-atj-gen-pkg-method-aux

(defthm jblockp-of-atj-gen-pkg-method-aux
  (b* ((block (atj-gen-pkg-method-aux imports jvar-imports)))
    (jblockp block))
  :rule-classes :rewrite)

Function: atj-gen-pkg-method

(defun atj-gen-pkg-method (pkg verbose$)
 (declare (xargs :guard (and (stringp pkg)
                             (booleanp verbose$))))
 (let ((__function__ 'atj-gen-pkg-method))
  (declare (ignorable __function__))
  (b*
   (((run-when verbose$) (cw "  ~s0~%" pkg))
    (jvar-imports "imports")
    (method-name (atj-gen-pkg-method-name pkg))
    (imports (pkg-imports pkg))
    (len-expr (jexpr-lit-int-dec-nouscores (len imports)))
    (newlist-expr (jexpr-newclass (jtype-class "ArrayList<>")
                                  (list len-expr)))
    (imports-block (jblock-locvar (jtype-class "List<Acl2Symbol>")
                                  jvar-imports newlist-expr))
    (imports-block
         (append imports-block
                 (atj-gen-pkg-method-aux imports jvar-imports)))
    (pkg-name-expr (atj-gen-pkg-name pkg))
    (defpkg-block (jblock-smethod *aij-type-pkg* "define"
                                  (list pkg-name-expr
                                        (jexpr-name jvar-imports))))
    (method-body (append imports-block defpkg-block)))
   (make-jmethod :access (jaccess-private)
                 :abstract? nil
                 :static? t
                 :final? nil
                 :synchronized? nil
                 :native? nil
                 :strictfp? nil
                 :result (jresult-void)
                 :name method-name
                 :params nil
                 :throws nil
                 :body method-body))))

Theorem: jmethodp-of-atj-gen-pkg-method

(defthm jmethodp-of-atj-gen-pkg-method
  (b* ((method (atj-gen-pkg-method pkg verbose$)))
    (jmethodp method))
  :rule-classes :rewrite)