		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-fnname

Generate a shallowly embedded ACL2 function name.

Signature
(atj-gen-shallow-fnname fn pkg-class-names fn-method-names curr-pkg) → method-name
Arguments: fn — Guard (symbolp fn).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; curr-pkg — Guard (stringp curr-pkg).
Returns: method-name — Type (stringp method-name).

In the shallow embedding approach, each ACL2 function is represented as a Java method. The Java methods for all the ACL2 functions that are translated to Java are partitioned by ACL2 packages: there is a Java class for each ACL2 package, and the Java method for each ACL2 function is in the Java class corresponding to the ACL2 package of the function.

These are all static methods, which can therefore be referenced as <class>.<method> in Java code, not dissimilarly to <pkg>::<fn> in ACL2. However, inside <class>, it suffices to use <method>, which is more readable. Furthermore, since we generate method synonyms under certain conditions, as explained in atj-gen-shallow-synonym-method, it suffices to use <method> if the function is imported by the package. Thus, we prepend the Java class name to the Java method name if and only if the current ACL2 package (the curr-pkg argument) differs from the ACL2 function's package and the package does not import the function.

The Java class name <class> is looked up in the alist pkg-class-names, and the Java method name <method> is looked up in the alist fn-method-names.

Definitions and Theorems

Function: atj-gen-shallow-fnname

(defun atj-gen-shallow-fnname (fn pkg-class-names
                                  fn-method-names curr-pkg)
 (declare (xargs :guard (and (symbolp fn)
                             (string-string-alistp pkg-class-names)
                             (symbol-string-alistp fn-method-names)
                             (stringp curr-pkg))))
 (declare (xargs :guard (not (equal curr-pkg ""))))
 (let ((__function__ 'atj-gen-shallow-fnname))
  (declare (ignorable __function__))
  (b*
   ((pkg (symbol-package-name fn))
    (class?
        (if (or (equal pkg curr-pkg)
                (member-eq fn (pkg-imports curr-pkg)))
            ""
          (b* ((class (atj-get-pkg-class-name pkg pkg-class-names)))
            (str::cat class "."))))
    (method (atj-get-fn-method-name fn fn-method-names)))
   (str::cat class? method))))

Theorem: stringp-of-atj-gen-shallow-fnname

(defthm stringp-of-atj-gen-shallow-fnname
  (b*
   ((method-name (atj-gen-shallow-fnname fn pkg-class-names
                                         fn-method-names curr-pkg)))
   (stringp method-name))
  :rule-classes :rewrite)