Decompose an abstract function declarator into a list of parameter declarations and an abstract object declarator.
(fun-adeclor-to-params+declor declor) → (mv params declor)
The inverse of this is not well-defined for every abstract object declarator, because the latter may include array declarators, which are not allowed in function declarators. We could define the inverse on object declarators that are restricted not to use array declarators; but we do not need the inverse for now.
Function:
(defun fun-adeclor-to-params+declor (declor) (declare (xargs :guard (fun-adeclorp declor))) (let ((__function__ 'fun-adeclor-to-params+declor)) (declare (ignorable __function__)) (fun-adeclor-case declor :base (mv declor.params (obj-adeclor-none)) :pointer (b* (((mv params sub) (fun-adeclor-to-params+declor declor.decl))) (mv params (make-obj-adeclor-pointer :decl sub))))))
Theorem:
(defthm param-declon-listp-of-fun-adeclor-to-params+declor.params (b* (((mv ?params ?declor) (fun-adeclor-to-params+declor declor))) (param-declon-listp params)) :rule-classes :rewrite)
Theorem:
(defthm obj-adeclorp-of-fun-adeclor-to-params+declor.declor (b* (((mv ?params ?declor) (fun-adeclor-to-params+declor declor))) (obj-adeclorp declor)) :rule-classes :rewrite)
Theorem:
(defthm fun-adeclor-to-params+declor-of-fun-adeclor-fix-declor (equal (fun-adeclor-to-params+declor (fun-adeclor-fix declor)) (fun-adeclor-to-params+declor declor)))
Theorem:
(defthm fun-adeclor-to-params+declor-fun-adeclor-equiv-congruence-on-declor (implies (fun-adeclor-equiv declor declor-equiv) (equal (fun-adeclor-to-params+declor declor) (fun-adeclor-to-params+declor declor-equiv))) :rule-classes :congruence)