List of type prescription rules for the models of C integer operations that involve one C integer type.
Definition:
(defconst *atc-integer-ops-1-type-prescription-rules* (b* ((ops '(plus minus bitnot lognot))) (atc-integer-ops-1-type-presc-rules-loop-ops ops *nonchar-integer-types*)))
Function:
(defun atc-integer-ops-1-type-presc-rules-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-type-presc-rules-loop-types)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (b* ((type (car types)) (fixtype (integer-type-to-fixtype type))) (cons (list :t (pack op '- fixtype)) (atc-integer-ops-1-type-presc-rules-loop-types op (cdr types))))))))
Theorem:
(defthm true-list-listp-of-atc-integer-ops-1-type-presc-rules-loop-types (b* ((rules (atc-integer-ops-1-type-presc-rules-loop-types op types))) (true-list-listp rules)) :rule-classes :rewrite)
Function:
(defun atc-integer-ops-1-type-presc-rules-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-type-presc-rules-loop-ops)) (declare (ignorable __function__)) (cond ((endp ops) nil) (t (append (atc-integer-ops-1-type-presc-rules-loop-types (car ops) types) (atc-integer-ops-1-type-presc-rules-loop-ops (cdr ops) types))))))
Theorem:
(defthm true-list-listp-of-atc-integer-ops-1-type-presc-rules-loop-ops (b* ((rule (atc-integer-ops-1-type-presc-rules-loop-ops ops types))) (true-list-listp rule)) :rule-classes :rewrite)