ATJ type identified by a short string.
This is the inverse of atj-type-id.
Function:
(defun atj-type-of-id (id) (declare (xargs :guard (stringp id))) (let ((__function__ 'atj-type-of-id)) (declare (ignorable __function__)) (cond ((equal id "AI") (atj-type-acl2 (atj-atype-integer))) ((equal id "AR") (atj-type-acl2 (atj-atype-rational))) ((equal id "AN") (atj-type-acl2 (atj-atype-number))) ((equal id "AC") (atj-type-acl2 (atj-atype-character))) ((equal id "AS") (atj-type-acl2 (atj-atype-string))) ((equal id "AY") (atj-type-acl2 (atj-atype-symbol))) ((equal id "AB") (atj-type-acl2 (atj-atype-boolean))) ((equal id "AP") (atj-type-acl2 (atj-atype-cons))) ((equal id "AV") (atj-type-acl2 (atj-atype-value))) ((equal id "JZ") (atj-type-jprim (primitive-type-boolean))) ((equal id "JC") (atj-type-jprim (primitive-type-char))) ((equal id "JB") (atj-type-jprim (primitive-type-byte))) ((equal id "JS") (atj-type-jprim (primitive-type-short))) ((equal id "JI") (atj-type-jprim (primitive-type-int))) ((equal id "JJ") (atj-type-jprim (primitive-type-long))) ((equal id "JF") (atj-type-jprim (primitive-type-float))) ((equal id "JD") (atj-type-jprim (primitive-type-double))) ((equal id "YZ") (atj-type-jprimarr (primitive-type-boolean))) ((equal id "YC") (atj-type-jprimarr (primitive-type-char))) ((equal id "YB") (atj-type-jprimarr (primitive-type-byte))) ((equal id "YS") (atj-type-jprimarr (primitive-type-short))) ((equal id "YI") (atj-type-jprimarr (primitive-type-int))) ((equal id "YJ") (atj-type-jprimarr (primitive-type-long))) ((equal id "YF") (atj-type-jprimarr (primitive-type-float))) ((equal id "YD") (atj-type-jprimarr (primitive-type-double))) (t (prog2$ (raise "Internal error: ~x0 does not identify a type." id) (atj-type-irrelevant))))))
Theorem:
(defthm atj-typep-of-atj-type-of-id (b* ((type (atj-type-of-id id))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-of-id-of-atj-type-id (equal (atj-type-of-id (atj-type-id x)) (atj-type-fix x)))