		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-conv

Check if a term may represent a conversion.

Signature
(atc-check-conv term) → (mv erp yes/no fn arg in-type out-type out-tyname)
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).; out-tyname — Type (tynamep out-tyname).

If the term is a call of one of the ACL2 functions that represents C integer conversions, we return the function, the argument term, the input (i.e. argument) type, the output type, and the C output type name. The type name is redundant, because it can be determined from the output type, but we return it for the callers' convenience, since this kind of ACL2 term represents a C cast.

If the term does not have the form explained above, we return an indication of failure.

Definitions and Theorems

Function: atc-check-conv

(defun atc-check-conv (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-conv))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil (irr-type)
     (irr-type)
     (irr-tyname))
    ((acl2::fun (no))
     (retok nil nil nil (irr-type)
            (irr-type)
            (irr-tyname)))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp dtype from stype)
     (atc-check-symbol-3part fn))
    (in-type (fixtype-to-integer-type stype))
    (out-type (fixtype-to-integer-type dtype))
    ((unless (and okp (eq from 'from)
                  in-type out-type))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of an integer conversion 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))
    (out-tyname (type-to-tyname out-type)))
   (retok t fn arg in-type out-type out-tyname))))

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

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

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

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

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

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

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

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

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

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

Theorem: tynamep-of-atc-check-conv.out-tyname

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

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

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