		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-fn-to-method

Turn an ACL2 function symbol into a Java method name.

Signature
(atj-fn-to-method fn) → method
Arguments: fn — Guard (symbolp fn).
Returns: method — Type (stringp method).

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.

The name of the Java method is obtained by turning the ACL2 function name into a valid Java identifier, via atj-chars-to-jchars-id. The resulting name must not be in *atj-disallowed-method-names*; if it is, we add a $ at the end, which makes the name allowed. However, if the function is a key in *atj-predefined-method-names*, we directly use the associated name instead. To avoid conflicts with these predefined names, we add a $ at the end of every method name that happens to be one of the predefined ones (where the function is not the primitive one associated to that name.

The generation of the method name does not consider the package name of the function: the package name is used, instead, to generate the name of the Java class that contains the method; see atj-pkg-to-class.

Definitions and Theorems

Function: atj-fn-to-method

(defun atj-fn-to-method (fn)
 (declare (xargs :guard (symbolp fn)))
 (let ((__function__ 'atj-fn-to-method))
  (declare (ignorable __function__))
  (b*
   ((predef? (assoc-eq fn *atj-predefined-method-names*))
    ((when (consp predef?)) (cdr predef?))
    (jchars (atj-chars-to-jchars-id (explode (symbol-name fn))
                                    t
                                    :dash t))
    (jstring (implode jchars))
    (jstring
     (if
      (or (member-equal jstring *atj-disallowed-method-names*)
          (member-equal jstring
                        (strip-cdrs *atj-predefined-method-names*)))
      (str::cat jstring "$")
      jstring)))
   jstring)))

Theorem: stringp-of-atj-fn-to-method

(defthm stringp-of-atj-fn-to-method
  (b* ((method (atj-fn-to-method fn)))
    (stringp method))
  :rule-classes :rewrite)