		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-pkg-name

Generate Java code to build an ACL2 package name.

Signature
(atj-gen-pkg-name pkg) → expr
Arguments: pkg — Guard (stringp pkg).
Returns: expr — Type (jexprp expr).

Since AIJ has a number of constants (i.e. static final fields) for a number of common ACL2 package names, we just reference the appropriate constant if the package name in question is among those. Otherwise, we build it in the general way; note that ACL2 package names can always be safely generated as Java string literals. Using the constants when possible makes the generated Java code faster. We introduce and use an alist to specify the correspondence between ACL2 package symbols and AIJ static final fields.

Definitions and Theorems

Function: atj-gen-pkg-name

(defun atj-gen-pkg-name (pkg)
  (declare (xargs :guard (stringp pkg)))
  (let ((__function__ 'atj-gen-pkg-name))
    (declare (ignorable __function__))
    (b* ((pair (assoc-equal pkg *atj-gen-pkg-name-alist*)))
      (if pair (jexpr-name (cdr pair))
        (jexpr-smethod *aij-type-pkg-name*
                       "make" (list (atj-gen-jstring pkg)))))))

Theorem: jexprp-of-atj-gen-pkg-name

(defthm jexprp-of-atj-gen-pkg-name
  (b* ((expr (atj-gen-pkg-name pkg)))
    (jexprp expr))
  :rule-classes :rewrite)