Turn a type specifier sequence and a function declarator into an identifier, a list of parameter declarations, and a type name.
(tyspec+declor-to-ident+params+tyname tyspec declor) → (mv id params tyname)
We decompose the declarator into an identifier and an abstract declarator, and we form a type name with the latter and the type specifier sequence.
The name of this ACL2 function does not mention
In essence, we turn (the constituents of) a function declaration into its name and parameters and type, which are somewhat mixed in the C syntax.
The inverse of this is not well-defined for every type name, because the latter may include array declarators, which are not allowed in function declarators. We could define the inverse on type names that are restricted not to use array declarators; but we do not need the inverse for now.
Function:
(defun tyspec+declor-to-ident+params+tyname (tyspec declor) (declare (xargs :guard (and (tyspecseqp tyspec) (fun-declorp declor)))) (let ((__function__ 'tyspec+declor-to-ident+params+tyname)) (declare (ignorable __function__)) (b* (((mv id fun-adeclor) (fun-declor-to-ident+adeclor declor)) ((mv params obj-adeclor) (fun-adeclor-to-params+declor fun-adeclor))) (mv id params (make-tyname :tyspec tyspec :declor obj-adeclor)))))
Theorem:
(defthm identp-of-tyspec+declor-to-ident+params+tyname.id (b* (((mv acl2::?id ?params ?tyname) (tyspec+declor-to-ident+params+tyname tyspec declor))) (identp id)) :rule-classes :rewrite)
Theorem:
(defthm param-declon-listp-of-tyspec+declor-to-ident+params+tyname.params (b* (((mv acl2::?id ?params ?tyname) (tyspec+declor-to-ident+params+tyname tyspec declor))) (param-declon-listp params)) :rule-classes :rewrite)
Theorem:
(defthm tynamep-of-tyspec+declor-to-ident+params+tyname.tyname (b* (((mv acl2::?id ?params ?tyname) (tyspec+declor-to-ident+params+tyname tyspec declor))) (tynamep tyname)) :rule-classes :rewrite)
Theorem:
(defthm tyspec+declor-to-ident+params+tyname-of-tyspecseq-fix-tyspec (equal (tyspec+declor-to-ident+params+tyname (tyspecseq-fix tyspec) declor) (tyspec+declor-to-ident+params+tyname tyspec declor)))
Theorem:
(defthm tyspec+declor-to-ident+params+tyname-tyspecseq-equiv-congruence-on-tyspec (implies (tyspecseq-equiv tyspec tyspec-equiv) (equal (tyspec+declor-to-ident+params+tyname tyspec declor) (tyspec+declor-to-ident+params+tyname tyspec-equiv declor))) :rule-classes :congruence)
Theorem:
(defthm tyspec+declor-to-ident+params+tyname-of-fun-declor-fix-declor (equal (tyspec+declor-to-ident+params+tyname tyspec (fun-declor-fix declor)) (tyspec+declor-to-ident+params+tyname tyspec declor)))
Theorem:
(defthm tyspec+declor-to-ident+params+tyname-fun-declor-equiv-congruence-on-declor (implies (fun-declor-equiv declor declor-equiv) (equal (tyspec+declor-to-ident+params+tyname tyspec declor) (tyspec+declor-to-ident+params+tyname tyspec declor-equiv))) :rule-classes :congruence)