		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Split-fn-fundef

Transform a function definition, splitting it if matches the target identifier, or else leaving it untouched.

Signature
(split-fn-fundef target-fn new-fn-name fundef split-point) → (mv er fundef1 fundef2)
Arguments: target-fn — Guard (identp target-fn).; new-fn-name — Guard (identp new-fn-name).; fundef — Guard (fundefp fundef).; split-point — Guard (natp split-point).
Returns: fundef1 — Type (fundefp fundef1).; fundef2 — Type (fundef-optionp fundef2).

Definitions and Theorems

Function: split-fn-fundef

(defun split-fn-fundef (target-fn new-fn-name fundef split-point)
 (declare (xargs :guard (and (identp target-fn)
                             (identp new-fn-name)
                             (fundefp fundef)
                             (natp split-point))))
 (let ((__function__ 'split-fn-fundef))
  (declare (ignorable __function__))
  (b* (((reterr) (c$::irr-fundef) nil)
       ((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
                   (dirdeclor-get-ident fundef.declor.direct.decl)))
        (retok (fundef-fix fundef) nil))
       ((erp new-fn truncated-items)
        (split-fn-block-item-list new-fn-name fundef.body.items
                                  fundef.spec fundef.declor.pointers
                                  (paramdecl-list-to-ident-paramdecl-map
                                       fundef.declor.direct.params)
                                  split-point)))
      (retok new-fn
             (make-fundef :extension fundef.extension
                          :spec fundef.spec
                          :declor fundef.declor
                          :decls fundef.decls
                          :body (stmt-compound truncated-items))))
     :otherwise (retok (fundef-fix fundef) nil))
    :otherwise (retok (fundef-fix fundef) nil)))))

Theorem: fundefp-of-split-fn-fundef.fundef1

(defthm fundefp-of-split-fn-fundef.fundef1
  (b* (((mv acl2::?er ?fundef1 ?fundef2)
        (split-fn-fundef target-fn
                         new-fn-name fundef split-point)))
    (fundefp fundef1))
  :rule-classes :rewrite)

Theorem: fundef-optionp-of-split-fn-fundef.fundef2

(defthm fundef-optionp-of-split-fn-fundef.fundef2
  (b* (((mv acl2::?er ?fundef1 ?fundef2)
        (split-fn-fundef target-fn
                         new-fn-name fundef split-point)))
    (fundef-optionp fundef2))
  :rule-classes :rewrite)