		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Split-fn-code-ensemble

Transform a code ensemble.

Signature
(split-fn-code-ensemble target-fn new-fn-name code split-point) → (mv er? new-code)
Arguments: target-fn — Guard (identp target-fn).; new-fn-name — Guard (identp new-fn-name).; code — Guard (code-ensemblep code).; split-point — Guard (natp split-point).
Returns: er? — Type (maybe-msgp er?).; new-code — Type (code-ensemblep new-code).

Definitions and Theorems

Function: split-fn-code-ensemble

(defun split-fn-code-ensemble
       (target-fn new-fn-name code split-point)
  (declare (xargs :guard (and (identp target-fn)
                              (identp new-fn-name)
                              (code-ensemblep code)
                              (natp split-point))))
  (b* (((code-ensemble code) code)
       ((reterr) (irr-code-ensemble))
       ((erp tunits)
        (split-fn-transunit-ensemble target-fn new-fn-name
                                     code.transunits split-point)))
    (retok (change-code-ensemble code
                                 :transunits tunits))))

Theorem: maybe-msgp-of-split-fn-code-ensemble.er?

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

Theorem: code-ensemblep-of-split-fn-code-ensemble.new-code

(defthm code-ensemblep-of-split-fn-code-ensemble.new-code
  (b* (((mv ?er? ?new-code)
        (split-fn-code-ensemble target-fn
                                new-fn-name code split-point)))
    (code-ensemblep new-code))
  :rule-classes :rewrite)