		Search-engine friendly clone of the ACL2 documentation.

Parse-expressions

Vl-mark-as-explicit-parens

Annotate an expression as having explicit parentheses.

Signature
(vl-mark-as-explicit-parens x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x), given the guard.

For some kinds of linting checks, we may want to know whether the original expression had any parens, e.g., we might want to warn the user if they have typed

a & b < c

Because this gets parsed as a & (b < c), which seems strange and may catch the user by surprise. On the other hand, if they've typed

a & (b < c)

Then, as strange as this is, it seems to be what they want, and we probably don't want to complain about it.

But these expressions will be identical after parsing unless we somehow remember where explicit parens were. To facilitate this, we set the VL_EXPLICIT_PARENS attribute on non-atoms that have explicit parens.

Note that we don't bother to set VL_EXPLICIT_PARENS on atoms, e.g., the following really are still parsed equivalently:

(a) & b      vs.    a & b

This is possibly unfortunate, but atoms don't have attributes so what else would we do?

Definitions and Theorems

Function: vl-mark-as-explicit-parens

(defun vl-mark-as-explicit-parens (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-mark-as-explicit-parens))
    (declare (ignorable __function__))
    (b* (((when (vl-fast-atom-p x)) x)
         (atts (vl-nonatom->atts x))
         (atts (acons "VL_EXPLICIT_PARENS" nil atts)))
      (change-vl-nonatom x :atts atts))))

Theorem: vl-expr-p-of-vl-mark-as-explicit-parens

(defthm vl-expr-p-of-vl-mark-as-explicit-parens
  (implies (and (vl-expr-p x))
           (b* ((new-x (vl-mark-as-explicit-parens x)))
             (vl-expr-p new-x)))
  :rule-classes :rewrite)