		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-dirdeclor-obj

Map a direct declarator to an object declarator in the language definition.

Signature
(ldm-dirdeclor-obj dirdeclor) → (mv erp declor1)
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).
Returns: declor1 — Type (c::obj-declorp 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.

For now we disallow parenthesized declarators for simplicity. To allow them, we need to make this function mutually recursive with ldm-declor-obj, which we will at some point.

This function will always result in a c::obj-declor of the :ident or :array kind; the :pointer kind is generated by ldm-declor-obj.

This function is called when we expect an object declarator, not a function declarator, for which we have a separate function.

Definitions and Theorems

Function: ldm-dirdeclor-obj

(defun ldm-dirdeclor-obj (dirdeclor)
 (declare (xargs :guard (dirdeclorp dirdeclor)))
 (declare (xargs :guard (dirdeclor-unambp 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 ~
                            or attribute specifiers ~
                            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: obj-declorp-of-ldm-dirdeclor-obj.declor1

(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: ldm-dirdeclor-obj-of-dirdeclor-fix-dirdeclor

(defthm ldm-dirdeclor-obj-of-dirdeclor-fix-dirdeclor
  (equal (ldm-dirdeclor-obj (dirdeclor-fix dirdeclor))
         (ldm-dirdeclor-obj dirdeclor)))

Theorem: ldm-dirdeclor-obj-dirdeclor-equiv-congruence-on-dirdeclor

(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)