List of rewrite rules for the return types of models of C integer operations that involve one C integer type.
Definition:
(defconst *atc-integer-ops-1-return-rewrite-rules* (b* ((ops '(plus minus bitnot lognot))) (atc-integer-ops-1-return-names-loop-ops ops *nonchar-integer-types*)))
Function:
(defun atc-integer-ops-1-return-names-loop-types (op types) (declare (xargs :guard (and (symbolp op) (type-listp types)))) (declare (xargs :guard (and (member-eq op '(plus minus bitnot lognot)) (type-nonchar-integer-listp types)))) (let ((__function__ 'atc-integer-ops-1-return-names-loop-types)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (b* ((type (car types)) (argfixtype (integer-type-to-fixtype type)) (restype (if (eq op 'lognot) (type-sint) (promote-type type))) (resfixtype (integer-type-to-fixtype restype)) (respred (pack resfixtype 'p))) (cons (pack respred '-of- op '- argfixtype) (atc-integer-ops-1-return-names-loop-types op (cdr types))))))))
Theorem:
(defthm symbol-listp-of-atc-integer-ops-1-return-names-loop-types (b* ((names (atc-integer-ops-1-return-names-loop-types op types))) (symbol-listp names)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-1-return-names-loop-ops (ops types) (declare (xargs :guard (and (symbol-listp ops) (type-listp types)))) (declare (xargs :guard (and (subsetp-eq ops '(plus minus bitnot lognot)) (type-nonchar-integer-listp types)))) (let ((__function__ 'atc-integer-ops-1-return-names-loop-ops)) (declare (ignorable __function__)) (cond ((endp ops) nil) (t (append (atc-integer-ops-1-return-names-loop-types (car ops) types) (atc-integer-ops-1-return-names-loop-ops (cdr ops) types))))))
Theorem:
(defthm symbol-listp-of-atc-integer-ops-1-return-names-loop-ops (b* ((names (atc-integer-ops-1-return-names-loop-ops ops types))) (symbol-listp names)) :rule-classes :rewrite)