		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-fndef-method-name

Name of the Java method that builds a deeply embedded ACL2 function definition.

Signature
(atj-gen-deep-fndef-method-name fn) → method-name
Arguments: fn — Guard (symbolp fn).
Returns: method-name — Type (stringp method-name).

We generate a private static method for each deeply embedded ACL2 function definition to build. This function generates the name of this method, which is distinct from all the other methods generated for the same class.

Definitions and Theorems

Function: atj-gen-deep-fndef-method-name

(defun atj-gen-deep-fndef-method-name (fn)
 (declare (xargs :guard (symbolp fn)))
 (let ((__function__ 'atj-gen-deep-fndef-method-name))
  (declare (ignorable __function__))
  (str::cat
     "addFunctionDef_"
     (implode
          (atj-chars-to-jchars-id (explode (symbol-package-name fn))
                                  nil
                                  :dash nil))
     "$$$"
     (implode (atj-chars-to-jchars-id (explode (symbol-name fn))
                                      nil
                                      :dash t)))))

Theorem: stringp-of-atj-gen-deep-fndef-method-name

(defthm stringp-of-atj-gen-deep-fndef-method-name
  (b* ((method-name (atj-gen-deep-fndef-method-name fn)))
    (stringp method-name))
  :rule-classes :rewrite)