• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
      • 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
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • ACL2
  • Macro-libraries
  • 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))))