		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-unary-expression

Check if a unary expression is statically well-formed.

Signature
(check-unary-expression op arg arg-result expr ctxt) → result
Arguments: op — Guard (unary-opp op).; arg — Guard (expressionp arg).; arg-result — Guard (type-resultp arg-result).; expr — Guard (expressionp expr).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

The arg-result parameter of this function is the result of checking the operand expression. If it is an error, we propagate it. Otherwise, we dispatch based on the unary operator: each operator's function returns a result, which may add proof obligations to the ones from the operand.

Definitions and Theorems

Function: check-unary-expression

(defun check-unary-expression (op arg arg-result expr ctxt)
 (declare (xargs :guard (and (unary-opp op)
                             (expressionp arg)
                             (type-resultp arg-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (let ((__function__ 'check-unary-expression))
  (declare (ignorable __function__))
  (type-result-case
   arg-result
   :err (type-result-err arg-result.info)
   :ok
   (b* ((type (ensure-single-type arg-result.types)))
    (if (not type)
        (type-result-err (list :type-mismatch-multi
                               (expression-fix arg)
                               arg-result.types))
     (unary-op-case
        op
        :not
        (check-not-expression arg
                              type arg-result.obligations expr ctxt)
        :minus (check-minus-expression
                    arg type
                    arg-result.obligations expr ctxt)))))))

Theorem: type-resultp-of-check-unary-expression

(defthm type-resultp-of-check-unary-expression
 (b* ((result (check-unary-expression op arg arg-result expr ctxt)))
   (type-resultp result))
 :rule-classes :rewrite)

Theorem: check-unary-expression-of-unary-op-fix-op

(defthm check-unary-expression-of-unary-op-fix-op
  (equal (check-unary-expression (unary-op-fix op)
                                 arg arg-result expr ctxt)
         (check-unary-expression op arg arg-result expr ctxt)))

Theorem: check-unary-expression-unary-op-equiv-congruence-on-op

(defthm check-unary-expression-unary-op-equiv-congruence-on-op
 (implies
   (unary-op-equiv op op-equiv)
   (equal
        (check-unary-expression op arg arg-result expr ctxt)
        (check-unary-expression op-equiv arg arg-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-unary-expression-of-expression-fix-arg

(defthm check-unary-expression-of-expression-fix-arg
  (equal (check-unary-expression op (expression-fix arg)
                                 arg-result expr ctxt)
         (check-unary-expression op arg arg-result expr ctxt)))

Theorem: check-unary-expression-expression-equiv-congruence-on-arg

(defthm check-unary-expression-expression-equiv-congruence-on-arg
 (implies
   (expression-equiv arg arg-equiv)
   (equal
        (check-unary-expression op arg arg-result expr ctxt)
        (check-unary-expression op arg-equiv arg-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-unary-expression-of-type-result-fix-arg-result

(defthm check-unary-expression-of-type-result-fix-arg-result
  (equal (check-unary-expression op arg (type-result-fix arg-result)
                                 expr ctxt)
         (check-unary-expression op arg arg-result expr ctxt)))

Theorem: check-unary-expression-type-result-equiv-congruence-on-arg-result

(defthm
  check-unary-expression-type-result-equiv-congruence-on-arg-result
 (implies
   (type-result-equiv arg-result arg-result-equiv)
   (equal
        (check-unary-expression op arg arg-result expr ctxt)
        (check-unary-expression op arg arg-result-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-unary-expression-of-expression-fix-expr

(defthm check-unary-expression-of-expression-fix-expr
 (equal
     (check-unary-expression op arg arg-result (expression-fix expr)
                             ctxt)
     (check-unary-expression op arg arg-result expr ctxt)))

Theorem: check-unary-expression-expression-equiv-congruence-on-expr

(defthm check-unary-expression-expression-equiv-congruence-on-expr
 (implies
   (expression-equiv expr expr-equiv)
   (equal
        (check-unary-expression op arg arg-result expr ctxt)
        (check-unary-expression op arg arg-result expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-unary-expression-of-context-fix-ctxt

(defthm check-unary-expression-of-context-fix-ctxt
 (equal
     (check-unary-expression op
                             arg arg-result expr (context-fix ctxt))
     (check-unary-expression op arg arg-result expr ctxt)))

Theorem: check-unary-expression-context-equiv-congruence-on-ctxt

(defthm check-unary-expression-context-equiv-congruence-on-ctxt
 (implies
   (context-equiv ctxt ctxt-equiv)
   (equal
        (check-unary-expression op arg arg-result expr ctxt)
        (check-unary-expression op arg arg-result expr ctxt-equiv)))
 :rule-classes :congruence)