		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-eval-pure-binop-expr

Propogate a constant through a pure c$::binop.

Signature
(const-prop-eval-pure-binop-expr binop left right) → value?
Arguments: binop — Guard (binopp binop).; left — Guard (c::valuep left).; right — Guard (c::valuep right).
Returns: value? — Type (c::value-optionp value?).

Definitions and Theorems

Function: const-prop-eval-pure-binop-expr

(defun const-prop-eval-pure-binop-expr (binop left right)
 (declare (xargs :guard (and (binopp binop)
                             (c::valuep left)
                             (c::valuep right))))
 (declare (xargs :guard (pure-binopp binop)))
 (let ((__function__ 'const-prop-eval-pure-binop-expr))
  (declare (ignorable __function__))
  (binop-case
   binop
   :mul (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-mul)
                                         left right))
   :div (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-div)
                                         left right))
   :rem (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-rem)
                                         left right))
   :add (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-add)
                                         left right))
   :sub (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-sub)
                                         left right))
   :shl (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-shl)
                                         left right))
   :shr (value-result-to-option
             (c::eval-binary-strict-pure (c::binop-shr)
                                         left right))
   :lt
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-lt)
                                                       left right))
   :gt
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-gt)
                                                       left right))
   :le
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-le)
                                                       left right))
   :ge
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-ge)
                                                       left right))
   :eq
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-eq)
                                                       left right))
   :ne
   (value-result-to-option (c::eval-binary-strict-pure (c::binop-ne)
                                                       left right))
   :bitand (value-result-to-option
                (c::eval-binary-strict-pure (c::binop-bitand)
                                            left right))
   :bitxor (value-result-to-option
                (c::eval-binary-strict-pure (c::binop-bitxor)
                                            left right))
   :bitior (value-result-to-option
                (c::eval-binary-strict-pure (c::binop-bitior)
                                            left right))
   :otherwise nil)))

Theorem: value-optionp-of-const-prop-eval-pure-binop-expr

(defthm value-optionp-of-const-prop-eval-pure-binop-expr
  (b* ((value? (const-prop-eval-pure-binop-expr binop left right)))
    (c::value-optionp value?))
  :rule-classes :rewrite)