		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-everything

Generate the top-level event.

Signature
(casesplit-gen-everything old$ conditions$ theorems$ hyps news new-name$ new-enable$ thm-name$ thm-enable$ verify-guards$ hints$ print$ show-only$ call names-to-avoid ctx state) → (mv erp event state)
Arguments: old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).; theorems$ — Guard (symbol-listp theorems$).; hyps — Guard (pseudo-term-listp hyps).; news — Guard (pseudo-term-listp news).; 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$).; 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 casesplit (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 definition of the new function, because the generated proofs are based on the unnormalized body.

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

(defun casesplit-gen-everything
       (old$ conditions$
             theorems$ hyps news new-name$
             new-enable$ thm-name$ thm-enable$
             verify-guards$ hints$ print$ show-only$
             call names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-term-listp conditions$)
                             (symbol-listp theorems$)
                             (pseudo-term-listp hyps)
                             (pseudo-term-listp news)
                             (symbolp new-name$)
                             (booleanp new-enable$)
                             (symbolp thm-name$)
                             (booleanp thm-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__ 'casesplit-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (appconds
         (casesplit-gen-appconds old$ conditions$
                                 hyps news 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 new-fn-local-event
         new-fn-exported-event)
     (casesplit-gen-new-fn old$
                           conditions$ news new-name$ new-enable$
                           verify-guards$ appcond-thm-names wrld))
    ((mv new-unnorm-event new-unnorm-name &)
     (install-not-normalized-event new-name$ t names-to-avoid wrld))
    ((mv old-to-new-thm-local-event
         old-to-new-thm-exported-event)
     (casesplit-gen-old-to-new-thm
          old$ theorems$
          new-name$ thm-name$ thm-enable$
          appcond-thm-names new-unnorm-name 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)
        (append
         appcond-thm-events
         (cons
          '(evmac-prepare-proofs)
          (cons
            new-fn-local-event
            (cons new-unnorm-event
                  (cons old-to-new-thm-local-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 '(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))))))
   (value
      (cons 'progn
            (cons encapsulate+
                  (cons transformation-table-event
                        (append print-result
                                '((value-triple :invisible))))))))))