		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-make/adjust-expr-unary

Build, and adjust if needed, a unary expression.

Signature
(dimb-make/adjust-expr-unary op arg) → expr
Arguments: op — Guard (unopp op).; arg — Guard (exprp arg).
Returns: expr — Type (exprp expr).

This is similar to dimb-make/adjust-expr-cast and dimb-make/adjust-expr-binary: see those functions' documentation first. Since some of the unary operators expect a cast expression as argument (as well as an expression with priority higher than a cast), the argument of a unary operators, as produced by the parser, may be an ambiguous cast expression that becomes a binary expression, which has therefore lower priority than a cast expression. This makes it necessary to adjust the expression so that the actual priorities match the expected priorities (where `matching' includes being higher, besides being equal).

For instance, ~ (a) + b is parsed as the unary operator ~ applied to the ambiguous (a) + b, which may be disambiguated to a binary expression, thus resulting (without adjustment) in ~ [ (a) + b ], where the square brackets indicate grouping. Instead, the correct expression is [ ~ (a) ] + b.

So this function builds, and adjusts if needed, a unary expression out of the operator op and operand A. If A has priority greater than or equal to the expected operand priority of op, we just build and return the unary expression. Otherwise, A must be a binary expression, say A1 op' A2. because this is the only kind that may arise from disambiguation with a lower priority than a cast expression; we throw a hard error if that is not the case, which we never expect to happen. To adjust the expression, we push the unary operator into the left operand, i.e. [ op A1 ] op' A2.

Note that A1 may be itself a binary expression, so we need to call this function recursively.

Definitions and Theorems

Function: dimb-make/adjust-expr-unary

(defun dimb-make/adjust-expr-unary (op arg)
 (declare (xargs :guard (and (unopp op) (exprp arg))))
 (declare (xargs :guard (expr-unambp arg)))
 (let ((__function__ 'dimb-make/adjust-expr-unary))
  (declare (ignorable __function__))
  (b*
   ((arg-expected (if (member-eq (unop-kind op)
                                 '(:predec :preinc
                                           :postdec :postinc
                                           :sizeof :alignof))
                      (expr-priority-unary)
                    (expr-priority-cast)))
    (arg-actual (expr->priority arg))
    ((when (expr-priority->= arg-actual arg-expected))
     (make-expr-unary :op op
                      :arg arg
                      :info nil))
    ((unless (expr-case arg :binary))
     (raise
      "Internal error: ~
                non-binary expression ~x0 ~
                used as argument of unary operator ~x1."
      (expr-fix arg)
      (unop-fix op))
     (expr-unary op arg nil)))
   (make-expr-binary
      :op (expr-binary->op arg)
      :arg1 (dimb-make/adjust-expr-unary op (expr-binary->arg1 arg))
      :arg2 (expr-binary->arg2 arg)
      :info nil))))

Theorem: exprp-of-dimb-make/adjust-expr-unary

(defthm exprp-of-dimb-make/adjust-expr-unary
  (b* ((expr (dimb-make/adjust-expr-unary op arg)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-dimb-make/adjust-expr-unary

(defthm expr-unambp-of-dimb-make/adjust-expr-unary
  (implies (expr-unambp arg)
           (b* ((?expr (dimb-make/adjust-expr-unary op arg)))
             (expr-unambp expr))))

Theorem: dimb-make/adjust-expr-unary-of-unop-fix-op

(defthm dimb-make/adjust-expr-unary-of-unop-fix-op
  (equal (dimb-make/adjust-expr-unary (unop-fix op)
                                      arg)
         (dimb-make/adjust-expr-unary op arg)))

Theorem: dimb-make/adjust-expr-unary-unop-equiv-congruence-on-op

(defthm dimb-make/adjust-expr-unary-unop-equiv-congruence-on-op
  (implies (unop-equiv op op-equiv)
           (equal (dimb-make/adjust-expr-unary op arg)
                  (dimb-make/adjust-expr-unary op-equiv arg)))
  :rule-classes :congruence)

Theorem: dimb-make/adjust-expr-unary-of-expr-fix-arg

(defthm dimb-make/adjust-expr-unary-of-expr-fix-arg
  (equal (dimb-make/adjust-expr-unary op (expr-fix arg))
         (dimb-make/adjust-expr-unary op arg)))

Theorem: dimb-make/adjust-expr-unary-expr-equiv-congruence-on-arg

(defthm dimb-make/adjust-expr-unary-expr-equiv-congruence-on-arg
  (implies (expr-equiv arg arg-equiv)
           (equal (dimb-make/adjust-expr-unary op arg)
                  (dimb-make/adjust-expr-unary op arg-equiv)))
  :rule-classes :congruence)