Map a direct declarator to an object declarator in the language definition.
(ldm-dirdeclor-obj dirdeclor) → (mv erp declor1)
The abstract syntax in the language definition does not have a separate type for direct object declarators, so we return an object declarator here. The input direct declarator must be an identifier followed by zero or more square-bracketed optional integer constant expressions. These zero or more array declarator constructs are handled recursively.
This function will always result in a c::obj-declor
of the
This function is called when we expect an object declarator, not a function declarator, for which we have a separate function.
Function:
(defun ldm-dirdeclor-obj (dirdeclor) (declare (xargs :guard (dirdeclorp dirdeclor))) (let ((__function__ 'ldm-dirdeclor-obj)) (declare (ignorable __function__)) (b* (((reterr) (c::obj-declor-ident (c::ident "irrelevant"))) ((when (dirdeclor-case dirdeclor :ident)) (b* ((ident (dirdeclor-ident->unwrap dirdeclor)) ((erp ident1) (ldm-ident ident))) (retok (c::obj-declor-ident ident1)))) ((when (dirdeclor-case dirdeclor :array)) (b* (((dirdeclor-array dirdeclor) dirdeclor) ((erp declor1) (ldm-dirdeclor-obj dirdeclor.decl)) ((when dirdeclor.tyquals) (reterr (msg "Unsupported type qualifiers ~ in direct declarator ~x0 for object." (dirdeclor-fix dirdeclor)))) ((when (not dirdeclor.expr?)) (retok (c::make-obj-declor-array :decl declor1 :size nil))) (iconst (check-expr-iconst dirdeclor.expr?)) ((unless iconst) (reterr (msg "Unsupported non-integer-constant size ~ in direct declarator ~x0 for object." (dirdeclor-fix dirdeclor)))) (iconst1 (ldm-iconst iconst))) (retok (c::make-obj-declor-array :decl declor1 :size iconst1))))) (reterr (msg "Unsupported direct declarator ~x0 for object." (dirdeclor-fix dirdeclor))))))
Theorem:
(defthm obj-declorp-of-ldm-dirdeclor-obj.declor1 (b* (((mv acl2::?erp ?declor1) (ldm-dirdeclor-obj dirdeclor))) (c::obj-declorp declor1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-dirdeclor-obj-of-dirdeclor-fix-dirdeclor (equal (ldm-dirdeclor-obj (dirdeclor-fix dirdeclor)) (ldm-dirdeclor-obj dirdeclor)))
Theorem:
(defthm ldm-dirdeclor-obj-dirdeclor-equiv-congruence-on-dirdeclor (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (ldm-dirdeclor-obj dirdeclor) (ldm-dirdeclor-obj dirdeclor-equiv))) :rule-classes :congruence)