• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
      • Simplify-defun
      • Isodata
      • Tailrec
      • Schemalg
      • Restrict
      • Expdata
      • Casesplit
        • Casesplit-implementation
          • Casesplit-event-generation
          • Casesplit-fn
          • Casesplit-input-processing
          • Casesplit-macro-definition
          • Casesplit-library-extensions
      • Simplify-term
      • Simplify-defun-sk
      • Parteval
      • 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

• Casesplit-implementation

Casesplit-fn

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

Signature

(casesplit-fn old 
              conditions theorems new-name new-enable 
              thm-name thm-enable verify-guards 
              hints 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: casesplit-fn

(defun casesplit-fn (old conditions theorems new-name new-enable
                         thm-name thm-enable verify-guards
                         hints print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'casesplit-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$ conditions$ hyps
                    news new-name$ new-enable$ thm-name$
                    verify-guards$ hints$ names-to-avoid))
          (casesplit-process-inputs
               old
               conditions theorems new-name new-enable
               thm-name thm-enable verify-guards
               hints print show-only ctx state))
         ((er event)
          (casesplit-gen-everything
               old$
               conditions$ theorems hyps news new-name$
               new-enable$ thm-name$ thm-enable
               verify-guards$ hints$ print show-only
               call names-to-avoid ctx state)))
      (value event))))