		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-make/adjust-expr-cast

Build, and adjust if needed, a cast expression.

Signature
(dimb-make/adjust-expr-cast type inc/dec arg) → expr
Arguments: type — Guard (tynamep type).; inc/dec — Guard (inc/dec-op-listp inc/dec).; arg — Guard (exprp arg).
Returns: expr — Type (exprp expr).

This is used to build or adjust a cast expression during disambiguation.

When dimb-expr encounters a cast expression, it recursively disambiguates the type name T0 and the argument expression E0, obtaining a type name T and an argument expression E. Then it should generally return the cast expression (T) E, but there are cases in which an adjustment is needed. Suppose that E0 was an ambiguous cast/binary expression, which gets disambiguated to a binary expression A op B. Then it means that the original code was (T0) A op B, which is a binary expression whose first operand is the cast expression (T0) A and whose second operand is the expression B. Thus, it would be incorrect for dimb-expr to return a cast expression, which would be (T) (A op B). Therefore, dimb-expr uses this function defined here to combine T and E properly, and return the result.

Note that A may be itself a binary expression, e.g. A1 op' A2. Thus, this function must be called recursively when attempting to make a cast out of T and A, because it may need to be adjusted to a binary expression with @'op''), pushing the cast down.

The same kind of adjustment may be needed, besides dimb-expr, also in functions like dimb-cast/and-to-cast, which turns ambiguous expressions of the form ( X ) IncDec & E, which is explained in expr, into cast expressions, possibly also applying the increment/decrement operators IncDec to the & E expression. But note that the parser, when constructing such an ambiguous expression, i.e. an expression of type expr of kind :cast/and-ambig, may need to put an equality binary expression into E (a proper equality expression, or one with higher priority), e.g. we may have (X) ++ & A == B, which must be grouped like [ (X) [ ++ [ & A ] ] ] == B and not like [ (X) [ ++ [ & [ A == B ] ] ] ], where the square brackets describe grouping in the AST but are not part of the syntax. Thus, we need to recursively push the increment/decrement operators in, as we go into possibly nested binary expressions.

This function takes T, IncDec, and E as inputs. If E is not a binary expression, we return the cast expression (T) E. If E is a binary expression, let that be A op B, then we return [ TIncDecA ] op B, where TIncDecA is the result of recursively calling this function on T, IncDec, and A.

The arg input of this function is always a binary expression, or an expression of lower priority. We stop the recursion as soon as the expression is not binary, in which case the expression could be a cast or unary or postfix or primary. If there are no IncDec operators, any of these kinds of expressions is appropriate as argument of the newly constructed cast expression. If there are IncDec operators, then the cast case would not be appropriate, but this should never happen by construction; we double-check that and throw a hard error if that happens. We also throw a hard error if arg has a lower priority than a logical conjunction expression, because that should never happen by construction.

In summary, this function builds and adjusts the expression so that the sub-expressions have priorities greater than or equal to the ones expected by the super-expressions at those place. Another way to express this condition on priorities is that the expression prints without any added parentheses. But this is not a function to adjust all kinds of priority mismatches: it only works on the ones that may arise during disambiguation.

Definitions and Theorems

Function: dimb-make/adjust-expr-cast

(defun dimb-make/adjust-expr-cast (type inc/dec arg)
 (declare (xargs :guard (and (tynamep type)
                             (inc/dec-op-listp inc/dec)
                             (exprp arg))))
 (declare (xargs :guard (and (tyname-unambp type)
                             (expr-unambp arg))))
 (let ((__function__ 'dimb-make/adjust-expr-cast))
  (declare (ignorable __function__))
  (cond
   ((expr-case arg :binary)
    (make-expr-binary
         :op (expr-binary->op arg)
         :arg1 (dimb-make/adjust-expr-cast
                    type inc/dec (expr-binary->arg1 arg))
         :arg2 (expr-binary->arg2 arg)
         :info nil))
   ((expr-priority-< (expr->priority arg)
                     (expr-priority-logand))
    (prog2$ (raise "Internal error: ~x0 has lower priority than &&."
                   arg)
            (expr-fix arg)))
   ((and (consp inc/dec)
         (expr-case arg :cast))
    (prog2$ (raise "Internal error: ~x0 applied to ~x1."
                   inc/dec arg)
            (expr-fix arg)))
   (t (make-expr-cast :type type
                      :arg (apply-pre-inc/dec-ops inc/dec arg))))))

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

(defthm exprp-of-dimb-make/adjust-expr-cast
  (b* ((expr (dimb-make/adjust-expr-cast type inc/dec arg)))
    (exprp expr))
  :rule-classes :rewrite)

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

(defthm expr-unambp-of-dimb-make/adjust-expr-cast
  (implies
       (and (tyname-unambp type)
            (expr-unambp arg))
       (b* ((?expr (dimb-make/adjust-expr-cast type inc/dec arg)))
         (expr-unambp expr))))

Theorem: dimb-make/adjust-expr-cast-of-tyname-fix-type

(defthm dimb-make/adjust-expr-cast-of-tyname-fix-type
  (equal (dimb-make/adjust-expr-cast (tyname-fix type)
                                     inc/dec arg)
         (dimb-make/adjust-expr-cast type inc/dec arg)))

Theorem: dimb-make/adjust-expr-cast-tyname-equiv-congruence-on-type

(defthm dimb-make/adjust-expr-cast-tyname-equiv-congruence-on-type
  (implies
       (tyname-equiv type type-equiv)
       (equal (dimb-make/adjust-expr-cast type inc/dec arg)
              (dimb-make/adjust-expr-cast type-equiv inc/dec arg)))
  :rule-classes :congruence)

Theorem: dimb-make/adjust-expr-cast-of-inc/dec-op-list-fix-inc/dec

(defthm dimb-make/adjust-expr-cast-of-inc/dec-op-list-fix-inc/dec
 (equal
      (dimb-make/adjust-expr-cast type (inc/dec-op-list-fix inc/dec)
                                  arg)
      (dimb-make/adjust-expr-cast type inc/dec arg)))

Theorem: dimb-make/adjust-expr-cast-inc/dec-op-list-equiv-congruence-on-inc/dec

(defthm
 dimb-make/adjust-expr-cast-inc/dec-op-list-equiv-congruence-on-inc/dec
 (implies
      (inc/dec-op-list-equiv inc/dec inc/dec-equiv)
      (equal (dimb-make/adjust-expr-cast type inc/dec arg)
             (dimb-make/adjust-expr-cast type inc/dec-equiv arg)))
 :rule-classes :congruence)

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

(defthm dimb-make/adjust-expr-cast-of-expr-fix-arg
  (equal (dimb-make/adjust-expr-cast type inc/dec (expr-fix arg))
         (dimb-make/adjust-expr-cast type inc/dec arg)))

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

(defthm dimb-make/adjust-expr-cast-expr-equiv-congruence-on-arg
  (implies
       (expr-equiv arg arg-equiv)
       (equal (dimb-make/adjust-expr-cast type inc/dec arg)
              (dimb-make/adjust-expr-cast type inc/dec arg-equiv)))
  :rule-classes :congruence)