		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-new-fn-body-nonpred

Generate the body of the new function, when :predicate is nil.

Signature
(expdata-gen-new-fn-body-nonpred old$ arg-surjmaps res-surjmaps new$ wrld) → new-body
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; new$ — Guard (symbolp new$).; wrld — Guard (plist-worldp wrld).
Returns: new-body — A pseudo-termp.

If old is non-executable, its body is obtained by removing the ``non-executable wrapper''.

First we transform any recursive calls via expdata-xform-rec-calls, which causes no change if old is not recursive, and then we replace x1, ..., xn with (back1 x1), ..., (backn xn); the resulting term is the code of the new function's body (see below). Then we construct an if as follows. The test is the conjunction of (newp1 x1), ..., (newpn xn). The `else' branch is nil or (mv nil ... nil), depending on whether old returns single or multiple results. For the `then' branch, there are three cases: (i) if no results are transformed, we use the core term above; (ii) if old is single-valued and its (only) result is transformed, we apply the back mapping of the result to the core term above; and (iii) if old is multi-valued and some results are transformed, we bind the core term above to an mv-let and we apply the back mappings of the results to the bound variables. The if is the final result, unless its test is just t, in which case we omit test and `else' branch.

The `else' branch should use quoted nils, but we use unquoted ones just so that the untranslation does not turn the if into an and. Technically, the unquoted nils are ``variable'' (symbols), and thus untranslation leaves them alone.

Definitions and Theorems

Function: expdata-gen-new-fn-body-nonpred

(defun expdata-gen-new-fn-body-nonpred
       (old$ arg-surjmaps res-surjmaps new$ wrld)
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (symbolp new$)
                        (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-new-fn-body-nonpred))
  (declare (ignorable __function__))
  (b*
   ((x1...xn (formals old$ wrld))
    (m (number-of-results old$ wrld))
    (old-body (if (non-executablep old$ wrld)
                  (unwrapped-nonexec-body old$ wrld)
                (ubody old$ wrld)))
    (old-body-with-new-rec-calls
      (expdata-xform-rec-calls old-body
                               old$ arg-surjmaps res-surjmaps new$))
    (old-body-with-back-of-x1...xn (expdata-gen-subst-x1...xn-with-back-of-x1...xn
                                        old-body-with-new-rec-calls
                                        old$ arg-surjmaps wrld))
    (newp-of-x1...xn
         (expdata-gen-newp-of-terms x1...xn arg-surjmaps))
    (newp-of-x1...xn-conj (conjoin newp-of-x1...xn))
    (then-branch
     (cond
      ((endp res-surjmaps)
       old-body-with-back-of-x1...xn)
      ((endp (cdr res-surjmaps))
       (apply-fn-into-ifs
            (expdata-surjmap->forth (cdar res-surjmaps))
            old-body-with-back-of-x1...xn))
      (t
       (b* ((y1...ym (expdata-gen-result-vars old$ m))
            (forth-of-y1...ym
                 (expdata-gen-forth-of-terms y1...ym res-surjmaps)))
         (make-mv-let-call 'mv
                           y1...ym
                           :all old-body-with-back-of-x1...xn
                           (fcons-term 'mv forth-of-y1...ym))))))
    (else-branch (if (> m 1)
                     (fcons-term 'mv (repeat m nil))
                   nil)))
   (cond ((not (recursivep old$ nil wrld))
          then-branch)
         ((equal newp-of-x1...xn-conj *t*)
          then-branch)
         (t (cons 'if
                  (cons (cons 'mbt$
                              (cons newp-of-x1...xn-conj 'nil))
                        (cons then-branch
                              (cons else-branch 'nil)))))))))