Push an external computation into a function (by pushing it through the top-level if-branches of the function).
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
(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.