		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-new-fn

Generate the new function definition.

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

The macro used to introduce the new function is determined by whether the new function must be enabled or not, and non-executable or not. We make it non-executable if and only if old is non-executable.

The formals of the new function consist of the formals of the old function followed by the variable a generated during the decomposition of the recursive branch of the old function. This variable is distinct from the formals of the old function by construction. The formals of the new function are return as one of the results.

The body of the new function is as described in the documentation and design notes. The non-recursive branch varies slightly, depending on the transformation's variant.

The new function's well-founded relation and measure are the same as the old function's. Following the design notes, the termination of the new function is proved in the empty theory, using the termination theorem of the old function.

The guard of the new function is obtained by conjoining the guard of the old function with the fact that the additional formal a is in the domain, as described in the documentation.

The guards of the new function are verified following the proof in the design notes. The facts used in the proof for the case in which right identity holds are a subset of those for the case in which right identity does not hold. We use the hints for the latter case also for the former case (which will ignore some of the supplied facts).

Definitions and Theorems

Function: tailrec-gen-new-fn

(defun tailrec-gen-new-fn
       (old$ test base nonrec updates combine q
             r variant$ domain$ new-name$ new-enable$
             a verify-guards$ appcond-thm-names wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (pseudo-termp test)
                         (pseudo-termp base)
                         (pseudo-termp nonrec)
                         (pseudo-term-listp updates)
                         (pseudo-termp combine)
                         (symbolp q)
                         (symbolp r)
                         (tailrec-variantp variant$)
                         (pseudo-termfnp domain$)
                         (symbolp new-name$)
                         (booleanp new-enable$)
                         (symbolp a)
                         (booleanp verify-guards$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-new-fn))
  (declare (ignorable __function__))
  (b*
   ((macro (function-intro-macro new-enable$
                                 (non-executablep old$ wrld)))
    (new-formals (rcons a (formals old$ wrld)))
    (body
       (b* ((combine-op (tailrec-gen-combine-op combine q r))
            (nonrec-branch (case variant$
                             ((:monoid :monoid-alt) a)
                             ((:assoc :assoc-alt)
                              (apply-term* combine-op a base))
                             (t (impossible))))
            (rec-branch
                 (subcor-var (cons a (formals old$ wrld))
                             (cons (apply-term* combine-op a nonrec)
                                   updates)
                             (apply-term new-name$ new-formals)))
            (body (cons 'if
                        (cons test
                              (cons nonrec-branch
                                    (cons rec-branch 'nil))))))
         (untranslate body nil wrld)))
    (wfrel (well-founded-relation old$ wrld))
    (measure (untranslate (measure old$ wrld)
                          nil wrld))
    (termination-hints
         (cons (cons '"Goal"
                     (cons ':use
                           (cons (cons ':termination-theorem
                                       (cons old$ 'nil))
                                 '(:in-theory nil))))
               'nil))
    (guard (untranslate (conjoin2 (guard old$ nil wrld)
                                  (apply-term* domain$ a))
                        t wrld))
    (guard-hints
     (case variant$
      ((:monoid :assoc)
       (b*
        ((z (car (if (symbolp domain$)
                     (formals domain$ wrld)
                   (lambda-formals domain$))))
         (domain-of-base-thm
              (cdr (assoc-eq :domain-of-base appcond-thm-names)))
         (domain-of-nonrec-thm
              (cdr (assoc-eq :domain-of-nonrec appcond-thm-names)))
         (domain-of-combine-thm
              (cdr (assoc-eq :domain-of-combine appcond-thm-names)))
         (domain-guard-thm
              (cdr (assoc-eq :domain-guard appcond-thm-names)))
         (combine-guard-thm
              (cdr (assoc-eq :combine-guard appcond-thm-names)))
         (domain-of-combine-instance
          (cons
              ':instance
              (cons domain-of-combine-thm
                    (cons ':extra-bindings-ok
                          (cons (cons (tailrec-gen-var-u old$)
                                      (cons a 'nil))
                                (cons (cons (tailrec-gen-var-v old$)
                                            (cons nonrec 'nil))
                                      'nil))))))
         (domain-guard-instance
            (cons ':instance
                  (cons domain-guard-thm
                        (cons ':extra-bindings-ok
                              (cons (cons z (cons a 'nil)) 'nil)))))
         (combine-guard-instance-base
             (cons ':instance
                   (cons combine-guard-thm
                         (cons ':extra-bindings-ok
                               (cons (cons q (cons a 'nil))
                                     (cons (cons r (cons base 'nil))
                                           'nil))))))
         (combine-guard-instance-nonrec
           (cons ':instance
                 (cons combine-guard-thm
                       (cons ':extra-bindings-ok
                             (cons (cons q (cons a 'nil))
                                   (cons (cons r (cons nonrec 'nil))
                                         'nil)))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':use
             (cons
              (cons
               (cons ':guard-theorem (cons old$ 'nil))
               (cons
                domain-guard-instance
                (cons
                 domain-of-base-thm
                 (cons
                  domain-of-nonrec-thm
                  (cons
                   combine-guard-instance-base
                   (cons
                        combine-guard-instance-nonrec
                        (cons domain-of-combine-instance 'nil)))))))
              'nil)))))
         'nil)))
      (:monoid-alt
       (b*
        ((z (car (if (symbolp domain$)
                     (formals domain$ wrld)
                   (lambda-formals domain$))))
         (domain-of-base-thm
              (cdr (assoc-eq :domain-of-base appcond-thm-names)))
         (domain-of-combine-uncond-thm
          (cdr
            (assoc-eq :domain-of-combine-uncond appcond-thm-names)))
         (domain-guard-thm
              (cdr (assoc-eq :domain-guard appcond-thm-names)))
         (combine-guard-thm
              (cdr (assoc-eq :combine-guard appcond-thm-names)))
         (domain-of-nonrec-when-guard-thm
          (cdr
              (assoc-eq
                   :domain-of-nonrec-when-guard appcond-thm-names)))
         (domain-of-combine-uncond-instance
          (cons
              ':instance
              (cons domain-of-combine-uncond-thm
                    (cons ':extra-bindings-ok
                          (cons (cons (tailrec-gen-var-u old$)
                                      (cons a 'nil))
                                (cons (cons (tailrec-gen-var-v old$)
                                            (cons nonrec 'nil))
                                      'nil))))))
         (domain-guard-instance
            (cons ':instance
                  (cons domain-guard-thm
                        (cons ':extra-bindings-ok
                              (cons (cons z (cons a 'nil)) 'nil)))))
         (combine-guard-instance-base
             (cons ':instance
                   (cons combine-guard-thm
                         (cons ':extra-bindings-ok
                               (cons (cons q (cons a 'nil))
                                     (cons (cons r (cons base 'nil))
                                           'nil))))))
         (combine-guard-instance-nonrec
           (cons ':instance
                 (cons combine-guard-thm
                       (cons ':extra-bindings-ok
                             (cons (cons q (cons a 'nil))
                                   (cons (cons r (cons nonrec 'nil))
                                         'nil)))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':use
             (cons
              (cons
               (cons ':guard-theorem (cons old$ 'nil))
               (cons
                domain-guard-instance
                (cons
                 domain-of-base-thm
                 (cons
                  domain-of-nonrec-when-guard-thm
                  (cons
                       combine-guard-instance-base
                       (cons combine-guard-instance-nonrec
                             (cons domain-of-combine-uncond-instance
                                   'nil)))))))
              'nil)))))
         'nil)))
      (:assoc-alt
       (b*
        ((z (car (if (symbolp domain$)
                     (formals domain$ wrld)
                   (lambda-formals domain$))))
         (domain-of-combine-thm
              (cdr (assoc-eq :domain-of-combine appcond-thm-names)))
         (domain-guard-thm
              (cdr (assoc-eq :domain-guard appcond-thm-names)))
         (combine-guard-thm
              (cdr (assoc-eq :combine-guard appcond-thm-names)))
         (domain-of-base-when-guard-thm
          (cdr
           (assoc-eq :domain-of-base-when-guard appcond-thm-names)))
         (domain-of-nonrec-when-guard-thm
          (cdr
              (assoc-eq
                   :domain-of-nonrec-when-guard appcond-thm-names)))
         (domain-of-combine-instance
          (cons
              ':instance
              (cons domain-of-combine-thm
                    (cons ':extra-bindings-ok
                          (cons (cons (tailrec-gen-var-u old$)
                                      (cons a 'nil))
                                (cons (cons (tailrec-gen-var-v old$)
                                            (cons nonrec 'nil))
                                      'nil))))))
         (domain-guard-instance
            (cons ':instance
                  (cons domain-guard-thm
                        (cons ':extra-bindings-ok
                              (cons (cons z (cons a 'nil)) 'nil)))))
         (combine-guard-instance-base
             (cons ':instance
                   (cons combine-guard-thm
                         (cons ':extra-bindings-ok
                               (cons (cons q (cons a 'nil))
                                     (cons (cons r (cons base 'nil))
                                           'nil))))))
         (combine-guard-instance-nonrec
           (cons ':instance
                 (cons combine-guard-thm
                       (cons ':extra-bindings-ok
                             (cons (cons q (cons a 'nil))
                                   (cons (cons r (cons nonrec 'nil))
                                         'nil)))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':use
             (cons
              (cons
               (cons ':guard-theorem (cons old$ 'nil))
               (cons
                domain-guard-instance
                (cons
                 domain-of-base-when-guard-thm
                 (cons
                  domain-of-nonrec-when-guard-thm
                  (cons
                   combine-guard-instance-base
                   (cons
                        combine-guard-instance-nonrec
                        (cons domain-of-combine-instance 'nil)))))))
              'nil)))))
         'nil)))
      (t (impossible))))
    (local-event
     (cons
      'local
      (cons
       (cons
        macro
        (cons
         new-name$
         (cons
          new-formals
          (cons
           (cons
            'declare
            (cons
             (cons
              'xargs
              (cons
               ':well-founded-relation
               (cons
                wfrel
                (cons
                 ':measure
                 (cons
                  measure
                  (cons
                   ':hints
                   (cons
                    termination-hints
                    (cons
                     ':guard
                     (cons
                      guard
                      (cons
                       ':verify-guards
                       (cons
                        verify-guards$
                        (append
                             (and verify-guards$
                                  (list :guard-hints guard-hints))
                             '(:guard-simplify :limited)))))))))))))
             'nil))
           (cons body 'nil)))))
       'nil)))
    (exported-event
     (cons
      macro
      (cons
       new-name$
       (cons
        new-formals
        (cons
         (cons
          'declare
          (cons
           (cons
            'xargs
            (cons
             ':well-founded-relation
             (cons
              wfrel
              (cons
               ':measure
               (cons
                measure
                (cons ':guard
                      (cons guard
                            (cons ':verify-guards
                                  (cons verify-guards$ 'nil)))))))))
           'nil))
         (cons body 'nil)))))))
   (mv local-event
       exported-event new-formals))))