		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).

General Form:

(wrap-output fn
             wrapper
             &key
             :new-name          ; default :auto
             :guard             ; default :auto
             :guard-hints       ; default :auto
             :theorem-disabled  ; default nil
             :function-disabled ; default :auto
             :verify-guards     ; default :auto
             :show-only         ; default nil
             :print             ; default :result
             )

Inputs:

fn — (required)

The function to transform.

wrapper — (required)

A unary function or a unary lambda (in which case any free variables in the lambda body become arguments of the new function).

:new-name — default :auto

New name to use for the function (if :auto, the transformation generates a name)

:guard — default :auto

Guard for the generated function

:guard-hints — default :auto

Hints for the guard proof

:theorem-disabled — default nil

Whether to disable the theorem(s) that replace the old function with the new

:function-disabled — default :auto

Whether to disable the new function. In a mutual-recursion nest this applies to all functions.

:verify-guards — default :auto

Whether to verify guards for the new function(s).

:show-only — default nil

Whether to simply show the result, without actually creating it.

:print — default :result

How much detail to print, an apt::print-specifier.

Description:

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).

If FN is defined in a mutual-recursion, then the :new-name and :guard options support :map syntax (see the Special Note in the documentation for apt::simplify-defun) such as (:map (name-1 val-1) ... (name-k val-k)).