		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-everything

Generate the top-level event.

Signature
(defmapping-gen-everything name$ doma$ domb$ alpha$ beta$ beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$ unconditional$ thm-names$ thm-enable$ hints$ print$ show-only$ call ctx state) → (mv erp event state)
Arguments: name$ — Guard (symbolp name$).; doma$ — Guard (pseudo-termfnp doma$).; domb$ — Guard (pseudo-termfnp domb$).; alpha$ — Guard (pseudo-termfnp alpha$).; beta$ — Guard (pseudo-termfnp beta$).; beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).; alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).; guard-thms$ — Guard (booleanp guard-thms$).; unconditional$ — Guard (booleanp unconditional$).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; hints$ — Guard (symbol-truelist-alistp hints$).; print$ — Guard (evmac-input-print-p print$).; show-only$ — Guard (booleanp show-only$).; call — Guard (pseudo-event-formp call).
Returns: event — A pseudo-event-formp.

This is a progn that consists of the expansion of defmapping (the encapsulate), followed by an event to extend the defmapping table, optionally followed by events to print the generated theorems. The progn ends with :invisible to avoid printing a return value.

The expansion starts with an implicitly local event to ensure logic mode. After the events to proof Other implicitly local event forms remove any default and override hints, to prevent such hints from sabotaging the generated proofs for the theorems that are not applicability conditions; this removal is done after proving the applicability conditions, in case their proofs rely on the default or override hints. We also add an explicitly local event to prevent mv-nth from being expanded in the generated proofs, which is accomplished via a system attachment.

If :print is :all, the expansion is wrapped to show ACL2's output in response to the submitted events. 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 expansion is printed on the screen and not returned as part of the event to submit, which is 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: defmapping-gen-everything

(defun defmapping-gen-everything
       (name$ doma$
              domb$ alpha$ beta$ beta-of-alpha-thm$
              alpha-of-beta-thm$ guard-thms$
              unconditional$ thm-names$ thm-enable$
              hints$ print$ show-only$ call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name$)
                             (pseudo-termfnp doma$)
                             (pseudo-termfnp domb$)
                             (pseudo-termfnp alpha$)
                             (pseudo-termfnp beta$)
                             (booleanp beta-of-alpha-thm$)
                             (booleanp alpha-of-beta-thm$)
                             (booleanp guard-thms$)
                             (booleanp unconditional$)
                             (symbol-symbol-alistp thm-names$)
                             (keyword-listp thm-enable$)
                             (symbol-truelist-alistp hints$)
                             (evmac-input-print-p print$)
                             (booleanp show-only$)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defmapping-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (a1...an (defmapping-gen-var-a1...an alpha$ wrld))
    (b1...bm (defmapping-gen-var-b1...bm beta$ wrld))
    (appconds (defmapping-gen-appconds
                   doma$ domb$ alpha$ beta$ a1...an b1...bm
                   beta-of-alpha-thm$ alpha-of-beta-thm$
                   guard-thms$ unconditional$ state))
    ((er (list appcond-events appcond-thm-names &))
     (evmac-appcond-theorems-no-extra-hints
          appconds hints$ nil print$ ctx state))
    ((mv local-thm-events exported-thm-events)
     (defmapping-gen-thms doma$ domb$ alpha$ beta$ a1...an b1...bm
                          beta-of-alpha-thm$ alpha-of-beta-thm$
                          unconditional$ thm-names$ thm-enable$
                          appconds appcond-thm-names wrld))
    (expansion
     (cons
      'encapsulate
      (cons
       'nil
       (cons '(logic)
             (cons '(set-ignore-ok t)
                   (append appcond-events
                           (cons '(evmac-prepare-proofs)
                                 (append local-thm-events
                                         exported-thm-events))))))))
    ((when show-only$)
     (if (member-eq print$ '(:info :all))
         (cw "~%~x0~|" expansion)
       (cw "~x0~|" expansion))
     (value '(value-triple :invisible)))
    (expansion+ (restore-output? (eq print$ :all)
                                 expansion))
    (call$ (defmapping-filter-call call))
    (extend-table (defmapping-gen-ext-table
                       name$
                       doma$ domb$ alpha$ beta$ unconditional$
                       thm-names$ call$ expansion))
    (print-result
     (and
       (member-eq print$ '(:result :info :all))
       (append (and (member-eq print$ '(:info :all))
                    '((cw-event "~%")))
               (defmapping-gen-print-result exported-thm-events)))))
   (value
      (cons 'progn
            (cons expansion+
                  (cons extend-table
                        (append print-result
                                '((value-triple :invisible))))))))))