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

Defequal-fn

Check redundancy, process the inputs, generated the events.

Signature

(defequal-fn name left left-present right 
             right-present vars enable verify-guards 
             left-to-right-name left-to-right-enable 
             right-to-left-name right-to-left-enable 
             print show-only call ctx state) 
 
  → 
(mv erp event state)

Arguments

left-present — Guard (booleanp left-present).

right-present — Guard (booleanp right-present).

call — Guard (pseudo-event-formp call).

Returns

event — A pseudo-event-formp.

Definitions and Theorems

Function: defequal-fn

(defun defequal-fn (name left left-present right
                         right-present vars enable verify-guards
                         left-to-right-name left-to-right-enable
                         right-to-left-name right-to-left-enable
                         print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp left-present)
                              (booleanp right-present)
                              (pseudo-event-formp call))))
  (let ((__function__ 'defequal-fn))
    (declare (ignorable __function__))
    (b* ((expansion? (defequal-redundant? call (w state)))
         ((when expansion?)
          (b* (((run-when show-only)
                (cw "~x0~|" expansion?)))
            (cw "~%The call ~x0 is redundant.~%" call)
            (value '(value-triple :invisible))))
         ((er (list x1...xn left-to-right right-to-left))
          (defequal-process-inputs
               name left left-present right
               right-present vars enable verify-guards
               left-to-right-name left-to-right-enable
               right-to-left-name right-to-left-enable
               print show-only ctx state))
         (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)))
      (value event))))