		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-decl-fun

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

Signature
(ldm-decl-fun decl) → (mv erp fundeclon)
Arguments: decl — Guard (declp decl).
Returns: fundeclon — Type (c::fun-declonp fundeclon).

The declaration must not be a static assertion declaration.

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

The initialization declarator must be a declarator, without initializer, and it must be a supported declarator for a function.

Definitions and Theorems

Function: ldm-decl-fun

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

Theorem: fun-declonp-of-ldm-decl-fun.fundeclon

(defthm fun-declonp-of-ldm-decl-fun.fundeclon
  (b* (((mv acl2::?erp ?fundeclon)
        (ldm-decl-fun decl)))
    (c::fun-declonp fundeclon))
  :rule-classes :rewrite)

Theorem: ldm-decl-fun-ok-when-decl-fun-formalp

(defthm ldm-decl-fun-ok-when-decl-fun-formalp
  (implies (decl-fun-formalp decl)
           (b* (((mv acl2::?erp ?fundeclon)
                 (ldm-decl-fun decl)))
             (not erp))))

Theorem: ldm-decl-fun-of-decl-fix-decl

(defthm ldm-decl-fun-of-decl-fix-decl
  (equal (ldm-decl-fun (decl-fix decl))
         (ldm-decl-fun decl)))

Theorem: ldm-decl-fun-decl-equiv-congruence-on-decl

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