		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-everything

Generate the top-level event.

Signature
(tailrec-gen-everything old$ test base nonrec updates combine q r variant$ domain$ new-name$ new-enable$ a wrapper$ wrapper-name$ wrapper-enable$ old-to-new-name$ old-to-new-enable$ new-to-old-name$ new-to-old-enable$ old-to-wrapper-name$ old-to-wrapper-enable$ wrapper-to-old-name$ wrapper-to-old-enable$ verify-guards$ hints$ print$ show-only$ call names-to-avoid ctx state) → (mv erp event state)
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).; wrapper$ — Guard (booleanp wrapper$).; wrapper-name$ — Guard (symbolp wrapper-name$).; wrapper-enable$ — Guard (booleanp wrapper-enable$).; old-to-new-name$ — Guard (symbolp old-to-new-name$).; old-to-new-enable$ — Guard (booleanp old-to-new-enable$).; new-to-old-name$ — Guard (symbolp new-to-old-name$).; new-to-old-enable$ — Guard (booleanp new-to-old-enable$).; old-to-wrapper-name$ — Guard (symbolp old-to-wrapper-name$).; old-to-wrapper-enable$ — Guard (booleanp old-to-wrapper-enable$).; wrapper-to-old-name$ — Guard (symbolp wrapper-to-old-name$).; wrapper-to-old-enable$ — Guard (booleanp wrapper-to-old-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; hints$ — Guard (symbol-alistp hints$).; print$ — Guard (evmac-input-print-p print$).; show-only$ — Guard (booleanp show-only$).; call — Guard (pseudo-event-formp call).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: event — A pseudo-event-formp.

This is a progn that consists of the expansion of tailrec (the encapsulate), followed by an event to extend the transformation table, optionally followed by events to print the exported events (if specified by the :print input). The progn ends with :invisible to avoid printing a return value.

The encapsulate starts with some implicitly local events to ensure logic mode and avoid errors due to ignored or irrelevant formals in the generated functions. Other implicitly local event forms remove any default and override hints, to prevent such hints from sabotaging the generated proofs; this removal is done after proving the applicability conditions, in case their proofs rely on the default or override hints.

The encapsulate also includes events to locally install the non-normalized definitions of the old, new, and (if generated) wrapper functions, because the generated proofs are based on the unnormalized bodies.

The encapsulate is stored into the transformation table, associated to the call to the transformation. Thus, the table event and (if present) the screen output events (which are in the progn but not in the encapsulate) are not stored into the transformation table, because they carry no additional information, and because otherwise the table event would have to contain itself.

If :print is :all, the encapsulate is wrapped to show ACL2's output in response to the submitted events. If :print is :result or :info or :all, the progn includes events to print the exported events on the screen without hints; these are the same event forms that are introduced non-locally and redundantly in the encapsulate. If :print is :info or :all, a blank line is printed just before the result, for visual separation; if :print is :result, the blank line is not printed.

If :show-only is t, the encapsulate is just printed on the screen and not returned as part of the event to submit, which in this case is just an :invisible form. In this case, if :print is :info or :all, a blank line is printed just before the encapsulate, for visual separation.

Definitions and Theorems

Function: tailrec-gen-everything

(defun tailrec-gen-everything
       (old$ test base nonrec updates
             combine q r variant$ domain$ new-name$
             new-enable$ a wrapper$ wrapper-name$
             wrapper-enable$ old-to-new-name$
             old-to-new-enable$ new-to-old-name$
             new-to-old-enable$ old-to-wrapper-name$
             old-to-wrapper-enable$
             wrapper-to-old-name$
             wrapper-to-old-enable$
             verify-guards$ hints$ print$ show-only$
             call names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (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 wrapper$)
                             (symbolp wrapper-name$)
                             (booleanp wrapper-enable$)
                             (symbolp old-to-new-name$)
                             (booleanp old-to-new-enable$)
                             (symbolp new-to-old-name$)
                             (booleanp new-to-old-enable$)
                             (symbolp old-to-wrapper-name$)
                             (booleanp old-to-wrapper-enable$)
                             (symbolp wrapper-to-old-name$)
                             (booleanp wrapper-to-old-enable$)
                             (booleanp verify-guards$)
                             (symbol-alistp hints$)
                             (evmac-input-print-p print$)
                             (booleanp show-only$)
                             (pseudo-event-formp call)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'tailrec-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (appconds
       (tailrec-gen-appconds old$ test base nonrec combine q r
                             domain$ variant$ verify-guards$ state))
    ((er (list appcond-thm-events
               appcond-thm-names names-to-avoid))
     (evmac-appcond-theorems-no-extra-hints
          appconds
          hints$ names-to-avoid print$ ctx state))
    ((mv old-unnorm-event
         old-unnorm-name names-to-avoid)
     (install-not-normalized-event old$ t names-to-avoid wrld))
    ((mv domain-of-old-event?
         domain-of-old-name? names-to-avoid)
     (if (member-eq variant$ '(:monoid :monoid-alt :assoc))
         (tailrec-gen-domain-of-old-thm
              old$ test nonrec
              updates variant$ domain$ names-to-avoid
              appcond-thm-names old-unnorm-name wrld)
       (mv nil nil names-to-avoid)))
    ((mv new-fn-local-event
         new-fn-exported-event new-formals)
     (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 new-unnorm-event
         new-unnorm-name names-to-avoid)
     (install-not-normalized-event new-name$ t names-to-avoid wrld))
    ((mv new-to-old-thm-local-event
         new-to-old-thm-exported-event)
     (tailrec-gen-new-to-old-thm
          old$ nonrec updates combine q r variant$
          domain$ new-name$ a new-to-old-name$
          new-to-old-enable$ appcond-thm-names
          old-unnorm-name domain-of-old-name?
          new-formals new-unnorm-name wrld))
    (gen-alpha (member-eq variant$ '(:monoid :monoid-alt)))
    ((mv alpha-event? alpha-name? names-to-avoid)
     (if gen-alpha
       (tailrec-gen-alpha-fn old$ test updates names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv test-of-alpha-event?
         test-of-alpha-name? names-to-avoid)
     (if gen-alpha (tailrec-gen-test-of-alpha-thm
                        old$
                        test alpha-name? names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv old-guard-of-alpha-event?
         old-guard-of-alpha-name? names-to-avoid)
     (if (and gen-alpha verify-guards$)
         (tailrec-gen-old-guard-of-alpha-thm
              old$ alpha-name? names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv domain-of-ground-base-event?
         domain-of-ground-base-name?
         names-to-avoid)
     (if gen-alpha (tailrec-gen-domain-of-ground-base-thm
                        old$ base
                        domain$ appcond-thm-names alpha-name?
                        test-of-alpha-name? names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv combine-left-identity-ground-event?
         combine-left-identity-ground-name?
         names-to-avoid)
     (if gen-alpha (tailrec-gen-combine-left-identity-ground-thm
                        old$ base combine q
                        r domain$ appcond-thm-names alpha-name?
                        test-of-alpha-name? names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv base-guard-event?
         base-guard-name? names-to-avoid)
     (if (and gen-alpha verify-guards$)
         (tailrec-gen-base-guard-thm
              old$
              base alpha-name? test-of-alpha-name?
              old-guard-of-alpha-name?
              names-to-avoid state)
       (mv nil nil names-to-avoid)))
    ((mv old-to-new-thm-local-event
         old-to-new-thm-exported-event)
     (tailrec-gen-old-to-new-thm
          old$ test
          base nonrec updates a variant$ new-name$
          old-to-new-name$ old-to-new-enable$
          appcond-thm-names domain-of-old-name?
          domain-of-ground-base-name?
          combine-left-identity-ground-name?
          new-formals new-to-old-name$ wrld))
    ((mv wrapper-fn-local-event?
         wrapper-fn-exported-event?)
     (if wrapper$ (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 nil nil)))
    ((mv wrapper-unnorm-event?
         wrapper-unnorm-name? &)
     (if wrapper$ (install-not-normalized-event
                       wrapper-name$ t names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv old-to-wrapper-thm-local-event?
         old-to-wrapper-thm-exported-event?)
     (if wrapper$ (tailrec-gen-old-to-wrapper-thm
                       old$ wrapper-name$ old-to-wrapper-name$
                       old-to-wrapper-enable$ old-to-new-name$
                       wrapper-unnorm-name? wrld)
       (mv nil nil)))
    ((mv wrapper-to-old-thm-local-event?
         wrapper-to-old-thm-exported-event?)
     (if wrapper$ (tailrec-gen-wrapper-to-old-thm
                       old$ wrapper-name$ wrapper-to-old-name$
                       wrapper-to-old-enable$ old-to-new-name$
                       wrapper-unnorm-name? wrld)
       (mv nil nil)))
    (theory-invariants
     (append
      (cons
       (cons
         'theory-invariant
         (cons (cons 'incompatible
                     (cons (cons ':rewrite
                                 (cons old-to-new-name$ 'nil))
                           (cons (cons ':rewrite
                                       (cons new-to-old-name$ 'nil))
                                 'nil)))
               'nil))
       'nil)
      (and
       wrapper$
       (cons
        (cons
         'theory-invariant
         (cons
           (cons 'incompatible
                 (cons (cons ':rewrite
                             (cons old-to-wrapper-name$ 'nil))
                       (cons (cons ':rewrite
                                   (cons wrapper-to-old-name$ 'nil))
                             'nil)))
           'nil))
        'nil))))
    (new-fn-numbered-name-event (cons 'add-numbered-name-in-use
                                      (cons new-name$ 'nil)))
    (wrapper-fn-numbered-name-event?
         (if wrapper$ (cons 'add-numbered-name-in-use
                            (cons wrapper-name$ 'nil))
           nil))
    (encapsulate-events
     (cons
      '(logic)
      (cons
       '(set-ignore-ok t)
       (cons
        '(set-irrelevant-formals-ok t)
        (append
         appcond-thm-events
         (cons
          '(evmac-prepare-proofs)
          (cons
           old-unnorm-event
           (append
            (and domain-of-old-name?
                 (list domain-of-old-event?))
            (cons
             new-fn-local-event
             (cons
              new-unnorm-event
              (cons
               new-to-old-thm-local-event
               (append
                (and gen-alpha (list alpha-event?))
                (append
                 (and gen-alpha (list test-of-alpha-event?))
                 (append
                  (and gen-alpha verify-guards$
                       (list old-guard-of-alpha-event?))
                  (append
                   (and gen-alpha
                        (list domain-of-ground-base-event?))
                   (append
                    (and gen-alpha
                         (list combine-left-identity-ground-event?))
                    (append
                     (and gen-alpha
                          verify-guards$ (list base-guard-event?))
                     (cons
                      old-to-new-thm-local-event
                      (append
                       (and wrapper$ (list wrapper-fn-local-event?))
                       (append
                        (and wrapper$ (list wrapper-unnorm-event?))
                        (append
                         (and
                             wrapper$
                             (list old-to-wrapper-thm-local-event?))
                         (append
                          (and
                             wrapper$
                             (list wrapper-to-old-thm-local-event?))
                          (cons
                           new-fn-exported-event
                           (append
                            (and wrapper$
                                 (list wrapper-fn-exported-event?))
                            (cons
                             old-to-new-thm-exported-event
                             (cons
                              new-to-old-thm-exported-event
                              (append
                               (and
                                wrapper$
                                (list
                                 old-to-wrapper-thm-exported-event?))
                               (append
                                (and
                                 wrapper$
                                 (list
                                  wrapper-to-old-thm-exported-event?))
                                (append
                                 theory-invariants
                                 (cons
                                  new-fn-numbered-name-event
                                  (and
                                   wrapper$
                                   (list
                                    wrapper-fn-numbered-name-event?))))))))))))))))))))))))))))))))
    (encapsulate (cons 'encapsulate
                       (cons 'nil encapsulate-events))
)
    ((when show-only$)
     (if (member-eq print$ '(:info :all))
         (cw "~%~x0~|" encapsulate)
       (cw "~x0~|" encapsulate))
     (value '(value-triple :invisible)))
    (encapsulate+ (restore-output? (eq print$ :all)
                                   encapsulate))
    (transformation-table-event
         (record-transformation-call-event call encapsulate wrld))
    (print-result
     (and
      (member-eq print$ '(:result :info :all))
      (append
       (and (member-eq print$ '(:info :all))
            '((cw-event "~%")))
       (cons
        (cons 'cw-event
              (cons '"~x0~|"
                    (cons (cons 'quote
                                (cons new-fn-exported-event 'nil))
                          'nil)))
        (append
         (and
          wrapper$
          (list
           (cons
            'cw-event
            (cons
                 '"~x0~|"
                 (cons (cons 'quote
                             (cons wrapper-fn-exported-event? 'nil))
                       'nil)))))
         (cons
          (cons
           'cw-event
           (cons
              '"~x0~|"
              (cons (cons 'quote
                          (cons old-to-new-thm-exported-event 'nil))
                    'nil)))
          (cons
           (cons
            'cw-event
            (cons
              '"~x0~|"
              (cons (cons 'quote
                          (cons new-to-old-thm-exported-event 'nil))
                    'nil)))
           (and
            wrapper$
            (list
             (cons
              'cw-event
              (cons
                '"~x0~|"
                (cons (cons 'quote
                            (cons old-to-wrapper-thm-exported-event?
                                  'nil))
                      'nil)))
             (cons
              'cw-event
              (cons
                '"~x0~|"
                (cons (cons 'quote
                            (cons wrapper-to-old-thm-exported-event?
                                  'nil))
                      'nil)))))))))))))
   (value
      (cons 'progn
            (cons encapsulate+
                  (cons transformation-table-event
                        (append print-result
                                '((value-triple :invisible))))))))))