		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-unop

Check if a term may represent a unary expression.

Signature
(atc-check-unop term) → (mv erp yes/no fn arg in-type out-type op)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; arg — Type (pseudo-termp arg).; in-type — Type (typep in-type).; out-type — Type (typep out-type).; op — Type (unopp op).

If the term is a call of one of the ACL2 functions that represent C unary operators, we return the function, the argument term the input and output types, and the C operator.

If the term does not have that form, we return an indication of failure. The term may represent some other kind of C expression.

Definitions and Theorems

Function: atc-check-unop

(defun atc-check-unop (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-unop))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil (irr-type)
     (irr-type)
     (irr-unop))
    ((acl2::fun (no))
     (retok nil nil nil (irr-type)
            (irr-type)
            (irr-unop)))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp op fixtype)
     (atc-check-symbol-2part fn))
    (in-type (fixtype-to-integer-type fixtype))
    ((unless (and okp
                  (member-eq op '(plus minus bitnot lognot))
                  in-type))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of an integer unary operation function, ~
                      but it is not in the \"C\" package."
       fn)))
    ((unless (list-lenp 1 args))
     (reterr (raise "Internal error: ~x0 not applied to 1 argument."
                    term)))
    (arg (first args))
    ((mv out-type unop)
     (case op
       (plus (mv (promote-type in-type) (unop-plus)))
       (minus (mv (promote-type in-type)
                  (unop-minus)))
       (bitnot (mv (promote-type in-type)
                   (unop-bitnot)))
       (lognot (mv (type-sint) (unop-lognot)))
       (t (prog2$ (impossible)
                  (mv (irr-type) (irr-unop)))))))
   (retok t fn arg in-type out-type unop))))

Theorem: booleanp-of-atc-check-unop.yes/no

(defthm booleanp-of-atc-check-unop.yes/no
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-unop.fn

(defthm symbolp-of-atc-check-unop.fn
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-unop.arg

(defthm pseudo-termp-of-atc-check-unop.arg
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (pseudo-termp arg))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-unop.in-type

(defthm typep-of-atc-check-unop.in-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (typep in-type))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-unop.out-type

(defthm typep-of-atc-check-unop.out-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (typep out-type))
  :rule-classes :rewrite)

Theorem: unopp-of-atc-check-unop.op

(defthm unopp-of-atc-check-unop.op
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (unopp op))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-unop-arg

(defthm pseudo-term-count-of-atc-check-unop-arg
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (implies yes/no
             (< (pseudo-term-count arg)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: type-nonchar-integerp-of-atc-check-unop-in-type

(defthm type-nonchar-integerp-of-atc-check-unop-in-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (implies yes/no
             (type-nonchar-integerp in-type))))

Theorem: type-nonchar-integerp-of-atc-check-unop-out-type

(defthm type-nonchar-integerp-of-atc-check-unop-out-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?arg ?in-type ?out-type ?op)
        (atc-check-unop term)))
    (implies yes/no
             (type-nonchar-integerp out-type))))