		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-declon-fun

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

Signature
(ldm-declon-fun declon) → (mv erp fundeclon)
Arguments: declon — Guard (declonp declon).
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-declon-fun

(defun ldm-declon-fun (declon)
 (declare (xargs :guard (declonp declon)))
 (declare (xargs :guard (declon-unambp declon)))
 (let ((__function__ 'ldm-declon-fun))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::fun-declon (c::tyspecseq-void)
                    (c::fun-declor-base (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)
     (check-decl-spec-list-all-typespec declspecs))
    ((when (not okp))
     (reterr
      (msg
       "Unsupported declaration specifier list ~
                      in declaration ~x0 for function."
       (declon-fix declon))))
    ((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)))
    ((init-declor initdeclor)
     (car initdeclors))
    ((when initdeclor.initer?)
     (reterr
      (msg
       "Unsupported initializer ~x0 ~
                      for function declaration."
       initdeclor.initer?)))
    ((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-declon-fun.fundeclon

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

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

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

Theorem: ldm-declon-fun-of-declon-fix-declon

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

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

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