		Search-engine friendly clone of the ACL2 documentation.

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 (see origexprs), 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.)

This only works if the origexprs transform is run early in the transformation sequence. When there's no VL_ORIG_EXPR attribute, we just print x as is.

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* (((when (vl-fast-atom-p x))
          (vl-pp-atom x))
         (atts (vl-nonatom->atts x))
         (lookup (cdr (hons-assoc-equal "VL_ORIG_EXPR" atts)))
         ((when lookup) (vl-pp-expr lookup)))
      (vl-pp-expr x))))

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)