Generate a shallowly embedded ACL2 function name.
(atj-gen-shallow-fnname fn pkg-class-names fn-method-names curr-pkg) → 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
The Java class name
Function:
(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:
(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)