		Search-engine friendly clone of the ACL2 documentation.

Defequal-event-generation

Defequal-gen-everything

Generate the top-level event.

Signature
(defequal-gen-everything name left right x1...xn enable verify-guards left-to-right left-to-right-enable right-to-left right-to-left-enable print show-only call) → event
Arguments: name — Guard (symbolp name).; left — Guard (symbolp left).; right — Guard (symbolp right).; x1...xn — Guard (symbol-listp x1...xn).; enable — Guard (booleanp enable).; verify-guards — Guard (booleanp verify-guards).; left-to-right — Guard (symbolp left-to-right).; left-to-right-enable — Guard (booleanp left-to-right-enable).; right-to-left — Guard (symbolp right-to-left).; right-to-left-enable — Guard (booleanp right-to-left-enable).; print — Guard (evmac-input-print-p print).; show-only — Guard (booleanp show-only).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defequal-gen-everything

(defun defequal-gen-everything
       (name left right x1...xn enable verify-guards
             left-to-right left-to-right-enable
             right-to-left right-to-left-enable
             print show-only call)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp left)
                             (symbolp right)
                             (symbol-listp x1...xn)
                             (booleanp enable)
                             (booleanp verify-guards)
                             (symbolp left-to-right)
                             (booleanp left-to-right-enable)
                             (symbolp right-to-left)
                             (booleanp right-to-left-enable)
                             (evmac-input-print-p print)
                             (booleanp show-only)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defequal-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((mv local-equality exported-equality)
     (defequal-gen-equality name
                            left right x1...xn enable verify-guards
                            left-to-right left-to-right-enable))
    ((mv local-right-to-left
         exported-right-to-left)
     (defequal-gen-right-to-left
          right-to-left right-to-left-enable
          name left right x1...xn left-to-right))
    (theory-invariant
        (defequal-gen-theory-invariant left-to-right right-to-left))
    (events
     (cons
      '(logic)
      (cons
         '(evmac-prepare-proofs)
         (cons local-equality
               (cons local-right-to-left
                     (cons exported-equality
                           (cons exported-right-to-left
                                 (cons theory-invariant 'nil))))))))
    (encapsulate (cons 'encapsulate (cons 'nil 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))
    (table-record (defequal-record-call call encapsulate))
    (print-result
     (and
      (member-eq print '(:result :info :all))
      (append
       (and (member-eq print '(:all))
            '((cw-event "~%")))
       (cons
        (cons 'cw-event
              (cons '"~x0~|"
                    (cons (cons 'quote
                                (cons exported-equality 'nil))
                          'nil)))
        (cons
         (cons 'cw-event
               (cons '"~x0~|"
                     (cons (cons 'quote
                                 (cons exported-right-to-left 'nil))
                           'nil)))
         (cons (cons 'cw-event
                     (cons '"~x0~|"
                           (cons (cons 'quote
                                       (cons theory-invariant 'nil))
                                 'nil)))
               'nil)))))))
   (cons 'progn
         (cons encapsulate+
               (cons table-record
                     (append print-result
                             '((value-triple :invisible)))))))))

Theorem: pseudo-event-formp-of-defequal-gen-everything

(defthm pseudo-event-formp-of-defequal-gen-everything
 (b*
  ((event
    (defequal-gen-everything name
                             left right x1...xn enable verify-guards
                             left-to-right left-to-right-enable
                             right-to-left right-to-left-enable
                             print show-only call)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)