		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-fns-to-methods

Generate the mapping from ACL2 function symbols to Java method names.

Signature
(atj-fns-to-methods fns) → fn-method-names
Arguments: fns — Guard (symbol-listp fns).
Returns: fn-method-names — Type (symbol-string-alistp fn-method-names), given (symbol-listp fns).

We call atj-fn-to-method on all the argument function symbols, and generate an alist from those to the corresponding Java method names. This function is called on all the functions that must be translated to Java.

For now each function symbol is translated independently from the others, but future versions of this function could generate mappings according to more ``global'' strategies. In this case, this function could be split into one that generates an alist for all the functions (to be translated) in a package (as the method names need to be unambiguous only within a class), and one that puts all the alist together.

The resulting alist is passed to the code generation functions, which use the alist to look up the Java method names corresponding to the ACL2 function symbols.

Definitions and Theorems

Function: atj-fns-to-methods

(defun atj-fns-to-methods (fns)
  (declare (xargs :guard (symbol-listp fns)))
  (declare (xargs :guard (no-duplicatesp-equal fns)))
  (let ((__function__ 'atj-fns-to-methods))
    (declare (ignorable __function__))
    (b* (((when (endp fns)) nil)
         (fn (car fns))
         (method (atj-fn-to-method fn))
         (rest-alist (atj-fns-to-methods (cdr fns))))
      (acons fn method rest-alist))))

Theorem: symbol-string-alistp-of-atj-fns-to-methods

(defthm symbol-string-alistp-of-atj-fns-to-methods
  (implies (symbol-listp fns)
           (b* ((fn-method-names (atj-fns-to-methods fns)))
             (symbol-string-alistp fn-method-names)))
  :rule-classes :rewrite)