		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-fundef

Transform a function definition.

Signature
(simpadd0-fundef fundef gin) → (mv new-fundef gout)
Arguments: fundef — Guard (fundefp fundef).; gin — Guard (ginp gin).
Returns: new-fundef — Type (fundefp new-fundef).; gout — Type (goutp gout).

The variable-type map resulting from the transformation of the function declarator includes the applicable parameters of the function, if the function declarator has the :function-params kind. We extend this variable-type map with the function itself, which is in scope just after the declarator; currently this extension is a no-op, because type-formalp does not hold on function types, but we want to have the more general code here. If declarations follow, which is the case only if the function declarator has the :function-names kind, the declarations may further extend the variable-type map before the body, with entries for the parameters declared there. In any case, the body is transformed with the variable-type map after the declarator and any following declarations.

The variable-type map resulting from transforming the body is discarded. We call a separate function, xeq-fundef, to complete the transformation and possibly generate a theorem. That function returns, among other things, a variable-type map that is like the one at the beginning of the function definition (before its declaration specifiers, declarator, etc.), with the addition of the function itself (no addition currently, as explained above, but the code is more general for future extensions).

Definitions and Theorems

Function: simpadd0-fundef

(defun simpadd0-fundef (fundef gin)
  (declare (xargs :guard (and (fundefp fundef) (ginp gin))))
  (declare (xargs :guard (and (fundef-unambp fundef)
                              (fundef-annop fundef))))
  (let ((__function__ 'simpadd0-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef)
         ((mv new-spec (gout gout-spec))
          (simpadd0-decl-spec-list fundef.spec gin))
         (gin (gin-update gin gout-spec))
         ((mv new-declor & (gout gout-declor))
          (simpadd0-declor fundef.declor t gin))
         (gin (gin-update gin gout-declor))
         (type (fundef-info->type fundef.info))
         (ident (declor->ident fundef.declor))
         (vartys-with-fun
              (if (and (ident-formalp ident)
                       (type-formalp type)
                       (not (type-case type :void))
                       (not (type-case type :char)))
                  (b* (((mv & cvar) (ldm-ident ident))
                       ((mv & ctype) (ldm-type type)))
                    (omap::update cvar ctype gout-declor.vartys))
                gout-declor.vartys))
         ((mv new-decls (gout gout-decls))
          (simpadd0-decl-list fundef.decls
                              (change-gin gin
                                          :vartys vartys-with-fun)))
         (gin (gin-update gin gout-decls))
         (vartys-for-body gout-decls.vartys)
         ((mv new-body (gout gout-body))
          (simpadd0-comp-stmt fundef.body
                              (change-gin gin
                                          :vartys vartys-for-body)))
         ((gin gin) (gin-update gin gout-body)))
      (xeq-fundef fundef.extension fundef.spec
                  new-spec fundef.declor new-declor
                  fundef.asm? fundef.attribs fundef.decls
                  new-decls fundef.body new-body
                  gout-body.thm-name fundef.info gin))))

Theorem: fundefp-of-simpadd0-fundef.new-fundef

(defthm fundefp-of-simpadd0-fundef.new-fundef
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin)))
    (fundefp new-fundef))
  :rule-classes :rewrite)

Theorem: goutp-of-simpadd0-fundef.gout

(defthm goutp-of-simpadd0-fundef.gout
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: fundef-unambp-of-simpadd0-fundef

(defthm fundef-unambp-of-simpadd0-fundef
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin)))
    (fundef-unambp new-fundef)))

Theorem: fundef-annop-of-simpadd0-fundef

(defthm fundef-annop-of-simpadd0-fundef
  (implies (and (fundef-unambp fundef)
                (fundef-annop fundef))
           (b* (((mv ?new-fundef ?gout)
                 (simpadd0-fundef fundef gin)))
             (fundef-annop new-fundef))))

Theorem: fundef-aidentp-of-simpadd0-fundef

(defthm fundef-aidentp-of-simpadd0-fundef
  (implies (and (fundef-unambp fundef)
                (fundef-aidentp fundef gcc))
           (b* (((mv ?new-fundef ?gout)
                 (simpadd0-fundef fundef gin)))
             (fundef-aidentp new-fundef gcc))))

Theorem: simpadd0-fundef-of-fundef-fix-fundef

(defthm simpadd0-fundef-of-fundef-fix-fundef
  (equal (simpadd0-fundef (fundef-fix fundef)
                          gin)
         (simpadd0-fundef fundef gin)))

Theorem: simpadd0-fundef-fundef-equiv-congruence-on-fundef

(defthm simpadd0-fundef-fundef-equiv-congruence-on-fundef
  (implies (c$::fundef-equiv fundef fundef-equiv)
           (equal (simpadd0-fundef fundef gin)
                  (simpadd0-fundef fundef-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-fundef-of-gin-fix-gin

(defthm simpadd0-fundef-of-gin-fix-gin
  (equal (simpadd0-fundef fundef (gin-fix gin))
         (simpadd0-fundef fundef gin)))

Theorem: simpadd0-fundef-gin-equiv-congruence-on-gin

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