		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-cache-const-methods

Atj-cache-const-methods

Cache constant methods in static final fields, in a list of Java class body declarations.

Signature
(atj-cache-const-methods elems) → new-elems
Arguments: elems — Guard (jcbody-element-listp elems).
Returns: new-elems — Type (jcbody-element-listp new-elems).

We leave member fields, member classes, and static initializers unchanged. If a member method satisfies the conditions described in atj-post-translation-cache-const-methods, we replace it with a field and a modified method as also explained there. Otherwise, we leave the method unchanged.

Definitions and Theorems

Function: atj-cache-const-methods

(defun atj-cache-const-methods (elems)
 (declare (xargs :guard (jcbody-element-listp elems)))
 (let ((__function__ 'atj-cache-const-methods))
  (declare (ignorable __function__))
  (b* (((when (endp elems)) nil)
       (elem (car elems))
       ((when (jcbody-element-case elem :init))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (memb (jcbody-element-member->get elem))
       ((when (or (jcmember-case memb :field)
                  (jcmember-case memb :class)))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (meth (jcmember-method->get memb))
       ((when (consp (jmethod->params meth)))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (body (jmethod->body meth))
       ((unless (= (len body) 1))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (stmt (car body))
       ((unless (jstatem-case stmt :return))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (expr (jstatem-return->expr? stmt))
       ((unless expr)
        (raise "Internal error: method ~x0 returns nothing."
               meth))
       ((when (consp (jexpr-methods expr)))
        (cons (jcbody-element-fix elem)
              (atj-cache-const-methods (cdr elems))))
       (result (jmethod->result meth))
       ((when (jresult-case result :void))
        (raise "Internal error: method ~x0 returns void."
               meth))
       (type (jresult-type->get result))
       (name (jmethod->name meth))
       (fld (make-jfield :access (jaccess-private)
                         :static? t
                         :final? t
                         :transient? nil
                         :volatile? nil
                         :type type
                         :name name
                         :init? expr))
       (meth (change-jmethod
                  meth
                  :body (list (jstatem-return (jexpr-name name))))))
    (list* (jcbody-element-member (jcmember-field fld))
           (jcbody-element-member (jcmember-method meth))
           (atj-cache-const-methods (cdr elems))))))

Theorem: jcbody-element-listp-of-atj-cache-const-methods

(defthm jcbody-element-listp-of-atj-cache-const-methods
  (b* ((new-elems (atj-cache-const-methods elems)))
    (jcbody-element-listp new-elems))
  :rule-classes :rewrite)