		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-declon-obj

Map a declaration to an object declaration in the language definition.

Signature
(ldm-declon-obj declon) → (mv erp objdeclon)
Arguments: declon — Guard (declonp declon).
Returns: objdeclon — Type (c::obj-declonp objdeclon).

The declaration must not be a static assertion declaration.

The declaration specifiers must include only type specifiers and storage class specifiers, each of which must form a supported sequence.

There must be a single initializer declarator.

Definitions and Theorems

Function: ldm-declon-obj

(defun ldm-declon-obj (declon)
 (declare (xargs :guard (declonp declon)))
 (declare (xargs :guard (declon-unambp declon)))
 (let ((__function__ 'ldm-declon-obj))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::obj-declon (c::scspecseq-none)
                    (c::tyspecseq-void)
                    (c::obj-declor-ident (c::ident "irrelevant"))
                    nil))
    ((when (declon-case declon :statassert))
     (reterr (msg "Unsupported static assertion declaration ~x0."
                  (declon-fix declon))))
    (extension (declon-declon->extension declon))
    (declspecs (declon-declon->specs declon))
    (initdeclors (declon-declon->declors declon))
    ((when extension)
     (reterr
      (msg
       "Unsupported GCC extension keyword ~
                      for tag (i.e. structure/union/enumeration) ~
                      declaration.")))
    ((mv okp tyspecs stor-specs)
     (check-decl-spec-list-all-typespec/stoclass declspecs))
    ((unless okp)
     (reterr
      (msg
       "Unsupported declaration specifiers ~x0 ~
                      for object declaration."
       declspecs)))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((erp scspecseq)
     (ldm-stor-spec-list stor-specs))
    ((unless (and (consp initdeclors)
                  (endp (cdr initdeclors))))
     (reterr
      (msg
       "Unsupported number of initializer declarators ~x0 ~
                      for object declaration."
       initdeclors)))
    ((init-declor initdeclor)
     (car initdeclors))
    ((erp objdeclor)
     (ldm-declor-obj initdeclor.declor))
    ((when initdeclor.asm?)
     (reterr
      (msg
       "Unsupported assembler name specifier ~x0 ~
                      for object declaration."
       initdeclor.asm?)))
    ((unless (endp initdeclor.attribs))
     (reterr
      (msg
       "Unsupported attribute specifiers ~x0 ~
                      for function declaration."
       initdeclor.attribs)))
    ((when (not initdeclor.initer?))
     (retok (c::make-obj-declon :scspec scspecseq
                                :tyspec tyspecseq
                                :declor objdeclor
                                :init? nil)))
    ((erp initer)
     (ldm-initer initdeclor.initer?)))
   (retok (c::make-obj-declon :scspec scspecseq
                              :tyspec tyspecseq
                              :declor objdeclor
                              :init? initer)))))

Theorem: obj-declonp-of-ldm-declon-obj.objdeclon

(defthm obj-declonp-of-ldm-declon-obj.objdeclon
  (b* (((mv acl2::?erp ?objdeclon)
        (ldm-declon-obj declon)))
    (c::obj-declonp objdeclon))
  :rule-classes :rewrite)

Theorem: ldm-declon-obj-ok-when-declon-obj-formalp

(defthm ldm-declon-obj-ok-when-declon-obj-formalp
  (implies (declon-obj-formalp declon)
           (b* (((mv acl2::?erp ?objdeclon)
                 (ldm-declon-obj declon)))
             (not erp))))

Theorem: ldm-declon-obj-ok-when-declon-block-formalp

(defthm ldm-declon-obj-ok-when-declon-block-formalp
  (implies (declon-block-formalp declon)
           (b* (((mv acl2::?erp ?objdeclon)
                 (ldm-declon-obj declon)))
             (not erp))))

Theorem: ldm-declon-obj-of-declon-fix-declon

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

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

(defthm ldm-declon-obj-declon-equiv-congruence-on-declon
  (implies (declon-equiv declon declon-equiv)
           (equal (ldm-declon-obj declon)
                  (ldm-declon-obj declon-equiv)))
  :rule-classes :congruence)