		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-struct-declon

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

Signature
(ldm-struct-declon structdeclon) → (mv erp structdeclon1)
Arguments: structdeclon — Guard (struct-declonp structdeclon).
Returns: structdeclon1 — Type (c::struct-declonp structdeclon1).

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-struct-declon

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

Theorem: struct-declonp-of-ldm-struct-declon.structdeclon1

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

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

(defthm ldm-struct-declon-ok-when-struct-declon-formalp
  (implies (struct-declon-formalp structdeclon)
           (b* (((mv acl2::?erp ?structdeclon1)
                 (ldm-struct-declon structdeclon)))
             (not erp))))

Theorem: ldm-struct-declon-of-struct-declon-fix-structdeclon

(defthm ldm-struct-declon-of-struct-declon-fix-structdeclon
  (equal (ldm-struct-declon (struct-declon-fix structdeclon))
         (ldm-struct-declon structdeclon)))

Theorem: ldm-struct-declon-struct-declon-equiv-congruence-on-structdeclon

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