		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))))
 (b* (((reterr) (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
                (c$::dirdeclor->ident fundef.declor.direct.declor)))
       (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
                                 (param-declon-list-to-ident-param-declon-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)