		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation

Atj-post-translate-body

Post-translate a Java method body generated from an ACL2 function.

Signature
(atj-post-translate-body name params body tailrecp) → new-body
Arguments: name — Guard (stringp name).; params — Guard (jparam-listp params).; body — Guard (jblockp body).; tailrecp — Guard (booleanp tailrecp).
Returns: new-body — Type (jblockp new-body), given the guard.

We always fold returns into ifs.

If the method is tail-recursive, which is signaled by the tailrecp flag, then we replace the tail recursion with a loop. It is critical that this step is performed after folding returns into ifs, because tail recursion elimination looks for recursive calls in returns.

The other post-translation steps are always performed. These are the post-translation steps that operate at the level of individual method bodies.

Definitions and Theorems

Function: atj-post-translate-body

(defun atj-post-translate-body (name params body tailrecp)
  (declare (xargs :guard (and (stringp name)
                              (jparam-listp params)
                              (jblockp body)
                              (booleanp tailrecp))))
  (let ((__function__ 'atj-post-translate-body))
    (declare (ignorable __function__))
    (b* ((body (atj-fold-returns body))
         (body (if tailrecp (atj-elim-tailrec name params body)
                 body))
         (body (atj-lift-loop-test body))
         (body (atj-remove-continue-in-jblock body))
         (body (atj-remove-array-write-calls body))
         (body (atj-simplify-conds-in-jblock body)))
      body)))

Theorem: jblockp-of-atj-post-translate-body

(defthm jblockp-of-atj-post-translate-body
 (implies
   (and (stringp name)
        (jparam-listp params)
        (jblockp body)
        (booleanp tailrecp))
   (b*
    ((new-body (atj-post-translate-body name params body tailrecp)))
    (jblockp new-body)))
 :rule-classes :rewrite)