		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-structdecl

Map a structure declaration to a structure declaration in the language definition.

Signature
(ldm-structdecl structdecl) → (mv erp structdecl1)
Arguments: structdecl — Guard (structdeclp structdecl).
Returns: structdecl1 — Type (c::struct-declonp structdecl1).

The specifiers and qualifiers must be all type specifiers, and must form a supported type specifier sequence.

There must be a single structure declarator, which must have a declarator and no constant expression.

Definitions and Theorems

Function: ldm-structdecl

(defun ldm-structdecl (structdecl)
 (declare (xargs :guard (structdeclp structdecl)))
 (declare (xargs :guard (structdecl-unambp structdecl)))
 (let ((__function__ 'ldm-structdecl))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::struct-declon
          (c::tyspecseq-void)
          (c::obj-declor-ident (c::ident "irrelevant"))))
    ((when (structdecl-case structdecl :empty))
     (reterr (msg "Unsupported empty structure declaration.")))
    ((when (structdecl-case structdecl :statassert))
     (reterr (msg "Unsupported structure declaration ~x0."
                  (structdecl-fix structdecl))))
    (extension (structdecl-member->extension structdecl))
    ((when extension)
     (reterr
      (msg
       "Unsupported GCC extension keyword ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl))))
    (specquals (structdecl-member->specqual structdecl))
    (declors (structdecl-member->declor structdecl))
    ((mv okp tyspecs)
     (check-spec/qual-list-all-typespec specquals))
    ((unless okp)
     (reterr
      (msg
       "Unsupported specifier and qualifier list ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl))))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((unless (and (consp declors)
                  (endp (cdr declors))))
     (reterr
      (msg
       "Unsupported number of declarators ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl))))
    ((structdeclor declor) (car declors))
    ((unless declor.declor?)
     (reterr
      (msg
       "Unsupported structure declarator ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl))))
    ((when declor.expr?)
     (reterr
      (msg
       "Unsupported structure declarator ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl))))
    ((erp objdeclor)
     (ldm-declor-obj declor.declor?))
    (attrib (structdecl-member->attrib structdecl))
    ((when attrib)
     (reterr
      (msg
       "Unsupporte GCC attributes ~
                      in structure declaration ~x0."
       (structdecl-fix structdecl)))))
   (retok (c::make-struct-declon :tyspec tyspecseq
                                 :declor objdeclor)))))

Theorem: struct-declonp-of-ldm-structdecl.structdecl1

(defthm struct-declonp-of-ldm-structdecl.structdecl1
  (b* (((mv acl2::?erp ?structdecl1)
        (ldm-structdecl structdecl)))
    (c::struct-declonp structdecl1))
  :rule-classes :rewrite)

Theorem: ldm-structdecl-ok-when-structdecl-formalp

(defthm ldm-structdecl-ok-when-structdecl-formalp
  (implies (structdecl-formalp structdecl)
           (b* (((mv acl2::?erp ?structdecl1)
                 (ldm-structdecl structdecl)))
             (not erp))))

Theorem: ldm-structdecl-of-structdecl-fix-structdecl

(defthm ldm-structdecl-of-structdecl-fix-structdecl
  (equal (ldm-structdecl (structdecl-fix structdecl))
         (ldm-structdecl structdecl)))

Theorem: ldm-structdecl-structdecl-equiv-congruence-on-structdecl

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