		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-wrapper-fn

Generate the wrapper function definition.

Signature
(tailrec-gen-wrapper-fn old$ test base nonrec updates a variant$ new-name$ wrapper-name$ wrapper-enable$ verify-guards$ appcond-thm-names domain-of-ground-base-name base-guard-name new-formals wrld) → (mv local-event exported-event)
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$).; wrapper-name$ — Guard (symbolp wrapper-name$).; wrapper-enable$ — Guard (booleanp wrapper-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; domain-of-ground-base-name — Guard (symbolp domain-of-ground-base-name).; base-guard-name — Guard (symbolp base-guard-name).; new-formals — Guard (symbol-listp new-formals).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

The macro used to introduce the new function is determined by whether the new function must be enabled or not. We always make it executable, since there seems to be no reason not to.

The wrapper function has the same formal arguments as the old function.

The body of the wrapper function is the rephrasing of the old function in terms of the new function.

The guard of the wrapper function is the same as the old function.

The guard hints are based on the proofs in the design notes. Since the base term is always ground, the proof for the case in which left identity holds (i.e. when the variant is :monoid or :monoid-alt) follows the proof for the special case of a ground base term.

This function is called only if the :wrapper input is t.

Definitions and Theorems

Function: tailrec-gen-wrapper-fn

(defun tailrec-gen-wrapper-fn
       (old$ test base nonrec updates a variant$
             new-name$ wrapper-name$ wrapper-enable$
             verify-guards$ appcond-thm-names
             domain-of-ground-base-name
             base-guard-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$)
                         (symbolp wrapper-name$)
                         (booleanp wrapper-enable$)
                         (booleanp verify-guards$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp domain-of-ground-base-name)
                         (symbolp base-guard-name)
                         (symbol-listp new-formals)
                         (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-wrapper-fn))
  (declare (ignorable __function__))
  (b*
   ((formals (formals old$ wrld))
    (body (tailrec-gen-old-as-new-term
               old$ test base nonrec updates
               a variant$ new-name$ new-formals wrld))
    (guard (untranslate (guard old$ nil wrld)
                        t wrld))
    (guard-hints
     (case variant$
      ((:monoid :monoid-alt)
       (cons
        (cons
         '"Goal"
         (cons
          ':in-theory
          (cons
           'nil
           (cons ':use
                 (cons (cons (cons ':guard-theorem (cons old$ 'nil))
                             (cons domain-of-ground-base-name
                                   (cons base-guard-name 'nil)))
                       'nil)))))
        'nil))
      (:assoc
       (b*
        ((domain-of-nonrec-thm
              (cdr (assoc-eq :domain-of-nonrec appcond-thm-names))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
                 ':use
                 (cons (cons (cons ':guard-theorem (cons old$ 'nil))
                             (cons domain-of-nonrec-thm 'nil))
                       'nil)))))
         'nil)))
      (:assoc-alt
       (b*
        ((domain-of-nonrec-when-guard-thm
          (cdr
             (assoc-eq
                  :domain-of-nonrec-when-guard appcond-thm-names))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':use
             (cons
                  (cons (cons ':guard-theorem (cons old$ 'nil))
                        (cons domain-of-nonrec-when-guard-thm 'nil))
                  'nil)))))
         'nil)))
      (t (impossible)))))
   (evmac-generate-defun wrapper-name$
                         :formals formals
                         :guard guard
                         :body body
                         :verify-guards verify-guards$
                         :guard-hints guard-hints
                         :guard-simplify :limited
                         :enable wrapper-enable$))))