		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-fundef

Map a function definition to the language definition.

Signature
(ldm-fundef fundef) → (mv erp fundef1)
Arguments: fundef — Guard (fundefp fundef).
Returns: fundef1 — Type (c::fundefp fundef1).

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

The declarator must be a supported function declarator.

There must be no declarations (between declarator and body).

Definitions and Theorems

Function: ldm-fundef

(defun ldm-fundef (fundef)
 (declare (xargs :guard (fundefp fundef)))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'ldm-fundef))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::fundef (c::tyspecseq-void)
                (c::fun-declor-base (c::ident "irrelevant")
                                    nil)
                nil))
    ((fundef fundef) fundef)
    ((mv okp tyspecs)
     (check-decl-spec-list-all-typespec fundef.spec))
    ((when (not okp))
     (reterr
      (msg
       "Unsupported declaration specifiers ~
                      in function definition ~x0."
       (fundef-fix fundef))))
    ((erp tyspecseq)
     (ldm-type-spec-list tyspecs))
    ((erp fundeclor)
     (ldm-declor-fun fundef.declor))
    ((when fundef.asm?)
     (reterr
      (msg
       "Unsupported assembler name specifier ~
                      in function definition ~x0."
       (fundef-fix fundef))))
    ((when fundef.attribs)
     (reterr
      (msg
       "Unsupported attribute specifiers ~
                      in function definition ~x0."
       (fundef-fix fundef))))
    ((when fundef.decls)
     (reterr
      (msg
       "Unsupported declarations ~
                      in function definition ~x0."
       (fundef-fix fundef))))
    ((erp body) (ldm-stmt fundef.body))
    ((unless (c::stmt-case body :compound))
     (reterr
      (msg
       "Unsupported non-compound statement body ~
                      in function definition ~x0."
       (fundef-fix fundef)))))
   (retok (c::make-fundef :tyspec tyspecseq
                          :declor fundeclor
                          :body (c::stmt-compound->items body))))))

Theorem: fundefp-of-ldm-fundef.fundef1

(defthm fundefp-of-ldm-fundef.fundef1
  (b* (((mv acl2::?erp ?fundef1)
        (ldm-fundef fundef)))
    (c::fundefp fundef1))
  :rule-classes :rewrite)

Theorem: ldm-fundef-ok-when-fundef-formalp

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

Theorem: ldm-fundef-of-fundef-fix-fundef

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

Theorem: ldm-fundef-fundef-equiv-congruence-on-fundef

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