		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

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: er? — Type (maybe-msgp er?).; 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
   (b* (((mv well-formedp fundef-name params)
         (dirdeclor-case
              fundef.declor.direct
              :function-params
              (mv t
                  (c$::dirdeclor->ident fundef.declor.direct.declor)
                  fundef.declor.direct.params)
              :function-names
              (mv t
                  (c$::dirdeclor->ident fundef.declor.direct.declor)
                  nil)
              :otherwise (mv nil nil nil)))
        ((unless (and well-formedp
                      (equal target-fn fundef-name)))
         (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 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))))

Theorem: maybe-msgp-of-split-fn-fundef.er?

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

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

(defthm fundefp-of-split-fn-fundef.fundef1
  (b* (((mv ?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 ?er? ?fundef1 ?fundef2)
        (split-fn-fundef target-fn
                         new-fn-name fundef split-point)))
    (fundef-optionp fundef2))
  :rule-classes :rewrite)