Turn an identifier and a type name into a type specifier sequence and an object declarator.
(ident+tyname-to-tyspec+declor id tyname) → (mv tyspec declor)
We decompose the type name into a type specifier sequence and an abstract object declarator, and we compose the latter with the identifier into an object declarator.
Given an identifier and a type (name), this function provides the constituents for declaring it.
This is the inverse of tyspec+declor-to-ident+tyname.
Function:
(defun ident+tyname-to-tyspec+declor (id tyname) (declare (xargs :guard (and (identp id) (tynamep tyname)))) (let ((__function__ 'ident+tyname-to-tyspec+declor)) (declare (ignorable __function__)) (b* (((tyname tyname) tyname)) (mv tyname.tyspec (ident+adeclor-to-obj-declor id tyname.declor)))))
Theorem:
(defthm tyspecseqp-of-ident+tyname-to-tyspec+declor.tyspec (b* (((mv ?tyspec ?declor) (ident+tyname-to-tyspec+declor id tyname))) (tyspecseqp tyspec)) :rule-classes :rewrite)
Theorem:
(defthm obj-declorp-of-ident+tyname-to-tyspec+declor.declor (b* (((mv ?tyspec ?declor) (ident+tyname-to-tyspec+declor id tyname))) (obj-declorp declor)) :rule-classes :rewrite)
Theorem:
(defthm ident+tyname-to-tyspec+declor-of-tyspec+declor-to-ident+tyname (b* (((mv id tyname) (tyspec+declor-to-ident+tyname tyspec declor))) (equal (ident+tyname-to-tyspec+declor id tyname) (mv (tyspecseq-fix tyspec) (obj-declor-fix declor)))))
Theorem:
(defthm tyspec+declor-to-ident+tyname-of-ident+tyname-to-tyspec+declor (b* (((mv tyspec declor) (ident+tyname-to-tyspec+declor id tyname))) (equal (tyspec+declor-to-ident+tyname tyspec declor) (mv (ident-fix id) (tyname-fix tyname)))))
Theorem:
(defthm ident+tyname-to-tyspec+declor-of-ident-fix-id (equal (ident+tyname-to-tyspec+declor (ident-fix id) tyname) (ident+tyname-to-tyspec+declor id tyname)))
Theorem:
(defthm ident+tyname-to-tyspec+declor-ident-equiv-congruence-on-id (implies (ident-equiv id id-equiv) (equal (ident+tyname-to-tyspec+declor id tyname) (ident+tyname-to-tyspec+declor id-equiv tyname))) :rule-classes :congruence)
Theorem:
(defthm ident+tyname-to-tyspec+declor-of-tyname-fix-tyname (equal (ident+tyname-to-tyspec+declor id (tyname-fix tyname)) (ident+tyname-to-tyspec+declor id tyname)))
Theorem:
(defthm ident+tyname-to-tyspec+declor-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (ident+tyname-to-tyspec+declor id tyname) (ident+tyname-to-tyspec+declor id tyname-equiv))) :rule-classes :congruence)