List of type prescription rules for the models of C integer conversions.
Definition:
(defconst *atc-integer-convs-type-prescription-rules* (atc-integer-convs-type-presc-rules-loop-src-types *nonchar-integer-types* *nonchar-integer-types*))
Function:
(defun atc-integer-convs-type-presc-rules-loop-dst-types (stype dtypes) (declare (xargs :guard (and (typep stype) (type-listp dtypes)))) (declare (xargs :guard (and (type-nonchar-integerp stype) (type-nonchar-integer-listp dtypes)))) (let ((__function__ 'atc-integer-convs-type-presc-rules-loop-dst-types)) (declare (ignorable __function__)) (cond ((endp dtypes) nil) ((equal stype (car dtypes)) (atc-integer-convs-type-presc-rules-loop-dst-types stype (cdr dtypes))) (t (b* ((sfixtype (integer-type-to-fixtype stype)) (dfixtype (integer-type-to-fixtype (car dtypes)))) (cons (list :t (pack dfixtype '-from- sfixtype)) (atc-integer-convs-type-presc-rules-loop-dst-types stype (cdr dtypes))))))))
Theorem:
(defthm true-list-listp-of-atc-integer-convs-type-presc-rules-loop-dst-types (b* ((rules (atc-integer-convs-type-presc-rules-loop-dst-types stype dtypes))) (true-list-listp rules)) :rule-classes :rewrite)
Function:
(defun atc-integer-convs-type-presc-rules-loop-src-types (stypes dtypes) (declare (xargs :guard (and (type-listp stypes) (type-listp dtypes)))) (declare (xargs :guard (and (type-nonchar-integer-listp stypes) (type-nonchar-integer-listp dtypes)))) (let ((__function__ 'atc-integer-convs-type-presc-rules-loop-src-types)) (declare (ignorable __function__)) (cond ((endp stypes) nil) (t (append (atc-integer-convs-type-presc-rules-loop-dst-types (car stypes) dtypes) (atc-integer-convs-type-presc-rules-loop-src-types (cdr stypes) dtypes))))))
Theorem:
(defthm true-list-listp-of-atc-integer-convs-type-presc-rules-loop-src-types (b* ((rules (atc-integer-convs-type-presc-rules-loop-src-types stypes dtypes))) (true-list-listp rules)) :rule-classes :rewrite)