Push an external computation into a function (by pushing it through the top-level if-branches of the function).
(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 )
The function to transform.
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 to use for the function (if :auto, the transformation generates a name)
Guard for the generated function
Hints for the guard proof
Whether to disable the theorem(s) that replace the old function with the new
Whether to disable the new function. In a mutual-recursion nest this applies to all functions.
Whether to verify guards for the new function(s).
Whether to simply show the result, without actually creating it.
How much detail to print, an apt::print-specifier.
Given a function
If the branch contains no recursive call then
If a top-level term is a lambda then the body of the lambda is treated as a branch unless free variables in
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)))
(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)))) ;; lambdathen if
(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 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)).