		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-everything

Generate the top-level event.

Signature
(parteval-gen-everything old$ static$ new-name$ new-enable$ thm-name$ thm-enable$ verify-guards$ untranslate$ print$ show-only$ case call wrld) → event
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; new-name$ — Guard (symbolp new-name$).; new-enable$ — Guard (booleanp new-enable$).; thm-name$ — Guard (symbolp thm-name$).; thm-enable$ — Guard (booleanp thm-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; untranslate$ — Guard (untranslate-specifier-p untranslate$).; print$ — Guard (evmac-input-print-p print$).; show-only$ — Guard (booleanp show-only$).; case — Guard (member case '(1 2 3)).; call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.

This is a progn that consists of the expansion of parteval (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.

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: parteval-gen-everything

(defun parteval-gen-everything
       (old$ static$ new-name$ new-enable$ thm-name$
             thm-enable$ verify-guards$ untranslate$
             print$ show-only$ case call wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbol-alistp static$)
                             (symbolp new-name$)
                             (booleanp new-enable$)
                             (symbolp thm-name$)
                             (booleanp thm-enable$)
                             (booleanp verify-guards$)
                             (untranslate-specifier-p untranslate$)
                             (evmac-input-print-p print$)
                             (booleanp show-only$)
                             (member case '(1 2 3))
                             (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'parteval-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((mv new-fn-local-event
         new-fn-exported-event new-formals)
     (parteval-gen-new-fn old$ static$ new-name$ new-enable$
                          verify-guards$ untranslate$ case wrld))
    ((mv old-to-new-thm-local-event
         old-to-new-thm-exported-event)
     (parteval-gen-old-to-new-thm
          old$ static$ new-name$ thm-name$
          thm-enable$ case new-formals wrld))
    (new-fn-verify-guards-event?
         (and verify-guards$
              (list (parteval-gen-new-fn-verify-guards
                         old$ static$
                         new-name$ thm-name$ case wrld))))
    (new-fn-numbered-name-event (cons 'add-numbered-name-in-use
                                      (cons new-name$ 'nil)))
    (encapsulate-events
     (cons
      '(logic)
      (cons
       '(set-ignore-ok t)
       (cons
        '(set-irrelevant-formals-ok t)
        (cons
         '(evmac-prepare-proofs)
         (cons
          new-fn-local-event
          (cons old-to-new-thm-local-event
                (append new-fn-verify-guards-event?
                        (cons new-fn-exported-event
                              (cons old-to-new-thm-exported-event
                                    (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-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 old-to-new-thm-exported-event 'nil))
                    'nil)))
         'nil))))))
   (cons 'progn
         (cons encapsulate+
               (cons transformation-table-event
                     (append print-result
                             '((value-triple :invisible)))))))))