		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-origexpr

Pretty-print the "original," un-transformed version of an expression.

Signature
(vl-pp-origexpr x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-expr-p x).

This is like vl-pp-expr but, if x has a VL_ORIG_EXPR attribute, we actually pretty-print the original version of x rather than the current version (which may be simplified, and hence not correspond as closely to the original source code.) Specifically, the elaboration transform may replace certain subexpressions with constants and leave behind an annotation giving the original version of x.

Definitions and Theorems

Function: vl-pp-origexpr-fn

(defun vl-pp-origexpr-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-pp-origexpr))
    (declare (ignorable __function__))
    (b* ((misc (vl-ps->misc))
         (prev-p (vl-ps->use-origexprs-p)))
      (vl-ps-seq (if (not prev-p)
                     (vl-ps-update-use-origexprs t)
                   ps)
                 (vl-pp-expr x)
                 (vl-ps-update-misc misc)))))

Theorem: vl-pp-origexpr-fn-of-vl-expr-fix-x

(defthm vl-pp-origexpr-fn-of-vl-expr-fix-x
  (equal (vl-pp-origexpr-fn (vl-expr-fix x) ps)
         (vl-pp-origexpr-fn x ps)))

Theorem: vl-pp-origexpr-fn-vl-expr-equiv-congruence-on-x

(defthm vl-pp-origexpr-fn-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-pp-origexpr-fn x ps)
                  (vl-pp-origexpr-fn x-equiv ps)))
  :rule-classes :congruence)