		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-old-as-new-term

Generate the term that rephrases (a generic call to) the old function in terms of the new function.

Signature
(tailrec-gen-old-as-new-term old$ test base nonrec updates a variant$ new-name$ new-formals wrld) → term
Arguments: old$ — Guard (symbolp old$).; test — Guard (pseudo-termp test).; base — Guard (pseudo-termp base).; nonrec — Guard (pseudo-termp nonrec).; updates — Guard (pseudo-term-listp updates).; a — Guard (symbolp a).; variant$ — Guard (tailrec-variantp variant$).; new-name$ — Guard (symbolp new-name$).; new-formals — Guard (symbol-listp new-formals).; wrld — Guard (plist-worldp wrld).
Returns: term — An untranslated term.

This is the right-hand side of the theorem that relates the old function to the new function (f{}f' in the design notes), and it is also the body of the wrapper function.

This is as described in the documentation and design notes. It varies slightly, depending on the transformation's variant. As explained in the documentation, for now it uses base<x1,...,xn> instead of the \beta function.

Definitions and Theorems

Function: tailrec-gen-old-as-new-term

(defun tailrec-gen-old-as-new-term
       (old$ test base nonrec updates
             a variant$ new-name$ new-formals wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp test)
                             (pseudo-termp base)
                             (pseudo-termp nonrec)
                             (pseudo-term-listp updates)
                             (symbolp a)
                             (tailrec-variantp variant$)
                             (symbolp new-name$)
                             (symbol-listp new-formals)
                             (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-old-as-new-term))
  (declare (ignorable __function__))
  (untranslate
   (case variant$
    ((:assoc :assoc-alt)
     (cons
      'if
      (cons
         test
         (cons base
               (cons (subcor-var (cons a (formals old$ wrld))
                                 (cons nonrec updates)
                                 (apply-term new-name$ new-formals))
                     'nil)))))
    ((:monoid :monoid-alt)
     (subst-var base
                a (apply-term new-name$ new-formals)))
    (t (impossible)))
   nil wrld)))