		Search-engine friendly clone of the ACL2 documentation.

Specialize

Specialize-fundef

Transform a function definition.

Signature
(specialize-fundef fundef target-fn target-param const) → (mv found new-fundef)
Arguments: fundef — Guard (fundefp fundef).; target-fn — Guard (identp target-fn).; target-param — Guard (identp target-param).; const — Guard (exprp const).
Returns: found — Type (booleanp found).; new-fundef — Type (fundefp new-fundef).

Definitions and Theorems

Function: specialize-fundef

(defun specialize-fundef (fundef target-fn target-param const)
 (declare (xargs :guard (and (fundefp fundef)
                             (identp target-fn)
                             (identp target-param)
                             (exprp const))))
 (let ((__function__ 'specialize-fundef))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef)
       ((declor fundef.declor) fundef.declor))
   (stmt-case
    fundef.body
    :compound
    (dirdeclor-case
     fundef.declor.direct :function-params
     (b*
      (((unless
         (equal target-fn
                (c$::dirdeclor->ident fundef.declor.direct.declor)))
        (mv nil (fundef-fix fundef)))
       ((mv success new-params removed-param)
        (param-declon-list-remove-param-by-ident
             fundef.declor.direct.params
             target-param))
       ((unless success)
        (prog2$ (raise "Function ~x0 did not have a parameter ~x1"
                       target-fn target-param)
                (mv nil (fundef-fix fundef))))
       (dirdeclor-params
            (make-dirdeclor-function-params
                 :declor fundef.declor.direct.declor
                 :params new-params
                 :ellipsis fundef.declor.direct.ellipsis))
       ((mv - decl)
        (param-declon-to-decl removed-param (initer-single const))))
      (mv t
          (make-fundef
               :extension fundef.extension
               :spec fundef.spec
               :declor (make-declor :pointers fundef.declor.pointers
                                    :direct dirdeclor-params)
               :decls fundef.decls
               :body (stmt-compound (cons (block-item-decl decl)
                                          fundef.body.items)))))
     :otherwise (mv nil (fundef-fix fundef)))
    :otherwise
    (prog2$
     (raise "Function definition body is not a compound statement.")
     (mv nil (fundef-fix fundef)))))))

Theorem: booleanp-of-specialize-fundef.found

(defthm booleanp-of-specialize-fundef.found
  (b* (((mv ?found ?new-fundef)
        (specialize-fundef fundef target-fn target-param const)))
    (booleanp found))
  :rule-classes :rewrite)

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

(defthm fundefp-of-specialize-fundef.new-fundef
  (b* (((mv ?found ?new-fundef)
        (specialize-fundef fundef target-fn target-param const)))
    (fundefp new-fundef))
  :rule-classes :rewrite)