Check if a list of type specifiers has formal dynamic semantics, when used to denote an integer type.
(type-spec-list-integer-formalp tyspecs) → yes/no
Cast expressions are supported only if
the destination type name denotes an integer type
that is not the plain
Function:
(defun type-spec-list-integer-formalp (tyspecs) (declare (xargs :guard (type-spec-listp tyspecs))) (declare (xargs :guard (type-spec-list-unambp tyspecs))) (let ((__function__ 'type-spec-list-integer-formalp)) (declare (ignorable __function__)) (b* ((tyspecs (type-spec-list-fix tyspecs))) (or (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-char))) (equal tyspecs (list (type-spec-unsigned) (type-spec-char))) (equal tyspecs (list (type-spec-short))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-short))) (equal tyspecs (list (type-spec-short) (type-spec-int))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-short) (type-spec-int))) (equal tyspecs (list (type-spec-unsigned) (type-spec-short))) (equal tyspecs (list (type-spec-unsigned) (type-spec-short) (type-spec-int))) (equal tyspecs (list (type-spec-int))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-int))) (equal tyspecs (list (type-spec-unsigned))) (equal tyspecs (list (type-spec-unsigned) (type-spec-int))) (equal tyspecs (list (type-spec-long))) (equal tyspecs (list (type-spec-long) (type-spec-int))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-int))) (equal tyspecs (list (type-spec-unsigned) (type-spec-long))) (equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-int))) (equal tyspecs (list (type-spec-long) (type-spec-long))) (equal tyspecs (list (type-spec-long) (type-spec-long) (type-spec-int))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-long))) (equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-long) (type-spec-int))) (equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-long))) (equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-long) (type-spec-int)))))))
Theorem:
(defthm booleanp-of-type-spec-list-integer-formalp (b* ((yes/no (type-spec-list-integer-formalp tyspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm type-spec-list-integer-formalp-of-type-spec-list-fix-tyspecs (equal (type-spec-list-integer-formalp (type-spec-list-fix tyspecs)) (type-spec-list-integer-formalp tyspecs)))
Theorem:
(defthm type-spec-list-integer-formalp-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (type-spec-list-integer-formalp tyspecs) (type-spec-list-integer-formalp tyspecs-equiv))) :rule-classes :congruence)