		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-everything

Generate the top-level event.

Signature
(isodata-gen-everything old$ arg-isomaps res-isomaps predicate$ undefined$ new$ new-enable$ old-to-new$ old-to-new-enable$ new-to-old$ new-to-old-enable$ newp-of-new$ newp-of-new-enable$ verify-guards$ untranslate$ hints$ print$ show-only$ compatibility names-to-avoid call ctx state) → (mv erp event state)
Arguments: old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; predicate$ — Guard (booleanp predicate$).; undefined$ — Either :base-case-then, :base-case-else, or a pseudo-termp.; new$ — Guard (symbolp new$).; new-enable$ — Guard (booleanp new-enable$).; old-to-new$ — Guard (symbolp old-to-new$).; old-to-new-enable$ — Guard (booleanp old-to-new-enable$).; new-to-old$ — Guard (symbolp new-to-old$).; new-to-old-enable$ — Guard (symbolp new-to-old-enable$).; newp-of-new$ — Guard (symbolp newp-of-new$).; newp-of-new-enable$ — Guard (symbolp newp-of-new-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; untranslate$ — Guard (untranslate-specifier-p untranslate$).; hints$ — Guard (symbol-truelist-alistp hints$).; print$ — Guard (evmac-input-print-p print$).; show-only$ — Guard (booleanp show-only$).; names-to-avoid — Guard (symbol-listp names-to-avoid).; call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

This is a progn that consists of the expansion of isodata (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 function. Other implicitly local events 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 and new 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: isodata-gen-everything

(defun isodata-gen-everything
       (old$ arg-isomaps res-isomaps
             predicate$ undefined$ new$ new-enable$
             old-to-new$ old-to-new-enable$
             new-to-old$ new-to-old-enable$
             newp-of-new$ newp-of-new-enable$
             verify-guards$ untranslate$
             hints$ print$ show-only$ compatibility
             names-to-avoid call ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (booleanp predicate$)
                         (symbolp new$)
                         (booleanp new-enable$)
                         (symbolp old-to-new$)
                         (booleanp old-to-new-enable$)
                         (symbolp new-to-old$)
                         (symbolp new-to-old-enable$)
                         (symbolp newp-of-new$)
                         (symbolp newp-of-new-enable$)
                         (booleanp verify-guards$)
                         (untranslate-specifier-p untranslate$)
                         (symbol-truelist-alistp hints$)
                         (evmac-input-print-p print$)
                         (booleanp show-only$)
                         (symbol-listp names-to-avoid)
                         (pseudo-event-formp call))))
 (let ((__function__ 'isodata-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (m (len res-isomaps))
    (isomaps (append (strip-cdrs arg-isomaps)
                     (strip-cdrs res-isomaps)))
    (isomaps (remove-duplicates-equal isomaps))
    (defiso-events
         (isodata-gen-defisos isomaps verify-guards$ print$))
    (appconds (isodata-gen-appconds old$ arg-isomaps res-isomaps
                                    predicate$ verify-guards$ wrld))
    ((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-fn-unnorm-event
         old-fn-unnorm-name names-to-avoid)
     (install-not-normalized-event old$ t names-to-avoid wrld))
    ((mv new-fn-local-event
         new-fn-exported-event)
     (isodata-gen-new-fn old$ arg-isomaps
                         res-isomaps predicate$ undefined$ new$
                         new-enable$ verify-guards$ untranslate$
                         compatibility appcond-thm-names wrld))
    ((mv new-fn-unnorm-event
         new-fn-unnorm-name &)
     (install-not-normalized-event new$ t names-to-avoid wrld))
    ((mv new-to-old-lemma-name
         new-to-old-lemma-event names-to-avoid)
     (if (>= m 2)
         (isodata-gen-new-to-old-lemma
              old$ arg-isomaps res-isomaps new$
              appcond-thm-names old-fn-unnorm-name
              new-fn-unnorm-name names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv new-to-list-of-mv-nth-name
         new-to-list-of-mv-nth-event
         names-to-avoid)
     (if (>= m 2)
         (isodata-gen-new-to-list-of-mv-nth
              old$ new$ new-fn-unnorm-name
              m names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv new-to-old-thm-local-event
         new-to-old-thm-exported-event)
     (isodata-gen-new-to-old-thm
          old$ arg-isomaps res-isomaps
          new$ new-to-old$ new-to-old-enable$
          appcond-thm-names old-fn-unnorm-name
          new-fn-unnorm-name new-to-old-lemma-name
          new-to-list-of-mv-nth-name wrld))
    ((mv newp-of-new-thm-local-event?
         newp-of-new-thm-exported-event?)
     (if (consp res-isomaps)
         (isodata-gen-newp-of-new-thm
              old$
              arg-isomaps res-isomaps new$ new-to-old$
              newp-of-new$ newp-of-new-enable$
              appcond-thm-names wrld)
       (mv nil nil)))
    (newp-of-new-thm-local-event?
         (and newp-of-new-thm-local-event?
              (list newp-of-new-thm-local-event?)))
    (newp-of-new-thm-exported-event?
         (and newp-of-new-thm-exported-event?
              (list newp-of-new-thm-exported-event?)))
    ((mv old-to-new-lemma-name
         old-to-new-lemma-event names-to-avoid)
     (if (>= m 2)
         (isodata-gen-old-to-new-lemma
              old$ arg-isomaps res-isomaps new$
              appcond-thm-names new-to-old-lemma-name
              names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv old-to-list-of-mv-nth-name
         old-to-list-of-mv-nth-event &)
     (if (>= m 2)
         (isodata-gen-old-to-list-of-mv-nth old$ old-fn-unnorm-name
                                            m names-to-avoid wrld)
       (mv nil nil names-to-avoid)))
    ((mv old-to-new-thm-local-event
         old-to-new-thm-exported-event)
     (isodata-gen-old-to-new-thm appcond-thm-names
                                 old$ arg-isomaps res-isomaps
                                 new$ old-to-new$ old-to-new-enable$
                                 new-to-old$ old-to-new-lemma-name
                                 old-to-list-of-mv-nth-name wrld))
    (new-fn-verify-guards-event?
         (and verify-guards$
              (list (isodata-gen-new-fn-verify-guards
                         appcond-thm-names
                         old$ arg-isomaps res-isomaps
                         predicate$ new$ new-to-old$ old-to-new$
                         old-fn-unnorm-name newp-of-new$ wrld))))
    (theory-invariant
     (cons
      'theory-invariant
      (cons
          (cons 'incompatible
                (cons (cons ':rewrite (cons new-to-old$ 'nil))
                      (cons (cons ':rewrite (cons old-to-new$ 'nil))
                            'nil)))
          'nil)))
    (new-fn-numbered-name-event (cons 'add-numbered-name-in-use
                                      (cons new$ 'nil)))
    (encapsulate-events
     (cons
      '(logic)
      (cons
       '(set-ignore-ok t)
       (cons
        '(set-irrelevant-formals-ok t)
        (append
         defiso-events
         (append
          appcond-thm-events
          (cons
           '(set-default-hints nil)
           (cons
            '(set-override-hints nil)
            (cons
             old-fn-unnorm-event
             (cons
              new-fn-local-event
              (cons
               new-fn-unnorm-event
               (append
                (and (>= m 2)
                     (list new-to-old-lemma-event
                           new-to-list-of-mv-nth-event))
                (cons
                 new-to-old-thm-local-event
                 (append
                  (and (>= m 2)
                       (list old-to-new-lemma-event
                             old-to-list-of-mv-nth-event))
                  (cons
                   old-to-new-thm-local-event
                   (append
                    newp-of-new-thm-local-event?
                    (append
                     new-fn-verify-guards-event?
                     (cons
                      new-fn-exported-event
                      (cons
                       new-to-old-thm-exported-event
                       (cons
                        old-to-new-thm-exported-event
                        (append
                             newp-of-new-thm-exported-event?
                             (cons theory-invariant
                                   (cons new-fn-numbered-name-event
                                         'nil)))))))))))))))))))))))
    (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)))
        (cons
         (cons
          'cw-event
          (cons
              '"~x0~|"
              (cons (cons 'quote
                          (cons new-to-old-thm-exported-event 'nil))
                    'nil)))
         (cons
          (cons
           'cw-event
           (cons
              '"~x0~|"
              (cons (cons 'quote
                          (cons old-to-new-thm-exported-event 'nil))
                    'nil)))
          (and
           newp-of-new-thm-exported-event?
           (cons
            (cons
             'cw-event
             (cons
              '"~x0~|"
              (cons
                   (cons 'quote
                         (cons (car newp-of-new-thm-exported-event?)
                               'nil))
                   'nil)))
            'nil)))))))))
   (value
      (cons 'progn
            (cons encapsulate+
                  (cons transformation-table-event
                        (append print-result
                                '((value-triple :invisible))))))))))