		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-cast/call-to-cast

Disambiguate an ambiguous cast or call expression to be a cast expression.

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

The form (X) IncDec (E)Pr of an ambiguous call or cast expression is described in detail in expr: refer to that description. This ambiguous expression is disambiguated in dimb-expr, by first disambiguating whether X is a type name or an expression. Based on that, the constituents of that ambiguous expression must be re-arranged into an unambiguous expression: this is done by this function, for the case in which X is a type name. The case in which X is an expression is handled in dimb-cast/call-to-call.

In this function, tyname is X, inc/dec is IncDec, and arg is (E)Pr. If X is a type name, the increment and decrement operators, if any, are pre-increment and pre-decrement operators applied to the expression (E)Pr.

Definitions and Theorems

Function: dimb-cast/call-to-cast

(defun dimb-cast/call-to-cast (tyname inc/dec arg)
  (declare (xargs :guard (and (tynamep tyname)
                              (inc/dec-op-listp inc/dec)
                              (exprp arg))))
  (declare (xargs :guard (and (tyname-unambp tyname)
                              (expr-unambp arg))))
  (let ((__function__ 'dimb-cast/call-to-cast))
    (declare (ignorable __function__))
    (dimb-make/adjust-expr-cast tyname inc/dec arg)))

Theorem: exprp-of-dimb-cast/call-to-cast

(defthm exprp-of-dimb-cast/call-to-cast
  (b* ((cast-expr (dimb-cast/call-to-cast tyname inc/dec arg)))
    (exprp cast-expr))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-dimb-cast/call-to-cast

(defthm expr-unambp-of-dimb-cast/call-to-cast
 (implies
      (and (tyname-unambp tyname)
           (expr-unambp arg))
      (b* ((?cast-expr (dimb-cast/call-to-cast tyname inc/dec arg)))
        (expr-unambp cast-expr))))

Theorem: dimb-cast/call-to-cast-of-tyname-fix-tyname

(defthm dimb-cast/call-to-cast-of-tyname-fix-tyname
  (equal (dimb-cast/call-to-cast (tyname-fix tyname)
                                 inc/dec arg)
         (dimb-cast/call-to-cast tyname inc/dec arg)))

Theorem: dimb-cast/call-to-cast-tyname-equiv-congruence-on-tyname

(defthm dimb-cast/call-to-cast-tyname-equiv-congruence-on-tyname
 (implies (tyname-equiv tyname tyname-equiv)
          (equal (dimb-cast/call-to-cast tyname inc/dec arg)
                 (dimb-cast/call-to-cast tyname-equiv inc/dec arg)))
 :rule-classes :congruence)

Theorem: dimb-cast/call-to-cast-of-inc/dec-op-list-fix-inc/dec

(defthm dimb-cast/call-to-cast-of-inc/dec-op-list-fix-inc/dec
 (equal (dimb-cast/call-to-cast tyname (inc/dec-op-list-fix inc/dec)
                                arg)
        (dimb-cast/call-to-cast tyname inc/dec arg)))

Theorem: dimb-cast/call-to-cast-inc/dec-op-list-equiv-congruence-on-inc/dec

(defthm
 dimb-cast/call-to-cast-inc/dec-op-list-equiv-congruence-on-inc/dec
 (implies (inc/dec-op-list-equiv inc/dec inc/dec-equiv)
          (equal (dimb-cast/call-to-cast tyname inc/dec arg)
                 (dimb-cast/call-to-cast tyname inc/dec-equiv arg)))
 :rule-classes :congruence)

Theorem: dimb-cast/call-to-cast-of-expr-fix-arg

(defthm dimb-cast/call-to-cast-of-expr-fix-arg
  (equal (dimb-cast/call-to-cast tyname inc/dec (expr-fix arg))
         (dimb-cast/call-to-cast tyname inc/dec arg)))

Theorem: dimb-cast/call-to-cast-expr-equiv-congruence-on-arg

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