• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
      • Clause-processor
        • Meta-extract
        • Set-skip-meta-termp-checks
        • Make-summary-data
        • 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
        • Set-skip-meta-termp-checks!
      • Tau-system
      • Forward-chaining
      • Equivalence
      • Congruence
      • Free-variables
      • Executable-counterpart
      • Induction
      • Type-reasoning
      • Compound-recognizer
      • Rewrite-quoted-constant
      • Elim
      • Well-founded-relation-rule
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Guard-holders
      • Refinement
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • 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))))