• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
      • Simplify-defun
      • Isodata
      • Tailrec
      • Schemalg
      • Restrict
      • Expdata
      • Casesplit
      • Simplify-term
      • Simplify-defun-sk
      • Parteval
        • Parteval-implementation
          • Parteval-event-generation
          • Parteval-fn
          • Parteval-input-processing
          • Parteval-macro-definition
      • Solve
      • Wrap-output
      • Propagate-iso
      • Simplify
      • Finite-difference
      • Drop-irrelevant-params
      • Copy-function
      • Lift-iso
      • Rename-params
      • Utilities
      • Simplify-term-programmatic
      • Simplify-defun-sk-programmatic
      • Simplify-defun-programmatic
      • Simplify-defun+
      • Common-options
      • Common-concepts
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parteval-implementation

Parteval-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature

(parteval-fn old static new-name new-enable thm-name 
             thm-enable verify-guards untranslate 
             print show-only call ctx state) 
 
  → 
(mv erp event state)

Arguments

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

Returns

event — A pseudo-event-formp.

If this call to the transformation is redundant, a message to that effect is printed on the screen. If the transformation is redundant and :show-only is t, the encapsulate, retrieved from the table, is shown on the screen.

Definitions and Theorems

Function: parteval-fn

(defun parteval-fn (old static new-name new-enable thm-name
                        thm-enable verify-guards untranslate
                        print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'parteval-fn))
    (declare (ignorable __function__))
    (b* ((encapsulate?
              (previous-transformation-expansion call (w state)))
         ((when encapsulate?)
          (b* (((run-when show-only)
                (cw "~x0~|" encapsulate?)))
            (cw "~%The transformation ~x0 is redundant.~%"
                call)
            (value '(value-triple :invisible))))
         ((er (list old$ static$ new-name$ new-enable$
                    thm-name$ verify-guards$ case &))
          (parteval-process-inputs
               old static new-name new-enable
               thm-name thm-enable verify-guards
               untranslate print show-only ctx state))
         (event (parteval-gen-everything
                     old$
                     static$ new-name$ new-enable$ thm-name$
                     thm-enable verify-guards$ untranslate
                     print show-only case call (w state))))
      (value event))))