Map a declarator to a function declarator in the language definition.
(ldm-declor-fun declor) → (mv erp fundeclor)
We map the direct declarator to a function declarator, and then we recursively add pointer layers based on the pointer part of the declarator.
This function is called when we expect a function declarator, not an object declarator, for which we have a separate function.
Function:
(defun ldm-declor-fun-loop (declor1 pointers) (declare (xargs :guard (and (c::fun-declorp declor1) (type-qual-list-listp pointers)))) (let ((__function__ 'ldm-declor-fun-loop)) (declare (ignorable __function__)) (b* (((reterr) (c::fun-declor-base (c::ident "irrelevant") nil)) ((when (endp pointers)) (retok (c::fun-declor-fix declor1))) (tyquals (car pointers)) ((unless (endp tyquals)) (reterr (msg "Unsupported type qualifiers ~x0 in pointer." (type-qual-list-fix tyquals)))) ((erp declor2) (ldm-declor-fun-loop declor1 (cdr pointers)))) (retok (c::fun-declor-pointer declor2)))))
Theorem:
(defthm fun-declorp-of-ldm-declor-fun-loop.declor2 (b* (((mv acl2::?erp ?declor2) (ldm-declor-fun-loop declor1 pointers))) (c::fun-declorp declor2)) :rule-classes :rewrite)
Theorem:
(defthm ldm-declor-fun-loop-of-fun-declor-fix-declor1 (equal (ldm-declor-fun-loop (c::fun-declor-fix declor1) pointers) (ldm-declor-fun-loop declor1 pointers)))
Theorem:
(defthm ldm-declor-fun-loop-fun-declor-equiv-congruence-on-declor1 (implies (c::fun-declor-equiv declor1 declor1-equiv) (equal (ldm-declor-fun-loop declor1 pointers) (ldm-declor-fun-loop declor1-equiv pointers))) :rule-classes :congruence)
Theorem:
(defthm ldm-declor-fun-loop-of-type-qual-list-list-fix-pointers (equal (ldm-declor-fun-loop declor1 (type-qual-list-list-fix pointers)) (ldm-declor-fun-loop declor1 pointers)))
Theorem:
(defthm ldm-declor-fun-loop-type-qual-list-list-equiv-congruence-on-pointers (implies (type-qual-list-list-equiv pointers pointers-equiv) (equal (ldm-declor-fun-loop declor1 pointers) (ldm-declor-fun-loop declor1 pointers-equiv))) :rule-classes :congruence)
Function:
(defun ldm-declor-fun (declor) (declare (xargs :guard (declorp declor))) (declare (xargs :guard (declor-unambp declor))) (let ((__function__ 'ldm-declor-fun)) (declare (ignorable __function__)) (b* (((reterr) (c::fun-declor-base (c::ident "irrelevant") nil)) ((declor declor) declor) ((erp declor1) (ldm-dirdeclor-fun declor.decl))) (ldm-declor-fun-loop declor1 declor.pointers))))
Theorem:
(defthm fun-declorp-of-ldm-declor-fun.fundeclor (b* (((mv acl2::?erp ?fundeclor) (ldm-declor-fun declor))) (c::fun-declorp fundeclor)) :rule-classes :rewrite)
Theorem:
(defthm ldm-declor-fun-of-declor-fix-declor (equal (ldm-declor-fun (declor-fix declor)) (ldm-declor-fun declor)))
Theorem:
(defthm ldm-declor-fun-declor-equiv-congruence-on-declor (implies (declor-equiv declor declor-equiv) (equal (ldm-declor-fun declor) (ldm-declor-fun declor-equiv))) :rule-classes :congruence)