• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
        • Isodata
        • Simplify-defun
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
          • Expdata-implementation
            • Expdata-event-generation
              • Expdata-gen-everything
              • Expdata-gen-thm-instances-to-terms-back
              • Expdata-gen-new-fn-body-nonpred
              • Expdata-gen-new-fn
              • Expdata-gen-new-fn-verify-guards
              • Expdata-gen-new-fn-verify-guards-hints-nonpred-rec-1res/mres
              • Expdata-gen-back-of-forth-instances-to-terms-back
              • Expdata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres
              • Expdata-gen-forth-image-instances-to-terms-back
              • Expdata-gen-forth-guard-instances-to-terms-back
              • Expdata-gen-new-to-old-thm-hints-rec-1res
              • Expdata-gen-defsurj
              • Expdata-gen-new-to-old-thm-hints-rec-mres
              • Expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back
              • Expdata-gen-new-fn-verify-guards-hints-pred-rec
              • Expdata-gen-lemma-instances-x1...xn-to-forth-rec-call-args-back
              • Expdata-gen-thm-instances-to-x1...xn
              • Expdata-gen-newp-of-new-thm-hints
              • Expdata-gen-all-back-guard-instances-to-mv-nth
              • Expdata-gen-result-vars
              • Expdata-gen-lemma-instances-x1...xn-to-rec-call-args-back
              • Expdata-gen-new-to-old-thm-hints-rec-0res
              • Expdata-gen-new-fn-verify-guards-hints-nonpred-rec-0res
              • Expdata-gen-newp-of-new-thm
              • Expdata-gen-new-to-old-thm
              • Expdata-gen-lemma-instances-var-to-rec-calls-back
              • Expdata-gen-new-fn-body-pred
              • Expdata-gen-old-to-new-thm-hints-1res
              • Expdata-gen-new-fn-verify-guards-hints-nonpred
              • Expdata-gen-new-fn-verify-guards-hints
              • Expdata-gen-all-back-of-forth-instances-to-terms-back
              • Expdata-gen-old-to-new-thm
              • Expdata-gen-new-to-old-thm-hints
              • Expdata-gen-new-fn-verify-guards-hints-pred-nonrec
              • Expdata-gen-all-forth-image-instances-to-terms-back
              • Expdata-gen-all-forth-guard-instances-to-terms-back
              • Expdata-gen-old-to-new-thm-hints-mres
              • Expdata-gen-appconds
              • Expdata-xform-rec-calls
                • Expdata-xform-rec-calls-lst
              • Expdata-gen-back-of-forth-instances-to-mv-nth
              • Expdata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn
              • Expdata-gen-forth-image-instances-to-mv-nth
              • Expdata-gen-forth-guard-instances-to-mv-nth
              • Expdata-gen-back-guard-instances-to-mv-nth
              • Expdata-gen-all-back-of-forth-instances-to-mv-nth
              • Expdata-gen-old-to-new-thm-formula
              • Expdata-gen-newp-guard-instances-to-x1...xn
              • Expdata-gen-new-to-old-thm-formula
              • Expdata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res
              • Expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
              • Expdata-gen-forth-image-instances-to-x1...xn
              • Expdata-gen-forth-image-instances-to-terms-back-aux
              • Expdata-gen-forth-guard-instances-to-x1...xn
              • Expdata-gen-forth-guard-instances-to-terms-back-aux
              • Expdata-gen-back-of-forth-instances-to-x1...xn
              • Expdata-gen-back-of-forth-instances-to-terms-back-aux
              • Expdata-gen-back-image-instances-to-x1...xn
              • Expdata-gen-back-guard-instances-to-x1...xn
              • Expdata-gen-newp-of-new-thm-formula
              • Expdata-gen-fn-of-terms
              • Expdata-gen-oldp-of-rec-call-args-under-contexts
              • Expdata-gen-new-fn-termination-hints
              • Expdata-gen-old-to-new-thm-hints
              • Expdata-gen-lemma-instance-x1...xn-to-fn-of-x1...xn
              • Expdata-gen-old-to-new-thm-hints-0res
              • Expdata-gen-new-fn-verify-guards-hints-pred
              • Expdata-gen-new-to-old-thm-hints-nonrec
              • Expdata-gen-subst-x1...xn-with-back-of-x1...xn
              • Expdata-gen-oldp-of-terms
              • Expdata-gen-newp-of-terms
              • Expdata-gen-new-fn-body
              • Expdata-gen-forth-of-terms
              • Expdata-gen-defsurjs
              • Expdata-gen-back-of-terms
              • Expdata-gen-new-fn-guard
              • Expdata-gen-result-vars-aux
              • Expdata-gen-new-fn-measure
              • Expdata-formal-of-newp
              • Expdata-formal-of-forth
              • Expdata-formal-of-back
              • Expdata-formal-of-unary
            • Expdata-fn
            • Expdata-input-processing
            • Expdata-macro-definition
        • Casesplit
        • 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
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Ethereum
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
      • Sha-2
      • Yul
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Axe
      • Poseidon
      • Where-do-i-place-my-book
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Expdata-event-generation

Expdata-xform-rec-calls

Transform all the calls of old.

Signature
(expdata-xform-rec-calls term old$ arg-surjmaps res-surjmaps new$) 
  → 
new-term
Arguments
term — Guard (pseudo-termp term).
old$ — Guard (symbolp old$).
arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).
res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).
new$ — Guard (symbolp new$).

Turn each call (old updatej-x1 ... updatej-xn) inside a term into one of the following:

  • (new (forth1 updatej-x1) ... (forthn updatej-xn)), if no results are transformed.
  • (back_r1 (new (forth1 updatej-x1) ... (forthn updatej-xn))), if old is single-valued and its result is transformed.
  • (mv-let (y1 ... ym) (new (forth1 updatej-x1) ... (forthn updatej-xn)) (mv (back_r1 y1) ... (back_rm ym))), if old is multi-valued and some of its results are transformed.

This term transformation is an intermediate step in the construction of the body of new from the body of old.

Subtopics

Expdata-xform-rec-calls-lst