		Search-engine friendly clone of the ACL2 documentation.

Wrap-output

Push an external computation into a function (by pushing it through the top-level if-branches of the function).

Given a function f and a (unary) wrapper function wrapper, the transformation acts on the top level if branches as follows:

If the branch contains no recursive call then wrapper is simply wrapped around the branch. Otherwise, if the branch contains a tail-recursive call then the recursive call is replaced by a recursive call of the transformed function f$1, and if the recursive call is not a tail call then wrapper is wrapped around the original call of f. In particular this means that the resulting function may no longer be recursive. The same rules apply if f lies in a mutual-recursion nest, so that the new functions may no longer be mutually recursive.

If a top-level term is a lambda then the body of the lambda is treated as a branch unless free variables in wrapper become bound in the body (TODO: treat this case).

Note furthermore that this transformation is applied to the untranslated (see trans) form of the body, so macros are not expanded. The only macros treated separately are and, or (TODO!), let, let*, b*, (TODO? mv-let) and cond.

The transformation produces the equivalence theorem

(defthm f-f$1-connection
    (equal (w (f arg-1 ... arg-n))
           (f$1 arg-1 ... arg-n free-1 ... free-k)))

where free-1, ..., free-k are free variables possibly introduced in wrapper if it is a lambda term.

Example Scenarios

Suppose foo is defined as follows

(defun foo (x)
     (cond ((<test-1>)
            (bar x))          ;; non-recursive
           ((<test-2>)
            (foo (bar x)))    ;; tail-recursive
           ((<test-3>)
            (bar (foo x)))    ;; recursive but not tail-recursive
           ((<test-4>)
            ((lambda (y) (foo y)) (foo x)))) ;; lambda

then if wrapper is a wrapper function then foo is transformed to the function

(defun foo$1 (x)
     (cond ((<test-1>)
            (wrapper (bar x)))
           ((<test-2>)
            (foo$1 (bar x)))
           ((<test-3>)
            (wrapper (bar (foo x))))
           ((<test-4>)
            ((lambda (y) (foo$1 y)) (foo x))))) ;; the argument is unchanged

If the term (lambda (x) (nth '2 x)) is wrapped around a function that returns (list x y z), then the new functions simply returns z. (This is useful for functions that axe has lifted).

Usage

(wrap-output fn                        ;; Function to refine
             wrapper                   ;; A unary function or unary lambda, where free variables are added as arguments
             [:theorem-disabled bool]  ;; Whether to disable the theorem(s) that replace the old function with the new, Default: nil
             [:function-disabled bool] ;; Whether to disable the new function, Default: nil
                                       ;; In a mutual-recursion nest this applies to all functions
             [:new-name map]           ;; New name to use for the function (if :auto, the transformation generates a name)
             [:guard map]              ;; Apply a guard to the generated function
             [:guard-hints hints]      ;; Hints for the guard proof, Default: nil
             [:show-only bool]         ;; Show event without execution
             [:print print-specifier]  ;; Specifies how output is printed (see @(see print-specifier))
             )
;; If a function is in a mutual-recursion nest then the parameters :new-name and :guard
;; can be applied separately through a list of doublets of the form
(:map (name-1 val-1) ... (name-k val-k))

TODO: Add check: For now, the wrapper should only be over one variable.