List of rewrite rules for the return types of models of C integer operations that involve two C integer types.
Definition:
(defconst *atc-integer-ops-2-return-rewrite-rules* (b* ((ops (list 'add 'sub 'mul 'div 'rem 'shl 'shr 'lt 'gt 'le 'ge 'eq 'ne 'bitand 'bitxor 'bitior))) (atc-integer-ops-2-return-names-loop-ops ops *nonchar-integer-types* *nonchar-integer-types*)))
Function:
(defun atc-integer-ops-2-return-names-loop-right-types (op ltype rtypes) (declare (xargs :guard (and (symbolp op) (typep ltype) (type-listp rtypes)))) (declare (xargs :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem 'shl 'shr 'lt 'gt 'le 'ge 'eq 'ne 'bitand 'bitxor 'bitior)) (type-nonchar-integerp ltype) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-integer-ops-2-return-names-loop-right-types)) (declare (ignorable __function__)) (cond ((endp rtypes) nil) (t (b* ((rtype (car rtypes)) (type (cond ((member-eq op '(lt gt le ge eq ne)) (type-sint)) ((member-eq op '(shl shr)) (promote-type ltype)) (t (uaconvert-types ltype rtype)))) (lfixtype (integer-type-to-fixtype ltype)) (rfixtype (integer-type-to-fixtype rtype)) (fixtype (integer-type-to-fixtype type)) (pred (pack fixtype 'p))) (cons (pack pred '-of- op '- lfixtype '- rfixtype) (atc-integer-ops-2-return-names-loop-right-types op ltype (cdr rtypes))))))))
Theorem:
(defthm symbol-listp-of-atc-integer-ops-2-return-names-loop-right-types (b* ((names (atc-integer-ops-2-return-names-loop-right-types op ltype rtypes))) (symbol-listp names)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-2-return-names-loop-left-types (op ltypes rtypes) (declare (xargs :guard (and (symbolp op) (type-listp ltypes) (type-listp rtypes)))) (declare (xargs :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem 'shl 'shr 'lt 'gt 'le 'ge 'eq 'ne 'bitand 'bitxor 'bitior)) (type-nonchar-integer-listp ltypes) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-integer-ops-2-return-names-loop-left-types)) (declare (ignorable __function__)) (cond ((endp ltypes) nil) (t (append (atc-integer-ops-2-return-names-loop-right-types op (car ltypes) rtypes) (atc-integer-ops-2-return-names-loop-left-types op (cdr ltypes) rtypes))))))
Theorem:
(defthm symbol-listp-of-atc-integer-ops-2-return-names-loop-left-types (b* ((names (atc-integer-ops-2-return-names-loop-left-types op ltypes rtypes))) (symbol-listp names)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-2-return-names-loop-ops (ops ltypes rtypes) (declare (xargs :guard (and (symbol-listp ops) (type-listp ltypes) (type-listp rtypes)))) (declare (xargs :guard (and (subsetp-eq ops (list 'add 'sub 'mul 'div 'rem 'shl 'shr 'lt 'gt 'le 'ge 'eq 'ne 'bitand 'bitxor 'bitior)) (type-nonchar-integer-listp ltypes) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-integer-ops-2-return-names-loop-ops)) (declare (ignorable __function__)) (cond ((endp ops) nil) (t (append (atc-integer-ops-2-return-names-loop-left-types (car ops) ltypes rtypes) (atc-integer-ops-2-return-names-loop-ops (cdr ops) ltypes rtypes))))))
Theorem:
(defthm symbol-listp-of-atc-integer-ops-2-return-names-loop-ops (b* ((names (atc-integer-ops-2-return-names-loop-ops ops ltypes rtypes))) (symbol-listp names)) :rule-classes :rewrite)