		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Eval-unary

Evaluate a unary operation that does not involve pointers, on a value, returning a value.

Signature
(eval-unary op arg) → val
Arguments: op — Guard (unopp op).; arg — Guard (valuep arg).
Returns: val — Type (value-resultp val).

Definitions and Theorems

Function: eval-unary

(defun eval-unary (op arg)
  (declare (xargs :guard (and (unopp op) (valuep arg))))
  (declare (xargs :guard (unop-nonpointerp op)))
  (let ((__function__ 'eval-unary))
    (declare (ignorable __function__))
    (case (unop-kind op)
      (:plus (plus-value arg))
      (:minus (minus-value arg))
      (:bitnot (bitnot-value arg))
      (:lognot (lognot-value arg))
      (t (error (impossible))))))

Theorem: value-resultp-of-eval-unary

(defthm value-resultp-of-eval-unary
  (b* ((val (eval-unary op arg)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-unary-of-unop-fix-op

(defthm eval-unary-of-unop-fix-op
  (equal (eval-unary (unop-fix op) arg)
         (eval-unary op arg)))

Theorem: eval-unary-unop-equiv-congruence-on-op

(defthm eval-unary-unop-equiv-congruence-on-op
  (implies (unop-equiv op op-equiv)
           (equal (eval-unary op arg)
                  (eval-unary op-equiv arg)))
  :rule-classes :congruence)

Theorem: eval-unary-of-value-fix-arg

(defthm eval-unary-of-value-fix-arg
  (equal (eval-unary op (value-fix arg))
         (eval-unary op arg)))

Theorem: eval-unary-value-equiv-congruence-on-arg

(defthm eval-unary-value-equiv-congruence-on-arg
  (implies (value-equiv arg arg-equiv)
           (equal (eval-unary op arg)
                  (eval-unary op arg-equiv)))
  :rule-classes :congruence)