		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-from-keyword

Map keywords back to ATJ types.

Signature
(atj-type-from-keyword kwd) → type
Arguments: kwd — Guard (keywordp kwd).
Returns: type — Type (atj-typep type).

This is the inverse of atj-type-to-keyword.

An error occurs if the keyword does not correspond to any ATJ type.

Definitions and Theorems

Function: atj-type-from-keyword

(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: atj-typep-of-atj-type-from-keyword

(defthm atj-typep-of-atj-type-from-keyword
  (b* ((type (atj-type-from-keyword kwd)))
    (atj-typep type))
  :rule-classes :rewrite)

Theorem: atj-type-from-keyword-of-atj-type-to-keyword

(defthm atj-type-from-keyword-of-atj-type-to-keyword
  (equal (atj-type-from-keyword (atj-type-to-keyword type))
         (atj-type-fix type)))