		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

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))
   (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
       (make-comp-stmt :labels (comp-stmt->labels fundef.body)
                       :items (cons (make-block-item-decl :decl decl
                                                          :info nil)
                                    (comp-stmt->items fundef.body)))
       :info fundef.info)))
    :otherwise (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)