Map an abstract declarator to an abstract object declarator in the language definition.
(ldm-absdeclor-obj absdeclor) → (mv erp adeclor1)
This is analogous to ldm-declor-obj,
but for abstract declarators.
But there is a difference in how we handle the direct abstract declarator,
since that may be present or not.
If not present, we wrap pointers around
the
This function is called when we expect an abstract object declarator, not a function declarator, for which we have a separate function.
Function:
(defun ldm-absdeclor-obj-loop (adeclor1 pointers) (declare (xargs :guard (and (c::obj-adeclorp adeclor1) (type-qual-list-listp pointers)))) (let ((__function__ 'ldm-absdeclor-obj-loop)) (declare (ignorable __function__)) (b* (((reterr) (c::obj-adeclor-none)) ((when (endp pointers)) (retok (c::obj-adeclor-fix adeclor1))) (tyquals (car pointers)) ((unless (endp tyquals)) (reterr (msg "Unsupported type qualifiers ~x0 in pointer." (type-qual-list-fix tyquals)))) ((erp adeclor2) (ldm-absdeclor-obj-loop adeclor1 (cdr pointers)))) (retok (c::obj-adeclor-pointer adeclor2)))))
Theorem:
(defthm obj-adeclorp-of-ldm-absdeclor-obj-loop.adeclor2 (b* (((mv acl2::?erp ?adeclor2) (ldm-absdeclor-obj-loop adeclor1 pointers))) (c::obj-adeclorp adeclor2)) :rule-classes :rewrite)
Theorem:
(defthm ldm-absdeclor-obj-loop-of-obj-adeclor-fix-adeclor1 (equal (ldm-absdeclor-obj-loop (c::obj-adeclor-fix adeclor1) pointers) (ldm-absdeclor-obj-loop adeclor1 pointers)))
Theorem:
(defthm ldm-absdeclor-obj-loop-obj-adeclor-equiv-congruence-on-adeclor1 (implies (c::obj-adeclor-equiv adeclor1 adeclor1-equiv) (equal (ldm-absdeclor-obj-loop adeclor1 pointers) (ldm-absdeclor-obj-loop adeclor1-equiv pointers))) :rule-classes :congruence)
Theorem:
(defthm ldm-absdeclor-obj-loop-of-type-qual-list-list-fix-pointers (equal (ldm-absdeclor-obj-loop adeclor1 (type-qual-list-list-fix pointers)) (ldm-absdeclor-obj-loop adeclor1 pointers)))
Theorem:
(defthm ldm-absdeclor-obj-loop-type-qual-list-list-equiv-congruence-on-pointers (implies (type-qual-list-list-equiv pointers pointers-equiv) (equal (ldm-absdeclor-obj-loop adeclor1 pointers) (ldm-absdeclor-obj-loop adeclor1 pointers-equiv))) :rule-classes :congruence)
Function:
(defun ldm-absdeclor-obj (absdeclor) (declare (xargs :guard (absdeclorp absdeclor))) (declare (xargs :guard (absdeclor-unambp absdeclor))) (let ((__function__ 'ldm-absdeclor-obj)) (declare (ignorable __function__)) (b* (((reterr) (c::obj-adeclor-none)) ((absdeclor absdeclor) absdeclor) ((erp adeclor1) (if absdeclor.decl? (ldm-dirabsdeclor-obj absdeclor.decl?) (retok (c::obj-adeclor-none))))) (ldm-absdeclor-obj-loop adeclor1 absdeclor.pointers))))
Theorem:
(defthm obj-adeclorp-of-ldm-absdeclor-obj.adeclor1 (b* (((mv acl2::?erp ?adeclor1) (ldm-absdeclor-obj absdeclor))) (c::obj-adeclorp adeclor1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-absdeclor-obj-of-absdeclor-fix-absdeclor (equal (ldm-absdeclor-obj (absdeclor-fix absdeclor)) (ldm-absdeclor-obj absdeclor)))
Theorem:
(defthm ldm-absdeclor-obj-absdeclor-equiv-congruence-on-absdeclor (implies (absdeclor-equiv absdeclor absdeclor-equiv) (equal (ldm-absdeclor-obj absdeclor) (ldm-absdeclor-obj absdeclor-equiv))) :rule-classes :congruence)