List of type prescription rules for the models of C integer operations that involve two C integer types.
Definition:
(defconst *atc-integer-ops-2-type-prescription-rules* (b* ((ops (list 'add 'sub 'mul 'div 'rem 'shl 'shr 'lt 'gt 'le 'ge 'eq 'ne 'bitand 'bitxor 'bitior))) (atc-integer-ops-2-type-presc-rules-loop-ops ops *nonchar-integer-types* *nonchar-integer-types*)))
Function:
(defun atc-integer-ops-2-type-presc-rules-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-type-presc-rules-loop-right-types)) (declare (ignorable __function__)) (cond ((endp rtypes) nil) (t (b* ((rtype (car rtypes)) (lfixtype (integer-type-to-fixtype ltype)) (rfixtype (integer-type-to-fixtype rtype))) (cons (list :t (pack op '- lfixtype '- rfixtype)) (atc-integer-ops-2-type-presc-rules-loop-right-types op ltype (cdr rtypes))))))))
Theorem:
(defthm true-list-listp-of-atc-integer-ops-2-type-presc-rules-loop-right-types (b* ((rules (atc-integer-ops-2-type-presc-rules-loop-right-types op ltype rtypes))) (true-list-listp rules)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-2-type-presc-rules-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-type-presc-rules-loop-left-types)) (declare (ignorable __function__)) (cond ((endp ltypes) nil) (t (append (atc-integer-ops-2-type-presc-rules-loop-right-types op (car ltypes) rtypes) (atc-integer-ops-2-type-presc-rules-loop-left-types op (cdr ltypes) rtypes))))))
Theorem:
(defthm true-list-listp-of-atc-integer-ops-2-type-presc-rules-loop-left-types (b* ((rules (atc-integer-ops-2-type-presc-rules-loop-left-types op ltypes rtypes))) (true-list-listp rules)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-2-type-presc-rules-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-type-presc-rules-loop-ops)) (declare (ignorable __function__)) (cond ((endp ops) nil) (t (append (atc-integer-ops-2-type-presc-rules-loop-left-types (car ops) ltypes rtypes) (atc-integer-ops-2-type-presc-rules-loop-ops (cdr ops) ltypes rtypes))))))
Theorem:
(defthm true-list-listp-of-atc-integer-ops-2-type-presc-rules-loop-ops (b* ((rules (atc-integer-ops-2-type-presc-rules-loop-ops ops ltypes rtypes))) (true-list-listp rules)) :rule-classes :rewrite)