		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-to-keyword

Map each ATJ type to a distinct keyword.

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

This is useful, for instance, to print ATJ types in a more readable form that hides the internal representation of their fixtype. We also use these keywords to refer to the types in the developer documentation.

Also see atj-type-from-keyword.

Definitions and Theorems

Function: atj-type-to-keyword

(defun atj-type-to-keyword (type)
  (declare (xargs :guard (atj-typep type)))
  (let ((__function__ 'atj-type-to-keyword))
    (declare (ignorable __function__))
    (atj-type-case
         type
         :acl2 (atj-atype-case type.get
                               :integer :ainteger
                               :rational :arational
                               :number :anumber
                               :character :acharacter
                               :string :astring
                               :symbol :asymbol
                               :boolean :aboolean
                               :cons :acons
                               :value :avalue)
         :jprim (primitive-type-case type.get
                                     :boolean :jboolean
                                     :char :jchar
                                     :byte :jbyte
                                     :short :jshort
                                     :int :jint
                                     :long :jlong
                                     :float :jfloat
                                     :double :jdouble)
         :jprimarr (primitive-type-case type.comp
                                        :boolean :jboolean[]
                                        :char :jchar[]
                                        :byte :jbyte[]
                                        :short :jshort[]
                                        :int :jint[]
                                        :long :jlong[]
                                        :float :jfloat[]
                                        :double :jdouble[]))))

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

(defthm keywordp-of-atj-type-to-keyword
  (b* ((kwd (atj-type-to-keyword type)))
    (keywordp kwd))
  :rule-classes :rewrite)

Theorem: atj-type-to-keyword-injective

(defthm atj-type-to-keyword-injective
  (equal (equal (atj-type-to-keyword type1)
                (atj-type-to-keyword type2))
         (atj-type-equiv type1 type2)))

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

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

Theorem: atj-type-to-keyword-atj-type-equiv-congruence-on-type

(defthm atj-type-to-keyword-atj-type-equiv-congruence-on-type
  (implies (atj-type-equiv type type-equiv)
           (equal (atj-type-to-keyword type)
                  (atj-type-to-keyword type-equiv)))
  :rule-classes :congruence)