• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
        • Defun-inst
        • Defequal
          • Defequal-implementation
            • Defequal-fn
            • Defequal-event-generation
              • Defequal-gen-everything
              • Defequal-gen-equality
              • Defequal-gen-right-to-left
              • Defequal-gen-theory-invariant
            • Defequal-input-processing
            • Defequal-table
            • Defequal-macro-definition
        • Defsoft
        • Defthm-inst
        • Defun2
        • Defunvar
        • Defun-sk2
        • Defchoose2
        • Defthm-2nd-order
        • Define-sk2
        • Defund-sk2
        • Define2
        • Defund2
      • Updates-to-workshop-material
      • Soft-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)