Map keywords back to ATJ types.
This is the inverse of atj-type-to-keyword.
An error occurs if the keyword does not correspond to any ATJ type.
Function:
(defun atj-type-from-keyword (kwd) (declare (xargs :guard (keywordp kwd))) (let ((__function__ 'atj-type-from-keyword)) (declare (ignorable __function__)) (case kwd (:ainteger (atj-type-acl2 (atj-atype-integer))) (:arational (atj-type-acl2 (atj-atype-rational))) (:anumber (atj-type-acl2 (atj-atype-number))) (:acharacter (atj-type-acl2 (atj-atype-character))) (:astring (atj-type-acl2 (atj-atype-string))) (:asymbol (atj-type-acl2 (atj-atype-symbol))) (:aboolean (atj-type-acl2 (atj-atype-boolean))) (:acons (atj-type-acl2 (atj-atype-cons))) (:avalue (atj-type-acl2 (atj-atype-value))) (:jboolean (atj-type-jprim (primitive-type-boolean))) (:jchar (atj-type-jprim (primitive-type-char))) (:jbyte (atj-type-jprim (primitive-type-byte))) (:jshort (atj-type-jprim (primitive-type-short))) (:jint (atj-type-jprim (primitive-type-int))) (:jlong (atj-type-jprim (primitive-type-long))) (:jfloat (atj-type-jprim (primitive-type-float))) (:jdouble (atj-type-jprim (primitive-type-double))) (:jboolean[] (atj-type-jprimarr (primitive-type-boolean))) (:jchar[] (atj-type-jprimarr (primitive-type-char))) (:jbyte[] (atj-type-jprimarr (primitive-type-byte))) (:jshort[] (atj-type-jprimarr (primitive-type-short))) (:jint[] (atj-type-jprimarr (primitive-type-int))) (:jlong[] (atj-type-jprimarr (primitive-type-long))) (:jfloat[] (atj-type-jprimarr (primitive-type-float))) (:jdouble[] (atj-type-jprimarr (primitive-type-double))) (otherwise (prog2$ (raise "The keyword ~x0 does not correspond to any ATJ type." kwd) (atj-type-irrelevant))))))
Theorem:
(defthm atj-typep-of-atj-type-from-keyword (b* ((type (atj-type-from-keyword kwd))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-from-keyword-of-atj-type-to-keyword (equal (atj-type-from-keyword (atj-type-to-keyword type)) (atj-type-fix type)))