• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
        • Rp-ruleset
        • Defthmrp
        • Rp-rewriter/meta-rules
        • Rp-utilities
        • Rp-rewriter-demo
        • Rp-rewriter/debugging
          • Pp-rw-stack
            • Show-rules
            • Rp-pr
          • Rp-rewriter/applications
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Rp-rewriter/debugging

    Pp-rw-stack

    Pretty printing of rewrite stack.

    Signature
    (pp-rw-stack &key (rp-state 'rp-state) 
                 (state 'state) 
                 (frames '-1) 
                 (frames-offset '0) 
                 (omit 'nil) 
                 (only 'nil) 
                 (evisc-tuple ''(nil 6 8 nil)) 
                 (untranslate 'nil) 
                 (search-source 'nil)) 
     
      → 
    state

    Rewrite stack for RP-Rewriter can be enabled with (rp::update-rp-brr t rp::rp-state) or disabled with (rp::update-rp-brr t rp::rp-state). Then users may print the stack with program-mode function pp-rw-stack.

    
     (pp-rw-stack :frames <number>
                  :frames-offset <number>
                  :omit <list-of-names>
                  :only <list-of-names>
                  :evisc-tuple <quoted-evisc-tuple>
                  :untranslate <t-or-nil>)
     
    

    frames: Number of rewriter steps to print. Default value is -1, which indicates all the frames.

    frames-offset: Number of frames to skip. Defualt value = 0.

    omit: Quoted list of runes or entries in a frame to omit. For example, it can have: (:rewrite some-rule), :context, a-meta-fnc-name etc. Default value is nil.

    only: Similar to omit print only the frames regarding given runes.

    evisc-tuple: See evisc-tuple. Used in order to shorten long terms. Default value: '(NIL 3 4 NIL)

    untranslate: whether or not to untranslate the term. See untranslate. Default value = nil.

    Definitions and Theorems

    Function: pp-rw-stack-fn

    (defun pp-rw-stack-fn
           (rp-state state frames frames-offset omit only
                     evisc-tuple untranslate search-source)
     (declare (xargs :stobjs (rp-state state)))
     (declare (xargs :stobjs (rp-state state)))
     (declare (xargs :guard t))
     (let ((__function__ 'pp-rw-stack))
      (declare (ignorable __function__))
      (b*
       ((rw-stack (rw-stack rp-state))
        ((unless rw-stack)
         (progn$
          (cw
           "Nothing to print. Run (rp::update-rp-brr t rp::rp-state) ~%")
          state))
        (rw-stack (nthcdr (nfix frames-offset) rw-stack)))
       (pp-rw-stack-aux rw-stack frames omit only evisc-tuple
                        untranslate search-source state))))