Retrieve the Java method name for an ACL2 function name from the mapping, ensuring that the name is present.
(atj-get-fn-method-name fn fn-method-names) → method
This function causes an error if the function name is not in the alist, but it should always be called with arguments that do not result in the error. In other words, the error is never expected to actually happen.
Function:
(defun atj-get-fn-method-name (fn fn-method-names) (declare (xargs :guard (and (symbolp fn) (symbol-string-alistp fn-method-names)))) (let ((__function__ 'atj-get-fn-method-name)) (declare (ignorable __function__)) (b* ((pair (assoc-equal fn fn-method-names)) ((unless (consp pair)) (raise "Internal error: no method name for function ~x0." fn) "")) (cdr pair))))
Theorem:
(defthm stringp-of-atj-get-fn-method-name (implies (symbol-string-alistp fn-method-names) (b* ((method (atj-get-fn-method-name fn fn-method-names))) (stringp method))) :rule-classes :rewrite)