		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-cast/call-to-call

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

Signature
(dimb-cast/call-to-call fun inc/dec rest) → call-expr
Arguments: fun — Guard (exprp fun).; inc/dec — Guard (inc/dec-op-listp inc/dec).; rest — Guard (exprp rest).
Returns: call-expr — Type (exprp call-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 an expression. The case in which X is a type name is handled in dimb-cast/call-to-call.

In this function, fun is X, inc/dec is IncDec, and rest is (E)Pr. If X is an expression, the increment and decrement operators, if any, are post-increment and post-decrement operators applied to the expression X. We apply them and we form a call expression. To do so, we need to separate (E) and Pr, turn (E) into (E1,...,En) according to the comma operators, and then apply the Pr to the call (X)(E1,...,En).

We perform the latter transformation via a recursion, because we need to go through the individual postfix constructs of Pr, till we reach (E), and then we re-apply the postfix constructs of Pr.

Definitions and Theorems

Function: dimb-cast/call-to-call-loop

(defun dimb-cast/call-to-call-loop (fun rest)
 (declare (xargs :guard (and (exprp fun) (exprp rest))))
 (declare (xargs :guard (and (expr-unambp fun)
                             (expr-unambp rest))))
 (let ((__function__ 'dimb-cast/call-to-call-loop))
  (declare (ignorable __function__))
  (b*
   (((when (expr-case rest :paren))
     (b* ((args (expr-to-asg-expr-list (expr-paren->inner rest))))
       (make-expr-funcall :fun fun
                          :args args)))
    ((when (expr-case rest :arrsub))
     (b*
      ((expr
        (dimb-cast/call-to-call-loop fun (expr-arrsub->arg1 rest))))
      (make-expr-arrsub :arg1 expr
                        :arg2 (expr-arrsub->arg2 rest))))
    ((when (expr-case rest :funcall))
     (b*
      ((expr
        (dimb-cast/call-to-call-loop fun (expr-funcall->fun rest))))
      (make-expr-funcall :fun expr
                         :args (expr-funcall->args rest))))
    ((when (expr-case rest :member))
     (b*
      ((expr
         (dimb-cast/call-to-call-loop fun (expr-member->arg rest))))
      (make-expr-member :arg expr
                        :name (expr-member->name rest))))
    ((when (expr-case rest :memberp))
     (b*
      ((expr
        (dimb-cast/call-to-call-loop fun (expr-memberp->arg rest))))
      (make-expr-memberp :arg expr
                         :name (expr-memberp->name rest)))))
   (prog2$ (raise "Internal error: unexpected expression ~x0."
                  (expr-fix fun))
           (irr-expr)))))

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

(defthm exprp-of-dimb-cast/call-to-call-loop
  (b* ((new-expr (dimb-cast/call-to-call-loop fun rest)))
    (exprp new-expr))
  :rule-classes :rewrite)

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

(defthm expr-unambp-of-dimb-cast/call-to-call-loop
  (implies (and (expr-unambp fun)
                (expr-unambp rest))
           (b* ((?new-expr (dimb-cast/call-to-call-loop fun rest)))
             (expr-unambp new-expr))))

Theorem: dimb-cast/call-to-call-loop-of-expr-fix-fun

(defthm dimb-cast/call-to-call-loop-of-expr-fix-fun
  (equal (dimb-cast/call-to-call-loop (expr-fix fun)
                                      rest)
         (dimb-cast/call-to-call-loop fun rest)))

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

(defthm dimb-cast/call-to-call-loop-expr-equiv-congruence-on-fun
  (implies (expr-equiv fun fun-equiv)
           (equal (dimb-cast/call-to-call-loop fun rest)
                  (dimb-cast/call-to-call-loop fun-equiv rest)))
  :rule-classes :congruence)

Theorem: dimb-cast/call-to-call-loop-of-expr-fix-rest

(defthm dimb-cast/call-to-call-loop-of-expr-fix-rest
  (equal (dimb-cast/call-to-call-loop fun (expr-fix rest))
         (dimb-cast/call-to-call-loop fun rest)))

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

(defthm dimb-cast/call-to-call-loop-expr-equiv-congruence-on-rest
  (implies (expr-equiv rest rest-equiv)
           (equal (dimb-cast/call-to-call-loop fun rest)
                  (dimb-cast/call-to-call-loop fun rest-equiv)))
  :rule-classes :congruence)

Function: dimb-cast/call-to-call

(defun dimb-cast/call-to-call (fun inc/dec rest)
  (declare (xargs :guard (and (exprp fun)
                              (inc/dec-op-listp inc/dec)
                              (exprp rest))))
  (declare (xargs :guard (and (expr-unambp fun)
                              (expr-unambp rest))))
  (let ((__function__ 'dimb-cast/call-to-call))
    (declare (ignorable __function__))
    (b* ((fun (expr-paren fun))
         (fun (apply-post-inc/dec-ops fun inc/dec)))
      (dimb-cast/call-to-call-loop fun rest))))

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

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

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

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

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

(defthm dimb-cast/call-to-call-of-expr-fix-fun
  (equal (dimb-cast/call-to-call (expr-fix fun)
                                 inc/dec rest)
         (dimb-cast/call-to-call fun inc/dec rest)))

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

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

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

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

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

(defthm
 dimb-cast/call-to-call-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-call fun inc/dec rest)
                 (dimb-cast/call-to-call fun inc/dec-equiv rest)))
 :rule-classes :congruence)

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

(defthm dimb-cast/call-to-call-of-expr-fix-rest
  (equal (dimb-cast/call-to-call fun inc/dec (expr-fix rest))
         (dimb-cast/call-to-call fun inc/dec rest)))

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

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