		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-make/adjust-expr-label-addr

Build, and adjust if needed, a label address expression.

Signature
(dimb-make/adjust-expr-label-addr arg) → expr
Arguments: arg — Guard (exprp arg).
Returns: expr — Type (exprp expr).

This is analogous to dimb-make/adjust-expr-unary, but for label address expression, which are conceptually similar to unary expressions, but have a different AST structure.

The unary operator && expects an identifier, so we test directly for that. If the argument is not an identifier, it must be a binary expression; the caller takes care of checking this.

Definitions and Theorems

Function: dimb-make/adjust-expr-label-addr

(defun dimb-make/adjust-expr-label-addr (arg)
 (declare (xargs :guard (exprp arg)))
 (declare (xargs :guard (expr-unambp arg)))
 (let ((__function__ 'dimb-make/adjust-expr-label-addr))
  (declare (ignorable __function__))
  (b*
   (((when (expr-case arg :ident))
     (expr-label-addr (expr-ident->ident arg)))
    ((unless (expr-case arg :binary))
     (raise
      "Internal error: ~
                non-binary expression ~x0 ~
                used as argument of unary operator &&."
      (expr-fix arg))
     (expr-fix arg)))
   (make-expr-binary
    :op (expr-binary->op arg)
    :arg1 (dimb-make/adjust-expr-label-addr (expr-binary->arg1 arg))
    :arg2 (expr-binary->arg2 arg)
    :info nil))))

Theorem: exprp-of-dimb-make/adjust-expr-label-addr

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

Theorem: expr-unambp-of-dimb-make/adjust-expr-label-addr

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

Theorem: dimb-make/adjust-expr-label-addr-of-expr-fix-arg

(defthm dimb-make/adjust-expr-label-addr-of-expr-fix-arg
  (equal (dimb-make/adjust-expr-label-addr (expr-fix arg))
         (dimb-make/adjust-expr-label-addr arg)))

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

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