Short string identifying an ATJ type.
We use a short two-letter string to identify each ATJ type.
For the
Function:
(defun atj-type-id (type) (declare (xargs :guard (atj-typep type))) (let ((__function__ 'atj-type-id)) (declare (ignorable __function__)) (atj-type-case type :acl2 (atj-atype-case type.get :integer "AI" :rational "AR" :number "AN" :character "AC" :string "AS" :symbol "AY" :boolean "AB" :cons "AP" :value "AV") :jprim (primitive-type-case type.get :boolean "JZ" :char "JC" :byte "JB" :short "JS" :int "JI" :long "JJ" :float "JF" :double "JD") :jprimarr (primitive-type-case type.comp :boolean "YZ" :char "YC" :byte "YB" :short "YS" :int "YI" :long "YJ" :float "YF" :double "YD"))))
Theorem:
(defthm stringp-of-atj-type-id (b* ((id (atj-type-id type))) (stringp id)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-id-injective (equal (equal (atj-type-id x) (atj-type-id y)) (atj-type-equiv x y)))
Theorem:
(defthm atj-type-id-of-atj-type-fix-type (equal (atj-type-id (atj-type-fix type)) (atj-type-id type)))
Theorem:
(defthm atj-type-id-atj-type-equiv-congruence-on-type (implies (atj-type-equiv type type-equiv) (equal (atj-type-id type) (atj-type-id type-equiv))) :rule-classes :congruence)