		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-make/adjust-expr-binary

Build, and adjust if needed, a binary expression.

Signature
(dimb-make/adjust-expr-binary op arg1 arg2) → expr
Arguments: op — Guard (binopp op).; arg1 — Guard (exprp arg1).; arg2 — Guard (exprp arg2).
Returns: expr — Type (exprp expr).

This has a similar purpose to dimb-make/adjust-expr-cast: see that function's documentation first. The same kind of incorrect grouping (prevented by the use of dimb-make/adjust-expr-cast) may arise with a binary expression A0 op B0. When encountering such a binary expression, dimb-expr first disambiguates A0 to A and B0 to B. But if A0 and/or B0 were ambiguous cast/binary expressions, and one or both get disambiguated to binary expressions, returning the expression A op B could be incorrect. For instance, op could be *, A could be a variable x, and B could be the expression (y) & z where y and z are variables. That is, A op B is x * (y) & z, which must be grouped as [ x * (y) ] & z (where the square brackets indicate the grouping), and not as x * [ (y) & z ]. The cue is that the priority of (y) & z is lower than the expected priority of the right operand of *: since our parser preserves parenthesized expressions, it should be the case that, in the AST, each sub-expression has priority greater than or equal to the expected priority by the super-expression at that place. So the adjustment performed by this function, like the one performed by dimb-make/adjust-expr-cast, can be seen as restoring that property of ASTs.

This function assumes that arg1 and arg2 already satisfy the property about priorities mentioned above, which is in fact the case when this function is called. This function attempts to construct the binary expression, but adjusts it so that the prioperty on priorities will hold. We compare the expected priorities for the left and right operand of op with the actual priorities of arg1 and arg2. Since each may match or mismatch, there are four possibilities. This may be a bit more general than needed in the disambiguator, because for instance the expression (x) + y * (z) & w could not lead, without adjustment, to [ (x) + y ] * [ (z) & w ], because the parser would parse all of y * (z) & w after the +, but the generality is easier to handle, compared to establishing restrictions on what the parser can produce. So we consider a case like [ (x) + y ] * [ (z) & w ] possible, with both sub-expressions mismatching, in the sense of having priority lower than expected by op.

A mismatch should be possible only if the sub-expression is a binary one, because the only decrease in priority during disambiguation can happen when the lower-priority expression is a binary one. We throw a hard error if that is not the case, which we expect to never happen.

If there is no mismatch, we just build the binary expression.

If only one sub-expression mismatches, we perform the adjustment by moving up the sub-expression's operator and redirecting one of its operands to the lowered operator. For instance, consider the adjustment from A * [ B + C ] to [ A * B ] + C:

  *               +    
 /              /    
A   +    --->   *   C  
   /          /      
  B   C       A   B

where the + is moved up and its operand B is redirected under the lowered *. The situation is symmetric if the expression is flipped, i.e. if the mismatch is in the left operand instead of the right one.

But note that, in the example above, B itself could be a + expression, which is now under *, and therefore needs to be adjusted. So the adjustment may need to be recursive: we recursively call this function to build the new binary sub-expression.

If both sub-expressions mismatch, we compare the priorities of the two sub-expressions, and we perform the adjustment as if only the lower-priority one mismatches. For instance, consider [ A & B ] * [ C + D ]: since & has lower priority than +, we move the & up, not the +. This results in A & [ B * [ C + D ] ], where the [ B * [ C + D ] ] is recursively adjusted: this further adjustment moves up the +, but it does not need to go above the &, which has lower priority; the result is then A & [ [ B * C] + D ].

The case in which the two mismatching sub-expressions have the same priority is handled in the same way as when the right one has lower priority. The reason for this asymmetry is that all the binary operations involved are left-associative. For instance, consider [ A + B ] * [ C + D ]. The correct adjustment is [ A + [ B * C ] ] + D, not [A + [ [ B * C ] + D ].

Definitions and Theorems

Function: dimb-make/adjust-expr-binary

(defun dimb-make/adjust-expr-binary (op arg1 arg2)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1)
                             (exprp arg2))))
 (declare (xargs :guard (and (expr-unambp arg1)
                             (expr-unambp arg2))))
 (let ((__function__ 'dimb-make/adjust-expr-binary))
  (declare (ignorable __function__))
  (b*
   (((mv arg1-expected arg2-expected)
     (binop-expected-priorities op))
    (arg1-actual (expr->priority arg1))
    (arg2-actual (expr->priority arg2))
    (arg1-mismatch (expr-priority-< arg1-actual arg1-expected))
    (arg2-mismatch (expr-priority-< arg2-actual arg2-expected))
    ((when (and arg1-mismatch
                (not (expr-case arg1 :binary))))
     (raise
      "Internal error: ~
                non-binary expression ~x0 ~
                used as left argument of binary operator ~x1."
      (expr-fix arg1)
      (binop-fix op))
     (expr-binary op arg1 arg2 nil))
    ((when (and arg2-mismatch
                (not (expr-case arg2 :binary))))
     (raise
      "Internal error: ~
                non-binary expression ~x0 ~
                used as right argument of binary operator ~x1."
      (expr-fix arg2)
      (binop-fix op))
     (expr-binary op arg1 arg2 nil)))
   (cond
    ((and arg1-mismatch
          (or (not arg2-mismatch)
              (expr-priority-> arg1-actual arg2-actual)))
     (b*
      ((new-op (expr-binary->op arg1))
       (new-arg1 (expr-binary->arg1 arg1))
       (new-arg2
           (dimb-make/adjust-expr-binary op (expr-binary->arg2 arg1)
                                         arg2)))
      (make-expr-binary :op new-op
                        :arg1 new-arg1
                        :arg2 new-arg2
                        :info nil)))
    ((and arg2-mismatch
          (or (not arg1-mismatch)
              (expr-priority-<= arg1-actual arg2-actual)))
     (b* ((new-op (expr-binary->op arg2))
          (new-arg1 (dimb-make/adjust-expr-binary
                         op arg1 (expr-binary->arg1 arg2)))
          (new-arg2 (expr-binary->arg2 arg2)))
       (make-expr-binary :op new-op
                         :arg1 new-arg1
                         :arg2 new-arg2
                         :info nil)))
    (t (make-expr-binary :op op
                         :arg1 arg1
                         :arg2 arg2
                         :info nil))))))

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

(defthm exprp-of-dimb-make/adjust-expr-binary
  (b* ((expr (dimb-make/adjust-expr-binary op arg1 arg2)))
    (exprp expr))
  :rule-classes :rewrite)

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

(defthm expr-unambp-of-dimb-make/adjust-expr-binary
  (implies (and (expr-unambp arg1)
                (expr-unambp arg2))
           (b* ((?expr (dimb-make/adjust-expr-binary op arg1 arg2)))
             (expr-unambp expr))))

Theorem: dimb-make/adjust-expr-binary-of-binop-fix-op

(defthm dimb-make/adjust-expr-binary-of-binop-fix-op
  (equal (dimb-make/adjust-expr-binary (binop-fix op)
                                       arg1 arg2)
         (dimb-make/adjust-expr-binary op arg1 arg2)))

Theorem: dimb-make/adjust-expr-binary-binop-equiv-congruence-on-op

(defthm dimb-make/adjust-expr-binary-binop-equiv-congruence-on-op
 (implies (binop-equiv op op-equiv)
          (equal (dimb-make/adjust-expr-binary op arg1 arg2)
                 (dimb-make/adjust-expr-binary op-equiv arg1 arg2)))
 :rule-classes :congruence)

Theorem: dimb-make/adjust-expr-binary-of-expr-fix-arg1

(defthm dimb-make/adjust-expr-binary-of-expr-fix-arg1
  (equal (dimb-make/adjust-expr-binary op (expr-fix arg1)
                                       arg2)
         (dimb-make/adjust-expr-binary op arg1 arg2)))

Theorem: dimb-make/adjust-expr-binary-expr-equiv-congruence-on-arg1

(defthm dimb-make/adjust-expr-binary-expr-equiv-congruence-on-arg1
 (implies (expr-equiv arg1 arg1-equiv)
          (equal (dimb-make/adjust-expr-binary op arg1 arg2)
                 (dimb-make/adjust-expr-binary op arg1-equiv arg2)))
 :rule-classes :congruence)

Theorem: dimb-make/adjust-expr-binary-of-expr-fix-arg2

(defthm dimb-make/adjust-expr-binary-of-expr-fix-arg2
  (equal (dimb-make/adjust-expr-binary op arg1 (expr-fix arg2))
         (dimb-make/adjust-expr-binary op arg1 arg2)))

Theorem: dimb-make/adjust-expr-binary-expr-equiv-congruence-on-arg2

(defthm dimb-make/adjust-expr-binary-expr-equiv-congruence-on-arg2
 (implies (expr-equiv arg2 arg2-equiv)
          (equal (dimb-make/adjust-expr-binary op arg1 arg2)
                 (dimb-make/adjust-expr-binary op arg1 arg2-equiv)))
 :rule-classes :congruence)