Source and destination ATJ types of a conversion function.
(atj-types-of-conv conv) → (mv src-types dst-types)
This is the inverse of atj-type-conv.
Function:
(defun atj-types-of-conv (conv) (declare (xargs :guard (symbolp conv))) (let ((__function__ 'atj-types-of-conv)) (declare (ignorable __function__)) (b* ((string (symbol-name conv)) ((unless (and (> (length string) 0) (eql (char string 0) #\[) (eql (char string (1- (length string))) #\]))) (raise "Internal error: ~x0 is not a conversion function." conv) (mv (list (atj-type-irrelevant)) (list (atj-type-irrelevant)))) (pos (position #\> string)) ((unless (natp pos)) (raise "Internal error: ~x0 is not a conversion function." conv) (mv (list (atj-type-irrelevant)) (list (atj-type-irrelevant)))) (src-id (subseq string 1 pos)) (dst-id (subseq string (1+ pos) (1- (length string)))) (src-types (atj-types-of-id src-id)) (dst-types (atj-types-of-id dst-id))) (mv src-types dst-types))))
Theorem:
(defthm atj-type-listp-of-atj-types-of-conv.src-types (b* (((mv ?src-types ?dst-types) (atj-types-of-conv conv))) (atj-type-listp src-types)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-listp-of-atj-types-of-conv.dst-types (b* (((mv ?src-types ?dst-types) (atj-types-of-conv conv))) (atj-type-listp dst-types)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-types-of-conv.src-types (b* (((mv ?src-types ?dst-types) (atj-types-of-conv conv))) (consp src-types)) :rule-classes :type-prescription)
Theorem:
(defthm consp-of-atj-types-of-conv.dst-types (b* (((mv ?src-types ?dst-types) (atj-types-of-conv conv))) (consp dst-types)) :rule-classes :type-prescription)