		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-everything

Generate the top-level event.

Signature
(restrict-gen-everything old restriction undefined new new-enable old-to-new old-to-new-enable new-to-old new-to-old-enable verify-guards hints print show-only call names-to-avoid ctx state) → (mv erp event state)
Arguments: old — Guard (symbolp old).; restriction — Guard (pseudo-termp restriction).; undefined — Guard (pseudo-termp undefined).; 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 (booleanp new-to-old-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 restrict (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.

If the old and new functions are reflexive, i.e. if the old function occurs in its termination theorem, just before the applicability conditions we introduce the n-ary stub described in the documentation, which is used in the :restriction-of-rec-calls applicability condition.

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

(defun restrict-gen-everything
       (old restriction undefined new
            new-enable old-to-new old-to-new-enable
            new-to-old new-to-old-enable
            verify-guards hints print
            show-only call names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (pseudo-termp restriction)
                             (pseudo-termp undefined)
                             (symbolp new)
                             (booleanp new-enable)
                             (symbolp old-to-new)
                             (booleanp old-to-new-enable)
                             (symbolp new-to-old)
                             (booleanp new-to-old-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__ 'restrict-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (recursivep (recursivep old nil wrld))
    (reflexivep
     (and
       recursivep
       (member-eq old
                  (all-ffn-symbs (termination-theorem old (w state))
                                 nil))))
    ((mv stub? names-to-avoid)
     (if reflexivep
         (fresh-logical-name-with-$s-suffix
              (intern-in-package-of-symbol
                   "?F"
                   (pkg-witness (symbol-package-name old)))
              'constrained-function
              names-to-avoid wrld)
       (mv nil names-to-avoid)))
    (stub-event?
         (and stub?
              (list (cons 'defstub
                          (cons stub?
                                (cons (repeat (arity old wrld) '*)
                                      '(=> *)))))))
    (appconds
      (restrict-gen-appconds old
                             restriction verify-guards stub? 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 old-unnorm-event
         old-unnorm names-to-avoid)
     (install-not-normalized-event old t names-to-avoid wrld))
    ((mv new-local-event
         new-exported-event new-body)
     (restrict-gen-new old restriction undefined
                       new new-enable verify-guards wrld))
    ((mv new-unnorm-event new-unnorm &)
     (install-not-normalized-event new t names-to-avoid wrld))
    ((mv old-to-new-local-event
         old-to-new-exported-event)
     (restrict-gen-old-to-new
          old restriction new new-body old-to-new
          old-to-new-enable appcond-thm-names
          stub? old-unnorm new-unnorm wrld))
    ((mv new-to-old-local-event
         new-to-old-exported-event)
     (restrict-gen-new-to-old old restriction new new-to-old
                              new-to-old-enable old-to-new wrld))
    (verify-guards-event?
     (and
      verify-guards
      (list
        (restrict-gen-verify-guards old new old-to-new
                                    appcond-thm-names stub? wrld))))
    (theory-inv-event
     (cons
      'theory-invariant
      (cons
           (cons 'incompatible
                 (cons (cons ':rewrite (cons old-to-new 'nil))
                       (cons (cons ':rewrite (cons new-to-old 'nil))
                             'nil)))
           'nil)))
    (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
         stub-event?
         (append
          appcond-thm-events
          (cons
           '(evmac-prepare-proofs)
           (cons
            old-unnorm-event
            (cons
             new-local-event
             (cons
              new-unnorm-event
              (cons
               old-to-new-local-event
               (cons
                new-to-old-local-event
                (append
                 verify-guards-event?
                 (cons
                      new-exported-event
                      (cons old-to-new-exported-event
                            (cons new-to-old-exported-event
                                  (cons theory-inv-event
                                        (cons 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-exported-event 'nil))
                          'nil)))
        (cons
         (cons
            'cw-event
            (cons '"~x0~|"
                  (cons (cons 'quote
                              (cons old-to-new-exported-event 'nil))
                        'nil)))
         (cons
          (cons
            'cw-event
            (cons '"~x0~|"
                  (cons (cons 'quote
                              (cons new-to-old-exported-event 'nil))
                        'nil)))
          'nil)))))))
   (value
      (cons 'progn
            (cons encapsulate+
                  (cons transformation-table-event
                        (append print-result
                                '((value-triple :invisible))))))))))