Execute a unary operator, on an expression value.
(exec-unary op arg env) → evalue+denv
We coerce the expression value to a value if needed. We apply the operator. The result is a value. The environment is unchanged.
Function:
(defun exec-unary (op arg env) (declare (xargs :guard (and (unopp op) (expr-valuep arg) (denvp env)))) (let ((__function__ 'exec-unary)) (declare (ignorable __function__)) (b* (((okf arg) (expr-value-to-value arg env)) ((okf val) (unop-case op :not (op-not arg) :neg (op-neg arg (denv->curve env)) :abs (op-abs arg) :abs-wrapped (op-abs-wrapped arg) :double (op-double arg (denv->curve env)) :inv (op-inv arg (denv->curve env)) :square (op-square arg (denv->curve env)) :square-root (op-square-root arg (denv->curve env)))) (eval (expr-value-value val))) (make-evalue+denv :evalue eval :denv (denv-fix env)))))
Theorem:
(defthm evalue+denv-resultp-of-exec-unary (b* ((evalue+denv (exec-unary op arg env))) (evalue+denv-resultp evalue+denv)) :rule-classes :rewrite)
Theorem:
(defthm exec-unary-of-unop-fix-op (equal (exec-unary (unop-fix op) arg env) (exec-unary op arg env)))
Theorem:
(defthm exec-unary-unop-equiv-congruence-on-op (implies (unop-equiv op op-equiv) (equal (exec-unary op arg env) (exec-unary op-equiv arg env))) :rule-classes :congruence)
Theorem:
(defthm exec-unary-of-expr-value-fix-arg (equal (exec-unary op (expr-value-fix arg) env) (exec-unary op arg env)))
Theorem:
(defthm exec-unary-expr-value-equiv-congruence-on-arg (implies (expr-value-equiv arg arg-equiv) (equal (exec-unary op arg env) (exec-unary op arg-equiv env))) :rule-classes :congruence)
Theorem:
(defthm exec-unary-of-denv-fix-env (equal (exec-unary op arg (denv-fix env)) (exec-unary op arg env)))
Theorem:
(defthm exec-unary-denv-equiv-congruence-on-env (implies (denv-equiv env env-equiv) (equal (exec-unary op arg env) (exec-unary op arg env-equiv))) :rule-classes :congruence)