Map a direct abstract declarator to an abstract object declarator in the language definition.
(ldm-dirabsdeclor-obj dirabsdeclor) → (mv erp adeclor1)
This is analogous to ldm-dirdeclor-obj, but for abstract declarators. But it has a different recursive structure because we must always have an array declarator, and the recursion ends when the nested direct declarator is absent.
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-dirabsdeclor-obj (dirabsdeclor) (declare (xargs :guard (dirabsdeclorp dirabsdeclor))) (let ((__function__ 'ldm-dirabsdeclor-obj)) (declare (ignorable __function__)) (b* (((reterr) (c::obj-adeclor-none)) ((unless (dirabsdeclor-case dirabsdeclor :array)) (reterr (msg "Unsupported direct abstract declarator ~x0 for object." (dirabsdeclor-fix dirabsdeclor)))) ((dirabsdeclor-array dirabsdeclor) dirabsdeclor) ((when dirabsdeclor.tyquals) (reterr (msg "Unsupported type qualifiers ~ in direct abstract declarator ~x0 for object." (dirabsdeclor-fix dirabsdeclor)))) ((erp iconst?) (if dirabsdeclor.expr? (b* ((iconst (check-expr-iconst dirabsdeclor.expr?))) (if iconst (retok (ldm-iconst iconst)) (reterr (msg "Unsupported non-integer-constant size ~ in direct abstract declarator ~x0 for object." (dirabsdeclor-fix dirabsdeclor))))) (retok nil))) ((when (dirabsdeclor-option-case dirabsdeclor.decl? :none)) (retok (c::make-obj-adeclor-array :decl (c::obj-adeclor-none) :size iconst?))) (dirabsdeclor.decl (dirabsdeclor-option-some->val dirabsdeclor.decl?)) ((erp adeclor1) (ldm-dirabsdeclor-obj dirabsdeclor.decl))) (retok (c::make-obj-adeclor-array :decl adeclor1 :size iconst?)))))
Theorem:
(defthm obj-adeclorp-of-ldm-dirabsdeclor-obj.adeclor1 (b* (((mv acl2::?erp ?adeclor1) (ldm-dirabsdeclor-obj dirabsdeclor))) (c::obj-adeclorp adeclor1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-dirabsdeclor-obj-of-dirabsdeclor-fix-dirabsdeclor (equal (ldm-dirabsdeclor-obj (dirabsdeclor-fix dirabsdeclor)) (ldm-dirabsdeclor-obj dirabsdeclor)))
Theorem:
(defthm ldm-dirabsdeclor-obj-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (ldm-dirabsdeclor-obj dirabsdeclor) (ldm-dirabsdeclor-obj dirabsdeclor-equiv))) :rule-classes :congruence)