		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-everything

Generate the top-level event.

Signature
(expdata-gen-everything old$ arg-surjmaps res-surjmaps predicate$ 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$ names-to-avoid call ctx state) → (mv erp event state)
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; predicate$ — Guard (booleanp predicate$).; 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 expdata (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: expdata-gen-everything

(defun expdata-gen-everything
       (old$ arg-surjmaps res-surjmaps
             predicate$ 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$
             names-to-avoid call ctx state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (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__ 'expdata-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (surjmaps (append (strip-cdrs arg-surjmaps)
                      (strip-cdrs res-surjmaps)))
    (surjmaps (remove-duplicates-equal surjmaps))
    (defsurj-events
         (expdata-gen-defsurjs surjmaps verify-guards$ print$))
    (appconds (expdata-gen-appconds old$ arg-surjmaps res-surjmaps
                                    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)
     (expdata-gen-new-fn old$
                         arg-surjmaps res-surjmaps predicate$
                         new$ new-enable$ verify-guards$
                         untranslate$ 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-thm-local-event
         new-to-old-thm-exported-event)
     (expdata-gen-new-to-old-thm
          old$ arg-surjmaps res-surjmaps
          new$ new-to-old$ new-to-old-enable$
          appcond-thm-names old-fn-unnorm-name
          new-fn-unnorm-name wrld))
    ((mv newp-of-new-thm-local-event?
         newp-of-new-thm-exported-event?)
     (if
      (consp res-surjmaps)
      (expdata-gen-newp-of-new-thm old$ arg-surjmaps
                                   res-surjmaps 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-thm-local-event
         old-to-new-thm-exported-event)
     (expdata-gen-old-to-new-thm
          appcond-thm-names old$ arg-surjmaps
          res-surjmaps new$ old-to-new$
          old-to-new-enable$ new-to-old$ wrld))
    (new-fn-verify-guards-event?
         (and verify-guards$
              (list (expdata-gen-new-fn-verify-guards
                         appcond-thm-names
                         old$ arg-surjmaps res-surjmaps
                         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
         defsurj-events
         (append
          appcond-thm-events
          (cons
           '(evmac-prepare-proofs)
           (cons
            old-fn-unnorm-event
            (cons
             new-fn-local-event
             (cons
              new-fn-unnorm-event
              (cons
               new-to-old-thm-local-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))))))))))