		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-binary-strict-pure

Execute a strict pure binary operation on expression values.

Signature
(exec-binary-strict-pure op arg1 arg2) → dval
Arguments: op — Guard (binopp op).; arg1 — Guard (expr-valuep arg1).; arg2 — Guard (expr-valuep arg2).
Returns: dval — Type (expr-value-resultp dval).

This ACL2 function wraps eval-binary-strict-pure to take and return expression values.

First we perform array-to-pointer conversion [C17:5.3.2.1/3], on both operands.

Definitions and Theorems

Function: exec-binary-strict-pure

(defun exec-binary-strict-pure (op arg1 arg2)
  (declare (xargs :guard (and (binopp op)
                              (expr-valuep arg1)
                              (expr-valuep arg2))))
  (declare (xargs :guard (and (binop-strictp op)
                              (binop-purep op))))
  (let ((__function__ 'exec-binary-strict-pure))
    (declare (ignorable __function__))
    (b* ((arg1 (apconvert-expr-value arg1))
         ((when (errorp arg1)) arg1)
         (arg2 (apconvert-expr-value arg2))
         ((when (errorp arg2)) arg2)
         (val1 (expr-value->value arg1))
         (val2 (expr-value->value arg2))
         (val (eval-binary-strict-pure op val1 val2))
         ((when (errorp val)) val))
      (make-expr-value :value val
                       :object nil))))

Theorem: expr-value-resultp-of-exec-binary-strict-pure

(defthm expr-value-resultp-of-exec-binary-strict-pure
  (b* ((dval (exec-binary-strict-pure op arg1 arg2)))
    (expr-value-resultp dval))
  :rule-classes :rewrite)

Theorem: exec-binary-strict-pure-of-binop-fix-op

(defthm exec-binary-strict-pure-of-binop-fix-op
  (equal (exec-binary-strict-pure (binop-fix op)
                                  arg1 arg2)
         (exec-binary-strict-pure op arg1 arg2)))

Theorem: exec-binary-strict-pure-binop-equiv-congruence-on-op

(defthm exec-binary-strict-pure-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (exec-binary-strict-pure op arg1 arg2)
                  (exec-binary-strict-pure op-equiv arg1 arg2)))
  :rule-classes :congruence)

Theorem: exec-binary-strict-pure-of-expr-value-fix-arg1

(defthm exec-binary-strict-pure-of-expr-value-fix-arg1
  (equal (exec-binary-strict-pure op (expr-value-fix arg1)
                                  arg2)
         (exec-binary-strict-pure op arg1 arg2)))

Theorem: exec-binary-strict-pure-expr-value-equiv-congruence-on-arg1

(defthm exec-binary-strict-pure-expr-value-equiv-congruence-on-arg1
  (implies (expr-value-equiv arg1 arg1-equiv)
           (equal (exec-binary-strict-pure op arg1 arg2)
                  (exec-binary-strict-pure op arg1-equiv arg2)))
  :rule-classes :congruence)

Theorem: exec-binary-strict-pure-of-expr-value-fix-arg2

(defthm exec-binary-strict-pure-of-expr-value-fix-arg2
  (equal (exec-binary-strict-pure op arg1 (expr-value-fix arg2))
         (exec-binary-strict-pure op arg1 arg2)))

Theorem: exec-binary-strict-pure-expr-value-equiv-congruence-on-arg2

(defthm exec-binary-strict-pure-expr-value-equiv-congruence-on-arg2
  (implies (expr-value-equiv arg2 arg2-equiv)
           (equal (exec-binary-strict-pure op arg1 arg2)
                  (exec-binary-strict-pure op arg1 arg2-equiv)))
  :rule-classes :congruence)