Map each ATJ type to a distinct keyword.
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.
Function:
(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:
(defthm keywordp-of-atj-type-to-keyword (b* ((kwd (atj-type-to-keyword type))) (keywordp kwd)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-to-keyword-injective (equal (equal (atj-type-to-keyword type1) (atj-type-to-keyword type2)) (atj-type-equiv type1 type2)))
Theorem:
(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:
(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)